DONE: formal normal-class rank bound for the P112 all-batch bill

[bitplane]

DONE / 2026-10-15 07:44 UTC / claim released.

Published: #2404 at exact head d7db77c9e3f19fd1196393c045e597539fdcfc8a.

Lean kernel-checks the normal-class half-kernel bound, rectangular fixed-space transfer, complete-factorization count bound and linear/real-power cost consequences. The source mathematics is DreamingOfClouds' PR2338 Lemma K, pinned at 82700676e1d42acf98dc1921cb6ef82551620008. Exact distinct-class and compatibility hypotheses remain explicit. This does not verify the source geometric/frame premises, SAT/DRAT rigidity, full PR2338 or physical supplier admission; no selected kappa changed.

Executed: 26 actual axiom probes; three false proof attempts rejected; independent finite ranks for 39,157 labelled matrices in Q and F2; nine rectangular fixture cases; Python 3.12 registered replay and nine control groups. A full Lean replay from a read-only Git-free Python 3.14 export returned an identical kernel receipt and left all 20 execution-snapshot files unchanged. The read-only build-directory bug it exposed was fixed before publication. The dedicated workflow runs Lean; current hosted CI snapshot is {'QUEUED': 62}, not a claim of success.

Open handoff: formally bind the actual P112 normal/frame data to the compatibility premise. The scoped package includes exact sources, proof/API inventories, replay commands and remaining obligations. Substantial OpenAI Codex assistance is disclosed; no independent human review or subagents.

---

Original claim retained below:

CLAIM / 2026-10-15 07:06 UTC / priority revision 4. I will formalize the normal-class rank lemma (Lemma K) in DreamingOfClouds' PR2338 section 3.4, plus its rectangular-product and charged-count consequences. The existing PR2342 three-call audit explicitly leaves the broader all-batch proof unchecked. This work targets one universal algebraic implication; it does not re-audit the P112 rigidity/frame premises or claim a new decoder floor. Evidence is LOCAL-ONLY until publication. Expires 2026-10-15 09:06 UTC.

Precise statement: for a finite t-by-t matrix K over a field and class maps alpha,beta into a linear order, assume alpha(i) != beta(i), and K(i,j) != 0 implies beta(i)=alpha(j). Prove 2dim ker(I-K) <= t. Transfer through K=CA to arbitrary rectangular A,C and derive the completed low/high term-count bill. Attempt sharp two-cycle controls and counterexamples after dropping either hypothesis. Use Lean kernel checking, source-bound theorem/axiom probes and independent exact finite fixtures; no axiom may encode the desired rank bound.

Pins: canonical main 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2; PR2338 82700676e1d42acf98dc1921cb6ef82551620008, README section 3.4. Credit DreamingOfClouds for Lemma K, Theorem Bk and the normal/frame argument; Sricharan Vagvala PR2294/PR2342 for the two/three-call lineage, and alephnan PR1714 for the batch model. Our addition is the formal implication with exact hypotheses, not the underlying proof idea.

Random nonce 39160e84f0f7e0d9acb16904f92cb37c selected independent-verification. I take its second suggestion, formal-interface-lemma, after checking that the newest raw-price and packing-cap questions already have independent audits (PR2359/2360). Scope changed from a selected-review lemma to this pending all-batch cost boundary. Expected package: research/lean-normal-class-rank/. Time budget roughly 60 minutes; stop at a kernel-checked implication or a precise counterexample/handoff. Full P112 geometric premises, physical supplier admission and kappa are outside scope.

The latest complete PR/Discussion search found no existing formalization of this lemma; PR2342 is the relevant deliberately narrower independent proof. Search coverage/limits will be retained in TASK.json. Prepared by Gareth Davidson with substantial OpenAI Codex assistance; no subagents or independent human review.