[petalas]

Result

Scoped proof with an exact finite certificate. No new κ, supplier or frontier change.

DreamingOfClouds's #2962 (research/decoder-certificate-ceilings, §2.1) proves that every certificate in the larger family F′ gives at most 24 on the E8 unit P120. It records as OPEN whether the Theorem C value 360/17 also bounds F′. This PR settles that item for P120.

Among all sets of k lines of E8, the least number of frames meeting the set is 765 for k = 8 and 701 for k = 7. Only pairwise-orthogonal sets attain these minima. For k ≤ 6, Bonferroni gives enough. So the least feasible uniform weight is 8/765, and the uniform F′ ceiling on P120 is 2025 · 8/765 = 360/17. With #2962's fake-decoder argument, every F′ certificate on P120 gives at most 360/17 ≈ 21.18, down from the proven 24. The result is the same under the README's constraint min(|D|, 8) and under the script's weaker min(|D|-1, 8) for non-orthogonal sets, because frames are the binding sets.

Proof outline:

1. Every line lies in 135 frames, every orthogonal pair in 15 and every non-orthogonal pair in 0.
2. By Bonferroni, an 8-set meeting at most 765 frames has at most 7 non-orthogonal pairs, and a 7-set meeting at most 701 has at most 4.
3. By Caro–Wei, such sets contain an orthogonal triple or an orthogonal 4-set, respectively.
4. Under the group generated by the root reflections, orthogonal triples form 1 orbit and orthogonal 4-sets form 2. The verifier checks that each reflection permutes the frames.
5. An exhaustive search over every extension of each representative, within the pair cap, gives the minima above.

Positive control: on E7, the same search reproduces #2962's MILP minima 55, 62 and 68. That includes a non-frame minimiser below the frame value 71, so the search finds such minimisers where they exist.

Evidence and reproduction

Package: research/e8-fprime-uniform-ceiling. Standard library only. Interpreter: CPython 3.12.15 (~/git/integer-mult-bounds/.venv/bin/python3.12), Darwin arm64. From the repository root:

python3.12 -W error -I -B research/e8-fprime-uniform-ceiling/verify.py
python3.12 -W error -I -O -B research/e8-fprime-uniform-ceiling/verify.py
python3.12 -B scripts/research_package.py --package research/e8-fprime-uniform-ceiling
python3.12 -B scripts/check_research_commit.py --package research/e8-fprime-uniform-ceiling --check-source-history

Local results: both verifier runs print PASS_E8_FPRIME_UNIFORM_CEILING mu8 765 ceiling 360/17 no_new_kappa (about 36 s each). The package check prints PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed, and the commit check prints PASS_RESEARCH_COMMIT_BYTES. RESULT.json must match byte for byte. The checks use require(), so they stay active under -O. A rejecting control confirms that weight 8/766 violates a frame's constraint.

Limitations and unrun obligations

• This covers the uniform frame-weight witness only. Whether 360/17 is the exact optimum of F′ over non-uniform weights is not decided.
• P112 is not computed. Its proven F′ ceiling is still 15968/667.
• Theorem C, the F′ constraint form and the fake-decoder argument are cited from Ceilings for linear rank-counting decoder certificates (360/17 on P120) and a one-sided lift bound (cost >= 72 for dim S >= 23) #2962 and not replayed.
• This PR gives no decoder floor, supplier, invoice or κ. Lean, Docker and selected replays were not run.

Open next questions

1. P112. Does 15968/757 bound F′ on P112? Use the stabilizer of the removed frame with the same pair caps and orthogonal cores. The blockers: P112 is not line-transitive, and its 1996 maximal orthogonal sets have mixed sizes.
2. Non-uniform optimum. Is 360/17 the exact F′ optimum on P120? A first step is an orbit-reduced LP with an exact dual.
3. E7/E6. Uniform weights stop at 945/68 on E7. Can non-uniform weights reach 945/71?

Related open work

• F-star family gap: the sub-anchor-box decomposition and a fixture-density sub-decoder census (no kappa) #2914 (navinor) studies the F-star family gap for three-total decoder certificates. That is a different certificate family and object, and this PR computes no number it reports.
• Prove P112 quadratic extension threshold is exactly 7 (no new κ) #5957 (this account, opened after the CLAIM) proves a deletion threshold of exactly 7 for quadratic extension on P112, using the frames that remain live after the deletion. It works on the same E8/P112 frame geometry but on a different quantity. This PR computes no P112 number, so there is nothing to compare.
• No other open PR studies E8 frame-meet minima or the F′ ceiling.

CI notes

Every check passed for head 600d46ea009d9f6665c07cd030d23c046c23f4c6: plan (3m47s) and replay (research/e8-fprime-uniform-ceiling) (4m3s). Run: https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40532400857. Locally, each registered check takes about 36 s.

Credit

DreamingOfClouds's #2962 supplies F, F′, Theorem C, the fake-decoder argument, the Bonferroni ceiling 24 and the E7/E6 MILP values used as the control. The charging-certificate shape is from #1977 and #798. The new contribution is the exact least meets for k = 7 and 8, the orbit-reduced proof that frames attain them, and the resulting 360/17 ceiling for F′ on P120.