Repository navigation
Research: two-sided boundary obstruction for R439 width-seven helpers - #1128
Merged
Merged
Conversation
Contributor
|
100-PR batch review at Merged to Reviewed scope: Two-sided boundary information forces full-width endings for all 439 helpers after B, and 433 after scatter; monotone common-frame suffix contract is essential. The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions. Batch review, attribution and evidence. Thank you for the contribution. |
This was referenced Oct 14, 2026
thakrarsagar
added a commit
to thakrarsagar/integer-mult-bounds
that referenced
this pull request
Oct 14, 2026
- The synthetic witness is described exactly: its post-scatter reads undo W_syn's moved compensation, so after B it equals CrocSwap#1179's prefix entrance on PR589; it now also fails without its late reads (new control). - The open triple's obstacle is scoped to A6R (B++C fixed); LC-fav also allows a rewritten B/C. 'Settles/decides' becomes 'narrows to one open triple'. - PROOF.md: cone lemma is CrocSwap#1128 section 1 (Lemma 2 is the dual of section 2); Lemma 1 states only x-free, pivot-free D' contributions; Step 4 folds scatter-extension snapshot terms into u; frames at sigma equal raw frames; reads during C reduce to the end of B (asserted: C at FULL, no target). - Donors: 5,212 enumerated, 5,059 placeable. W_t are coordinate subspaces (recorded); the structural reason is restated accordingly. - Relaxation checked to contain every admission; census sanity checks are labelled as such; flipped-byte control recorded; engine-2 coverage stated precisely; credits for eumemic, DreamingOfClouds, CrocSwap#967, CrocSwap#915/CrocSwap#926, CrocSwap#1043, CrocSwap#1079, CrocSwap#1256.
Mister-Meeseeks
pushed a commit
that referenced
this pull request
Oct 14, 2026
Tests the case #1128 and #1179 leave open: can a common-frame helper entrance (all 4,954 supports of #1253's closure, plus 5,212 source donors) be compensated after the scatter instead of by a frame-0 prefix? On the selected PR589 word and the four merged star words, the sound necessary test (LC-fav) admits only #1179's kernel pair 444+470 and the triple 444+470+578; the strict class A6 admits only the kernel pair; with storage relays (A6R) the triple stays open. Two engines with no shared code agree on K, the closure (= #1253's certificate), every dirt-only space and every verdict; a synthetic word's built witness replays; mutations flip verdicts.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The selected PR #589 word cannot obtain a width-seven helper by replacing cleanup C alone. An exact inverse-row certificate requires rank eight for all 439 helpers after B. A second necessary condition tracks every register that carries the helper's dirty input. At the earlier cut after D/A/scatter, the two conditions require rank eight for 433 helpers and leave six explicit rank-seven candidates.
Review files: Proof and scope · Evidence · Source pins and credit.
This is a scoped negative result, with no new kappa. It tests the physical boundary that is missing from PR #1023's hypothetical width-seven hosting gains. The proof permits arbitrary finite reversible linear suffixes, arbitrary rational frames, target access, extra restored dirty registers, and simultaneous helper endpoint changes. Frames must move monotonically, all scalar operations must use a common frame, and the suffix cannot add a COPY or another transport operation. The six early-cut survivors are necessary-condition survivors, not constructions.
The package also checks that every helper has a nonzero compensation column. This excludes a rank-one entrance when semantic compensation must finish before the fixed raw entry and targets must remain at frame zero. A separate complete optimistic cost argument excludes one paid 0 -> 1 -> 7 -> 8 bridge wrapper. Neither argument excludes a changed A, helper basis, compensation timing, copy pattern, or recursive interface.
Reproduce from the repository root:
Expected final line:
Validation: all 878 helper/cut rows, all 439 compensation columns, and all 661 dirty input columns in the selected local scalar word pass. Eight altered certificates are rejected for their specified errors. Three small controls distinguish the restoration and erasure conditions. The checker uses set replay, Gaussian elimination and integer determinants; it does not import the packed-row derivation. Certificate regeneration and the verifier under
python3 -Oalso pass. A separate sprint agent reproduced the verifier and reviewed the proof. This is AI-assisted review, not independent human review.Only research/bit-width-seven-boundary/ is added. Exact base: abdc6a7002abdbcd9e21bfc5e1a795784deacfdf. The sole mathematical input is the PR #589 tuned word, SHA-256
e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f. It is unchanged at main ba82555c64e1879e4b7decce28186f208fcb8262, whose selected PR #1042 bound is0.001672188119205421; the complex side still binds. Source and context heads are in SOURCES.json. No selected record or upstream/ file changes.The attempted inverse cleanup fails for all helpers after B. Moving the cut earlier leaves the six stated candidates. An exploratory screen of 198,137 later gate-boundary pairs finds local readouts but supplies no complete width reduction; it is not proof evidence. The exact stopping rule covers both cuts and all compensation columns. No randomness is used. No new physical word, hosted invoice, native replay, selected cold replay, full repository suite, remote CI, or formal verification of the full multiplication theorem is claimed. All inherited realization and analytic assumptions remain.
Credit @DreamingOfClouds and @eumemic for the BIT word and interface lineage; Zhihao Chen (@jacklightChen) for earlier scalar-interface work; @DaysSky for idle-axis hosting; Jeremy Kothe (@jeremykothe2) and Dominik Scholz (@DominikScholz) for related complex boundary mechanisms; and Sagar Thakrar (@thakrarsagar) for PR #1023. PR #1043 deletes helper 470 and PR #1079 gives a source-substitution census. PR #1048 fixes endpoints and audits one/two-move reframing. PR #1100 studies positive single-write frames. PR #1105 audits projected target-feedback cleanup; this proof requires the complete final map. Final overlap review read PR #1122 at
a2551e70fce0cc34348f50f1a94e7cc4c80bbcbf: it changes A/B/semantic D and preserves paid paths, so its prefix is outside this theorem. The results do not conflict or combine savings.Prepared for Ali Romman (@aliromman), with substantial OpenAI Codex assistance in the research, proof, implementation and review. New material is Apache-2.0.