Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2,036 changes: 2,036 additions & 0 deletions research/r439-later-retirement-cuts/CERTIFICATE.json

Large diffs are not rendered by default.

572 changes: 572 additions & 0 deletions research/r439-later-retirement-cuts/LATER-CUTS.json

Large diffs are not rendered by default.

187 changes: 187 additions & 0 deletions research/r439-later-retirement-cuts/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,187 @@
# R439: complete later-cut retirement census

**Scoped bit-supplier negative result and precise handoff; no new kappa.**
For PR1128's six width-seven candidates, this package checks every boundary
along the fixed PR589 B word: **713 cuts and 4,278 helper/cut pairs**. It supplies the complete
necessary-condition census for the later-cut first-restoration question left
explicitly open by Ross Richardson's concurrent PR1256.

A cut numbered k is **after exactly the first k B records**. Thus cut 10 is
after zero-based B[9]. The D/A/scatter prefix and B chronology are fixed.

| Helper | Cuts with joint restoration/erasure rank seven | Cuts also passing first-restoration target access |
|---:|---|---|
| 465 | 0–48 | **10–48** (39 cuts) |
| 466 | 0–78 | **none** |
| 468 | 0–88 | **31–88** (58 cuts) |
| 469 | 0–555 | **none** |
| 470 | 0–517 | **0–517** (518 cuts) |
| 476 | 0–284 | **none** |

Every later cut outside the second column has joint rank eight. These are
**necessary-condition windows**, not feasible suffixes or constructions.
No B/C replacement, physical owner allocation or supplier invoice is supplied.

The sharp chronology point is helper466: its blocking target208 is first
read at B[88], but the joint bound has already risen to eight after B[78].
Simply waiting for that target read cannot save it. Helpers465 and468 do
escape their initial target-access obstruction after B[9] and B[30],
respectively, but only until the joint bound rises after B[48] and B[88].
For helpers469 and476, at least one inaccessible required target dependency
remains at every cut with joint rank seven.

## Exact contract and argument

The sole mathematical input is the frozen PR589 tuned word. At each cut,
write the 661-register scalar state as `w=M u` over F2. All source, target
and helper inputs are independent. Each prefix gate is an invertible
transvection, including the already-consumed retained scatter; no new access
to its COPY channels is allowed. Current frames F_r are rational subspaces
of Q^8. Frame changes must be monotone. Scalar operations must use a common
frame, extra dirty workspace must start independently and be restored, and
there is no new COPY, descent, reset or other high-to-low transport.

We test a suffix whose **first restoration block** operates at a single
rational frame J, with no lower-frame preprocessing after the chosen cut,
and restores the designated helper h to its original dirty input s_h.
After that block, arbitrary allowed multi-frame scalar work is permitted.
The ultimate endpoint for h must have dimension at most seven; other source,
target and helper endpoints and scalar values retain their original contract.
This is the first-restoration model of PR1256, not arbitrary suffix synthesis.

Let R_h be the support of `e_h^T M^-1`, and D_h the support of the h-th column
of M. The restoration/erasure argument from PR1128 gives the necessary bound

`U_h = span(F_h, {F_r : r in R_h union D_h}) <= final_frame(h)`.

All these joins have rank seven or eight in the completed census. A rank-eight
join excludes every proper final frame in this interface, even with arbitrary
rational choices, target access and restored dirty scratch. For a rank-seven
join, a first restoration block must use a frame containing

`J_h = span(F_h, {F_r : r in R_h})`.

The required final target value `y_t + x_(t-111)` has the unique boundary row
`b_t = (e_t + e_(t-111))^T M^-1`. If b_t uses a coordinate forced into the
restoration block, but J_h is not contained in t's final frame V_t, no allowed
completion can supply that dependence to t. Every touched register has moved
to J_h or a larger frame; monotonicity prevents any of its information from
reaching V_t. Untouched boundary coordinates and fresh independent dirt cannot
encode the missing independent coordinate. Enlarging the first restoration
frame cannot cure a failed containment.

This is PR1256's information-access implication. We apply it at **every**
later B boundary, where both inverse rows and frames change. The complete
certificate records contiguous runs with identical restoration donors, join
rank, restoration rank and lost-target sets. No cut, rational station or
support-size cutoff is sampled. The proof establishes the stated exclusions;
passing the two tests supplies no sufficiency claim.

For helper466, the target-access witness is target208 at every eligible cut
0–78. At cut79 the joint rank is eight; at cut89, after target208's original
read, it is still eight. The 469/476 lost-target sets are likewise nonempty
through every rank-seven cut. Full sets and every transition are retained in
[LATER-CUTS.json](LATER-CUTS.json).

## Predecessors and evidence-driven scope change

Ali Romman's PR1128 (`df29b159239b79d7e451d6ddda826a73e0e50a67`) establishes the
boundary lemma and the six after-scatter candidates. Ross Richardson's
PR1256 (`d6d5a994fcdcd8d04ec439ff988daa8f37b17ece`) establishes the initial
six-case target-access obstruction and an explicit finite helper470 retirement
using rank two before rank seven. Its construction is predecessor evidence,
not implemented or repriced here. Its native/physical/H4 obligations remain.

This session initially derived the same stationary stars and endpoint-cap
failures independently. The final overlap refresh found PR1256 before any
submission. That initial material is retained in [STATION-NOTE.md](STATION-NOTE.md)
and `CERTIFICATE.json` as corroboration only. It is not the novelty claim.
The one evidence-driven pivot is exactly PR1256's listed later-cut question;
its README says no search there was performed. In particular, our no-window
result for helper466 explains why its proposed target-read follow-up fails
in the fixed chronology, while the two other suggested candidates retain
precise finite windows. Earlier helper470 deletion belongs to Ali Romman's
PR1043; its savings are not combined with anything here.

Fresh OS seed **17** selected the original user's bit-supplier track. The
three initial candidates, first scope, pivot and stopping rule are in
`TASK.json`. There was no pinned sprint issue, so the authorized local-claim
fallback was used. The initial snapshot covered 850 open PR bodies; the final
pre-pivot refresh covered 855 and all 12 returned discussions. PR1253 concerns
common-first-contact kernel entrances and PR1250 source-mask deletion; both
are distinct and neither is a mathematical dependency here.

## Reproduce and negative controls

Python 3.12, standard library only, from the repository root:

```sh
python3.12 scripts/research_package.py --package research/r439-later-retirement-cuts
```

The principal commands also run on Python 3.10+:

```sh
python3 -I -O -B research/r439-later-retirement-cuts/later_cuts.py
python3 -I -O -B research/r439-later-retirement-cuts/check_later_cuts.py
python3 -I -O -B research/r439-later-retirement-cuts/test_later_cuts.py
```

Expected markers include `PASS_LATER_BIT_CUTS pairs=4278` and
`PASS_INDEPENDENT_LATER_CUTS full_inverse_rebuilds=713 helper_cut_pairs=4278`,
followed by passing tests and `PASS_REGISTERED_RESEARCH_PACKAGE`.

The primary engine incrementally updates inverse rows with each B
transvection, using packed binary rows and rational geometry. The separate
checker imports no primary engine, reconstructs the **entire inverse from
scratch at every one of the 713 boundaries**, and uses independently replayed
set-valued scalar states and fraction-free integer geometry. It checks each
restoration identity directly and agrees on every run and boundary, not just
the total counts. Both inherit only the exact raw word; no predecessor
executable code is imported. Separate code paths are not independent human
review.

The test suite rejects wrong boundary indexing, shifted donor support,
missing target obligations, false pass windows, incomplete cut coverage and
changed source bytes. It checks optimized source-only relocation and parsed
certificate regeneration. The retained stationary suite adds all ten legal
witness-gate omissions, three endpoint-cap failures with relaxed positive
controls, six certificate mutations in both engines, a wrong station, damaged
original cleanup and source-corruption tests.

Base `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`; input SHA256
`e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f`.
`SOURCES.json` pins base Git blobs, historical context and both predecessor
heads/documents. See `VALIDATION.md` for actual local runs and omitted work.

## Scope, cost and credit

This is an exact finite census plus the cited necessary-condition arguments.
It is not a formal proof-assistant verification of the multiplication theorem.
Even optimistically free suffix work cannot repair a failed information-access
condition within this model. The surviving windows still require full source
access, target effects, restoration, frame transitions, copies, recursive
children, physical hosting, precision/tape and outer/all-size admission before
any new paid profile or exponent can be claimed. The selected complex supplier
remains binding. No native replay, complete cold supplier replay, production
adoption, remote CI or new kappa is claimed. `upstream/`, frozen predecessor
packages and the selected frontier are unchanged.

Credit **Ali Romman** (PR1128 and earlier PR1043), **Ross Richardson**
(PR1256), **Sagar Thakrar** (PR1023 width-seven hosting incentive),
DreamingOfClouds (PR589/545), eumemic (PR555/543), and their retained
compiler/hosting lineage. Prepared for **Philipp (@mightyOil)** with substantial
**OpenAI Codex / GPT-6 Astra** assistance in proof, code, tests and writing.
New material is Apache-2.0.

## Open next questions

Can helper465 at cut10 or helper468 at cut31 be restored through a fully
priced legal suffix? Those are the earliest new necessary-condition windows;
start there and preserve all dirty columns, pending target reads and physical
frame paths. The census supplies no such suffix and does not justify a new
search outside the 39/58 windows without a changed assumption. For helper470,
PR1256 already gives a finite cut-zero continuation; native H4, owner-window
and precision admission are the more useful next checks. Changes to the prefix,
lower-frame preparation, target-read reordering or added transport are outside
this census and require a new explicit contract and complete cost.
85 changes: 85 additions & 0 deletions research/r439-later-retirement-cuts/SOURCES.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,85 @@
{
"schema_version": 1,
"base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8",
"files": [
{
"path": "certificates/selected-result.json",
"usage": "provenance",
"git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
"sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
},
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
"git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
"sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
},
{
"path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz",
"usage": "input",
"git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a",
"sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
},
{
"path": "research/bit589-width-packing/README.md",
"usage": "provenance",
"git_blob": "a915381a7a38d3728205a2120aa034f94537ca0f",
"sha256": "671ca8a9d9e78348eae1e5c605ead1606df3d5e23d251600f0bdf60175479f1e"
},
{
"path": "docs/research/community-batch1099-review.md",
"usage": "provenance",
"git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099",
"sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb"
},
{
"path": "research/community-frontier1094-audit/SELECTED-SOURCE.json",
"usage": "provenance",
"git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8",
"sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b"
}
],
"predecessors": [
{
"pr": 1128,
"head": "df29b159239b79d7e451d6ddda826a73e0e50a67",
"author": "Ali Romman (@aliromman)",
"role": "Boundary lemma and six-survivor premise; independently replayed, no executable code imported.",
"documents": [
{
"path": "research/bit-width-seven-boundary/README.md",
"git_blob": "f1930385706e38cc3b9995b8ba01f3ac9d06034b",
"sha256": "29b61651091c0870f9762efb6f93ebfa358d7bb8206d04012b18192cf4dabfab"
},
{
"path": "research/bit-width-seven-boundary/PROOF.md",
"git_blob": "b3bedffde3ee5f1914873ec7918039ab6614678c",
"sha256": "f9fb4706dd523229e8351646c5ef011d8bd16eebc3dd6c35a778b352c123b387"
},
{
"path": "research/bit-width-seven-boundary/CERTIFICATE.json",
"git_blob": "6982d303d1ba1dfa0b33a2a7f1a1acc9b8a5b2ee",
"sha256": "06ea7280e8a0829b283e352d5590a7cc832ee0973335c24dbac02505d493fa36"
}
]
},
{
"pr": 1256,
"head": "d6d5a994fcdcd8d04ec439ff988daa8f37b17ece",
"author": "Ross Richardson",
"role": "First-restoration target-access lemma, after-scatter classification, finite470 continuation; later-cut question. No executable code imported.",
"documents": [
{
"path": "research/bit-early-retirement-cut/README.md",
"git_blob": "4f3716685c7a22ec4c1b8a68c8beb69021acd0a9",
"sha256": "57b952674aefc3fb6287ceaab7c940c100916dba8ba97104e1838c785e3d8e9f"
},
{
"path": "research/bit-early-retirement-cut/CERTIFICATE.json",
"git_blob": "b7a8d17755711ccb901742c59dd775c586be1c8d",
"sha256": "735c507caf32715f978e9c0ca67cb056184c751593cd8c58e9dd97232def7a46"
}
]
}
]
}
41 changes: 41 additions & 0 deletions research/r439-later-retirement-cuts/STATION-NOTE.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
# Initial stationary fixtures: independent corroboration only

The session began by replaying PR1128's 439-helper after-scatter boundary and
checking a single rank-seven station. Concurrent Ross Richardson PR1256
subsumes this question and gives the stronger future-target-access argument
and finite two-frame helper470 continuation. This appendix claims no priority
or new supplier result. README.md describes the later-cut contribution.

433 helpers have rank-eight restoration/erasure joins. The other six are
465/466/468/469/470/476. The first three cannot perform all isolation work at
their forced station while retaining their dirty-carrying targets' final
frames. The other three admit scalar/frame-local isolation:

```
station 517: 469 ^= 50; 413 ^= 469; 479 ^= 469
station 513: 470 ^= 77; 444 ^= 470; 475 ^= 470
station 514: 476 ^= 67; 476 ^= 328; 476 ^= 331; 476 ^= 385
```

These programs restore the designated independent dirty input and remove it
from all other registers, preserving their other coefficients. Their counts
3/3/4 are minimal in binary ADDs: the first two change three required
destinations; the third computes the parity of five essential boundary
coordinates, whose dependency graph requires four edges. All participating
registers can reach the station and retain their final-frame cap. However,
future target information may already have become inaccessible; none is an
admitted suffix. In particular these stationary programs must not be confused
with PR1256's two-frame helper470 program, which leaves source77 at rank two.

`CERTIFICATE.json`, `verify.py`, `independent.py` and `test_package.py` retain
this complete after-scatter replay and its controlled scalar fixtures. The
primary also checks the original B/C map on all661 columns. The six test
groups cover both complete engines, ten gate omissions, three target-cap
failures plus relaxed positive controls, six receipt mutations, a wrong
station, damaged original cleanup, exact regeneration, isolated relocation
and source corruption. These checks support the later-cut implementations;
they do not establish a complete physical supplier or new kappa.

Credit Ali Romman's PR1128, Ross Richardson's PR1256 and the PR589/555 lineage.
Prepared for Philipp (@mightyOil), with substantial OpenAI Codex assistance.
Apache-2.0.
Loading
Loading