Research: a stronger P112 two-call COPY floor for arbitrary cross forms

research/p112-cross-form-rank-tradeoff/CountFloor.lean

@@ -0,0 +1,60 @@
+import Lean
+
+/-
+Copyright (c) 2026 commdata2338. Apache-2.0.
+Prepared with substantial OpenAI Codex assistance.
+
+Only the integer-count interface is formalized. Matrix ranks, support
+classification, and the derivation of hcharge are explicit external premises.
+-/
+namespace P112CrossForm
+
+theorem floor_of_counts (k n d mu charge : Nat)
+    (hk : k ≤ 8)
+    (hinc : 16 ≤ n + d)
+    (hschur : 16 ≤ n + mu)
+    (hcharge : 8 * n + (8 - k) * d + k * mu ≤ charge) :
+    128 ≤ charge := by
+  match k with
+  | 0 => omega
+  | 1 => omega
+  | 2 => omega
+  | 3 => omega
+  | 4 => omega
+  | 5 => omega
+  | 6 => omega
+  | 7 => omega
+  | 8 => omega
+  | k + 9 => omega
+
+-- This is the source-level specialization for the new rank-(4,4) region.
+theorem rank_four_floor (n d mu charge : Nat)
+    (hinc : 16 ≤ n + d)
+    (hschur : 16 ≤ n + mu)
+    (hcharge : 8 * n + 4 * d + 4 * mu ≤ charge) :
+    128 ≤ charge := by
+  exact floor_of_counts 4 n d mu charge (by decide) hinc hschur hcharge
+
+-- Pure directions are charged separately; their counts each dominate mu.
+theorem floor_of_term_prices (k n d mu charge c01 c10 p01 p10 : Nat)
+    (hk : k ≤ 8) (hinc : 16 ≤ n + d) (hschur : 16 ≤ n + mu)
+    (hp01 : mu ≤ p01) (hp10 : mu ≤ p10) (hcross : k ≤ c01 + c10)
+    (hbill : 8 * n + (8 - k) * d + c01 * p01 + c10 * p10 ≤ charge) :
+    128 ≤ charge := by
+  have h01 := Nat.mul_le_mul_left c01 hp01
+  have h10 := Nat.mul_le_mul_left c10 hp10
+  have hsum := Nat.mul_le_mul_right mu hcross
+  rw [Nat.add_mul] at hsum
+  apply floor_of_counts k n d mu charge hk hinc hschur
+  omega
+
+-- Concrete counterexamples to dropping one of the mathematical inputs.
+example : 16 ≤ 8 + 8 ∧ 8 * 8 + (8 - 0) * 0 + 0 * 8 ≤ 64 ∧ ¬128 ≤ 64 := by decide
+example : 16 ≤ 0 + 16 ∧ 8 * 0 + (8 - 8) * 16 + 8 * 0 ≤ 0 ∧ ¬128 ≤ 0 := by decide
+example : 16 ≤ 8 + 8 ∧ 8 * 8 + (8 - 8) * 8 ≤ 64 ∧ ¬128 ≤ 64 := by decide
+example : 16 ≤ 16 + 0 ∧ 7 * 16 ≤ 112 ∧ ¬128 ≤ 112 := by decide
+
+#print axioms floor_of_counts
+#print axioms rank_four_floor
+#print axioms floor_of_term_prices
+end P112CrossForm

research/p112-cross-form-rank-tradeoff/PROOF.md

@@ -0,0 +1,170 @@
+# A Schur price for arbitrary two-call P112 cross forms
+
+This is a scoped written proof, with rechecked finite P112 premises. Only the
+integer-count implication in section 4 is formalized in Lean. No physical
+supplier or multiplication theorem is claimed.
+
+## 1. Model and inherited premises
+
+Use Sagar Thakrar's PR2294 section 4 model, based on alephnan's PR1714:
+two independent P112 calls, root-code factors, any finite number of terms,
+ordinary transpose over the complex numbers, and separate-total union rank
+prices. Let X be the fixed 112-by-8 P112 root matrix. Since X^T X=56 I,
+exactness is equivalent to
+
+    sum_j a_j c_j^T = I_16,     a_j,c_j in C^8 direct-sum C^8.
+
+Delete terms with a zero factor. A factor block x has support supp(Xx).
+Reader labels and source labels use dual binary coordinates; their within-call
+pairing is the ordinary dot product. This is a change of coordinates from the
+nondegenerate form b in PR2294, not a changed within-call pairing.
+
+The independently checked finite premises are:
+
+* Each nonzero root-code support spans the full binary space of dimension 9
+  or one of eight coordinate-support hyperplanes, on both sides.
+* Every ordered pair of nonzero within-call support spans pairs at rank at
+  least 8. Coordinate support pairs all have rank exactly 8.
+
+For completeness, the support implication follows from the finite census:
+for each of the 511 nonzero binary functionals, collect the roots on which
+it evaluates to one. Their rational span has rank 8 in 503 cases, and rank 7
+in eight cases with distinct coordinate-line kernels. If a functional kills
+the labels of supp(Xx), these collected roots are orthogonal to x. Thus only
+one of those eight kernels can occur for nonzero x. Two distinct annihilating
+functionals would force x into two distinct coordinate lines, which intersect
+only at zero. This proves the span classification over C as well, since
+rational matrix rank is unchanged by extension to C. The 64 hyperplane-pair
+ranks, plus monotonicity when either span is full, prove the second premise.
+
+Put arbitrary independent binary forms beta01 and beta10 between the two
+call summands. They need not be transposes and need not arise from a single
+nine-dimensional label table. Within-call pairings are unchanged. Price each
+term by the rank over F2 of the union pairing matrix on its actual reader
+and source support spans. This is the 18-dimensional direct-sum model of
+PR2294, not the single-table rank-nine model of PR2338.
+
+Write r01,r10 for the global ranks of the two forms. Write c01,c10 for
+their minimum ranks over the 64 ordered coordinate-support hyperplane pairs.
+Monotonicity shows these are lower bounds for all nonzero root-code support
+pairs. Restriction loses at most one rank per side, so
+
+    c01 >= max(0,r01-2),   c10 >= max(0,r10-2).
+
+All these ranks are binary ranks, unlike the complex ranks in section 3.
+
+## 2. The double-term price
+
+Call a term *pure 01* if only a^0 and c^1 are nonzero, and *pure 10*
+for the reverse direction. All other terms are *non-pure*. A non-pure
+term is *double* if all four blocks are nonzero.
+
+Every non-pure term costs at least 8. A double term costs at least
+
+    16 - k,     k = min(8,r01,r10).                            (1)
+
+Proof: in each diagonal within-call block choose a nonsingular 8-by-8
+minor; these choices independently select rows and columns in each call.
+The resulting 16-by-16 submatrix is [A B; C D], with A and D invertible.
+Over F2, block elimination gives
+
+    rank [A B; C D] = 8 + rank(D - C A^-1 B)
+                   >= 16 - rank(C A^-1 B)
+                   >= 16 - min(rank B,rank C)
+                   >= 16 - min(r01,r10).
+
+The retained within-call minor also gives rank at least 8. Combining them
+gives (1). No symmetry of B or C is used. This improves PR2294's general
+double-term bound max(8,16-rho01-rho10) using the smaller of the two ranks.
+The independently exhaustive 2-by-2 analogue checks all 9,216 choices with
+invertible diagonal blocks, with equality achieved for each cross-rank pair.
+That census is a control for, not a proof of, the arbitrary-size argument.
+
+## 3. Complex coefficient counts
+
+Let n be the number of non-pure terms, d the number of double terms,
+and p01,p10 the pure counts. Each identity diagonal block has rank 8 over
+C, so at least eight terms must have both factors nonzero in that call.
+Counting across calls gives
+
+    n+d >= 16.                                               (2)
+
+Let R01 and R10 be the sums of the pure coefficient outer products in
+the two directions. Define t01=rank_C R01, t10=rank_C R10 and
+mu=min(t01,t10). Then t01<=p01 and t10<=p10. The non-pure terms sum to
+
+    [I_8  -R01; -R10  I_8].
+
+The complex Schur complement implies this matrix has rank at least
+16-mu. A sum of n rank-one matrices has rank at most n. Therefore
+
+    n+mu >= 16.                                              (3)
+
+This is PR2294's count argument, retained with credit. It concerns the
+aggregate pure coefficient matrices, not binary form ranks.
+
+## 4. The strengthened sufficient condition
+
+**Theorem.** If c01+c10 >= k=min(8,r01,r10), every exact factorization
+in section 1 has COPY cost at least 128. The minimum is exactly 128.
+
+The total charge is at least
+
+    8n + (8-k)d + c01*p01 + c10*p10
+      >= 8n + (8-k)d + (c01+c10)mu
+      >= 8n + (8-k)d + k*mu.                                 (4)
+
+If n>=16, (4) is at least 128. Otherwise let delta=16-n. Equations
+(2) and (3) give d>=delta and mu>=delta. Since 0<=k<=8,
+
+    8n+(8-k)d+k*mu >= 8n+(8-k)delta+k*delta = 128.
+
+The usual eight coordinate terms per call give I_16 and cost 16*8=128,
+independently of the cross forms, proving sharpness.
+
+`P112CrossForm.floor_of_counts` in `CountFloor.lean` formalizes exactly
+the natural-number implication from 0<=k<=8, (2), (3), and (4) to the
+floor. `rank_four_floor` specializes it to k=4. `floor_of_term_prices`
+also proves the passage from separately charged pure directions in (4),
+assuming their counts each dominate mu and their price sum dominates k.
+The binary matrix bound,
+complex rank argument, support census interpretation, and initial
+per-term bill in (4) are **not** formalized in that file. Its counterexamples demonstrate
+that omitting the incidence count, Schur count, pure surcharge or rank-eight
+within-call charge invalidates the corresponding weakened claim.
+
+## 5. Rank-only corollary and boundary
+
+A sufficient condition depending only on global ranks is
+
+    max(0,r01-2)+max(0,r10-2) >= min(8,r01,r10).                (5)
+
+In particular (5) holds whenever max(r01,r10)>=4 or either rank is zero.
+For the first assertion, assume r01>=r10. If r10<=2, r01-2>=2>=r10;
+if r10>=2, r01+r10-4>=r10. Both bounds dominate min(8,r01,r10).
+
+Among the 100 ordered rank pairs in {0,...,9}^2, condition (5) certifies
+93. The seven not decided by this rank-only test are exactly
+
+    (1,1), (1,2), (2,1), (2,2), (2,3), (3,2), (3,3).
+
+PR2294's global rank-sum-at-least-12 corollary covers 28 pairs; its
+zero-form result and form-specific condition provide additional coverage.
+Our comparison is with that specific rank-only corollary, not a claim
+that every one of the other 65 pairs was previously unresolved.
+
+The rank-(4,4) forms in RESULT.json have c01+c10<8 but satisfy (5),
+so PR2294 Proposition B's old form-specific test does not decide them
+while the new theorem does. The 100 concrete form pairs checked by the
+verifier are examples, not an enumeration of all binary forms. Each has
+five exact decoder fixtures, including a non-coordinate mixed factorization.
+
+The seven residual rank pairs are not counterexamples or proven openings:
+their actual c01,c10 can still satisfy section 4. No sub-128 decoder was
+found or claimed. The criterion is sufficient, with no converse asserted.
+No physical chart conversion, common-label embedding, supplier hosting,
+precision, recursive interface, rank-power moment or kappa consequence is
+established. The contribution is a COPY-rank-sum floor in the stated model.
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+New work is Apache-2.0; predecessor text retains its original credit.

research/p112-cross-form-rank-tradeoff/README.md

@@ -0,0 +1,126 @@
+# P112 cross forms: a Schur rank tradeoff and formal COPY-floor interface
+
+Two independent P112 root-code decoders still require **COPY cost 128**
+under a broader class of arbitrary cross-call binary forms. If their global
+ranks are r01,r10 and their minimum support-restricted ranks are c01,c10,
+the sufficient condition is
+
+    c01 + c10 >= min(8, r01, r10).
+
+This follows by charging a term touching both calls at least
+`16-min(8,r01,r10)`, then using the exact coefficient identity to count
+terms. The [written proof](PROOF.md) and [Lean count theorem](CountFloor.lean)
+state the different evidence boundaries explicitly. This is a COPY-rank-sum
+floor, not a physical supplier, rank-power moment bound or new kappa.
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+
+## Scope and result
+
+The model is PR2294 section 4: arbitrary directed cross forms on two copies
+of a nine-dimensional binary space, unchanged within-call P112 pairings,
+any finite number of complex root-code factors, and separate-total union
+rank prices. The union pairing need not fit a single nine-dimensional table.
+
+The rank-only sufficient test
+`max(0,r01-2)+max(0,r10-2) >= min(8,r01,r10)` covers **93 of the 100 ordered
+global rank pairs** in `0..9`. It covers every pair with maximum at least
+four and every pair with a zero rank. Seven low-rank pairs remain undecided
+by that test; they are listed in the proof and RESULT.json. They are not
+claimed to admit savings.
+
+PR2294's form-specific sufficient condition requires `c01+c10>=8`; its
+rank-sum-at-least-12 corollary covers 28 global rank pairs. This package
+strengthens those tests. Its explicit rank-(4,4) example has support minima
+(3,3), so the old test fails while the new test proves the exact minimum
+128. Sixteen within-call coordinate terms attain 128 for every cross form.
+
+## Evidence and reproduction
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3 -I -B scripts/research_package.py --package research/p112-cross-form-rank-tradeoff --check-only
+python3 -I -B scripts/research_package.py --package research/p112-cross-form-rank-tradeoff
+python3 -I -B research/p112-cross-form-rank-tradeoff/test_integrity.py
+```
+
+The registered replay independently constructs the Hamming-shell root set,
+checks 12,544 label pairings, both 511-functional support censuses, all 64
+within-call support ranks, 9,216 small block matrices and 505 exact decoder
+cost fixtures. Eight mathematical controls reject weakened hypotheses.
+A deliberately degenerate rank-(1,1) example makes the criterion abstain;
+finite decoders tested there do not decide its unrestricted minimum.
+
+Expected marker:
+
+```text
+PASS_P112_CROSS_FORM_RANK_TRADEOFF ranks=93/100 blocks=9216 decoders=505 controls=8 abstentions=1
+```
+
+The five coefficient identities are checked in dimension 16, which is
+equivalent to all 224-by-224 scalar demand entries because the source-bound
+root matrix has an explicit left inverse. Binary term costs are computed
+on actual support spans, preserving matrix rank. No predecessor verifier is
+imported. Replay compares every structured RESULT.json field and preserves
+explicit checks under `python -O`. Typical local replay is a few seconds.
+
+Separately, use **Lean 4.21.0** with its bundled core libraries;
+Mathlib and Lake are unnecessary:
+
+```sh
+lean +leanprover/lean4:v4.21.0 -j1 research/p112-cross-form-rank-tradeoff/CountFloor.lean
+python3 -I -B research/p112-cross-form-rank-tradeoff/check_lean.py --lean /path/to/lean
+```
+
+The second command requires the selected executable to report 4.21.0. It
+builds three theorems, checks four concrete counterexamples and rejects four
+false proof files. Their axiom audits list only `propext` and `Quot.sound`.
+The registered Python replay does **not** build Lean; its pass is finite
+certificate evidence only. The complete matrix/rank proof is written,
+not kernel formalized. Local checks are author checks, not independent review.
+
+`--write-result` on verify.py regenerates RESULT.json for intentional updates;
+ordinary replay is read-only. Source and predecessor pins are in SOURCES.json.
+
+## Task, overlap and attribution
+
+Task `formal-interface-lemma`, refined to the rank-price/count interface;
+the full card is in [TASK.json](TASK.json). The claim is in
+[Discussion #2372](https://github.com/CrocSwap/integer-mult-bounds/discussions/2372). Base:
+`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`.
+
+* Sagar Thakrar (@thakrarsagar), [PR2294](https://github.com/CrocSwap/integer-mult-bounds/pull/2294),
+  head `18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0`, supplies the arbitrary
+  cross-form model, support premises, original count argument, weaker
+  sufficient conditions and the open question. Its proof is retained verbatim
+  under sources/ with its credit and Apache-2.0 notice.
+* Alephnan's PR1714 supplies the root-code batch model; Mihir Srivastava's
+  PR845 and Adam Gall's PR1098 supply the support-lemma lineage. The fixed
+  main-branch P112 single-lift geometry is an immutable input.
+* DreamingOfClouds' [PR2338](https://github.com/CrocSwap/integer-mult-bounds/pull/2338),
+  head `82700676e1d42acf98dc1921cb6ef82551620008`, proves related batch floors
+  with a single rank-nine label table. Its text is pinned for scope comparison;
+  none of its SAT results is a premise of this proof.
+
+The new contribution is the minimum-of-cross-ranks Schur price, its coupling
+to the prior complex count argument, the expanded sufficient region and the
+kernel-checked conditional count interface. It does not re-claim the original
+128 isometric-chart floor. All new work is Apache-2.0. Substantial OpenAI
+Codex assistance was used for derivation, implementation, checking and writing.
+
+## Open next questions
+
+1. Decide the remaining rank pairs (1,1), (1,2), (2,1), (2,2), (2,3),
+   (3,2), (3,3) when the actual support minima fail the new criterion.
+   A small first step is to classify which of the eight hyperplanes kill
+   each rank-one form. This matters because this proof leaves exactly that
+   low-rank source of possible sub-128 behavior; coefficient identities
+   and per-term support restrictions still have to be enforced jointly.
+2. Formalize the matrix-to-count premises. Start with the 16-by-16 block
+   Schur bound over F2 and C and then the support classification. This would
+   reduce the current written-proof boundary; the Python census and the
+   natural-number theorems alone do not formalize those implications.
+
+No physical implementation or additional construction search is justified
+by this sufficient-condition result alone.