[petalas]

Summary

At the single 93-line puncture of ToikY's #1609, the coordinate completion keeps COPY72 for every complex perturbation scalar. The new result extends the source's fixed-scalar comparison to all scalars and bounds savings for every fixed basis whose dual directions are roots.

Claim type: scoped written proof supported by exact finite certificates. For the fixed normal v=(1,-1,2,0,0,0,0,0) and the perturbation q_j -> q_j+c v:

coordinate basis:  C(c) = 72 for every complex c
root dual basis:   C_A(c) >= C_A(0)       outside {-2/3, 2/3}
                   C_A(c) >= C_A(0) - 1   for every complex c

The certificate checks all 120 root directions. Exactly three supports lose rank when the target column is removed, with rank-pair histogram (8,8):27, (9,8):3, (9,9):90. The target-root direction cannot cancel. The other two cancel at different scalars, so at most one basis term can lose rank. Column dependence survives arbitrary source-row restriction.

Only research/masked-e8-copy-bill-perturbation/ is added. No best masked completion, all-pairs optimum, physical supplier, new kappa or selected-frontier change is claimed.

Evidence

Before, #1609 reports COPY72 at its witness and coordinate comparator and asks for the deficient-column scalar variation. After, the four complete coordinate support classes have eight ranks of nine. The 120-direction certificate gives the one-unit necessary bound for root dual bases.

At head 2c4bb35a8f49bc1ed5576ac075dca0314c6b02a0, local CPython 3.12.15, standard library only, from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/masked-e8-copy-bill-perturbation/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/masked-e8-copy-bill-perturbation/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/masked-e8-copy-bill-perturbation --check-only
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/masked-e8-copy-bill-perturbation
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/masked-e8-copy-bill-perturbation --check-source-history

For other machines, replace the interpreter path with CPython 3.12. Observed results:

• PASS_MASKED_E8_COPY_BILL_PERTURBATION coordinate=72 support_classes=4 root_directions=120 critical=3 possible_saving_scalars=-2/3,2/3 max_root_basis_saving=1 in both direct modes. Each registered command took under one second locally, against a 120-second command timeout.
• PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed, about two seconds for the whole registered replay.
• PASS_PACKAGE_METADATA_AND_PINS and PASS_RESEARCH_COMMIT_BYTES, five committed files and the base source-history commit checked.
• Normal, optimized and relocated Git-free replays emit identical deterministic JSON receipts, bound to all five package-file hashes. Replay leaves package bytes unchanged.

Every coordinate representative checks all 8,649 product entries. Each binary pairing rank is computed by row elimination and a separate transpose/XOR algorithm. Controls include all 512 binary 3-by-3 matrices and their 1,536 single-column deletions, three invalid-input rejections, a wrong-normal diagonal failure, and a restriction where a critical direction does not save rank.

Limitations

The one-unit bound compares each fixed basis with its own all-pairs comparator. It does not prove attainment or a lower bound for that comparator. It does not classify arbitrary complex dual directions, other punctures or extra-term completions. The scalar COPY diagnostic omits gathering, arbitrary-dirty restoration, frame changes, hosting, precision/tape, all-size/compiler realization and analytic transfer.

No selected cold replay, Lean or Docker run was performed. Independent human and formal proof-kernel review are unclaimed. The optional selected-baseline orientation command failed locally because the sparse checkout omits research/global-lambda-lowering/LICENSE; none of this package's mathematical replay depends on that file.

Open next questions

Characterize target-column dependence for every complex dual direction at this fixed puncture. A first step is to classify the hyperplane sections of its 93 live roots and test the pairing rank of each complement with and without the target column. This would extend the necessary scalar-saving test beyond root directions. Complete coverage of the complex hyperplane sections is the blocker; sampling would not settle it.

Related open work

• #7169 gives an explicit non-coordinate COPY71 completion and a separate COPY63 all-pairs comparator on the same 93 live lines. Its displayed frame is outside this package's root-dual-direction hypothesis. Those two profiles are not computed here. The shared residual counts agree: zero masked errors and 56 unmasked target-column errors for a nonzero perturbation.

• #7168 optimizes the Gram class through 24 deletions with arbitrary invertible matrix M. This package fixes 27 deletions and a specific masked perturbation family, so it computes no competing minimum.

• #7167 counts ANF monomials for P104 frame-indicator hosting. That is a different charge from the binary support-pairing ranks here.

• #7174 excludes an 8k block-mask realization of a fixed 96-line complement. This package treats a different 93-line set and computes no block-realization rank.

• #5064 checkpoints nine-factor completion walks on P112/P120. This is a finite direction certificate and scalar proof at a different 93-line puncture.

• #5088 studies two-star support dictionaries on P112. No such dictionary or search is used here.

• #2832 gives general decoder-floor reductions on P112/P120. This package proves no unrestricted decoder floor.

• #2985 studies one-sided P112 residue closures, with a different live set and lift model.

• #3029 studies two-sided P112 deficiency budgets. The factors here have a fixed root-linear side and only one target row varies.

• #3074 pads one-sided P112 decoders to P120. No padding or P112 floor is inferred here.

• #3154 reduces the P112 floor to named conjectures. This fixed-puncture scalar result does not settle those conjectures.

• #3045 allows non-dense fitting binary pairings for square root-code decoders. Here the dense pairing is fixed and the completion can leave all-pairs exactness.

• #3040 studies rank-eight rigidity through eight deletions. The retained Research: sharp 27-deletion boundary for one-sided E8 masked rigidity #1609 example has 27 deletions and is treated only for its scalar COPY costs.

• #3566 binds a tetrad-local P112 decoder to selected ports. This package supplies no selected-port or physical binding.

• #3604 studies P112 tetrad co-delivery and centre costs. Those consumer costs are outside this scalar perturbation model.

• #3895 studies tensor/product-root block decoders with a changed label form. This package keeps the original E8 pairing and eight terms.

The complementary construction claim studies the broader first-failure census and non-coordinate constructions. Neither is answered here. The original claim and progress finding identify this fixed-puncture question.

Overlap was refreshed against canonical main e54523517d0f03e58352e647c403a5af3e525a57, 466 paginated open PR records and 7,089 Discussion records, with fresh open/own-PR lists and #1166 before committing. Merged source/keyword searches and README searches found no published copy of this result. Sparse local notes, arbitrary diffs and unpublished work remain coverage limits. The completion check read this account's open PRs created since the claim: #7132, #7133, #7134, #7135, #7167, #7168, #7169, #7170, #7172, #7173, #7174, #7175 and #7176. The E8 neighbors are described above; the others study stock, guards, stage ranks, doubled centre Gram spectra, helper invoices or connector chains. No extra computations were run to check their results, and no disagreement was found in a quantity computed by both packages.

CI notes

CI did not certify this package. At exact head 2c4bb35a8f49bc1ed5576ac075dca0314c6b02a0, run 42984005087 completed with the plan job failing and the package replay job skipped. The completed checks were read once; run metadata confirms the exact head.

The failed step is "Onboarding helper tests". Its log reports one failure among 760 tests, with 24 skipped:

test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
AssertionError: '`make frontier7000-verify`' not found in the CI verification document

On canonical main e54523517d0f03e58352e647c403a5af3e525a57, certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md still describes #6030 and make frontier6030-verify. I checked those base files and the failed job log directly. This PR changes neither shared file.

The same sole failing test, the same missing-command assertion, and the 760-test / 24-skipped totals appear in the failed logs I inspected for other contributors' run 42905094314 and run 42903313790. Previously inspected account runs #7135, 42914936342 and #7134, 42914997118 show that same failure and skipped package replay. These are the other runs checked here.

The evidence for this package remains the local normal, optimized, relocated, registered, metadata and committed-byte/source-history checks above. The head is unchanged. No repository-level fix, retrigger commit or job rerun was made.

Merge danger

Door: two-way. Blast radius: one new research directory. Existing packages, selected records, source archives and shared code are unchanged.

Credit

This contribution was produced by Nick Petalas. ToikY's #1609 supplies the puncture, normal, fixed-scalar witness and open question. Philipp / mightyOil's #1191 supplies the local spanning mechanism, and DreamingOfClouds's #717 the separate-term COPY model. The retained E8 lineage keeps its predecessor credit. New work is Apache-2.0.