[petalas]

Summary

Scoped written proof with exact finite certificates, answering the fewer-than-16-deletions half of DreamingOfClouds's #6888 open question 1. No new κ, supplier or multiplication theorem.

#6888: every D with 16 <= d <= 24 has Gram-class cost c >= 56.
Here:  every D with 0 <= d <= 24 has c >= 72 - 2 min(d,8).
       Some D of each size attains equality, with eight explicit terms.

The new lower-bound step proves that, at d <= 7, deficient directions are precisely the deleted root lines. The attaining construction pairs simple roots along a Dynkin matching. At d=8 it has c=56, every price is 7, det M=65536, and v-c=56. Its M is nonscalar. These are 112 live lines, not the fixed P112 unit obtained by deleting an orthogonal frame. This gives the minimum over deleted sets, not the minimum for each fixed set, and does not contradict exact-decoder floors with stronger matrix constraints.

Credit DreamingOfClouds's #6888 for the model, Cauchy-Binet/Sylvester/domination argument, ray census and question. Its c>=56 argument already applies for every d<=24. The new work is the small-deletion argument and attainment. Only research/p104-gram-class-exact-floor/ changes.

Evidence

Before this result, #6888 explicitly left d<=15 outside its conclusion. The standalone exact verifier now checks 25 attaining designs, all 61,320 root-support/hyperplane cases, rank-nine mask factorization, the eight ray-census inputs and orthogonal-complement ranks. It detects singular repeated terms. Controls give cost 64 for identity pairing on the same deleted simple roots and 72 after restoring the deleted lines.

At head 114eafd694efcfae1f811cbaccf7962385919386, local CPython 3.12.15 checks pass. Both registered normal/optimized commands run in under one second each; the complete registered run takes about 1.5 seconds. The generator was rerun into scratch and its parsed JSON agreed with the committed data. The commit-byte/source-history check authenticates seven files and the base commit.

From the repository root:

~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-gram-class-exact-floor
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-gram-class-exact-floor --check-source-history
~/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error -X dev research/p104-gram-class-exact-floor/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error -X dev research/p104-gram-class-exact-floor/verify.py

Expected markers are PASS_P104_GRAM_CLASS_EXACT_FLOOR designs=25 root_hyperplanes=61320 no_new_kappa, PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed, and PASS_RESEARCH_COMMIT_BYTES. Any CPython 3.12 can replace that interpreter path. Standard library only.

The proof uses E8 Weyl chambers and positive-root expansions. The finite inputs are checked exactly. No solver, Lean, Docker, selected cold replay, physical COPY implementation, independent human acceptance or formal proof-kernel acceptance is claimed. The result excludes d>=25, carriers outside the Gram class and other line systems. It does not settle the scalar-M subclass.

Related open work

• Rank-8 rigidity of the E8 pattern with arbitrary extra zeros after deleting any at most 8 lines (hypothesis (1) of Lemma RIGD; no kappa claim) #3040 studies fitting rank-eight realizations after arbitrary small deletions; the nonscalar design here need not satisfy its fitting-zero constraints.

• Non-dense fitting B: every E8 term with x·y ≠ 0 has rank ≥ 9; square root-code floors E8 ≥ 72, P112 ≥ 64, P104 ≥ 56, D4 ≥ 12 for any fitting B (no κ claim) #3045 proves square exact-decoder floors for fitting tables on fixed units; this package allows arbitrary invertible M and varies D.

• Decoder floors: universality, projection transfer and batching reductions; C(P112) ≥ 64 reduced to named conjectures, C(P120) ≥ 72 restated on N₀ (no κ claim) #2832 studies exact masked-decoder floors, projection transfer and batching; no such exact-decoder identity is supplied here.

• Research: one-sided residue closures — Circuit Lemma, relative root counting and plane lemma close 480 of the 603 d>=4 residues (116 open; no kappa claim) #2985 studies one-sided fixed-P112 residue closures; the small-deletion Gram optimization here has a different matrix constraint.

• Research: one-sided residue closures, part 2 — Lemma Q4, count lemma + E6 dim-cover and rerunnable span passes close 78 more of the 116 open residues (38 open; no kappa claim) #3049 continues those one-sided residue closures; this result does not close its remaining cells.

• One-sided padding lemma: P112 to P120 at cost exactly +8 (L120 suffices for Delta >= n_nf) #3074 pads exact one-sided P112 decoders to P120; the nonscalar certificate here is not an input to that padding lemma.

• Checkpoint eight masked-decoder basis searches (exploratory; no new K) #5064 searches masked completions on fixed P112/P120; this construction changes the deleted set and does not improve those decoder costs.

• Bind P112 tetrad decoder to selected ports; no kappa change #3566 binds a tetrad masked decoder to selected P112 ports; this package has no physical port binding or decoder implementation.

• Add exact complex rank-16 block decoder screen #3895 studies tensor block decoders in a growing alphabet; this theorem keeps the scalar E8 Gram class and fixed binary mask.

• Add selected centre decoder demand floor audit #3918 gives a source-bound selected centre-demand rank floor; this theorem does not price or replace that physical demand.

• Scope rank-two native and decoder obstructions (no new κ) #7098 studies source-bound rank-two/native and decoder restrictions; its word and caller hypotheses are outside this Gram model.

• Lower P104 frame-0 hosting from 40 to 14 monomials (no κ) #7167 studies polynomial hosting charges for E8 frame indicators, rather than the binary support-pairing cost of a Gram design.

• Exhibit a non-coordinate COPY71 completion at the first-failure boundary #7169 exhibits masked and all-pairs COPY constructions on one 93-line unit, with 27 deletions, outside this theorem's d<=24 range. No shared fixed-set optimum is computed here.

• Bound scalar COPY savings at one 93-line E8 puncture (no κ) #7170 bounds scalar COPY perturbations at that 27-deletion boundary; this theorem neither treats that boundary nor compares its fixed-frame costs.

• Exclude the proposed 96-line E8 complement at inner dimension 8k (no κ) #7174 excludes a fitting rank-8k realization of one 96-line complement. This theorem bounds Gram-design cost for every D of size 24 but does not assert attainment for that particular complement or impose its fitting-zero constraints.

• Prove doubled centre Gram stabilization by width ten (no κ) #7172 studies the tensor-width spectrum of a doubled centre Gram operator, a different operator and quantity from this scalar mask-rank minimum.

The own-open-PR check since the CLAIM also read #7173, #7175 and #7176. They concern commuting-stage rank budgets, fixed-invoice helper-split ceilings and six-source chain windows, respectively. None computes this Gram-class minimum. The earlier #7132, #7133, #7134 and #7135 study different quantities. No numerical agreement or disagreement is claimed outside the computations in this package.

A refreshed overlap search covered 466 open PRs and 7,089 discussion records with complete pagination. Sparse local coverage was 171 of 10,178 notes; git grep on canonical origin/main supplemented it. Live open PRs, merged-title searches, main-package searches, recent handoffs and this account's PRs were checked again before committing. Canonical main remained e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8. No duplicate was found; this is not a novelty certificate.

Open next questions

• Characterize fixed deleted sets with d<=7 that attain 72-2d, starting with the odd-inner-product matching graph on independent deleted roots.
• Determine the minimum with M proportional to I on the eight-simple-root deleted set. The scalar matrix identity couples the term pairs and is absent from the cost-56 certificate.

CI notes

CI did not certify this package. At head 114eafd694efcfae1f811cbaccf7962385919386, run 42983916692, plan job 130400491084, failed in Onboarding helper tests. I read the checks once and inspected the job log. It reports exactly one failing test among 760, 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

The document still describes #6030, while certificates/selected-result.json names make frontier7000-verify on base e54523517d0f03e58352e647c403a5af3e525a57. Both files are unchanged by this PR. The package replay job was skipped because plan failed. Local evidence above remains the verification evidence; the planning failure supplies no scientific certification.

I independently inspected the logs and job outcomes of all these comparison runs. Each has the same sole test failure, 760 tests with 24 skipped, and skipped package replay:

• Other contributors: 42905094314 and 42903313790.
• Close the six-bit fit window of the selected BIT stage's stock prescription at log2 e = 52182660963730.92 (no κ) #7132: 42914704054.
• Classify dyadic aligned windows of the capped source guard and prove its length bound sharp (no κ) #7133: 42983300354.
• Prove the exact odd-rectangle residual-rank floor for any stage size and hub count: 72ρ at u = h = ρ (no κ) #7134: 42914997118.
• Prove the best-quotient staircase of the sharp net splitting tax (no κ) #7135: 42914936342.
• Lower P104 frame-0 hosting from 40 to 14 monomials (no κ) #7167: 42983769381.
• Exhibit a non-coordinate COPY71 completion at the first-failure boundary #7169: 42983930022.
• Bound scalar COPY savings at one 93-line E8 puncture (no κ) #7170: 42984005087.

No fix, retrigger commit, job rerun or push was made. The repository-level navigation repair is left to the maintainers.

Merge danger

Two-way door. The change is confined to a new research package, with no selected-frontier or shared-runtime edit. The scientific risk is the stated scoped proof, which remains subject to review.