DONE: Lean general decoder rank bound and nonzero-minor cost interface

[bitplane]

DONE / 2026-10-15T02:50:55.593253+00:00 / priority revision 4. Claim released.

Completed the general rectangular decoder rank-to-cost interface requested in handoff item 5, with the original-field cost preserved under a field extension, its Hadamard form and a nonzero-minor lower-bound corollary. Author-checked Lean proofs and independent finite arithmetic; no independent human review. Public artifact: PR2267, exact head f7e8e8a3ff8a889366f97e222eef262d61312b58. Both fresh local Lean build modes passed; all 18 axiom reports use only the standard three axioms. The specific jet/valuation determinant witness is the next separate proof obligation. No new mathematical rank principle, supplier or κ is claimed. Hosted CI was queued at publication.

The existing rank-sum, support-restriction and field-map helpers are DreamingOfClouds’s unchanged source from PR2162 head 113a718265c62aec301c5695f4bfb9c421bef7ab, with notice and license preserved. New statements do not assume diagonal/full-rank output, unit diagonal, admissibility or injective minor selectors. Explicit expanded signatures and rectangular rational-function-field/empty-family examples are included.

Validation: all four local Lean modules built against Mathlib 55b7917b472489c7c56a0fa6393af05cfd536599 with all nine dependency heads checked. Existing-cache and fresh dependency-fetch modes produced identical receipts. Three invalid proofs omitting support or nonzero-minor hypotheses received actual type errors. The independent Python implementation passed 196,608 cases. Registered CPython 3.12.3 replay and eight failure-control groups passed; both lightweight commands also passed under optimized CPython 3.14.4 in a read-only Git-free export with all 18 files unchanged. The default command explicitly reports kernel_checked=false; the dedicated workflow runs Lean. Mathlib itself used the official cache rather than a full source rebuild.

Canonical main and predecessor remained unchanged at the final checkpoint. Final overlap completely paginated 490 open PRs and 973 Discussion records, without warnings; all six targeted matches reviewed. Published PR title, body, head, remote branch and 19-file scope were read back and verified. No selected or frozen sources changed.

Next useful task: instantiate minor_le_cost for one pinned jet certificate, then prove the particular nonzero determinant from a formal leading-coefficient/valuation argument. That task requires its own precise statement and is unclaimed here. Gareth Davidson/@bitplane with substantial OpenAI Codex assistance; no subagents.

---

Original claim (historical; now released):

CLAIM / 2026-10-15T02:19:40.356800+00:00 / priority revision 4.

Taking item 5 of DreamingOfClouds’s explicit Lean handoff: expose the general decoder rank-to-cost bound needed by the non-diagonal jet/generic-rank arguments. Evidence is currently LOCAL-ONLY; the pinned Lean toolchain and Mathlib cache are available, but no new proof is complete.

Precise scope: arbitrary finite rectangular matrices B over a field F, a field homomorphism F→L, and finitely many L-valued row/column weights whose supports lie in declared sets S_j,U_j. Prove rank_L(Σ_j diag(p_j) map(B) diag(q_j)) ≤ Σ_j rank_F B[S_j,U_j], without diagonal-output or nonzero-output-diagonal assumptions. Provide the entrywise Hadamard form and a corollary turning a nonzero selected minor over L into a base-field cost lower bound. These are generic interface lemmas; the valued/jet leading-term argument, specific anti-Fano certificate, T=3 conjecture, supplier implementation and kappa remain outside scope.

Predecessor PR2162 head 113a718265c62aec301c5695f4bfb9c421bef7ab, research/char2-jets/lean/DecoderDuality.lean. Its rank_sum_le, support-restriction and field-map lemmas already contain the proof ingredients and will be imported with exact-source credit. This is a requested formal interface completion, not a new mathematical rank principle or independent reproof of those helpers. Inspecting the existing diagonal theorem exposed exactly which output assumptions to remove.

Method: immutable predecessor Lean source, kernel-checked bridge theorems, explicit rectangular/non-diagonal and empty-support examples, rejected missing-support/minor hypotheses, source/axiom inventory and a reproducible pinned build. Toolchain Lean4.33.0-rc1; Mathlib 55b7917b472489c7c56a0fa6393af05cfd536599. Success means actual Lean acceptance with only the stated standard axioms and all real hypotheses displayed; stop at this interface, without claiming formalization of the jet theorem. No numerical improvement or changed paid invoice is being claimed.

Base 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2; original OS nonce d8d89da538eb6248543c95377394d893, independent-verification / formal-interface-lemma, scope key e3ffea67887eeb4c396c. Scope refined from the suggested theorem-binding audit to this explicit formalization handoff; no reroll. Source-baseline orientation passed. Fresh overlap completely paginated482openPRs and961Discussion records, no warnings; all5 targeted matches inspected, no competing general-rank formalization found.

Expected artifact: one small Lean extension with theorem/source binding, exact pinned dependencies, acceptance/negative controls, documentation and a focused PR. About60minutes for implementation/verification. Claim expires 2026-10-15T04:19:40.356800+00:00. Gareth Davidson/@bitplane with substantial OpenAI Codex assistance; no subagents or independent human review.