diff --git a/research/p112-cross-form-rank-tradeoff/CountFloor.lean b/research/p112-cross-form-rank-tradeoff/CountFloor.lean
new file mode 100644
index 0000000000..ba63f036ce
--- /dev/null
+++ b/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
diff --git a/research/p112-cross-form-rank-tradeoff/PROOF.md b/research/p112-cross-form-rank-tradeoff/PROOF.md
new file mode 100644
index 0000000000..f29d1c7c18
--- /dev/null
+++ b/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.
diff --git a/research/p112-cross-form-rank-tradeoff/README.md b/research/p112-cross-form-rank-tradeoff/README.md
new file mode 100644
index 0000000000..107a0a05c0
--- /dev/null
+++ b/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.
diff --git a/research/p112-cross-form-rank-tradeoff/RESULT.json b/research/p112-cross-form-rank-tradeoff/RESULT.json
new file mode 100644
index 0000000000..a78c57fd65
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/RESULT.json
@@ -0,0 +1,160 @@
+{
+  "block_census": {
+    "matrices": 9216,
+    "tight_by_cross_rank": {
+      "0,0": 36,
+      "0,1": 324,
+      "0,2": 216,
+      "1,0": 324,
+      "1,1": 1296,
+      "1,2": 1296,
+      "2,0": 216,
+      "2,1": 1296,
+      "2,2": 216
+    }
+  },
+  "controls": [
+    "missing_incidence",
+    "missing_schur",
+    "missing_pure_surcharge",
+    "undercounted_within_price",
+    "overstrong_schur",
+    "missing_within_rank",
+    "codimension_two_loss",
+    "missing_cross_endpoint_term"
+  ],
+  "form_fixtures": {
+    "coefficient_endpoints": 5,
+    "criterion_passes": 100,
+    "decoder_cases": 505,
+    "form_pairs": 100,
+    "new_rank44_example": {
+      "beta01_rows": [
+        1,
+        2,
+        4,
+        8,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "beta10_rows": [
+        4,
+        8,
+        16,
+        32,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "decoder_costs": {
+        "noncoordinate_schur": 201,
+        "one_cross": 132,
+        "schur": 185,
+        "standard": 128,
+        "two_cross": 136
+      },
+      "k": 4,
+      "ranks": [
+        4,
+        4
+      ],
+      "support_minima": [
+        3,
+        3
+      ]
+    },
+    "old_criterion_passes": 47,
+    "undecided_control": {
+      "beta01_rows": [
+        33,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        33,
+        0
+      ],
+      "beta10_rows": [
+        33,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        33,
+        0
+      ],
+      "decoder_costs": {
+        "noncoordinate_schur": 148,
+        "one_cross": 128,
+        "schur": 142,
+        "standard": 128,
+        "two_cross": 128
+      },
+      "ranks": [
+        1,
+        1
+      ],
+      "support_minima": [
+        0,
+        0
+      ],
+      "verdict": "criterion inconclusive"
+    }
+  },
+  "rank_region": {
+    "certified_pairs": 93,
+    "prior_rank_sum12_pairs": 28,
+    "unresolved_pairs": [
+      [
+        1,
+        1
+      ],
+      [
+        1,
+        2
+      ],
+      [
+        2,
+        1
+      ],
+      [
+        2,
+        2
+      ],
+      [
+        2,
+        3
+      ],
+      [
+        3,
+        2
+      ],
+      [
+        3,
+        3
+      ]
+    ]
+  },
+  "scope": "written conditional matrix proof; finite premises; separate Lean count theorem",
+  "support_censuses": [
+    {
+      "7": 8,
+      "8": 503
+    },
+    {
+      "7": 8,
+      "8": 503
+    }
+  ],
+  "support_pair_ranks": 64,
+  "within_pairings": 12544
+}
diff --git a/research/p112-cross-form-rank-tradeoff/SOURCES.json b/research/p112-cross-form-rank-tradeoff/SOURCES.json
new file mode 100644
index 0000000000..0089d9cd0d
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/SOURCES.json
@@ -0,0 +1,47 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "path": "research/p112-single-lift/reference-geometry.json",
+      "usage": "input",
+      "git_blob": "d862663d3c0ffe3c72df510e89997beb85cef640",
+      "sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080"
+    }
+  ],
+  "predecessors": [
+    {
+      "head": "18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0",
+      "source_path": "research/p112-batch-chart-change/PROOF.md",
+      "local_path": "sources/PR2294-PROOF.md",
+      "git_blob": "177c27bd6c4f75a2524eb2e8ade74045b7abb060",
+      "sha256": "b0aef60119916aea6f768a92896be3b934a017a14e0ffdb17d66d6187ae3438b"
+    },
+    {
+      "head": "82700676e1d42acf98dc1921cb6ef82551620008",
+      "source_path": "research/decoder-floors-frontier-format/README.md",
+      "local_path": "sources/PR2338-README.md",
+      "git_blob": "a1751a2a0b35d8607cf901da6fae6036cdb9e1bc",
+      "sha256": "0a941616cd2fac679182e5bb97e9a307bf22e42ac9541bbca3fadc81b1fda2b5"
+    },
+    {
+      "head": "82700676e1d42acf98dc1921cb6ef82551620008",
+      "source_path": "research/decoder-floors-frontier-format/NOTICE.md",
+      "local_path": "sources/PR2338-NOTICE.md",
+      "git_blob": "8b1f75f7e7c0002b5c08b2e06e5bed32fae5b6f0",
+      "sha256": "95ffb286f159eaab0e1620fc860fea91b94fe14a28ed4a4da52716f52f53bc7a"
+    }
+  ]
+}
diff --git a/research/p112-cross-form-rank-tradeoff/TASK.json b/research/p112-cross-form-rank-tradeoff/TASK.json
new file mode 100644
index 0000000000..0d194fa1e1
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/TASK.json
@@ -0,0 +1,85 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "PR2294 arbitrary two-call P112 cross forms: a stronger Schur rank price, the exact conditional COPY128 count interface in Lean, and its finite source binding.",
+  "scope_change_reason": "Take the named open cross-form interface in PR2294 rather than repeat a selected-supplier arithmetic proof. The formalization covers the natural-number implication only; matrix premises remain explicit.",
+  "bottleneck_link": "Eliminates additional two-call cross-form coupling ranks as routes to a lower separate COPY bill, while making the matrix-to-count proof boundary explicit. No supplier or kappa improvement.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the sufficient-condition theorem, exact P112 premises, Lean count implication and negative controls; leave the seven low-rank pairs and physical implementation open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; CountFloor.lean (Lean4.21.0, propext and Quot.sound only); RESULT.json (93 rank pairs,9216 block matrices,505 decoder fixtures,8 controls and1 abstention).",
+  "author": "commdata2338",
+  "ai_assistance": "Substantial OpenAI Codex (GPT-6 Astra) assistance in derivation, implementation, checking and writing; no independent human review claimed.",
+  "open_questions": [
+    {
+      "question": "Decide the seven residual global rank pairs when the actual support-minimum criterion fails.",
+      "why_it_matters": "This is the remaining low-rank region not excluded by the new sufficient condition.",
+      "first_step": "Classify rank-one forms by which of the eight reader/source hyperplanes annihilate them.",
+      "blocked_by": "Must enforce exact complex coefficient identities and support-dependent prices jointly; finite fixture costs do not prove a minimum."
+    },
+    {
+      "question": "Formalize the binary and complex matrix-to-count implications.",
+      "why_it_matters": "The current kernel theorem assumes the matrix-derived arithmetic inequalities.",
+      "first_step": "Prove the block Schur lower bound with invertible within-call8-by8 minors.",
+      "blocked_by": "Needs a matrix-rank library and formal binding of the finite P112 support premises."
+    }
+  ],
+  "selection": {
+    "type": "live-open-question override",
+    "task_id": "formal-interface-lemma",
+    "scope_key": "636f26dec98e26b296e8",
+    "card_retrieval_nonce": "e08434b24e3b43ce5b9af0fdcc95d1ac",
+    "request": "PR2294 section4 and open question1",
+    "priority_revision": 4
+  },
+  "predecessors": {
+    "2294": "18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0",
+    "2338": "82700676e1d42acf98dc1921cb6ef82551620008"
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2372",
+  "final_refresh": {
+    "utc": "2026-10-15T07:04:46.599084+00:00",
+    "main_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+    "priority_revision": 4,
+    "changed_since_base": []
+  }
+}
diff --git a/research/p112-cross-form-rank-tradeoff/VERIFY.json b/research/p112-cross-form-rank-tradeoff/VERIFY.json
new file mode 100644
index 0000000000..a12fcd182a
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/VERIFY.json
@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p112-single-lift/reference-geometry.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact source pins, P112 support premises, Schur block census, explicit decoder endpoints and prices, eight mathematical failure controls, abstention and full RESULT.json equality"
+    }
+  ]
+}
diff --git a/research/p112-cross-form-rank-tradeoff/check_lean.py b/research/p112-cross-form-rank-tradeoff/check_lean.py
new file mode 100644
index 0000000000..24844b05da
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/check_lean.py
@@ -0,0 +1,55 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Build the core-only Lean count lemma and reject four false variants."""
+import argparse
+from pathlib import Path
+import shutil
+import subprocess
+import tempfile
+
+HERE = Path(__file__).resolve().parent
+
+
+def invoke(executable, filename):
+    return subprocess.run([executable, "-j1", "-DwarningAsError=true", str(filename)],
+                          capture_output=True, text=True, timeout=60)
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument("--lean", default=shutil.which("lean"))
+    args = parser.parse_args()
+    if not args.lean:
+        raise SystemExit("Lean 4.21.0 required; pass --lean PATH (no automatic installation)")
+    version = subprocess.check_output([args.lean, "--version"], text=True, timeout=60).strip()
+    if not version.startswith("Lean (version 4.21.0,"):
+        raise SystemExit("Expected Lean 4.21.0, got " + version)
+    result = invoke(args.lean, HERE / "CountFloor.lean")
+    if result.returncode or "sorryAx" in result.stdout + result.stderr:
+        raise SystemExit(result.stdout + result.stderr)
+    for name in ("floor_of_counts", "rank_four_floor", "floor_of_term_prices"):
+        expected = f"'P112CrossForm.{name}' depends on axioms: [propext, Quot.sound]"
+        if expected not in result.stdout:
+            raise SystemExit("Unexpected axiom audit: " + result.stdout)
+    # Each missing-hypothesis variant is false, with a concrete witness in
+    # CountFloor.lean. A failed proof here is a compiler control, not its proof.
+    controls = [
+        "example : 128 ≤ 64 := by decide\n",
+        "example : 128 ≤ 0 := by decide\n",
+        "example : (8 : Nat) * 8 ≥ 128 := by omega\n",
+        "example : (7 : Nat) * 16 ≥ 128 := by omega\n",
+    ]
+    with tempfile.TemporaryDirectory(prefix="p112-count-controls-") as directory:
+        for i, content in enumerate(controls):
+            path = Path(directory) / f"False{i}.lean"
+            path.write_text("import Lean\n" + content)
+            failed = invoke(args.lean, path)
+            if failed.returncode == 0 or "error:" not in failed.stdout:
+                raise SystemExit("False theorem accepted or wrong failure: " + failed.stdout + failed.stderr)
+    print(version)
+    print(result.stdout.strip())
+    print("PASS_LEAN_P112_COUNT_FLOOR theorems=3 concrete_counterexamples=4 rejected_proofs=4")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/research/p112-cross-form-rank-tradeoff/sources/PR2294-PROOF.md b/research/p112-cross-form-rank-tradeoff/sources/PR2294-PROOF.md
new file mode 100644
index 0000000000..177c27bd6c
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/sources/PR2294-PROOF.md
@@ -0,0 +1,281 @@
+# Two-call P112 batch floor under changed cross-call label charts
+
+Scope: k = 2 independent P112 all-pairs demands (C = I_2), root-code factors,
+separate-total union price, exactly as in merged PR1714
+(`research/p112-batch-centre-floor`, alephnan). The **only** change is the
+cross-call label chart. This is a written proof with exact finite premises
+rechecked by `verify.py`. It is not a Lean proof and has not had independent
+human review.
+
+## 0. Inherited model and premises
+
+X is the 112 x 8 live P112 root matrix (norm four, frame-adapted Hamming
+coordinates), with `X^T X = 56 I_8`. Labels ell_i live in the nine-dimensional
+binary space V with nondegenerate symmetric pairing b, where
+`b(ell_i, ell_j) = 1 + x_i.x_j/2 mod 2` (PR1714 section 1).
+
+A factorization is `D T^T = I_2 (x) X X^T` with `D = (I_2 (x) X) A` and
+`T = (I_2 (x) X) Cf`. A and Cf are complex 16 x m matrices, and the transpose
+is ordinary. Since `I_2 (x) X` has the left inverse `(1/56)(I_2 (x) X^T)`,
+this is equivalent to
+
+    A Cf^T = I_16.                                                    (0)
+
+Term j has the reader column `a_j = (a_j^0, a_j^1)` and the source column
+`c_j = (c_j^0, c_j^1)`, with one 8-block per call. Terms with a zero column
+are discarded.
+
+**Inherited finite premises** (PR845 Mihir Srivastava; PR1098 Adam Gall;
+PR1714 alephnan; rechecked here by an independent stdlib construction):
+
+* (S) *Support lemma.* For nonzero complex `a in C^8`, the label span of
+  `supp(Xa)` is V or one of eight hyperplanes `H_k = span ell(E_k)`, where
+  `E_k = supp(X e_k)`. Rechecked: 503 of 511 binary functionals have
+  complement rank 8 and eight have rank 7 with coordinate-line kernels.
+* (P) *Pair lemma.* `rank b|(U x W) >= 8` for any two such spans U, W.
+  Rechecked: all 64 ordered pairs `(E_i, E_j)` have F2 rank 8. The cases
+  involving V (`V x H_k`, rank 8; `V x V`, rank 9) follow from
+  nondegeneracy of b (Gram rank 9, checked).
+* Consequently every root-code support span has dimension >= 8. Taking
+  U = W in (P) gives `rank <= dim U`.
+
+## 1. Changed chart
+
+Call 1 keeps the chart ell. Call 2's row i carries the label `phi(ell_i)`
+for a linear bijection phi of V. A term's union reader-label set is
+
+    L(S_j) = ell(supp X a_j^0)  union  phi ell(supp X a_j^1),
+
+and similarly for the source set L(T_j). Its price is the F2 rank of the
+pairing matrix `[b(s,t)]` for s in L(S_j) and t in L(T_j). A general pair of
+charts (phi_1, phi_2) reduces to `phi = phi_1^{-1} phi_2` only when phi_1
+is an isometry. This package treats call 1 fixed.
+
+**Isometric charts.** Take phi in O(V,b), so `b(phi x, phi y) = b(x, y)`.
+Then call 2's own pairing, and hence its standalone P112 demand price, is
+unchanged; only the cross-call pairing `b(x, phi y)` changes. Conversions
+between charts are granted **free**. This favourable grant only
+strengthens the negative conclusion below.
+
+Equivalent V (+) V description: put the union pairing
+`Gamma = [[G, G phi], [phi^T G, G]]` on V (+) V, with call-s labels in
+summand s. The price of a term is the rank of Gamma on the two union
+spans. `verify.py` checks that the single-V and V (+) V computations
+agree on its fixtures.
+
+## 2. PR1714's per-term step does not extend to changed charts
+
+PR1714 section 3 shows that every active term costs at least eight "even
+when the chosen blocks have different call indices". That uses the
+common chart. Under phi, consider a **pure cross term**, with reader
+column only in call 1 and source column only in call 2:
+`a = (a^0, 0)` and `c = (0, c^1)`. Its price is `rank b|(U x phi W)`, where
+U and W are root-code spans. Hence
+
+    price = dim U - dim(U cap (phi W)^perp) >= dim U + dim W - 9 >= 7.   (1)
+
+Equality needs `U = H_i`, `W = H_j` and `phi v_j in H_i`, where `H_k = v_k^perp`.
+Thus the price is 7 exactly when `b(v_i, phi v_j) = 0`. Under the common chart,
+`b(v_i, v_j) = 1` for all i and j, which is PR1714's 64-pair check.
+
+Let w0 be the characteristic vector, with `b(x,x) = b(x,w0)`. For any
+isotropic u, meaning `b(u,u) = 0`, the transvection `t_u(x) = x + b(x,u) u`
+lies in O(V,b). Then
+
+    b(v_i, t_u v_j) = 1 + b(v_i,u) b(v_j,u),
+
+so t_u makes exactly `s^2` ordered pairs rank 7, where
+`s = #{k : b(v_k,u) = 1}`. The verifier checks this formula on all 255
+isotropic transvections. Its finite census has s^2 = 0 for 15 vectors,
+16 for 224 vectors, and 64 for 16 vectors. Thus **some isometric charts
+make all 64 exceptional cross pairs rank 7**.
+
+The fixed-seed sample has 162 charts, including the identity and the
+targeted chart. Its observed counts are 0, 16, 24, 28, 32, 36, 40 and 64.
+Direct 56 x 56 F2 ranks agree with the formula on 1,600 chart/pair
+instances. So the per-term step **does not extend** to changed charts.
+This is not an error in PR1714, which asserts the step only under its
+common chart.
+
+## 3. Theorem A (isometric charts): the minimum is still 128
+
+**Theorem A.** For every phi in O(V,b) and every exact root-code
+factorization of `I_2 (x) X X^T`, the total union price is at least 128.
+The standard decoder `u_s (x) X e_k` on both sides attains 128. Equality
+requires that the factorization have no pure cross term.
+
+*Proof.* Classify each active term:
+
+* N, **non-pure**: some call s has both `a^s != 0` and `c^s != 0`.
+* P01: `a = (a^0, 0)` and `c = (0, c^1)`.
+* P10: `a = (0, a^1)` and `c = (c^0, 0)`.
+
+These cases exhaust all active terms because there are only two calls.
+
+*Prices.* A non-pure term contains the within-call block for call s as
+a submatrix of its union pairing matrix. For s = 2, isometry gives
+`b(phi x, phi y) = b(x,y)`. Monotonicity and (P) therefore give price >= 8.
+By (1), a pure cross term has price >= 7.
+
+*Counting.* A P01 term's outer product `a c^T` lies only in the (0,1)
+block. A P10 term's lies only in the (1,0) block. Write
+`R01 = sum_{P01} a^0 (c^1)^T` with `r01 = rank R01 <= |P01|`, and define
+R10 and r10 likewise. By (0),
+
+    Q_N := sum_{N} a_j c_j^T = [[I, -R01], [-R10, I]].
+
+The Schur complement over C gives
+`rank Q_N = 8 + rank(I - R10 R01) >= 16 - min(r01, r10)`. A sum of |N|
+rank-one matrices has rank at most |N|, so
+
+    |N| >= 16 - min(r01, r10).                                          (2)
+
+*Total.* Let mu = min(r01, r10). Then
+
+    total >= 8|N| + 7(|P01| + |P10|)
+          >= 8(16 - mu) + 7(r01 + r10)
+          >= 128 + 6 mu + 7(r01 + r10 - 2 mu) >= 128.                   (3)
+
+If a pure term exists, then `|P01| + |P10| >= 1`. If mu = 0, the excess
+`7(|P01| + |P10|) >= 7` is strict. If mu >= 1, then 6mu > 0. Hence
+equality forces `P01 = P10 = {}`. The standard decoder has 16 terms; each
+pairs `H_k` with itself inside one call, so it costs 128 under every
+phi. QED.
+
+*Rank-7 cross terms therefore never help.* Every pure cross term adds
+at least 7 units. It can remove at most `8 min(r01, r10)` units from the
+non-pure count, and only when both directions are present.
+
+**Exact fixtures** (targeted transvection chart, with full 224 x 224
+all-pairs replay):
+
+* One-cross decoder: 16 non-pure terms plus one rank-7 P01 term. Its
+  cost is 135, matching the lower bound in (3). The same decoder costs 136
+  under the common chart.
+* Two-cross decoder: 15 non-pure terms and two rank-7 pure terms. Its cost
+  is 135, against the bound 134.
+* Schur-pattern decoder with `R01 = R10 = I`: 8 non-pure terms and 16 pure
+  terms. Its cost is 188, against the bound 176.
+
+## 4. Proposition B (general cross forms; sufficient condition only)
+
+Secondary model: on V (+) V, keep b as both within-call blocks. Allow
+arbitrary cross forms beta01 (call-1 reader, call-2 source) and beta10.
+Let c01 and c10 be the minimum ranks of beta01 and beta10 on pairs of
+root-code spans. By monotonicity, these minima are taken over the 64
+hyperplane pairs.
+
+**Proposition B.** If `c01 + c10 >= 8`, every exact k = 2 root-code
+factorization costs at least 128.
+
+*Proof.* Non-pure terms still cost at least 8 by the within-call
+submatrix and (P). Count (2) does not depend on prices. Thus
+
+    total >= 8(16 - mu) + c01 r01 + c10 r10
+          >= 128 + (c01 + c10 - 8) mu + c01 (r01 - mu) + c10 (r10 - mu)
+          >= 128.  QED
+
+**Corollary B' (invertible charts in the V (+) V reading).** Let phi be
+any linear bijection of V, isometric or not. Keep b as each call's own
+pairing and take the cross forms `beta01(x,y) = b(x, phi y)` and
+`beta10(x,y) = b(phi x, y)`. For hyperplanes U, W,
+`rank b|(U x phi W) >= dim U + dim W - 9 = 7`, so `c01, c10 >= 7` and
+Proposition B gives the floor 128. More generally, any cross forms with
+`rank beta01 + rank beta10 >= 12` qualify: restricting a form to a pair of
+hyperplanes lowers its rank by at most 2, so `c01 + c10 >= 12 - 4 = 8`.
+Only the single-V reading of a non-isometric chart, where call 2's own
+pairing changes, is left open by this route.
+
+This is **only a sufficient condition**. The zero form beta = 0 has
+`c01 = c10 = 0` but still obeys the floor:
+
+**Proposition C (beta = 0).** If both cross forms vanish, every exact
+factorization costs at least 128.
+
+*Proof.* The union pairing matrix is block diagonal. A term's price is
+the sum, over calls s with `a^s != 0 != c^s`, of its within-call ranks,
+each at least 8. Diagonal block s of (0) is `I_8`, the sum of
+`a^s (c^s)^T` over terms with both parts nonzero. So at least eight such
+(term, s) incidences exist for each s. The total is at least
+`8 * 16 = 128`. QED
+
+This is the "beta = 0 pitfall": the cheap-looking Schur pattern
+`Q_N = [[I,-I],[-I,I]]` (rank 8) plus 16 pure cross terms of price 0
+costs exactly `8 * 16 + 0 = 128`, because each both-call term costs 16.
+The verifier replays it exactly.
+
+**Proposition D (any cross forms; necessary conditions for going below
+128).** Call a non-pure term *double* if `a^0, c^0, a^1, c^1` are all
+nonzero. For such a term, let rho01_j be the rank of beta01 from the
+call-1 reader span to the call-2 source span. Let rho10_j be the rank of
+beta10 from the call-2 reader span to the call-1 source span. Then every
+exact k = 2 root-code factorization satisfies
+
+    total >= 128 - sum_{double j} min(8, rho01_j + rho10_j) + sum_{pure j} price_j.   (4)
+
+*Proof.* Let n_s count the terms with `a^s != 0 != c^s`. Diagonal block s
+of (0) is `I_8`, so `n_s >= 8`. Every non-pure term counts in n_0 or n_1,
+and the d double terms count in both. Hence the non-double non-pure terms
+number at least `16 - 2d`, and each costs at least 8 by (P).
+
+A double term's union matrix is `[[G00, B01], [B10, G11]]`. Here G00 and
+G11 are within-call blocks of rank at least 8 each. B01 and B10 are its
+cross blocks, of ranks rho01_j and rho10_j. Subadditivity of rank gives a
+price of at least `max(8, 16 - rho01_j - rho10_j)`. Summing,
+
+    total >= 8(16 - 2d) + sum_double max(8, 16 - rho01_j - rho10_j) + sum_pure,
+
+which is (4). QED
+
+Corollaries:
+
+* Proposition C is the case beta = 0, where every rho is 0.
+* A sub-128 decoder in any cross-form model needs two things. First,
+  `mu = min(r01, r10) >= 1`; otherwise (2) gives `|N| >= 16` and the
+  total is at least 128. Second, it needs double terms whose cross-form
+  ranks strictly exceed what the pure terms pay. In the verifier,
+  inequality (4) is checked on four exact families, 50 forms each. Its
+  minimum value is 128 there.
+
+**Remark (coordinate families, every cross form).** In the two-cross and
+Schur-pattern families, each both-call term pairs `H_p (+) H_q` with
+itself. G restricted to `H_p x H_p` is invertible by (P). The Schur
+complement then gives price
+
+    8 + rank(G_q - beta10 G_p^{-1} beta01) >= 16 - min(rank beta01, rank beta10),
+
+with all forms restricted to the relevant hyperplanes. The two pure terms
+on the same pair cost `rank beta01 + rank beta10`. Each such group
+therefore costs at least 16, and both families cost >= 128 for every
+cross form. In the one-cross family, mu = 0. Its cost is
+`128 + rank beta01|(H_p x H_q)`.
+
+The verifier checks these families, plus a non-coordinate Schur pattern
+`[I;-I] M M^{-1} [I,-I]` with M upper-triangular all-ones, on three kinds
+of cross form:
+
+* beta = 0;
+* the targeted chart;
+* 48 seeded random cross-form pairs.
+
+All but beta = 0 meet the sufficient condition of Proposition B. That
+makes this a weak finite search; it does **not** show that every cross
+form, or every decoder, obeys the floor.
+
+## 5. What is not proved
+
+* An exact minimum for arbitrary cross forms, which may be below 128 for
+  some form and some non-coordinate decoder. No such decoder was
+  constructed. None of the cross forms here is a legal or priced
+  interface.
+* General k, C != I_2, outside-code overcomplete factors, masked
+  identities and temporal relations. Non-isometric charts in the single-V
+  model change call 2's own demand price, so they are out of scope here
+  (their V (+) V reading is covered by Corollary B').
+* Any physical meaning. Chart conversions are granted free. A real
+  interface would have to pay for them, and that would only raise costs.
+  The floor is internal to PR1714's algebraic separate-total objective;
+  it is not a lower bound for arbitrary interacting circuits.
+
+Prepared by thakrarsagar with substantial AI assistance from Claude
+(Anthropic, Claude Opus 5.5). Apache-2.0.
diff --git a/research/p112-cross-form-rank-tradeoff/sources/PR2338-NOTICE.md b/research/p112-cross-form-rank-tradeoff/sources/PR2338-NOTICE.md
new file mode 100644
index 0000000000..8b1f75f7e7
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/sources/PR2338-NOTICE.md
@@ -0,0 +1,16 @@
+# Notice
+
+Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root).
+
+## Credits
+
+- **#446** (cost model, Theorem C), **#595**, **#1590**, **#2111**, **#2125**, **#2162**, **#2228**, **#2244**, **#2277**: the model, the dense pairing, the root-code floors (#2228 Theorem 4), Theorem 4′ and the frame-intersection certificate (#2277 §5) that this package extends. The statements "P112 ≥ 64 for every rank-8 realisation" (Theorem P), the cross-call batching bounds with `GL(9)` charts and `k ≥ 3` (Theorem B, Bk) and the every-`B` coordinate-block minrank are new here, built on those. Rigidity of the minimal-rank label table (Theorem R) is new here for E8, P112, P104 (#968's unit and class representatives), E7 and E6 only: for P111 it is prior work of **#620** (GamingPuzzled, SAT) and **#1097** (bitplane, merged, LRAT-checked in the general model), and **#1815** (jmbarrancoml) is the one-sided P112 predecessor; here P111 is re-derived on #589's lines.
+- **#968**, **#1077**, **#1180**, **#1212**, **#1213**, **#1236**, **#1744**, **#757**, **#761**, **#620**, **#1097**, **#1815**, **#1331** (Arham-Tahir64), **#1249** (bbMisk, independent check of #1236), **#717** (ours; term-cost model, frontier-word censuses): the E8 / P112 / P104 / P111 floors for 8 terms, for factors in the live root code, rigidity, and the 9-term decoder outside the root code (#1180, whose cost 65 and shape are re-derived in `c4`).
+- **#1224** (joaqcoo; the merge lemma, one-sided overcomplete structure), **#1633** (bbMisk; excess-rank budgets), **#1714** (the independent-call batch model), **#2294** (thakrarsagar; the `k = 2` / `O(9)` / Gram batching core, found independently of Theorem B and credited for priority), **#2293** (navinor; independent audit of our Lemma CR2 / Theorem B2), **#2176**, **#2206**, **#2232**, **#2240**, **#2247**, **#2137**, **#2272**, **#2267**, Discussion 1267 (philippeVV; co-star families), Discussion 1166 (1337isnot1337; child-merging screen).
+- **#589** (P111 bit word): `data/p111_lines.json` is the `lines` array of `research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz` on `main` (sha256 pinned in `SOURCES.json`).
+- Tools: kissat 4.0.4 (SAT; never CaDiCaL); `drat-trim` (Marijn Heule and Nathan Wetzler), not vendored here, optional.
+- No file is copied from another contributor. `lib/roots.py`, `lib/satgen.py`, `lib/frames.py`, `lib/report.py`, `scripts/provenance.py`, `checks/c5_attaining_decoders.py`, `data/p104_frames.json` and `LICENSE` are the author's own files from the package of #2277 (`research/overcomplete-and-realisation-floors`).
+
+## New in this package
+
+Everything under `research/decoder-floors-frontier-format/`: `README.md`, `verify.sh`, `SOURCES.json`, `MANIFEST.sha256`, `lib/*.py`, `checks/*.py`, `sat/*.py`, `scripts/provenance.py`, and the evidence files `data/*.json`, `sat/results.jsonl`, `sat/results_misc.jsonl`, `sat/proofs/` (all produced by the generators in this package; the P104 class representatives `data/p104reps.json` and `data/h4_F1.json` were exported from the author's working card `STRAYS`, and are re-verified by the checks: `c1.gauge`, `c2`).
diff --git a/research/p112-cross-form-rank-tradeoff/sources/PR2338-README.md b/research/p112-cross-form-rank-tradeoff/sources/PR2338-README.md
new file mode 100644
index 0000000000..a1751a2a0b
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/sources/PR2338-README.md
@@ -0,0 +1,291 @@
+# 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
+
+> **Scope, stated first.** This package says one thing: *for decoders of the E8-family units that are hosted the way the frontier hosts them* — one global label
+> table in `F2^9` (so the admissible pairing `B` of the whole unit has `F2`-rank `≤ 9`), with the factors of every term in the column space of a minimal-rank realisation
+> (`col P ⊆ col M`, `col Q ⊆ row M`, rank `M = T = 8`; the square decoder of a *rank-9* realisation is **not** covered, OPEN §5.2 (c)), any number of terms, any number of independently batched calls — **the copy cost of the decoder cannot be lowered
+> below P112 64, E8 72, P104 56 (P104 means #968's unit, `F1 = H4`; E7 49 on its own rank-7 table), and two independent P112 calls cost at least 128**, all attained. It contains **no κ claim**, no window,
+> no supplier, no word-side (helper, transport, packing) cost. Everything outside that format is listed in §5 as **OPEN**, with what each escape would have to achieve.
+> Nothing here removes the need to price an escape; it only says where the escapes are. **Credit, stated first:** the P111 row of Theorem R (rigidity of the rank-9 fitting matrix of a P111 pattern) is prior work of #620 (GamingPuzzled; SAT) and #1097 (bitplane, merged; LRAT-checked in the general model), and #1815 (jmbarrancoml, merged) proves a one-sided P112 fitting rigidity; what is new here is Theorem R on E8, P112, P104 (#968's unit and class representatives), E7, E6, plus P111 on #589's 111 lines in the symmetric and general model with DRAT (§3.1, §3.7). Other P104 units are **not claimed** (§6, §5.6).
+>
+> **Labels.** **PROVEN** (proof in this README, or a cited proof of a merged / open PR of the swarm); **CHECKED** (recomputed by `verify.sh`: exact integer / `Fraction` / bit
+> arithmetic, or SAT whose UNSAT verdict carries a DRAT proof that `drat-trim` verifies; kissat 4.0.4 only, never CaDiCaL); **RECORDED** (a result of the author's working
+> cards that this package does **not** re-run, stated with its exact scope and where the evidence is; nothing in §2 marked PROVEN or CHECKED depends on a RECORDED item
+> unless that is said); **OPEN**.
+
+## 0. Reading this package
+
+```sh
+bash research/decoder-floors-frontier-format/verify.sh /fresh/output/dir        # Python >= 3.11, standard library only
+DRAT_TRIM=/path/to/drat-trim KISSAT=/path/to/kissat bash research/decoder-floors-frontier-format/verify.sh /fresh/output/dir
+```
+
+Step 0 checks every file against `MANIFEST.sha256` and every pin of `SOURCES.json` (hard stop on a mismatch). Then seven check scripts print one `PASS` / `FAIL` line per
+assertion (`SKIP` for anything that needs `kissat` or `drat-trim` when it is absent: those lines are not PASS). `verify.sh` exits nonzero on any FAIL. One core;
+6-7 minutes of CPU with both tools (358 s and 417 s user in two runs on a loaded machine; the 30 rigidity instances are re-solved and the UNSAT proofs re-checked), about 20 s without them (4 SKIP lines).
+`HIT_FULL=1` additionally re-solves three slow clique-hitting instances (kissat only, no proof; §3.6).
+
+| script | what it recomputes |
+|---|---|
+| `checks/c1_rigidity.py` | Theorem R: regenerates 30 CNFs (hash, #vars, #clauses), recorded verdicts, 4 shipped DRAT proofs, and (with kissat) re-solves all 30; 16 UNSAT proofs re-checked with drat-trim, 14 SAT models decoded |
+| `checks/c2_support_propagation.py` | Lemma 1.1 census (all `2^h − 1` label classes) on D4, D6, E7, E8, P112, P104; survivors, pair ranks, exactness of the per-term rank |
+| `checks/c3_batch_premises.py` | labels of P112 in `F2^9`, normals `w_i`, `b(w_i,w_j) = 1`, `ρ(N(f_i),N(f_j)) = 8`, frame lemma, an `O(9)` chart with all 64 cross pairs of rank 7 |
+| `checks/c4_masked_costar.py` | #1180's nine-term identity (cost 65), co-star dead sets, survivor 7-cliques |
+| `checks/c5_attaining_decoders.py` | the decoders that attain the floors (E8 72, E7 49, D6 30, D4 12, P112 64, P104 56), exact `Fraction` arithmetic |
+| `checks/c6_block_minrank_punctures.py` | EDGE E1a (every admissible `B`: the block `N(f)` of P112 has minrank 8; 8 DRAT proofs) and the C4.1 clique-hitting bounds on punctures |
+| `checks/c7_p111_unit.py` | the P111 bit unit of #589's word: 111 lines of an E8 line system, `rank_F2 B_d = 9`, an 8-frame |
+
+Layout: `lib/` (E8-family units, Bron–Kerbosch, exact `F2` / `Q` linear algebra, CNF helpers; `roots.py`, `satgen.py`, `frames.py`, `report.py` are the author's own files from
+#2277's package, `units.py`, `supprop.py`, `solve.py` are new), `sat/` (generators `rigid.py`, `misc.py`, `hitting.py`; registries; recorded results
+`results.jsonl`, `results_misc.jsonl`; shipped DRAT proofs `proofs/*.drat.xz`; author tools `mkresults.py`, `mkmisc.py`), `data/` (frames, the 111 P111 lines, one chart).
+
+## 1. Setting
+
+A **unit** is a set of `v` pairwise non-proportional lines `r_t ∈ Q^8` of the E8 root system (`E8`: 120 lines, `P112 = E8 − F0`, `P104 := E8 − F0 − F1` with `F1 = H4`, the second frame of #968's unit (the swarm has other P104 units, e.g. #1399's 896 admissible ones; those are not covered here, §6 and §5.6; the 1,260 frames `F1` disjoint from `F0` fall into invariant classes by the number of live 8-frames of the unit, `759 / 767 / 801`, and `H4` lies in the 759 class), `E7`, `E6`, the bit unit `P111` of #589). A **realisation** `M` has `M_tt ≠ 0` and `M_ts = 0` for orthogonal `t ≠ s`. A **decoder** is `M = Σ_j p_j q_jᵀ`
+with an **admissible (fitting) pairing** `B ∈ F2^{v×v}`: `B_tt = 1`, `B_ts = 0` for non-orthogonal `t ≠ s`, free on orthogonal pairs. Cost `= Σ_j rank_F2 B[R_j, A_j]`, `R_j = supp p_j`,
+`A_j = supp q_j` (the copy-pairing rank sum that the invoice charges; every bound below therefore also holds for any costlier physical charge). The **dense** pairing is
+`B_d = 1` on every orthogonal pair (and the diagonal); `rank_F2 B_d = h = 9` for E8, P112, P104, P111, `7` for E7, E6.
+**Model hypothesis (the frontier format).** The registers of the word carry labels in one `F2^h`; the pairing used by every term is a block of one matrix `B = U Vᵀ`
+(or `P Pᵀ`, the physical symmetric form) with `U, V ∈ F2^{v×h}`, i.e. `rank B ≤ h`. That the frontier word hosts its decoders on a single table of dimension `h = 9` is an
+engineering fact of the word; the code that fixes it is in this repository: `research/complex-571-cold14-k492/code/construct_k_triangle.py:20` (`P=D['binary_ports'] … h=9`), `:183–187` (the centre frames are `hyper(P[frame[i]])`, so the physical pairing is `J + Gram(even parts)`, symmetric of rank `≤ 9`) and `:364` (`'ports':P[8:]`); the working card `EDGE/HOSTING.md` (not shipped) records the same reading, with the term-cost model of #717 (cost = dimension of the label span). It is **not** proved here, it is the hypothesis whose negation is §5 item 1.
+**Label classes** (as in #2277 §1): `C = col B_d` (dim `h`); a class is the support of a nonzero `w ∈ C`; `Def(R) = {w ∈ C : supp w ∩ R = ∅}`, `δ(R) = dim Def(R)`.
+**Frames.** A `T`-frame is `T` pairwise orthogonal lines (`T = 8` for E8, P112, P104, P111; 7 for E7). Every realisation has rank `≥ T` (a frame gives an invertible diagonal minor).
+
+## 2. Master table: escape class → status → certificate
+
+"Class X" = one label table with `h = 9` (`h = 7` for E7), factors in `col M / row M` of a rank-`T` realisation.
+
+| # | escape class | what is shown | status | certificate |
+|---|---|---|---|---|
+| 1 | non-dense admissible `B` of rank `≤ 9` (E8, P112, P104 = #968's unit and three class representatives, P111) or `≤ 7` (E7, E6) | every fitting `B` of that rank **equals the dense `B`**, general `UVᵀ` and symmetric `PPᵀ` | **CHECKED** (16 DRAT-verified UNSAT + 10 SAT controls + 4 non-dense witnesses) | `c1`, §3.1 (Theorem R); the P111 case is #620 / #1097's, re-derived on #589's lines |
+| 2 | factors in the E8 root code, any `m`, dense `B` | P112 ≥ 64, E8 ≥ 72, P104 (#968's) ≥ 56, E7 ≥ 49 | **PROVEN** (cited, not re-run: #2228 Thm 4; #1180) + attained (**CHECKED**, `c5`) | #2228, #1180; with row 1 this is every `B` at `h = 9` |
+| 3 | any rank-8 realisation, factors in `col M`, any `m` | **P112 ≥ 64**; P104 (#968's unit) ≥ 56; E8 ≥ 72, E7 ≥ 49 | **PROVEN** from **CHECKED** (Lemma 1.1 census) | §3.2 (Theorem P), `c2`; E8/E7/P104 also #2277 Cor. 5.3 |
+| 4 | ≤ 8 paid terms, factors anywhere | square ⇒ row 3 | **PROVEN** | §3.3 |
+| 5 | #1180's outside-code nine-term example | costs exactly 65; its shape is ≥ 64 for **every** `B` | **CHECKED** + **PROVEN** | `c4`, `c6`, §3.3 |
+| 6 | co-star nine-term masked decoders (Disc. 1267) | all 120 dead sets span in every rank-8 realisation ⇒ each is a square decoder of a rank-9 realisation (pins them to §5 item 2(c)) | **CHECKED** (`c4`) + **PROVEN** consequence | §3.3 |
+| 7 | batches: `k` independent P112 calls on one `F2^9` table, any chart, factors in `col M_c`, any `m` | `k = 2`: ≥ 128 + 3t; `k ≥ 3` (symmetric charts): ≥ 64k + 3t; attained | **PROVEN** from **CHECKED** premises | §3.4 (Thm B, Bk), `c3`; k = 2 / O(9) / Gram also swarm #2294 |
+| 8 | any `B` on a single coordinate block | `rank_F2 B[N(f), N(f)] ≥ 8` for every admissible `B`, all 8 `f` | **CHECKED** (8 DRAT) | `c6`, §3.5 (EDGE E1a) |
+| 9 | punctures of the coordinate term under any table | clique hitting: `f(2) ≥ 14`, `f(6) ≥ 46`, `f(7) ≥ 52`, `f(8) = 56`; `s/f(s) ≤ 1/7` on the computed values | **CHECKED** (s = 2, 6: DRAT; 7, 8 exact); s = 3, 4, 5 **RECORDED** (kissat UNSAT re-run with `HIT_FULL=1`, no DRAT here) | `c6`, §3.5 |
+| 10 | P111 bit unit | rigid at `h = 9` (sym + general; **prior work of #620 / #1097**, re-derived on #589's lines); set-decoders with ≤ 12 totals cost ≥ 63, and with 13 totals ≥ 63 | rigidity **CHECKED** (2 DRAT); ≥ 63 for ≤ 12 and for 13 totals **RECORDED** | `c1`, `c7`, §3.7 |
+| 11 | E8 square root-code decoders for **every** `B` (no `h` cap) | ≥ 72 (4022 pair classes) | **RECORDED** (4022 DRAT verified in the working card; not re-run) | §3.8 |
+| 12 | `FL(4)`: every D4 decoder, every `B`, every `m` | ≥ 12 | **RECORDED** (support-level enumeration, 144 classes) | §3.8 |
+| 13 | E7 square maximal-normal root-code decoders, every `B` | ≥ 49 (no ≥ 5 root–root partners) | **RECORDED** (exact enumeration + independent audit in the working card) | §3.8 |
+| 14 | P104 delivery (#968's decoder) under any `F2^9` table | no helper-free nested delivery (24 DRAT) | **RECORDED** | §3.8 |
+| 15 | PUNCT2 near-miss unions `p = 25..44`, any physical table, any `m` | no decoder beats P102's 54/102 (Model C) | **RECORDED** | §3.8 |
+| 16 | **label tables of rank `h ≥ 10`** | non-dense fitting tables exist (row 1, witnesses); a 112-port unit needs cost ≤ 59 at `h = 10` to tie P112-`h = 9` (≤ 55 at `h = 11`) | **OPEN** | §5.1 |
+| 17 | **factors outside `col M`, `m ≥ 9`** | `m = 9`: `ρ ∈ {8, 9}`; (b) `ρ = 8` one outside factor, (c) `ρ = 9` square rank-9, (d) `m ≥ 10` | **OPEN** | §5.2 |
+| 18 | **bit window of 14 totals** (13 totals: RECORDED closed, row 10) | 14-total run in progress in the working card, not final | **OPEN** | §5.3 |
+| 19 | **puncture windows `p ≥ 45`** | — | **OPEN** | §5.4 |
+| 20 | **batches `m ≥ 17` outside `col M`**, GL charts with `k ≥ 3`, mixed units, correlated demands, `h ≥ 10` joint tables | — | **OPEN** | §5.5 |
+| 21 | **P104 units other than #968's** (Theorem R for all 1,260 frames `F1`; the Lemma 1.1 census for them) and **rank-9 square decoders** | — | **OPEN** | §5.6, §5.2 (c) |
+
+Rows 11–15 are *beyond* what the headline needs: at `h = 9` row 1 already forces `B = B_d`, so the headline uses `B_d` only. Their role is to show that the dense-pairing
+statements are not hiding a cheap non-dense escape *inside* the `h = 9` class; row 1 does that, and rows 11–13 give the independent every-`B` statements for the
+(square, root-code) sub-class.
+
+## 3. Results
+
+### 3.1 Theorem R: the minimal-rank label table is unique (CHECKED, DRAT)
+
+**Theorem R.** Let `U ∈ {E8, P112, P104, P111}` (P104 as defined in §1, plus the class representatives below) and let `B ∈ F2^{v×v}` fit `U` with `rank_F2 B ≤ 9`. Then `B = B_d`. The same holds for `E7, E6` with `rank B ≤ 7`. (**Credit:** for P111 this is #620's and #1097's result; see the paragraph after the table.)
+It holds in the general model `B = U Vᵀ` and in the symmetric model `B = P Pᵀ` (the physical one: `B_d = J + C` with `C` the alternating Gram of the even-weight label parts,
+which is `PPᵀ` for odd-weight labels `P_t = 1 + e_t`). For P104 the statement is checked for `H4`'s `F1` (the frame of #968; its unit has 759 live 8-frames, so it lies in the 759 class) and one representative of each of the three invariant
+classes (`759 / 767 / 801` live 8-frames) of frames disjoint from `F0`: **three classes, four instances** (`H4` is in the 759 class). **These classes are not proven to be single orbits**, and the backfill over all 1,260 frames was not finished,
+so P104 is claimed only for #968's unit (`F1 = H4`); Theorem P's census was run on `H4` only, and Theorem R / Theorem P for every other P104 unit is **not claimed** (§6, OPEN §5.6).
+
+*Encoding (`sat/rigid.py`).* `B = U Vᵀ` with `U, V ∈ F2^{v×h}`; constraints `⟨U_t, V_t⟩ = 1`, `⟨U_t, V_s⟩ = 0` for every non-orthogonal ordered pair `t ≠ s`; mode `alt` adds the clause
+"some orthogonal ordered pair (unordered in the symmetric model) has `B_ts = 0`"; mode `ctl` omits it. Products and parities are Tseitin variables with constant folding.
+*Gauge (PROVEN).* Let `S` be a pairwise non-orthogonal `k`-clique (`k = 8` for E8, P112, P104, P111; 7 for E7; 5 for E6; pinned in `results.jsonl`, `c1.gauge` checks the clique).
+Then `B[S,S] = I_k`, so `U[S]` has rank `k`; `GL(h)` acts by `U ↦ U g`, `V ↦ V g^{-T}`, preserves `B` and is transitive on rank-`k` `k`-tuples, so `U[S] = (e_1..e_k)` w.l.o.g. In the
+symmetric model with `k = 8`, `h = 9`: `P[S]` is orthonormal, `W = span P[S]` is nondegenerate, `W^⊥ = ⟨w⟩` with `w·w = 1` (`det I_9 = det I_8 · w·w`), so an isometry in `O(9)` maps
+`P[S]` to `(e_1..e_8)`; this needs `k ≥ h − 1`, which `registry()` asserts for every symmetric UNSAT instance. (For SAT instances the gauge is only a restriction, so a SAT verdict stands.)
+Rank `≤ h` is equivalent to a factorisation with `h` columns, so UNSAT of `alt` says every fitting `B` of rank `≤ h` is dense. (The general model contains the symmetric one as a sub-model, so general-model UNSAT already implies the symmetric statement and, for E7 and E6 where only the general model is run, covers the physical table; the symmetric runs are redundant but consistent.)
+
+| group (`results.jsonl`) | instances | verdict | check |
+|---|---|---|---|
+| `alt`, minimal rank | P112, E8, P104 (H4, 759, 767, 801), P111, each sym + gen (14 instances); E7, E6 gen at `h = 7` (2) | **UNSAT**, every proof verified by drat-trim (binary DRAT, kissat 4.0.4) | `c1.status`, `c1.resolve`; four proofs shipped (`proofs/`, sym P112 / E8 / P104-H4 / P111) |
+| `ctl`, no extra clause | P112, E8, P104-H4, P111 (sym + gen), E7, E6 | **SAT**; every decoded model is a fitting matrix with 0 non-dense orthogonal entries (model is `B_d`) | `c1.ctl` |
+| negative controls | `SUB20`, `SUB40` (the gauge clique plus the first 20 / 40 other lines of P112, `h = 9`, gen); P112 at `h = 10` (sym 59 of 3304, gen 89 of 6608 orthogonal pairs with `B_ts = 0`) | **SAT**: a non-dense fitting `B` exists | `c1.neg` |
+
+(The encoding is the one of the author's working card `STRAYS/rigid2.py`; the clique choice here is deterministic and pinned, so the CNFs differ from the card's files, with the
+same verdicts. The `h = 10` row shows the instance family does detect non-rigidity; the `SUB` rows show the same at `h = 9` on sub-units.)
+
+**Prior work on P111 and one-sided P112 rigidity (credit; this changes the novelty of Theorem R).** #620 (GamingPuzzled, open) found by SAT, without proof logs, that the rank-9 fitting matrix of its archived P111 pattern is unique; #1097 (bitplane, merged 2026-10-13) proof-checked this with LRAT: "fitting rank ≤ 9, unequal to `B0`" is UNSAT in the general (asymmetric) model with an 8-port gauge. That is the P111 row of Theorem R, and it is **theirs**. *Which set?* #1097's object is the archived sorted Hamming-root order of #620 with indices `39, 52, 57, 71, 76, 78, 103, 109, 114` deleted (`encoding.py:9`); #589's 111 lines (`data/p111_lines.json`) are a different 111-subset of the same 120 Hamming-coordinate lines: 104 lines in common (up to sign), 7 on each side only (a one-off comparison against #1097's retained `e8units.hamming_e8`, not part of `verify.sh`; whether the two sets are `W(E8)`-equivalent was not checked). So Theorem R here **re-derives** the P111 statement on #589's puncture, in both the general and the symmetric model, with DRAT, and does not rely on #1097. #1815 (jmbarrancoml, merged 2026-10-14) is the one-sided predecessor for P112: with the two column spaces fixed, unit diagonals and the required zeros force `N = RRᵀ` and `B = UUᵀ`; Theorem R removes the column-space hypothesis on `B` (every fitting `B` of rank `≤ 9` is dense). What is new here is Theorem R on E8, P112, P104 (#968's unit and representatives), E7 and E6.
+
+**Corollary R1 (PROVEN from Theorem R and the theorems of §3.2 / rows 2).** In the frontier format (one `F2^9` table, `F2^7` for E7), every term pairs through the dense `B_d`. Hence
+every statement made below for the dense pairing holds for every hosted decoder, and *the overcomplete "any `B`" slack* (orthogonal-normal blocks of fitting minrank 5–6;
+orthogonal E8 root–root terms of rank 6) *does not exist at `h = 9`*: it needs a non-dense `B`, hence `h ≥ 10`.
+**Corollary R2 (two-call tables, PROVEN).** If a two-call batch uses one `F2^9` and each call's block fits P112, the labels are `(P, PΦ)` with `Φ ∈ O(9, F2)` (general model:
+`(U, V), (UΦ, VΦ^{-T})`, `Φ ∈ GL(9)`). *Proof.* By Theorem R both blocks equal `B_d`, of rank 9. `P_1P_1ᵀ = P_2P_2ᵀ` has rank 9, so `P_1, P_2` have the same column space and `P_2 = P_1Φ`;
+then `P_1(ΦΦᵀ − I)P_1ᵀ = 0` with `P_1` of full column rank gives `ΦΦᵀ = I`. ∎
+
+### 3.2 Theorem P: P112 ≥ 64 in every rank-8 realisation (PROVEN from CHECKED)
+
+Setting (#2277 §5). `K` is any field (the swarm uses `Q` / `C`; Lemma 1.1 and Theorem P are field-independent). Let `M` be a realisation of rank exactly `T = 8` (the minimum), `M = P₀ N Q₀ᵀ`, `P₀, Q₀ ∈ K^{v×8}` bases of `col M`, `col Mᵀ`, `N ∈ GL_8`; `π(t)` is row `t` of `P₀`.
+Consider decoders with `p_j = P₀x_j`, `q_j = Q₀y_j` (every square decoder `m = 8` is of this form; for `m > 8` this is the hypothesis `col P ⊆ col M`). Then `N = Σ_j x_j y_jᵀ`, so at least 8 terms
+are nonzero.
+
+**Lemma 3.1 (support-only bound; #2277 Lemma 5.1, restated).** For `R, A ⊆ [v]`, `rank_F2 B_d[R, A]` depends only on the subspaces `Def(R), Def(A) ⊆ C`, and `≥ h − δ(R) − δ(A)`.
+*Proof.* Take `B_d = X Yᵀ`, `X = Y ∈ F2^{v×h}` of full column rank (`B_d` symmetric), `col X = C`. `ker X_R ≅ Def(R)` via `w = Xz`, so `rank X_R = h − δ(R)`, and the row space of `X_R` is
+the annihilator of `ker X_R`, i.e. determined by `Def(R)`; likewise for `A`. Sylvester gives the bound. ∎
+**Lemma 3.2 (Theorem 4′; #2277 §5, restated).** `cost ≥ Σ_{j : x_j, y_j ≠ 0} (h − δ(R(x_j)) − δ(A(y_j)))`, with `R(x) = {t : π(t)·x ≠ 0}`. If `w ∈ Def(R(x))` then `π(supp w) ⊆ x^⊥`: the class
+`supp w` is *deficient* (its `π`-image lies in a hyperplane). *Proof.* Lemma 3.1 and the count of nonzero terms. ∎
+
+**Lemma 1.1 (support propagation; working card `IDEAL3` §1.1, PROVEN here).** Let `E` be an 8-frame and write a functional `h*` that kills `π(O)` as `h* = Σ_{e ∈ E} c_e σ(e)`, where `σ(e) = N κ(e)ᵀ`, `κ(e)` = row `e` of `Q₀`
+(`π(e)·σ(e′) = M_{ee′}`: for a frame `E` the `σ(e)` are the dual basis of `{π(e)}` up to the nonzero scalars `M_ee`, and `σ(e)` depends on the line only). (i) `c_e = 0` for `e ∈ E ∩ O`: `h*(π(e)) = c_e M_ee`. (ii) For every 8-frame `F`: `supp_E(c) ⊆ (E ∖ O) ∩ ⋃_{g ∈ F∖O} N̄(g)`,
+`N̄(x) = {x} ∪ {lines non-orthogonal to x}`. *Proof.* (i) is the displayed identity. For (ii), applying (i) to `F` gives `h* ∈ span σ(F∖O)`; expanding `σ(g)` in the dual basis of `E`,
+`σ(g) = Σ_e (M_eg/M_ee) σ(e)`, whose `E`-support lies in `{e : M_eg ≠ 0} ⊆ N̄(g) ∩ E` (`M_eg = 0` for orthogonal `e ≠ g`). ∎
+*Corollary.* If iterating (ii) over all frames ends with some `S_E = ∅`, the class `O` is non-deficient in **every** rank-8 realisation.
+
+**Census (CHECKED, `c2`).** For every one of the `2^h − 1` classes: D4 (3 frames), D6 (15), E7 (135), E8 (2025): **all** certified. P112 (1260 frames): **exactly 8 classes uncertified** (the
+8 sets of 56 live lines orthogonal to one removed root; each has `rank_Q = 7`, i.e. is Gram-deficient, so the certificate is sharp); P104 (`H4`'s unit, 759 frames; the census was run on this unit only): 16 uncertified (sets of 52), also
+exactly the Gram-deficient ones. In both units the uncertified classes contain **no 2-dimensional subspace** (`a ⊕ b` is never one). For each uncertified `O`, the classes with support inside `O` are
+`{O}` alone (`c2.def`), so `Def(V∖O) = ⟨w_O⟩` and the single-deficiency rank is `rank B_d[V∖O, V] = 8`; over all ordered pairs of P112 survivors `rank B_d[V∖O, V∖O′] = 8` (64 of 64), and
+for P104 the values are `8` (192) and `7` (64).
+
+**Theorem P (PROVEN from the CHECKED census).** For P112, every rank-8 realisation `M`, every decoder with `col P ⊆ col M`, `col Q ⊆ row M` (all square decoders, any `m` otherwise), dense `B`:
+**cost ≥ 64**, attained by the removed-frame coordinate decoder (`c5`). For P104 = #968's unit (`F1 = H4`; the census of Lemma 1.1 is run on this unit only): **cost ≥ 56**, attained (`c5`).
+*Proof.* A nonzero `w ∈ Def(R(x_j))` is a deficient class (Lemma 3.2), hence one of the 8 (16) survivors (Corollary of Lemma 1.1; the census). Survivors contain no 2-dimensional subspace, so
+`δ(R(x_j)), δ(A(y_j)) ≤ 1`, and by Lemma 3.1 and the census the term's rank is `9` (no deficiency), `8` (one) or, for both deficient, the pair rank: `8` in P112, `≥ 7` in P104. So every nonzero
+term costs `≥ 8` (P112), `≥ 7` (P104); at least 8 terms are nonzero. ∎
+For E8 (72) and E7 (49) no class is deficient (census), so every term costs `h`; with at least `T` terms the floors are `8·9 = 72`, `7·7 = 49`. (#2277 Cor. 5.3 gives all of E8 72, E7 49, D6 30, D4 12, P104 56
+via the weaker clause-(c) certificate; its P112 value was 56, and "P112 ≥ 64 for every realisation" was listed there as open — Theorem P closes it.) **Sharpness (CHECKED, `c5`):**
+frame decoders with `M = Gram` cost 72 (E8), 49 (E7), 30 (D6), 12 (D4); the removed-frame decoder of P112 costs 64; the eight frame-pair terms of #968 cost 56 on P104.
+
+### 3.3 Few terms, outside `col M`, #1180 and the co-star (PROVEN / CHECKED)
+
+*(working card `STRAYS-MASK` §1–§3; dense `B`, which at `h = 9` is every `B` by Theorem R)*
+**1.1 Free-term absorption.** A term with `B[R_j, A_j] = 0` contributes `0` to the cost and nothing on the diagonal or on orthogonal pairs, so the paid part `N = Σ_{paid} p_j q_jᵀ` is again a realisation
+of the same pattern with the same cost; w.l.o.g. every term is paid.
+**1.2 Merge lemma (#1224 Lemma D, both sides).** If `q_i = c q_k` then `p_i q_iᵀ + p_k q_kᵀ = (c p_i + p_k) q_kᵀ`; the new row support lies in `R_i ∪ R_k`, and
+`rank B[R_i ∪ R_k, A_k] ≤ rank B[R_i, A_k] + rank B[R_k, A_k]` (`A_i = A_k`). The merge does not raise the cost for **any** `B`. W.l.o.g. no two row normals and no two column normals are proportional.
+**1.3 `m ≤ 8`.** `rank N ≥ α_⊥ = 8`, so `m ≥ 8`; `m = 8 = rank N` is the square case with factors in `col N / row N` (every factor lies in the column space of a rank-8 matrix with 8 terms), so Theorem P
+gives `≥ 64` (P112), `≥ 56` (P104, #968's unit), **whatever the factors, the realisation or the masking**. This covers every component of #1213, not only the connected one.
+**1.4 `m = 9` trichotomy.** `a = rank P = ρ + s`, `b = rank Q = ρ + t`; Sylvester: `ρ ≥ a + b − 9`, so `s + t ≤ 9 − ρ` with `ρ = rank N ∈ {8, 9}`. (a) `ρ = 8`, `s = t = 0`: Theorem P; (b) `ρ = 8`, `s + t = 1`: §5.2 (b) (#1180 / #1224's residual class); (c) `ρ = 9`: square in a rank-9 realisation (OPEN, §5.2 (c)).
+**#1180's example (CHECKED, `c4`).** Its nine-term identity `D Tᵀ = 8·Gram` holds on all `112 × 112` entries (`ex1180`-form: `t_1 = R_0 + z`, outside terms `(t_1, R_0)` and `(−z, R_0)`) and its term ranks under `B_d`
+are `[8]×8 + [1]`, **total 65**. Its two outside-`col M` terms share the column vector `R_0`: by the merge lemma (any `B`) the example costs at least the removed-frame decoder, whose terms are the blocks `B[N(f), N(f)]`,
+each of fitting minrank 8 for every `B` (`c6`, §3.5), so **after merging the two outside terms it is the removed-frame decoder, which costs ≥ 64 for every admissible `B` by E1a**: the "outside `col M`" in #1180's example is only a split of a proportional pair.
+**Co-star (CHECKED, `c4`; PROVEN consequence over any field of characteristic 0, the scope of the working card `STRAYS-MASK` Theorem 3.2).** *Definitions.* The **dead set** of a term `p qᵀ` on the row side is `{t : p_t = 0}` (the lines the term does not touch), on the column side `{t : q_t = 0}`; a set of lines is **spanning** if its images `π(t)` span `K^8` in every rank-8 realisation. For each of the 120 root lines `α`, the dead set `V ∖ S_α` (`S_α` = live lines orthogonal to `α`, plus `α` if live; `|S_α| = 60` for the 112 live `α`, 56 for the 8 removed) is certified spanning in every
+rank-8 realisation (Lemma 1.1). *Lemma (inside dead sets; STRAYS-MASK Lemma 3.1).* If a term of a rank-8 realisation has its column factor in `row M` (`q = Q₀ȳ`, `ȳ ≠ 0`, an "inside" side), its dead set `{t : κ(t)·ȳ = 0}` has images in the hyperplane `ȳ^⊥`, so it is not spanning and cannot contain `V ∖ S_α` (rows by transposition: the pattern is symmetric). *Consequence.* Let a nine-term masked co-star decoder (philippeVV, Discussion 1267; every term's supports inside co-stars, arbitrary coefficients, zeros, any `k`) have `ρ` = the rank of the full nine-term sum. If a term is free, or two row or two column normals are proportional, the paid or merged part has `≤ 8` terms, hence is square, and Theorem P gives `≥ 64` outright. Otherwise `ρ = 8` would give `s + t ≤ 1` (§1.4), so one side, say `t = 0`, is inside for all nine terms, contradicting the Lemma; `ρ ≥ 10 > m` is impossible. So `ρ = 9` and the decoder is a square
+biorthogonal decoder of a **rank-9** realisation: cases (a), (b) of §1.4 are empty for co-stars. This pins the open `k = 7/8/9` families to §5.2 (c); it does not close them. Every survivor class contains an
+orthogonal 7-clique and no 8-clique (`c4.survclique`), so its killing functional is unique up to scale in every rank-8 realisation.
+
+### 3.4 Batching: independent calls on one `F2^9` table (PROVEN from CHECKED)
+
+*(working card `STRAYS-BATCH`; the model is #1714's: `k` independent P112 calls, `C = I_k`, cross-call blocks of the requested matrix are 0.)* The requested matrix is `M_1 ⊕ … ⊕ M_k`, `M_c = P_cQ_cᵀ` a rank-8
+realisation (Gram: `P_c = Q_c = X`). A decoder is `Σ_j d_j t_jᵀ = M` with `d_j = (P_ca_j^{(c)})_c`, `t_j = (Q_cc_j^{(c)})_c`; exactness is `A Cᵀ = I_{8k}`. One label table on all `112k` lines; each call's block fits P112,
+so by Theorem R it is dense and by Corollary R2 call `c` carries labels `PΦ_c`. The charge of term `j` is `rank_F2` of the pairing between the span of the output labels of its union support `S_j` and the span of the input
+labels of `T_j` (the cheapest charge, #1714; every costlier charge is covered). **Premises (CHECKED, `c3`; they are Lemma 1.1's sharpness in label language):**
+(P1) in any rank-8 realisation the support of `P_c x`, `x ≠ 0`, has label span `V` (dim 9) or one of 8 hyperplanes `H_i = w_i^⊥` (it avoids the deficient class `O_i`, the live lines orthogonal to `f_i`); the survivors contain no 2-dimensional
+subspace, so no support avoids two classes and every span has dim ≥ 8. (P2) `b(w_i, w_j) = 1` for all 64 ordered pairs, and `ρ(N(f_i), N(f_j)) = 8` for all 64 pairs, `i = j` included.
+**Theorem B (`k = 2`, PROVEN).** For every chart `Φ` (`O(9)` symmetric or `GL(9)` general) every decoder satisfies `Σ_j cost_j ≥ 128 + 3t`, `t = #{j : cost_j = 7}`; the minimum is 128 (two coordinate decoders), only at `t = 0`.
+*Step 1.* Union spans have dim ≥ 8 (P1), so cost `≥ 8 + 8 − 9 = 7`; at cost 7 both spans are hyperplanes. *Step 2 (rank-7 terms are pure cross-call).* If `a_j` has a nonzero part in call `c`, that part's span (dim ≥ 8) lies in the output span `H`
+of dim 8, hence equals it, so `H` is a call-`c` output hyperplane; likewise `H′` is the input hyperplane of every call where `c_j` is nonzero. If one call had both parts nonzero, `(H, H′)` would be an output / input hyperplane pair of
+that call, which pairs at rank 8 by (P2). So `calls(a_j) ∩ calls(c_j) = ∅`. *Step 3 (rank count).* With `N = Σ_{cost 7} a_jc_jᵀ = [[0, N₁₂],[N₂₁, 0]]`, `t₁₂ + t₂₁ = t`, `rank N₁₂ ≤ t₁₂`, `rank N₂₁ ≤ t₂₁`; the other active terms
+cost ≥ 8 and sum to `I₁₆ − N`, so there are at least `rank(I − N) = 8 + rank(I₈ − N₂₁N₁₂) = 16 − d` of them, `d = dim ker(I₈ − N₂₁N₁₂) ≤ min(t₁₂, t₂₁) ≤ t/2`. So `Σ cost ≥ 7t + 8(16 − d) ≥ 128 + 7t − 8min(t₁₂,t₂₁) ≥ 128 + 3t`. ∎
+**The counting floor 120 is not the truth** (`c3.chart.rank7`): there is a chart `Φ ∈ O(9, F2)` (shipped in `data/chart_rank7.json`) for which all 64 cross pairs (call-1 support `N(f_i)`, call-2 support `N(f_k)`) pair at rank 7, while within a call the same pairings have rank 8.
+Per-term counting alone gives 120; the extra 8 units come from the rank argument.
+**Theorem Bk (`k ≥ 3`, symmetric model, PROVEN).** Charts `Φ_c ∈ O(9, F2)`, any rank-8 realisations, any `m`: `Σ cost ≥ 64k + 3t`. *Proof.* Steps 1–2 verbatim. Every hyperplane is `n^⊥` for a unique normal; slot `(c,i)` has normal `Φ_cw_i`, and
+`b(n, n) = 1` by (P2). Partition the `8k` slots into classes by normal (at most one slot per call). A rank-7 term has `b(n, n′) = 0`, so `n ≠ n′`; `a_j` is supported in the class of `n`, `c_j` in the class of `n′`. For `x ∈ Z^P_{c,i}`, `y ∈ Z^Q_{c,i′}` (`Z^P_{c,i}` := the coefficient vectors `x` whose call-`c` output support `supp P_c x` avoids `O_i`, i.e. lies in the hyperplane slot `(c,i)` with normal `Φ_c w_i`; `Z^Q_{c,i′}` := the same on the input side, `supp Q_c y` avoiding `O_{i′}`),
+`i ≠ i′`: `yᵀx = Σ_{e ∈ E}(y·q_c(e))(p_c(e)·x)/M_ee` over any 8-frame `E` of live lines; a summand needs `e ∈ N(f_i) ∩ N(f_{i′})`, and `c3.framelemma` finds for every `i < i′` a frame with `E ∩ N(f_i) ∩ N(f_{i′}) = ∅`, so `yᵀx = 0`. Hence
+`K = CᵀA` over the rank-7 terms has `K_ij ≠ 0` only if `class(c_i) = class(a_j)`, `K_ii = 0`. *Lemma K:* `corank(I_{8k} − ACᵀ) = corank(I_t − K) ≤ t/2` (order the classes; the larger of `{j : α(j) < β(j)}`, `{j : α(j) > β(j)}` has size `≥ t/2`, along `K`-arcs inside it the class strictly
+moves, so `K[S,S]` is nilpotent up to a permutation and `I − K[S,S]` is invertible). So `Σ cost ≥ 7t + 8(8k − t/2) = 64k + 3t`. ∎ (Every batch with exactly `8k` terms needs no factor hypothesis, #1714 §5.)
+**Credit.** #2294 (thakrarsagar) proves the `k = 2`, `O(9)`, Gram-root-code core first (its Theorem A: `≥ 128 + 6μ + 7(r_01 + r_10 − 2μ)`, `μ = min(r_01, r_10)`) and independently finds that some isometric charts make all 64 exceptional pairs rank 7; the derivation above was done
+before #2294 was read and is the same inequality. Beyond #2294: `GL(9)` charts of the general factor model, any rank-8 realisation (the Theorem P setting), and `k ≥ 3` in the symmetric model.
+
+### 3.5 One coordinate block under any `B`; punctures (CHECKED)
+
+**EDGE E1a (`c6`, 8 DRAT).** For each removed root `f` (all 8), `N(f)` is the 56-line support of the coordinate term. *Every* admissible `B` has `rank_F2 B[N(f), N(f)] ≥ 8`: the instance "`rank ≤ 7`" (gauge: the largest non-orthogonal
+clique in `N(f)`, 7 lines) is UNSAT with a drat-trim-verified proof (8 proofs of about 70 kB each; one shipped), and "`rank ≤ 8`" is SAT (the dense block). So no choice of `B` lowers a coordinate term of the removed-frame decoder, and with
+`m ≥ 8` the removed-frame decoder costs `≥ 64` for every `B`. (Together with the merge lemma this is the "shape ≥ 64 for every `B`" of §3.3.) `ω_non(N(f)) = 7` and `α_⊥(N(f)) = 4` are recomputed in `c6`.
+**Punctures (NEWWORD C4.1).** A puncture `D ⊆ N(f)` (lines deleted from the support) that brings `rank B[R∖D, R∖D]` to `≤ 8 − s` for some admissible `B` must hit every `(9 − s)`-clique of pairwise non-orthogonal lines (a clique `C` has `B[C,C] = I`
+for every admissible `B`). `f(s)` := the least size of such a hitting set. Proven bounds: `f(2) ≥ 14` (the 576 7-cliques cannot be hit by 13 lines; DRAT), `f(6) ≥ 46` (the largest triangle-free kept set has 10 lines: 11 is UNSAT, DRAT; the working card
+had 15 and `≥ 42`), `f(7) ≥ 52` (`α_⊥(N(f)) = 4`, exact), `f(8) = 56`. Recorded (kissat UNSAT, working-card DRAT; `HIT_FULL=1` re-solves them here without a proof): `f(3) ≥ 23`, `f(4) ≥ 32`, `f(5) ≥ 38` (the card's `s = 1` value, `z ≥ 8`, is EDGE's separate
+`killgauge` SAT result and is not reproduced here). The ratios `s/f(s)` are `.1429, .130, .125, .132, .130, .135, .143` (`s = 2..8`; `c6.f` prints the proven ones): **no computed `s ∈ {2..8}` exceeds 1/7** (`s = 3–5` RECORDED, `s = 1` not computed here). The puncture-saving statement
+("punctured coordinate decoders tie P112 at best under any global label table") is therefore the clique-hitting bound plus the card's price model (break-even `s/f(s) > .1441`, margin under 1%, inside the price model's error): the **bound** is CHECKED, the
+**pricing consequence** is RECORDED and is not claimed as a theorem.
+
+### 3.6 Slow instances
+
+`HIT_FULL=1` re-solves `hit_k6_z22`, `hit_k5_z31`, `hit_k4_z37` (the `s = 3, 4, 5` bounds) with kissat only; recorded (kissat 4.0.4, UNSAT, no proof; wall time under machine load): `hit_k6_z22` 102 s, `hit_k5_z31` 227 s, `hit_k4_z37` 9 s, i.e. `f(3) ≥ 23`, `f(4) ≥ 32`, `f(5) ≥ 38`; their results are in `sat/results_misc.jsonl` (flagged `slow`) and re-derived by `HIT_FULL=1`. No DRAT is checked for these here (the proofs are 100–200 MB).
+
+### 3.7 The bit side: P111 (rigidity CHECKED, prior work of #620 / #1097; "≥ 63" RECORDED)
+
+**P111 is rigid at `h = 9` (CHECKED, `c1`, `c7`; prior work: #620 by SAT, #1097 LRAT-checked in the general model, see §3.1).** On #589's set, which is not #1097's (§3.1), the statement is re-derived here in two models. The 111 live lines of #589's word (`data/p111_lines.json`; the source file's sha256 is pinned in `SOURCES.json` and equals the entry of `research/e8-bit-p111-tuned/MANIFEST.sha256` on `main`) are a sub-configuration of an E8 line system
+(`c7`); `alt` is UNSAT in the symmetric and the general model (drat-trim verified; the symmetric proof is shipped), the controls are SAT with the dense `B`. So at `h = 9` the bit side is also a dense-`B` question.
+**RECORDED (not reproduced here): P111 set-decoders with at most 12 retained totals cost ≥ 63.** The working card `STRAYS-BIT` proves it premise-free from the full census of the E8 line matroid's flats (ranks 1–6: `120 / 4,900 / 85,680 / 661,542 / 2,091,600 / 2,221,780`, maximal line counts `1, 3, 6, 12, 20, 36`;
+the rank-6 flats with ≥ 24 lines are exactly the 4,900 sets `a^⊥ ∩ b^⊥`), `G ≥ 12` (no live code word is covered by rank-≤ 6 sets of total rank ≤ 11, exhaustive) and an induction `D(Λ) ≥ r_k + D(Λ ∩ a_k^⊥)`. That enumeration needs 378 s with numpy and was **not ported to the standard library**; this package
+does not verify it and no other statement here uses it. It extends #757 / #761 (63 optimal on the shipped P111 for 9, 10 and 11+ label terms) and agrees with #620 (63 for P111; exact SAT, cost ≤ 62 UNSAT, 8 totals UNSAT; also #1097's rank-9 uniqueness above).
+**RECORDED (another agent's working card, `STRAYS-BIT` closure 2; not re-run and not reviewed here): P111 word-priced bit decoders with 13 totals cost ≥ 63.** In the word's pricing (the set-decoder model: retained totals are arbitrary live-line sets, each priced by the rank of its span) the card reports exact rational Farkas certificates for all 132 code classes of excess 4 (re-checked there with `Fraction`s only), on top of `G(3) ≥ 15` and `G(4) ≥ 14` (exhaustive: no ≤ 4-set low cover of total rank ≤ 13, no 3-set low cover of total rank ≤ 14), and `P110` (P111 minus line 38) `≥ 63` for `n ≤ 12` totals, which is P110's whole hosting window (`R = 439 ≤ 4·110`). The card also reports rigidity at `h = 9` on P110 (controls SAT). The card's status for **14 totals** is *in progress*: of the 51,973 excess-5 classes, 51,233 have Farkas certificates and 735 are integer-only (kissat UNSAT, drat-trim verified for the 55 classes with `κ = 6, 7`; `κ = 8, 9` pending, no final count). So: **13 totals RECORDED closed; 14 totals in progress, OPEN** (§5.3). Not covered by the card: decoders outside the set-decoder model (a retained total charged below its source span's rank, i.e. a projected or asymmetric copy) and `≥ 15` totals (excluded by hosting, `R ≤ 4v`).
+
+### 3.8 Recorded results of the working cards (not re-run)
+
+* **E8□ (IDEAL3 §4.6).** Every square E8 root-code decoder costs `≥ 72` for **every** `B` (4,022 non-orthogonal pair classes, each with fitting minrank `≥ 9`); the card's `census/e8drat.out` ends "DONE 4022 classes; not verified: 0". The proof logs (139 MB) are not shipped. Not needed at `h = 9`.
+* **FL(4) (IDEAL3 §2).** The Frame Lemma for `n ≤ 4` (PROVEN modulo a 144-class support-level enumeration) gives `D4 ≥ 12` for every decoder, every realisation, every `m`, every `B`. Lemmas 4.1 (maximal-pair reduction) and 4.2 (`k`-term averaging) of IDEAL3 §4 are the shared-`B` reductions used by E8□ and the E7 statement below.
+* **E7 (STRAYS S4).** Square maximal-normal root-code decoders cost `≥ 49` for every `B`: no decoder has ≥ 5 root–root partners (256 bad partners, 16 compatible 5-sets, 0 six-sets, 0 completions; Sonnet enumeration, independently re-audited). The 49 *on E7's own rank-7 table*, the case in the headline, needs only Theorem R at `h = 7` (CHECKED) and #2277 Cor. 5.3.
+* **P104 delivery (NEWWORD C4.2).** For #968's P104 frame-pair decoder (cost 56, rank-7 terms) no global admissible label table in `F2^9`, with any per-term gather orientation, allows helper-free nested delivery (24 DRAT-verified instances; pairs `(0,1), (0,4), (1,4)`, same orientation, both directions; the graph of class-1 pairs is triangle-free and 3-regular on the 8 terms, so among any three mutually adjacent terms two share an orientation). Extends EDGE-B's Delivery Lemma from the dense table to every table. Escape: `h > 9` (a P104 at `h = 10` already loses to P112 at `h = 9` on the format ceiling: `3.931e-3 < 3.995e-3`).
+* **PUNCT2, `p = 25..44` (NEWWORD c5).** Model C (dense pairing, column-space factors): at the 1,323 near-miss unions the bilinear forms vanishing on orthogonal live pairs have nullity 1 (`N ∝ Gram`), so every 8-term decoder is biorthogonal; for `m ≥ 9` merging and PUNCT2's deficiency census (`d ≤ 2`) give cost `≥ 5m ≥ 45 > 40.24` (`p = 44`) and `≥ 7m − 12 ≥ 51 > 44.47` (`p = 36`); rigidity at the two representatives is DRAT-verified and the 1,323 unions form two `W(E8)` orbits. So no decoder in the class beats P102's 54/102; the "+13–15%" near-miss points were relaxation artefacts. Depends on PUNCT2's census inputs, which are not shipped.
+* **E7 frame decoders (NEWWORD c3).** No E7 root-line decoder with `m = 8` and every cross `⟨y_i, x_j⟩ = ±1`; best type mixes cost `≥ 39` on `≤ 50` ports (`x ≥ .78`), none beats P56's `x = .75` even with per-term-optimal `B` and free delivery (scope: crosses in `{0, ±1}`, root-line normals).
+* **EDGE (coordinate block, minrank 8 every `B`):** CHECKED in §3.5. EDGE-B's Delivery Lemma (dense table) is the one C4.2 extends; not re-run.
+
+## 4. How to cite this
+
+"For every decoder hosted on one `F2^9` label table (Theorem R: the pairing is the dense one), with factors in the column space of a rank-8 realisation and any number of terms (Theorem P; #2228 Thm 4 for the root code), the copy costs of the E8-family units are exactly
+P112 64, E8 72, P104 56 (#968's unit, `F1 = H4`; E7 49 on rank-7 tables), and `k` independent P112 calls cost `≥ 64k` (`= 128` for `k = 2`; symmetric / physical table for `k ≥ 3`, `GL` charts with `k ≥ 3` are open, §5.5) (Theorem B, Bk; #2294). Remaining escapes: tables of rank `≥ 10`, rank-9 square decoders and overcomplete factors outside `col M` with `≥ 9` terms, the bit window of 14 totals (13 is RECORDED closed), puncture windows `p ≥ 45`, batches of `≥ 17` terms outside `col M`, other P104 units."
+
+## 5. OPEN (each leaves class X; priced where a price exists; none constructed)
+
+<a id="open-1"></a>
+### 5.1 Label tables of rank `h ≥ 10`
+
+Non-dense fitting tables exist at rank 10 (`c1.neg`: `P112_sym_h10_alt`, `P112_gen_h10_alt` are SAT). *Price* (working card `STRAYS/PRICE-P112-H10.md`, a Sonnet helper's pricing, not a theorem; it reproduces the P104 rows of NEWWORD `c4/PRICE-H10.md`): a 112-port unit at
+`h = 10` must reach **cost ≤ 59 (−5 units)** to tie P112-at-`h = 9`, before any helper growth; at `h = 11`, `≤ 55`. **Status: undecided.** Per-term floors under a global rank-10 cap were probed on the first orthogonal-normal class (free-`B` minrank 6) and timed out at 20 minutes for cap 7 at both `h = 10` and `h = 12`. Per-term `≥ 8` at rank `≤ 10` would close `h = 10` (since `m ≥ 8`).
+For E8 overcomplete under any `B`: non-orthogonal terms `≥ 9`, other orthogonal terms `≥ 8`, orthogonal root–root terms are 6; counting alone allows `m ∈ {9, 10, 11}` below 72; the `m = 9` root-normal family is jointly `≥ 65` (EDGE). Another agent works this (working card `STRAYS-H10`).
+<!-- UPDATE IF CLOSED: §5.1 / master row 16 — state the h = 10 (and h = 11) per-term floor or the decoder found, its status label, the check script and DRAT proofs, and update §4 and the title. -->
+
+<a id="open-2"></a>
+### 5.2 Factors outside `col M`, `m ≥ 9`
+
+Proven (§3.3): `m ≤ 8` ⇒ `≥ 64` / 56 for any factors and any realisation; `m = 9`: `ρ = rank(paid part) ∈ {8, 9}`, `s + t ≤ 9 − ρ`. **Open:** (b) `ρ = 8` with one factor outside `col M` (#1180's residual class; necessary conditions proven, 42k of 45k class pairs uncertified at support level);
+(c) `ρ = 9`, square in a rank-9 realisation (needs a rank-9 analogue of Lemma 1.1, `Σδ ≥ 18` to reach ≤ 63; contains every philippeVV co-star `k = 7/8/9` family, §3.3); (d) `m ≥ 10` (budget `s + t ≤ m − ρ`, #1633; the average term rank would have to drop below 6.4). All under dense `B`, which at `h = 9` is every `B`. (working card `STRAYS-MASK`; `STRAYS-MASK2` continues.)
+<!-- UPDATE IF CLOSED: §5.2 / master row 17 — which of (b), (c), (d) closed, the theorem, status labels and checks. -->
+
+<a id="open-3"></a>
+### 5.3 Bit window of 14 totals (13 totals: RECORDED closed)
+
+P111 set-decoders with `14` retained totals: the `≤ 12` and `13`-total bounds are RECORDED (§3.7); the 14-total finite per-code check is still running in the working card (`STRAYS-BIT`, no final count), so it stays OPEN. `≥ 15` totals are excluded by hosting in the current word (`R ≤ 4v`).
+<!-- UPDATE IF CLOSED: §5.3 / master row 18 — the 14-total bound, its status label and check. -->
+
+<a id="open-4"></a>
+### 5.4 Puncture windows `p ≥ 45`
+
+PUNCT2's exclusion covers `p = 25..44` (RECORDED, §3.8). For `45 ≤ p ≤ 112`: is `cost ≥ (54/102)(120 − p)` in Model C (dense or rank-≤ 9 `B`), column-space factors, any `m`? The census of `d ≥ 3` kernels and non-root flats beyond 44 has not been run; the `T²` law (#2125, argued) predicts no gain for `v ≲ 64`. (working card `PUNCT3`.)
+<!-- UPDATE IF CLOSED: §5.4 / master row 19 — the p-range now covered, the theorem, status labels and checks. -->
+
+<a id="open-5"></a>
+### 5.5 Batches outside class X
+
+`m ≥ 17` terms with factors outside `col M` (every 16-term batch needs no factor hypothesis, #1714 §5); `GL(9)` charts with `k ≥ 3` (mathematical only: the physical table is symmetric; the obstruction is a possible loop in the component quotient of the output / input hyperplane graph, so
+Lemma K's ordering argument may fail; the bound needs only `corank(I_t − K) ≤ 7t/8`); `h ≥ 10` joint tables (pure cross terms may cost `< 7`; #2294 Props B–D cover cross blocks that factor through the call labels as bilinear forms); correlated demands (`C ≠ I`, #1714 §4); mixed-unit batches; a second call on a different unit.
+<!-- UPDATE IF CLOSED: §5.5 / master row 20 — which batch case closed, theorem, status labels and checks. -->
+
+<a id="open-6"></a>
+### 5.6 Other P104 units; rank-9 square decoders
+
+Theorem R and the Lemma 1.1 census (Theorem P) are run for P104 = #968's unit (`F1 = H4`) only, with Theorem R also at one representative of each of the classes `759 / 767 / 801`. **Not claimed:** Theorem R for all 1,260 frames `F1`, the census and Theorem P for any other P104 unit (the swarm has many, e.g. #1399's 896 admissible ones). The rank-9 square case is §5.2 (c).
+<!-- UPDATE IF CLOSED: §5.6 / master row 21 — which P104 units are now covered, the check scripts and DRAT proofs. -->
+
+**Out of scope by construction:** non-E8 units (BIGTHEORY: no-go only for `h ≤ 13`; #2222-type large-`h` units are compensation-bound), and all word-side overheads (helpers, transport, packing). 1337isnot1337's rank-16 child-merging screen (Discussion 1166, `< 0.21%` even at zero overhead) is a word-side route, not a decoder saving.
+
+## 6. What was not reproduced
+
+See §3.5 (steps `s = 3, 4, 5` of the puncture table; `s = 1` not computed), §3.7 (the 12- and 13-total bit bounds) and §3.8: every RECORDED item is a result of the working cards that this package neither re-runs nor depends on for rows 1–10 of §2, with the single exception noted in §3.5 (the pricing
+consequence of the puncture table). Differences between the working cards and this package, none of them a failed reproduction: the SAT instances are regenerated with a deterministic gauge clique (the card's files differ, the verdicts agree); `f(6)` is `≥ 46` here (card: `≥ 42` from a looser 15-set instance); the `h = 10` witnesses differ from the card's
+(non-dense in 59 / 89 orthogonal entries rather than 171 / 381); the card's "rank(B − B_dense) = 8" for the `h = 10` witness is not claimed. Not claimed: Theorem R for all 1260 frames of P104 (class representatives only), and Theorem P or any P104 statement for units other than #968's (`F1 = H4`); the rank-9 square case (§5.2 (c)); novelty of the P111 row of Theorem R (#620 / #1097).
+
+## 7. Credits and related PRs
+
+Our PRs: #1590 (model, merged), #2111, #2125, #2162 (Lemma CR2 / Theorem B2; navinor's independent audit #2293 passes our CR2/B2 on 58 instances), #2228 (root-code floors Thm 4, dense polar law), #2244, #2277 (Theorem 4′, frame-intersection certificate, Cor. 5.3). Swarm: #968 (frame-pair P104 decoder), #1180 (outside-code nine-term example), #1212 / #1213 / #1236 (rank-8 rigidity, components, root-star supports), #1744 (global fitting rank ≥ 9 on P112), #757 / #761 (P111 63), #620 (GamingPuzzled; P111 rank-9 uniqueness and 63, found by SAT) and #1097 (bitplane, merged; LRAT proof of that uniqueness in the general model, on the archived Hamming order, not on #589's set), #1815 (jmbarrancoml, merged; one-sided P112 fitting rigidity), #1331 (Arham-Tahir64, merged; the coordinate COPY 64 is not improved by one free rectangle; related to E1a and the punctures), #1249 (bbMisk, merged; independent verification of #1236's 64), #717 (ours; term cost = dimension of the label span, frontier-word censuses and decoder floors; the hosting model rests on it), #2176 / #2206 (forced minors, exact pairing costs),
+#2232 / #2240 / #2247 / #2137 (E6 screens, 1337isnot1337), #2272 (dense-polar small-`T` screen), #2267 (rectangular Lean form of the shadow lemma), #2294 (k = 2 batching, thakrarsagar), #1714 (batch model), #1224 (joaqcoo; the merge lemma and one-sided overcomplete structure), #1633 (bbMisk; excess-rank budgets), Discussion 1267 (philippeVV; co-star families).
+Tools: kissat 4.0.4, drat-trim (Marijn Heule, Nathan Wetzler). See `NOTICE.md`.
+
+Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0.
diff --git a/research/p112-cross-form-rank-tradeoff/test_integrity.py b/research/p112-cross-form-rank-tradeoff/test_integrity.py
new file mode 100644
index 0000000000..0bcd3c5c9e
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/test_integrity.py
@@ -0,0 +1,74 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Relocated replay and corruption rejection through the public verifier CLI."""
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+import unittest
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+GEOMETRY = Path("research/p112-single-lift/reference-geometry.json")
+
+
+class IntegrityTests(unittest.TestCase):
+    @classmethod
+    def setUpClass(cls):
+        cls.temp = tempfile.TemporaryDirectory(prefix="p112-cross-form-replay-")
+        cls.root = Path(cls.temp.name)
+        cls.package = cls.root / "research/p112-cross-form-rank-tradeoff"
+        shutil.copytree(HERE, cls.package, ignore=shutil.ignore_patterns("__pycache__", "*.olean"))
+        (cls.root / GEOMETRY).parent.mkdir(parents=True)
+        shutil.copyfile(ROOT / GEOMETRY, cls.root / GEOMETRY)
+
+    @classmethod
+    def tearDownClass(cls):
+        cls.temp.cleanup()
+
+    def run_replay(self, optimized=False):
+        return subprocess.run([sys.executable, "-I", "-B"] + (["-O"] if optimized else [])
+                              + [str(self.package / "verify.py")], cwd=self.root,
+                              text=True, capture_output=True, timeout=120)
+
+    def test_relocation_optimized(self):
+        result = self.run_replay(True)
+        self.assertEqual(result.returncode, 0, result.stderr[-1500:])
+        self.assertIn("PASS_P112_CROSS_FORM_RANK_TRADEOFF", result.stdout)
+
+    def mutate(self, path, transform, expected):
+        original = path.read_bytes()
+        try:
+            path.write_bytes(transform(original))
+            result = self.run_replay(True)
+            self.assertNotEqual(result.returncode, 0)
+            self.assertIn(expected, result.stderr)
+        finally:
+            path.write_bytes(original)
+
+    def test_source_drift(self):
+        self.mutate(self.root / GEOMETRY, lambda b: b + b"\n", "input pin:")
+
+    def test_predecessor_drift(self):
+        self.mutate(self.package / "sources/PR2294-PROOF.md", lambda b: b + b"\n",
+                    "predecessor pin:")
+
+    def test_false_receipt(self):
+        def alter(payload):
+            result = json.loads(payload)
+            result["rank_region"]["certified_pairs"] = 100
+            return json.dumps(result).encode()
+        self.mutate(self.package / "RESULT.json", alter, "committed result equality")
+
+    def test_receipt_type_change(self):
+        def alter(payload):
+            result = json.loads(payload)
+            result["rank_region"]["unresolved_pairs"][0][0] = True
+            return json.dumps(result).encode()
+        self.mutate(self.package / "RESULT.json", alter, "committed result equality")
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/research/p112-cross-form-rank-tradeoff/verify.py b/research/p112-cross-form-rank-tradeoff/verify.py
new file mode 100644
index 0000000000..7ea286387f
--- /dev/null
+++ b/research/p112-cross-form-rank-tradeoff/verify.py
@@ -0,0 +1,385 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Independent exact finite premises and controls; no predecessor code imports.
+
+The arbitrary-factorization result is the written proof. CountFloor.lean
+formalizes its arithmetic interface, with matrix premises explicitly assumed.
+"""
+import argparse
+from collections import Counter
+from fractions import Fraction
+import hashlib
+import itertools
+import json
+from math import gcd
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+GEOMETRY = "research/p112-single-lift/reference-geometry.json"
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def reject(action, label):
+    try:
+        action()
+    except ValueError:
+        return label
+    raise ValueError("control was accepted: " + label)
+
+
+def basis(rows):
+    pivots = {}
+    for row in rows:
+        while row:
+            p = row.bit_length() - 1
+            if p in pivots:
+                row ^= pivots[p]
+            else:
+                pivots[p] = row
+                break
+    return tuple(pivots.values())
+
+
+def rank2(rows):
+    return len(basis(rows))
+
+
+def rankq(rows):
+    """Fraction-free elimination with primitive integer rows."""
+    pivots = {}
+    for source in rows:
+        row = list(source)
+        for p, other in sorted(pivots.items()):
+            if row[p]:
+                a, b = other[p], row[p]
+                row = [a * x - b * y for x, y in zip(row, other)]
+                g = 0
+                for x in row:
+                    g = gcd(g, x)
+                if g > 1:
+                    row = [x // g for x in row]
+        p = next((i for i, x in enumerate(row) if x), None)
+        if p is not None:
+            pivots[p] = row
+    return len(pivots)
+
+
+def rankq_reference(rows):
+    """A separate Fraction oracle used on the coefficient endpoints."""
+    a = [[Fraction(x) for x in row] for row in rows]
+    r = 0
+    for c in range(len(a[0]) if a else 0):
+        p = next((i for i in range(r, len(a)) if a[i][c]), None)
+        if p is None:
+            continue
+        a[r], a[p] = a[p], a[r]
+        a[r] = [x / a[r][c] for x in a[r]]
+        for i in range(r + 1, len(a)):
+            q = a[i][c]
+            a[i] = [x - q * y for x, y in zip(a[i], a[r])]
+        r += 1
+    return r
+
+
+def parity(x):
+    return x.bit_count() & 1
+
+
+def dot(x, y):
+    return sum(a * b for a, b in zip(x, y))
+
+
+def form(matrix, x, y):
+    return parity(x & sum(parity(row & y) << i for i, row in enumerate(matrix)))
+
+
+def restricted(matrix, left, right):
+    return rank2(sum(form(matrix, x, y) << j for j, y in enumerate(right))
+                 for x in left)
+
+
+def pins():
+    manifest = json.loads((HERE / "SOURCES.json").read_text())
+    for item in manifest["files"]:
+        if item["usage"] == "input":
+            need(hashlib.sha256((ROOT / item["path"]).read_bytes()).hexdigest()
+                 == item["sha256"], "input pin: " + item["path"])
+    for item in manifest.get("predecessors", []):
+        need(hashlib.sha256((HERE / item["local_path"]).read_bytes()).hexdigest()
+             == item["sha256"], "predecessor pin: " + item["local_path"])
+
+
+def geometry():
+    data = json.loads((ROOT / GEOMETRY).read_text())
+    x, labels, duals = data["X"], data["labels"], data["duals"]
+    need(len(x) == len(labels) == len(duals) == 112, "geometry size")
+    # Reconstruct the norm-four Hamming-shell lines independently of the file.
+    shell = set()
+    for a in range(1, 8):
+        for b in range(2):
+            support = [i for i in range(8) if parity(a & i) == b]
+            for signs in itertools.product((-1, 1), repeat=3):
+                row = [0] * 8
+                row[support[0]] = 1
+                for i, sign in zip(support[1:], signs):
+                    row[i] = sign
+                shell.add(tuple(row))
+    def canonical(row):
+        sign = next(t for t in row if t)
+        return tuple(t if sign > 0 else -t for t in row)
+    need({canonical(row) for row in x} == shell, "independent Hamming shell")
+    need(rank2(labels) == rank2(duals) == 9, "two full label spans")
+    for i in range(8):
+        for j in range(8):
+            need(sum(row[i] * row[j] for row in x) == 56 * (i == j), "left inverse")
+    for i in range(112):
+        for j in range(112):
+            d = dot(x[i], x[j])
+            need(d % 2 == 0, "even root dot")
+            need(parity(duals[i] & labels[j]) == (1 + d // 2) % 2,
+                 "within-call pairing")
+    histories = []
+    for name, lab in [("reader", duals), ("source", labels)]:
+        history, exceptional = Counter(), []
+        for h in range(1, 512):
+            rows = [row for row, label in zip(x, lab) if parity(h & label)]
+            r = rankq(rows)
+            history[r] += 1
+            if r < 8:
+                zeros = [i for i in range(8) if all(row[i] == 0 for row in rows)]
+                need(r == 7 and len(zeros) == 1, name + " exceptional kernel")
+                exceptional.extend(zeros)
+        need(history == {8: 503, 7: 8}, name + " support census")
+        need(sorted(exceptional) == list(range(8)), name + " coordinate exceptions")
+        histories.append({str(k): v for k, v in sorted(history.items())})
+    readers = [basis(duals[i] for i in range(112) if x[i][j]) for j in range(8)]
+    sources = [basis(labels[i] for i in range(112) if x[i][j]) for j in range(8)]
+    ident = tuple(1 << i for i in range(9))
+    for u in readers:
+        for v in sources:
+            need(len(u) == len(v) == 8 and restricted(ident, u, v) == 8,
+                 "64 within-support ranks")
+    return data, readers, sources, histories
+
+
+def matrix_census():
+    mats = [tuple((word >> (2 * i)) & 3 for i in range(2)) for word in range(16)]
+    gl = [a for a in mats if rank2(a) == 2]
+    tight = Counter()
+    total = 0
+    for a, d, b, c in itertools.product(gl, gl, mats, mats):
+        rows = tuple(a[i] | (b[i] << 2) for i in range(2)) + \
+               tuple(c[i] | (d[i] << 2) for i in range(2))
+        actual = rank2(rows)
+        rb, rc = rank2(b), rank2(c)
+        lower = 4 - min(2, rb, rc)
+        need(actual >= lower, "block Schur minimum-rank bound")
+        if actual == lower:
+            tight[f"{rb},{rc}"] += 1
+        total += 1
+    need(total == 9216 and len(tight) == 9, "exhaustive block coverage and sharpness")
+    return {"matrices": total, "tight_by_cross_rank": dict(sorted(tight.items()))}
+
+
+def unit(i):
+    return tuple(int(i == j) for j in range(16))
+
+
+def decoder_fixtures():
+    standard = [(unit(i), unit(i)) for i in range(16)]
+    one = [(unit(i), tuple(int(j == i) - int(i == 0 and j == 8)
+                          for j in range(16))) for i in range(16)]
+    one.append((unit(0), unit(8)))
+    two = [(unit(i), unit(i)) for i in range(16) if i not in (0, 8)]
+    z = tuple(int(i == 0) - int(i == 8) for i in range(16))
+    two += [(z, z), (unit(0), unit(8)), (unit(8), unit(0))]
+    schur = []
+    for i in range(8):
+        z = tuple(int(j == i) - int(j == i + 8) for j in range(16))
+        schur += [(z, z), (unit(i), unit(i + 8)), (unit(i + 8), unit(i))]
+    mixed = []
+    for k in range(8):
+        a = tuple(int(i <= k) for i in range(8))
+        c = tuple(int(i == k) - int(i == k + 1) for i in range(8))
+        mixed.append((a + tuple(-v for v in a), c + tuple(-v for v in c)))
+        mixed += [(unit(k), unit(k + 8)), (unit(k + 8), unit(k))]
+    return {"standard": standard, "one_cross": one, "two_cross": two,
+            "schur": schur, "noncoordinate_schur": mixed}
+
+
+def coefficient_counts(terms):
+    endpoint = [[sum(a[i] * c[j] for a, c in terms) for j in range(16)] for i in range(16)]
+    need(endpoint == [[int(i == j) for j in range(16)] for i in range(16)], "I16 endpoint")
+    kinds = []
+    for a, c in terms:
+        ac = [any(a[8 * s:8 * s + 8]) for s in range(2)]
+        cc = [any(c[8 * s:8 * s + 8]) for s in range(2)]
+        need(any(ac) and any(cc), "discard zero factors")
+        kinds.append("D" if all(ac + cc) else "N" if any(ac[s] and cc[s] for s in range(2))
+                     else "P01" if ac[0] else "P10")
+    ranks = []
+    for name, i0, j0 in [("P01", 0, 8), ("P10", 8, 0)]:
+        matrix = [[sum(a[i0 + i] * c[j0 + j] for (a, c), kind in zip(terms, kinds)
+                       if kind == name) for j in range(8)] for i in range(8)]
+        r = rankq(matrix)
+        need(r == rankq_reference(matrix), "independent coefficient rank")
+        ranks.append(r)
+    n, d = sum(k in ("N", "D") for k in kinds), kinds.count("D")
+    mu = min(ranks)
+    need(n + d >= 16 and n + mu >= 16, "incidence and Schur counts")
+    return kinds, n, d, mu, ranks
+
+
+def price_data(data, terms):
+    x, duals, labels = data["X"], data["duals"], data["labels"]
+    def spans(coef, lab):
+        return [basis(label for row, label in zip(x, lab)
+                      if dot(row, coef[8 * s:8 * s + 8])) for s in range(2)]
+    return [(spans(a, duals), spans(c, labels)) for a, c in terms]
+
+
+def cost(b, c, reader, source):
+    rows = []
+    for s in range(2):
+        for u in reader[s]:
+            bits, j = 0, 0
+            for t in range(2):
+                for v in source[t]:
+                    bit = parity(u & v) if s == t else form(b if s == 0 else c, u, v)
+                    bits |= bit << j
+                    j += 1
+            rows.append(bits)
+    return rank2(rows)
+
+
+def form_fixtures(data, readers, sources):
+    fixture_data = {}
+    for name, terms in decoder_fixtures().items():
+        fixture_data[name] = (coefficient_counts(terms), price_data(data, terms))
+    # Each rank is realized by an actual form; these are fixtures, not all forms.
+    pairs, sufficient, old_sufficient, example = 0, 0, 0, None
+    total_checks = 0
+    undecided_control = None
+    cases = []
+    for r, s in itertools.product(range(10), repeat=2):
+        b = tuple((1 << i) if i < r else 0 for i in range(9))
+        c = tuple((1 << ((i + 2) % 9)) if i < s else 0 for i in range(9))
+        cases.append((r, s, b, c, "rank_pair"))
+    # This rank-(1,1) case forces abstention; a few decoders cannot decide it.
+    ar = next(v for v in range(1, 512) if all(not parity(v & u) for u in readers[0]))
+    ac = next(v for v in range(1, 512) if all(not parity(v & u) for u in sources[0]))
+    low = tuple(ac if (ar >> i) & 1 else 0 for i in range(9))
+    cases.append((1, 1, low, low, "undecided_control"))
+    for r, s, b, c, case in cases:
+        need(rank2(b) == r and rank2(c) == s, "prescribed form ranks")
+        c01 = min(restricted(b, u, v) for u in readers for v in sources)
+        c10 = min(restricted(c, u, v) for u in readers for v in sources)
+        k = min(8, r, s)
+        need(c01 >= max(0, r - 2) and c10 >= max(0, s - 2), "codimension loss")
+        if case == "rank_pair":
+            sufficient += c01 + c10 >= k
+            old_sufficient += c01 + c10 >= 8
+        prices = {}
+        for name, ((kinds, n, d, mu, ranks), entries) in fixture_data.items():
+            charges = [cost(b, c, left, right) for left, right in entries]
+            for kind, charge in zip(kinds, charges):
+                lower = 16 - k if kind == "D" else 8 if kind == "N" else c01 if kind == "P01" else c10
+                need(charge >= lower, "term-price premise")
+            strong = 8 * n + (8 - k) * d + c01 * kinds.count("P01") + c10 * kinds.count("P10")
+            need(sum(charges) >= strong, "additive rank price")
+            if c01 + c10 >= k:
+                formal_input = 8 * n + (8 - k) * d + k * mu
+                need(sum(charges) >= formal_input >= 128, "formal count interface")
+            prices[name] = sum(charges)
+            if name == "standard":
+                need(sum(charges) == 128, "sharp separate-call attainer")
+            total_checks += 1
+        if (r, s) == (4, 4):
+            example = {"beta01_rows": list(b), "beta10_rows": list(c), "ranks": [r, s],
+                       "support_minima": [c01, c10], "k": k, "decoder_costs": prices}
+            need(c01 + c10 < 8 and c01 + c10 >= k, "strict extension example")
+        if case == "rank_pair":
+            pairs += 1
+        else:
+            need([c01, c10, k] == [0, 0, 1], "criterion must abstain")
+            undecided_control = {"ranks": [r, s], "support_minima": [c01, c10],
+                                 "beta01_rows": list(b), "beta10_rows": list(c),
+                                 "decoder_costs": prices, "verdict": "criterion inconclusive"}
+    return {"form_pairs": pairs, "decoder_cases": total_checks,
+            "criterion_passes": sufficient, "old_criterion_passes": old_sufficient,
+            "new_rank44_example": example, "coefficient_endpoints": len(fixture_data),
+            "undecided_control": undecided_control}
+
+
+def rank_region():
+    yes, no, prior = [], [], []
+    for r, s in itertools.product(range(10), repeat=2):
+        test = max(0, r - 2) + max(0, s - 2) >= min(8, r, s)
+        (yes if test else no).append([r, s])
+        if r + s >= 12:
+            prior.append([r, s])
+    need(len(yes) == 93 and len(prior) == 28, "rank-only region")
+    need(no == [[1, 1], [1, 2], [2, 1], [2, 2], [2, 3], [3, 2], [3, 3]], "seven unresolved rank pairs")
+    return {"certified_pairs": len(yes), "prior_rank_sum12_pairs": len(prior), "unresolved_pairs": no}
+
+
+def controls():
+    result = []
+    # These are witnesses that individual theorem hypotheses cannot be dropped.
+    result.append(reject(lambda: need(8 * 8 >= 128, "incidence absent"), "missing_incidence"))
+    need(8 + 8 >= 16, "first control retains Schur")
+    result.append(reject(lambda: need(8 * 0 + 0 * 16 + 8 * 0 >= 128, "Schur absent"), "missing_schur"))
+    need(0 + 16 >= 16, "second control retains incidence")
+    result.append(reject(lambda: need(8 * 8 + 0 * 8 >= 128, "pure price absent"), "missing_pure_surcharge"))
+    # Replacing the within-call rank-eight price by seven would be false.
+    result.append(reject(lambda: need(7 * 16 >= 128, "within price undercount"),
+                         "undercounted_within_price"))
+    # An overstrong block lower bound fails at A=D=B=C=I_2.
+    ident = (1, 2)
+    block = tuple(ident[i] | (ident[i] << 2) for i in range(2)) * 2
+    need(rank2(block) == 2, "sharp Schur control")
+    result.append(reject(lambda: need(rank2(block) >= 3, "extra rank unit"), "overstrong_schur"))
+    zero = (0, 0)
+    result.append(reject(lambda: need(rank2(zero + zero) >= 4, "missing invertible diagonal"), "missing_within_rank"))
+    mat = (1, 2, 4, 8, 0, 0, 0, 0, 0)
+    u = tuple(1 << i for i in range(1, 9))
+    v = tuple(1 << i for i in range(9) if i != 1)
+    need(restricted(mat, u, v) == 2, "two-codimension loss attainer")
+    result.append(reject(lambda: need(restricted(mat, u, v) >= 3, "one loss only"), "codimension_two_loss"))
+    damaged = decoder_fixtures()["two_cross"][:-1]
+    result.append(reject(lambda: coefficient_counts(damaged), "missing_cross_endpoint_term"))
+    return result
+
+
+def run():
+    pins()
+    data, readers, sources, histories = geometry()
+    return {"scope": "written conditional matrix proof; finite premises; separate Lean count theorem",
+            "support_censuses": histories, "within_pairings": 12544, "support_pair_ranks": 64,
+            "block_census": matrix_census(), "rank_region": rank_region(),
+            "form_fixtures": form_fixtures(data, readers, sources), "controls": controls()}
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument("--write-result", action="store_true")
+    args = parser.parse_args()
+    result = run()
+    path = HERE / "RESULT.json"
+    if args.write_result:
+        path.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n")
+    else:
+        # JSON booleans and integers must remain distinct (Python True == 1).
+        committed = json.dumps(json.loads(path.read_text()), sort_keys=True, separators=(",", ":"))
+        generated = json.dumps(result, sort_keys=True, separators=(",", ":"))
+        need(committed == generated, "committed result equality")
+    print("PASS_P112_CROSS_FORM_RANK_TRADEOFF ranks=93/100 blocks=9216 decoders=505 controls=8 abstentions=1")
+
+
+if __name__ == "__main__":
+    main()