[Matarener]

Requested by Mark

Change and mathematical scope

Proof (with recorded finite searches) that every nine-term decoder of a rank-9 B-form realisation M = D₁ G D₂ + c βᵀ of the P104 pattern costs at least 56, including singular D. No κ claim, no supplier word; this is a lower-bound / obstruction result for the masked carrier floor of #2338 on P104.

• Case I (|supp c|, |supp β| ≤ 12): proved by counting.
• Case II/III (|supp β| ≤ 4 or |supp c| ≤ 4, any D): proved reduction to a census statement; census run recorded on Kaggle, 0 configurations alive (regular D: V0–V3, 701 each; singular D: 740 pairs, 446 configurations).
• Coverage: |supp c| ≥ 13 forces |supp β| ≤ 4 (exact biclique check).
• Lean: BForm.bform_floor builds with no sorry (axioms propext, Classical.choice, Quot.sound). The finite facts and the census enter as named hypotheses (Capacity, RootFact, SpanFact, BicliqueFact, CensusFact).

Remaining obligations: non-B-form, non-A2 rank-9 realisations of P104 (open), decoders with ≥ 10 terms, P112/E8.

Task and overlap

Base 3f0152a32. Task complex-rank-shape-decoder, scope refined to the B-form case on P104. Only research/p104-bform-nine-term-floor/ is added.
Overlap: research/e8-rank9-realisations §5 lists the B-form decoder floor as open; a2-family-decoder-floors / a2-family-b-locus cover the A2 family; the census extends research/nine-term-outside-colspace (cnt9b) with the 104 port classes as extra column classes, repeated survivors and, for singular D, an exact root-rank bound lbz.

Validation

python3 scripts/research_package.py --package research/p104-bform-nine-term-floor --check-only
python3.12 scripts/research_package.py --package research/p104-bform-nine-term-floor

The bounded verifier re-runs S0–S3 and the lbz self-test, authenticates the census logs by sha256, scans the Lean sources for sorry/admit/axiom, and runs failure controls (tampered log, corrupted hash). The full census replay (~1.5 h on 4 cores) is in kaggle/; logs in evidence/kaggle/. Lean: cd lean && lake exe cache get && lake build. An earlier S2 run failed on exactly the 104 port pairs; the lemma was corrected (S2') and the check now asserts that structure.

Credit

Prepared by Matarener with Claude (Anthropic) via Claude Code; census runs on Kaggle; Lean formalisation by Claude. Census code from research/nine-term-outside-colspace (DreamingOfClouds), extended. Apache-2.0.

Open next questions

1. Is every rank-9 realisation of the P104 pattern B-form or A2? With this package and the A2 floors it would close nine-term case (c) of Decoder floors are tight in the frontier format: one F2^9 label table, factors in col M of a rank-8 realisation (P112 64, E8 72, P104 (#968's unit) 56; two-call batches 128) — no κ claim #2338 on P104.
2. Formalise the E8 hyperplane classification so RootFact and SpanFact become Lean theorems (in progress).

🤖 Generated with Claude Code

https://claude.ai/code/session_011VhYmBxety7X1WKrP33NdX