[petalas]

Summary

Scoped written proof with an exact finite configuration, answering the concrete complement case of DreamingOfClouds's #6854 open question 1. No new kappa, word or supplier.

S96 = complement of the explicit D24 in #6854
  contains an eight-line forced-zero gauge plus six K2,3 pair lines
  six invertible diagonal blocks need at least 6k coordinate rank
  five used gauge coordinates supply at most 5k
  therefore no realisation with inner dimension 8k.

This holds over every field and for every k >= 1, with distinct U and W allowed. The new step is the explicit S96 geometry and its 14-line witness. The gauge and Hall rank argument are credited to DreamingOfClouds's #6846/#6854; the general star bounds of #6933 and #7114 are prior work and are not improved here. Only research/e8-pseudoforest-line-sets/ is added.

Evidence

Before: #6854's 13-line family misses S96 and its complement case is explicitly left open. After: the displayed K2,3 configuration certifies that this particular candidate also fails. This does not exclude all 96-line sets.

The checker regenerates the 120 E8 lines and verifies the witness's exact support table and forced zeros. It enumerates all 192 eight-cliques of S96; every corresponding pair-line graph is K4,4, so each contains a K2,3 and none contains the older K4-minus-an-edge configuration. For the six displayed pair lines with the gauge retained, all 64 subsets are checked and the 63 proper subsets receive exact integer unit-vector patterns. Three controls reject a singular diagonal, a nonzero forced-zero pair and an incomplete K4,4.

The complete registered replay passes with CPython 3.12.15 on macOS arm64, standard library only. The normal and optimized commands were individually timed at 0.08 s and 0.10 s; these are check-budget records. The output is:

PASS_E8_S96_HALL gauges=192 witness_lines=14 repair_subsets=63 no_new_kappa
PASS_REGISTERED_RESEARCH_PACKAGE research/e8-pseudoforest-line-sets outcome=negative-result

Metadata/pins and committed-byte/source-history checks also pass. Reproduce from the repository root:

~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e8-pseudoforest-line-sets
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e8-pseudoforest-line-sets --check-source-history
~/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error -X dev research/e8-pseudoforest-line-sets/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error -X dev research/e8-pseudoforest-line-sets/verify.py

Any CPython 3.12 can replace the interpreter path. The predecessor's check.py is read as hash-pinned data solely for D24; it is never executed. No predecessor solver or certificate replay is part of this contribution.

Limitations and unrun obligations

The proof assumes the precise whole-block label mask in #6854. It does not establish that mask for a word, exclude other 96-line sets, compute a new global cardinality threshold, optimize a larger family's hitting set, or exhibit a largest realisable set. Ranks strictly between 8k and 9k, different masks and physical implementation remain outside the result. No Lean, Docker, selected cold replay, independent human review or proof-kernel acceptance is claimed. The full rank claim is a written proof, not a conclusion from finite-field search.

The CLAIM contemplated a broader search. The single FINDING update records the delivered narrowing to this complement and leaves the global hitting-set and largest-construction parts open.

Related open work

• P104 port window is exactly 9 in characteristic 2 (no κ) #7114 proves general star-configuration rank bounds and the P104 window value. This package supplies a concrete S96 configuration and does not strengthen that theorem.
• Prove the star-pattern floor n+1 on the wheel W4 and K33 at minimum degree 3 (no κ) #7129 proves stronger star bounds for W4 and K3,3; this package does not compute its open K2,3 window value.
• Prove the E8 ports-per-dimension law N_e = 2^(e-2) + 4 in closed form (no κ) #7127 counts E8/P104 ports in subspaces; the quantity here is label realisability of a fixed complement, not a port-count optimum.
• Exhibit a 104 by 13 factorisation of the P104 window over F_5. #7014 gives rank-13/14/15 factors for P104/P112/P120; this package constructs no factor for those full port sets and compares none of those numbers.
• Witness a characteristic-3 rank-32 pattern on P120. #7087 gives a characteristic-3 rank-32 pattern on P120; this package concerns inner dimension 8k on S96 and computes no competing P120 rank.
• 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 treats rank-eight fitting rigidity after at most eight deletions, with a different fitting-zero constraint; this package deletes the specific 24 lines and uses the Prove no subset of ≥97 E8 lines has a rank-8 complex realisation (minimum hitting set 24, spectral + local certificate; no κ) #6854 mask.
• 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 fitting-table decoder cost floors; this package supplies no decoder identity or cost comparison.
• Prove the exact E8 Gram-class minimum through 24 deletions (no κ) #7168 optimizes Gram-class costs through 24 deletions; that scalar design problem differs from the block-mask realisability question here.
• Exhibit a non-coordinate COPY71 completion at the first-failure boundary #7169 constructs a one-sided COPY71 completion on a fixed 93-line first-failure unit; this package computes no COPY bill and concerns the different 96-line complement.
• Bound scalar COPY savings at one 93-line E8 puncture (no κ) #7170 bounds scalar COPY changes on that 93-line puncture; this package excludes inner dimension 8k on S96 and compares no COPY value.
• Lower P104 frame-0 hosting from 40 to 14 monomials (no κ) #7167 computes frame-indicator hosting minima on E8 lines; this package neither constructs nor prices a host.
• Host one P104 frame-indicator row and charge its new monomials. #7031 hosts the frame-0 indicator; its monomial charge is not recomputed here.
• Host P104 frame 1 and intersect its new monomials with the recorded forty. #7046 hosts frame 1 and studies shared monomials; no such hosting quantity is computed here.
• Prove no F2 sum of letters hosts the P104 frame-0 indicator. #7047 studies frame-0 Boolean letter sums; no letter polynomial is supplied here.
• Checkpoint eight masked-decoder basis searches (exploratory; no new K) #5064 searches masked completions on fixed P112/P120 units; this package gives a necessary obstruction on a different fixed line subset.
• Bind P112 tetrad decoder to selected ports; no kappa change #3566 binds a tetrad decoder to P112 ports; this package makes no physical decoder binding.

Before committing, canonical main was re-fetched and remained e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8. Live overlap covered 467 open PR titles/bodies, this account's current open PRs including #7167/#7168, the latest 30 handoff comments, active discussions, canonical-main README searches and merged semantic searches. The cached card search reports complete remote pagination but sparse local coverage, so Git searches supplemented it. No duplicate concrete complement result was found; this is bounded overlap evidence.

The completion-time own-open-PR check read the titles and result statements of #7167, #7168, #7169, #7170, #7172, #7173, #7175 and #7176. The related E8 line/decoder results are listed above. The other four concern tensor-Gram polynomials, commuting-stage ranks, fixed-profile splitting ceilings and connector-chain windows. None supplies a numerical value computed by this package, so no additional numerical agreement or disagreement is claimed.

Open next questions

1. Can a different 96-line set avoid both the old 13-line family and pair-line Hall deficiencies? First classify the 24-line hitting sets of that family and inspect representative complements.
2. What is the largest E8 subset with an 8k realisation under this mask? Construct a candidate, then inspect all its gauges. Passing these necessary Hall tests still does not construct U and W.

CI notes

CI did not certify this package. At head a47e7e5b626c8dfde099b6d8aaab9b650e9ca30b, run 42984295238, plan job 130401695825, failed in Onboarding helper tests. I read the completed checks once and inspected the job log. It reports exactly 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 doc

The package replay job 130404097922 was skipped because plan failed. The package evidence remains the local normal/optimized replay, metadata/pins and committed-byte/source-history checks recorded above. Hosted CI supplied no mathematical certification.

The mismatch is present in canonical main's own files at e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json requires make frontier7000-verify, while docs/ci-verification.md still opens with "Current selected-family replay: #6030" and names make frontier6030-verify. I confirmed those source bytes and previously reproduced the failing test locally. This PR changes neither file nor the test.

I also inspected the failed logs of these seven other runs. Each has the same sole failing test, missing #7000 command, and summary of 760 tests with one failure and 24 skipped:

• Other contributors: 42905094314, 42903313790.
• Lower P104 frame-0 hosting from 40 to 14 monomials (no κ) #7167: 42983769381.
• Prove the exact E8 Gram-class minimum through 24 deletions (no κ) #7168: 42983916692.
• Bound scalar COPY savings at one 93-line E8 puncture (no κ) #7170: 42984005087.
• Certify fixed-profile helper-split first-crossing ceilings for #7000 (no κ) #7175: 42984445251.
• Prove sharp c=6 endpoint chain windows (no κ) #7176: 42984461381.

No repository-level fix, new commit, push, failed-job rerun or retrigger was made in response to this failure.

Credit

This package was produced by Nick Petalas. Credit DreamingOfClouds for #6846/#6854's model, Hall mechanism, D24 and concrete open question, and for the related general bounds in #6933/#7114. New work is Apache-2.0.

Merge danger

Two-way door. Five files are added in one opt-in research package; shared code, workflows, the selected record and frozen predecessors are unchanged.