From 9ab51a1a90da57a55d1ef75f20ecd4b2705b3f52 Mon Sep 17 00:00:00 2001
From: conorholds <86416572+conorholds@users.noreply.github.com>
Date: Sun, 18 Oct 2026 12:33:56 -0700
Subject: [PATCH] Prove the uniform E8 coset budget and two-sided rank-nine
 floor

---
 .../e8-one-coset-deficiency/CERTIFICATE.json  |  117 ++
 research/e8-one-coset-deficiency/FORMAL.md    |  134 ++
 research/e8-one-coset-deficiency/PROOF.md     |  603 ++++++
 research/e8-one-coset-deficiency/README.md    |  237 +++
 research/e8-one-coset-deficiency/RESULT.json  | 1669 +++++++++++++++++
 research/e8-one-coset-deficiency/SOURCES.json |   66 +
 .../e8-one-coset-deficiency/SPARSE-PAIR.md    |  284 +++
 research/e8-one-coset-deficiency/TASK.json    |   79 +
 research/e8-one-coset-deficiency/VERIFY.json  |   24 +
 research/e8-one-coset-deficiency/controls.py  |  119 ++
 research/e8-one-coset-deficiency/fixtures.py  |  323 ++++
 .../formal/BinaryCliqueCore.lean              |  289 +++
 .../formal/ConsumerArithmetic.lean            |   31 +
 research/e8-one-coset-deficiency/geometry.py  |  324 ++++
 .../e8-one-coset-deficiency/independent.py    |  555 ++++++
 .../e8-one-coset-deficiency/sparse_pair.py    |  381 ++++
 research/e8-one-coset-deficiency/verify.py    |  229 +++
 17 files changed, 5464 insertions(+)
 create mode 100644 research/e8-one-coset-deficiency/CERTIFICATE.json
 create mode 100644 research/e8-one-coset-deficiency/FORMAL.md
 create mode 100644 research/e8-one-coset-deficiency/PROOF.md
 create mode 100644 research/e8-one-coset-deficiency/README.md
 create mode 100644 research/e8-one-coset-deficiency/RESULT.json
 create mode 100644 research/e8-one-coset-deficiency/SOURCES.json
 create mode 100644 research/e8-one-coset-deficiency/SPARSE-PAIR.md
 create mode 100644 research/e8-one-coset-deficiency/TASK.json
 create mode 100644 research/e8-one-coset-deficiency/VERIFY.json
 create mode 100644 research/e8-one-coset-deficiency/controls.py
 create mode 100644 research/e8-one-coset-deficiency/fixtures.py
 create mode 100644 research/e8-one-coset-deficiency/formal/BinaryCliqueCore.lean
 create mode 100644 research/e8-one-coset-deficiency/formal/ConsumerArithmetic.lean
 create mode 100644 research/e8-one-coset-deficiency/geometry.py
 create mode 100644 research/e8-one-coset-deficiency/independent.py
 create mode 100644 research/e8-one-coset-deficiency/sparse_pair.py
 create mode 100644 research/e8-one-coset-deficiency/verify.py

diff --git a/research/e8-one-coset-deficiency/CERTIFICATE.json b/research/e8-one-coset-deficiency/CERTIFICATE.json
new file mode 100644
index 0000000000..21864b382d
--- /dev/null
+++ b/research/e8-one-coset-deficiency/CERTIFICATE.json
@@ -0,0 +1,117 @@
+{
+  "schema_version": 1,
+  "model": "Standard E8 roots scaled by 2; A8 label order",
+  "single_types": [
+    {"weight":1,"normal":1,"rows":[8,9,10,11,12,13,14,36],"determinant":-512},
+    {"weight":2,"normal":3,"rows":[1,2,3,4,5,6,7,43],"determinant":-256},
+    {"weight":3,"normal":7,"rows":[0,1,21,22,23,24,36,49],"determinant":512},
+    {"weight":4,"normal":15,"rows":[3,4,5,6,7,10,16,36],"determinant":-256},
+    {"weight":5,"normal":31,"rows":[0,1,2,3,30,31,32,36],"determinant":-1024},
+    {"weight":6,"normal":63,"rows":[5,6,7,12,18,23,27,36],"determinant":-256},
+    {"weight":7,"normal":127,"rows":[0,1,2,3,4,5,35,36],"determinant":-512},
+    {"weight":8,"normal":255,"rows":[7,14,20,25,29,32,34,36],"determinant":-256},
+    {"weight":9,"normal":511,"rows":[0,1,2,3,4,5,6,36],"determinant":256}
+  ],
+  "forbidden_pairs": [
+    {"counts":[0,0,2,7],"a":511,"b":508,"rows":[0,15,16,17,18,19,20,36],"determinant":1024},
+    {"counts":[0,0,4,5],"a":511,"b":496,"rows":[0,1,2,26,27,28,29,38],"determinant":512},
+    {"counts":[0,0,6,3],"a":511,"b":448,"rows":[0,1,2,3,4,33,40,119],"determinant":-512},
+    {"counts":[0,0,8,1],"a":511,"b":256,"rows":[0,1,2,3,4,5,6,42],"determinant":-512},
+    {"counts":[0,1,1,7],"a":510,"b":509,"rows":[0,85,86,87,88,89,90,100],"determinant":512},
+    {"counts":[0,1,3,5],"a":510,"b":497,"rows":[0,1,2,65,66,67,68,69],"determinant":512},
+    {"counts":[0,1,5,3],"a":510,"b":449,"rows":[0,1,2,3,4,67,68,119],"determinant":-512},
+    {"counts":[0,1,7,1],"a":510,"b":257,"rows":[0,1,2,3,4,5,6,69],"determinant":-512},
+    {"counts":[0,2,0,7],"a":508,"b":511,"rows":[0,15,16,17,18,19,20,36],"determinant":1024},
+    {"counts":[0,2,2,5],"a":508,"b":499,"rows":[0,15,26,27,28,29,38,85],"determinant":-1024},
+    {"counts":[0,2,4,3],"a":508,"b":451,"rows":[0,15,16,17,33,34,40,119],"determinant":2048},
+    {"counts":[0,2,6,1],"a":508,"b":259,"rows":[0,15,16,17,18,19,42,89],"determinant":1024},
+    {"counts":[0,3,1,5],"a":504,"b":503,"rows":[2,9,15,38,39,40,41,42],"determinant":512},
+    {"counts":[0,3,3,3],"a":504,"b":455,"rows":[2,3,4,9,15,40,41,119],"determinant":-512},
+    {"counts":[0,3,5,1],"a":504,"b":263,"rows":[2,3,4,5,6,9,15,42],"determinant":-512},
+    {"counts":[0,4,0,5],"a":496,"b":511,"rows":[0,1,2,26,27,28,29,38],"determinant":512},
+    {"counts":[0,4,2,3],"a":496,"b":463,"rows":[0,1,2,26,33,34,40,119],"determinant":1024},
+    {"counts":[0,4,4,1],"a":496,"b":271,"rows":[0,1,2,26,27,28,42,112],"determinant":1024},
+    {"counts":[0,5,1,3],"a":480,"b":479,"rows":[4,11,17,22,26,40,41,119],"determinant":-512},
+    {"counts":[0,5,3,1],"a":480,"b":287,"rows":[4,5,6,11,17,22,26,42],"determinant":-512},
+    {"counts":[0,6,0,3],"a":448,"b":511,"rows":[0,1,2,3,4,33,40,119],"determinant":-512},
+    {"counts":[0,6,2,1],"a":448,"b":319,"rows":[0,1,2,3,4,33,42,119],"determinant":1024},
+    {"counts":[0,7,1,1],"a":384,"b":383,"rows":[6,13,19,24,28,31,33,42],"determinant":-512},
+    {"counts":[0,8,0,1],"a":256,"b":511,"rows":[0,1,2,3,4,5,6,42],"determinant":-512},
+    {"counts":[1,0,1,7],"a":510,"b":508,"rows":[0,85,86,87,88,89,90,100],"determinant":512},
+    {"counts":[1,0,3,5],"a":510,"b":496,"rows":[0,1,2,65,66,67,68,69],"determinant":512},
+    {"counts":[1,0,4,4],"a":510,"b":480,"rows":[4,5,6,7,66,71,75,86],"determinant":512},
+    {"counts":[1,0,5,3],"a":510,"b":448,"rows":[0,1,2,3,4,67,68,119],"determinant":-512},
+    {"counts":[1,0,7,1],"a":510,"b":256,"rows":[0,1,2,3,4,5,6,69],"determinant":-512},
+    {"counts":[1,1,0,7],"a":508,"b":510,"rows":[0,85,86,87,88,89,90,100],"determinant":512},
+    {"counts":[1,1,2,5],"a":508,"b":498,"rows":[0,16,17,18,19,20,21,36],"determinant":1024},
+    {"counts":[1,1,4,3],"a":508,"b":450,"rows":[0,18,19,20,23,27,30,36],"determinant":1024},
+    {"counts":[1,1,6,1],"a":508,"b":258,"rows":[0,20,25,29,32,34,35,36],"determinant":1024},
+    {"counts":[1,2,1,5],"a":504,"b":502,"rows":[2,10,11,12,13,14,16,37],"determinant":1024},
+    {"counts":[1,2,2,4],"a":504,"b":486,"rows":[4,5,6,7,9,10,15,37],"determinant":-512},
+    {"counts":[1,2,3,3],"a":504,"b":454,"rows":[2,3,4,12,13,14,18,37],"determinant":512},
+    {"counts":[1,2,5,1],"a":504,"b":262,"rows":[2,3,4,5,6,14,37,69],"determinant":512},
+    {"counts":[1,2,6,0],"a":504,"b":6,"rows":[9,10,11,12,13,14,15,37],"determinant":512},
+    {"counts":[1,3,0,5],"a":496,"b":510,"rows":[0,1,2,65,66,67,68,69],"determinant":512},
+    {"counts":[1,3,2,3],"a":496,"b":462,"rows":[0,1,2,27,28,29,30,38],"determinant":512},
+    {"counts":[1,3,4,1],"a":496,"b":270,"rows":[0,1,2,29,32,34,35,38],"determinant":512},
+    {"counts":[1,4,0,4],"a":480,"b":510,"rows":[4,5,6,7,66,71,75,86],"determinant":512},
+    {"counts":[1,4,1,3],"a":480,"b":478,"rows":[4,12,13,14,18,23,27,39],"determinant":1024},
+    {"counts":[1,4,3,1],"a":480,"b":286,"rows":[4,5,6,14,20,25,29,39],"determinant":512},
+    {"counts":[1,4,4,0],"a":480,"b":30,"rows":[11,12,13,14,17,22,26,39],"determinant":512},
+    {"counts":[1,5,0,3],"a":448,"b":510,"rows":[0,1,2,3,4,67,68,119],"determinant":-512},
+    {"counts":[1,5,2,1],"a":448,"b":318,"rows":[0,1,2,3,4,34,40,119],"determinant":512},
+    {"counts":[1,6,1,1],"a":384,"b":382,"rows":[6,14,20,25,29,32,34,41],"determinant":1024},
+    {"counts":[1,6,2,0],"a":384,"b":126,"rows":[13,14,19,24,28,31,33,41],"determinant":512},
+    {"counts":[1,7,0,1],"a":256,"b":510,"rows":[0,1,2,3,4,5,6,69],"determinant":-512},
+    {"counts":[2,0,2,5],"a":508,"b":496,"rows":[0,15,26,27,28,29,38,85],"determinant":-1024},
+    {"counts":[2,0,4,3],"a":508,"b":448,"rows":[0,15,16,17,33,34,40,119],"determinant":2048},
+    {"counts":[2,0,6,1],"a":508,"b":256,"rows":[0,15,16,17,18,19,42,89],"determinant":1024},
+    {"counts":[2,1,1,5],"a":504,"b":500,"rows":[3,4,5,6,7,10,15,38],"determinant":-512},
+    {"counts":[2,1,3,3],"a":504,"b":452,"rows":[5,6,7,12,15,16,17,40],"determinant":-1024},
+    {"counts":[2,1,5,1],"a":504,"b":260,"rows":[7,14,15,16,17,18,42,43],"determinant":512},
+    {"counts":[2,2,0,5],"a":496,"b":508,"rows":[0,15,26,27,28,29,38,85],"determinant":-1024},
+    {"counts":[2,2,2,3],"a":496,"b":460,"rows":[0,15,26,33,34,40,44,87],"determinant":1024},
+    {"counts":[2,2,4,1],"a":496,"b":268,"rows":[0,15,26,27,28,42,44,89],"determinant":1024},
+    {"counts":[2,3,1,3],"a":480,"b":476,"rows":[5,6,7,12,17,22,26,40],"determinant":-1024},
+    {"counts":[2,3,3,1],"a":480,"b":284,"rows":[7,14,17,18,19,22,42,45],"determinant":-512},
+    {"counts":[2,4,0,3],"a":448,"b":508,"rows":[0,15,16,17,33,34,40,119],"determinant":2048},
+    {"counts":[2,4,2,1],"a":448,"b":316,"rows":[0,15,16,17,33,42,46,119],"determinant":-1024},
+    {"counts":[2,5,1,1],"a":384,"b":380,"rows":[7,14,19,24,28,31,42,47],"determinant":-512},
+    {"counts":[2,6,0,1],"a":256,"b":508,"rows":[0,15,16,17,18,19,42,89],"determinant":1024},
+    {"counts":[3,0,1,5],"a":504,"b":496,"rows":[2,9,15,38,39,40,41,42],"determinant":512},
+    {"counts":[3,0,3,3],"a":504,"b":448,"rows":[2,3,4,9,15,40,41,119],"determinant":-512},
+    {"counts":[3,0,4,2],"a":504,"b":384,"rows":[6,7,13,19,41,102,105,107],"determinant":512},
+    {"counts":[3,0,5,1],"a":504,"b":256,"rows":[2,3,4,5,6,9,15,42],"determinant":-512},
+    {"counts":[3,1,0,5],"a":496,"b":504,"rows":[2,9,15,38,39,40,41,42],"determinant":512},
+    {"counts":[3,1,2,3],"a":496,"b":456,"rows":[2,9,15,27,28,29,30,40],"determinant":512},
+    {"counts":[3,1,4,1],"a":496,"b":264,"rows":[2,9,15,29,32,34,35,42],"determinant":512},
+    {"counts":[3,2,1,3],"a":480,"b":472,"rows":[4,11,17,23,24,25,27,40],"determinant":512},
+    {"counts":[3,2,2,2],"a":480,"b":408,"rows":[6,7,13,19,22,23,26,41],"determinant":1024},
+    {"counts":[3,2,3,1],"a":480,"b":280,"rows":[4,5,6,11,17,25,42,103],"determinant":512},
+    {"counts":[3,3,0,3],"a":448,"b":504,"rows":[2,3,4,9,15,40,41,119],"determinant":-512},
+    {"counts":[3,3,2,1],"a":448,"b":312,"rows":[2,3,4,9,15,34,42,119],"determinant":512},
+    {"counts":[3,4,0,2],"a":384,"b":504,"rows":[6,7,13,19,41,102,105,107],"determinant":512},
+    {"counts":[3,4,1,1],"a":384,"b":376,"rows":[6,13,19,25,29,32,34,42],"determinant":512},
+    {"counts":[3,5,0,1],"a":256,"b":504,"rows":[2,3,4,5,6,9,15,42],"determinant":-512},
+    {"counts":[4,0,2,3],"a":496,"b":448,"rows":[0,1,2,26,33,34,40,119],"determinant":1024},
+    {"counts":[4,0,4,1],"a":496,"b":256,"rows":[0,1,2,26,27,28,42,112],"determinant":1024},
+    {"counts":[4,1,1,3],"a":480,"b":464,"rows":[5,6,7,12,18,23,26,40],"determinant":-512},
+    {"counts":[4,1,3,1],"a":480,"b":272,"rows":[7,14,20,25,26,27,28,42],"determinant":-1024},
+    {"counts":[4,2,0,3],"a":448,"b":496,"rows":[0,1,2,26,33,34,40,119],"determinant":1024},
+    {"counts":[4,2,2,1],"a":448,"b":304,"rows":[0,1,2,26,33,42,112,119],"determinant":2048},
+    {"counts":[4,3,1,1],"a":384,"b":368,"rows":[7,14,20,25,28,31,33,42],"determinant":-1024},
+    {"counts":[4,4,0,1],"a":256,"b":496,"rows":[0,1,2,26,27,28,42,112],"determinant":1024},
+    {"counts":[5,0,1,3],"a":480,"b":448,"rows":[4,11,17,22,26,40,41,119],"determinant":-512},
+    {"counts":[5,0,3,1],"a":480,"b":256,"rows":[4,5,6,11,17,22,26,42],"determinant":-512},
+    {"counts":[5,1,0,3],"a":448,"b":480,"rows":[4,11,17,22,26,40,41,119],"determinant":-512},
+    {"counts":[5,1,2,1],"a":448,"b":288,"rows":[4,11,17,22,26,34,42,119],"determinant":512},
+    {"counts":[5,2,1,1],"a":384,"b":352,"rows":[6,13,19,24,28,32,42,117],"determinant":512},
+    {"counts":[5,2,2,0],"a":384,"b":96,"rows":[31,32,33,59,80,95,105,111],"determinant":-512},
+    {"counts":[5,3,0,1],"a":256,"b":480,"rows":[4,5,6,11,17,22,26,42],"determinant":-512},
+    {"counts":[6,0,2,1],"a":448,"b":256,"rows":[0,1,2,3,4,33,42,119],"determinant":1024},
+    {"counts":[6,1,1,1],"a":384,"b":320,"rows":[7,14,20,25,29,32,33,42],"determinant":-512},
+    {"counts":[6,2,0,1],"a":256,"b":448,"rows":[0,1,2,3,4,33,42,119],"determinant":1024},
+    {"counts":[7,0,1,1],"a":384,"b":256,"rows":[6,13,19,24,28,31,33,42],"determinant":-512},
+    {"counts":[7,1,0,1],"a":256,"b":384,"rows":[6,13,19,24,28,31,33,42],"determinant":-512}
+  ]
+}
diff --git a/research/e8-one-coset-deficiency/FORMAL.md b/research/e8-one-coset-deficiency/FORMAL.md
new file mode 100644
index 0000000000..a1eb896b14
--- /dev/null
+++ b/research/e8-one-coset-deficiency/FORMAL.md
@@ -0,0 +1,134 @@
+# Formal scope
+
+Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0.
+
+The package includes `formal/BinaryCliqueCore.lean` and
+`formal/ConsumerArithmetic.lean`, both importing only Lean `Init`. All six
+declarations passed targeted Lean 4.21.0 checks with warnings treated as errors,
+one Lean thread, and an external 512 MiB RSS watchdog. The files were checked
+serially:
+
+| Source | Result | Elapsed | Peak process-group RSS |
+|---|---|---|---|
+| `BinaryCliqueCore.lean` | PASS, exit zero | 1.417 s | 262.30 MiB |
+| `ConsumerArithmetic.lean` | PASS, exit zero | 1.135 s | 235.02 MiB |
+
+Status: **PASS** for these scoped formal results.
+
+## Statements and explicit assumptions
+
+`BinaryCliqueCore.lean` defines `binarySum zero add xs` as the right-associated
+sum of a finite list. Its five declarations prove:
+
+1. `detector_sum_zero`: an additive Boolean-valued detector vanishes on a sum
+   when it vanishes on every summand.
+2. `detector_sum_selected`: if a list has no repeated vectors, a detector which
+   is one on one selected vector and zero on the others evaluates to one on
+   their sum.
+3. `compatible_clique_zero_sum_empty`: a distinct list of nonzero pairwise
+   compatible vectors has zero sum only if it is empty. Pairing additivity
+   detects every odd member of a putative relation. The remaining even members
+   have pairwise distinct Boolean colors, so there are at most two. A nonzero
+   singleton and two distinct vectors cannot have zero sum.
+4. `compatible_transversal_zero_sum_empty`: for membership predicates `Z i`
+   with pairwise trivial intersections, nonzero choices from distinct indices
+   cannot collide. If all nonzero cross-choices are compatible, any finite
+   zero relation among these grouped choices has an empty active index list.
+5. `BinaryNine.clique_zero_sum_empty`: instantiate the clique theorem in the
+   concrete binary space `Fin 9 → Bool`. Zero is pointwise false, addition is
+   pointwise XOR, and the pairing is the XOR of coordinatewise AND over the
+   explicit coordinate list `[0, 1, 2, 3, 4, 5, 6, 7, 8]`. All addition and
+   pairing laws required by the abstract theorem are proved. Distinctness,
+   nonzero vectors, orthogonality, and the even-color condition remain explicit
+   premises.
+
+`ConsumerArithmetic.lean` proves `copy_ge_seventy_two`: for arbitrary natural
+numbers `COPY`, `m`, `s`, and `t`, the two explicit premises
+`9 * m ≤ COPY + 9 * s + 9 * t` and `8 + s + t ≤ m` imply `72 ≤ COPY`.
+This is only the arithmetic consequence. The file does not derive either
+premise from ranks, dimensions, the Sylvester inequality, or E8 geometry.
+
+In the first four declarations, the operations are parameters, not undeclared
+axioms. Their exact laws are explicit premises:
+
+- `add x zero = x` and `add x y = zero ↔ x = y`, the characteristic-two
+  cancellation law;
+- `β x zero = false` and
+  `β x (add y z) = Bool.xor (β x y) (β x z)`;
+- pairing zero for distinct compatible vectors;
+- different Boolean colors for distinct even compatible vectors, where even
+  means `β x x = false`;
+- for the grouped-family corollary, trivial intersections and compatibility of
+  all nonzero cross-choices, together with membership/nonzero conditions on
+  the selected grouped vectors.
+
+`BinaryNine.clique_zero_sum_empty` discharges the first two algebraic premise
+groups for its concrete operations. It retains the geometric orthogonality and
+even-color premises. Neither symmetry nor nondegeneracy of `β` is silently
+assumed by the abstract proof. No fixed number of summands is assumed.
+
+Each public theorem has a `#print axioms` audit. The successful checks reported
+no axioms for `detector_sum_zero`, and only `propext`, `Classical.choice`, and
+`Quot.sound` for the other four clique/grouping declarations. The arithmetic
+theorem depends only on `propext`. There were no `sorryAx` dependencies or
+compiler warnings. Neither source contains a `sorry` or custom
+`axiom` declaration.
+
+## Boundary of the formal result
+
+This is a checked binary clique argument with a concrete nine-coordinate
+instantiation, not a formalization of the complete E8 theorem over fields of
+characteristic different from two. The identification of the E8 quotient with
+the concrete binary coordinate space, its geometric color map, nondegeneracy,
+and verification of the geometric compatibility premises are not formalized.
+Neither are the construction of the annihilators `Z i`, their
+intersection/cross-compatibility properties, the grouping of arbitrary scalar
+relations, the equivalence with Mathlib `LinearIndependent`, the finrank
+direct-sum budget, the scalar rank comparisons and field transfer, or the
+derivation of the two Sylvester/deficiency consumer premises. Those steps
+remain in PROOF.md; only their final natural-number consequence is separately
+formalized in `ConsumerArithmetic.lean`.
+
+The further singleton-pair classification and rank-(10,8) consequence in
+`SPARSE-PAIR.md` are written proofs. No new formal declaration covers their
+projective-ray classification, filtered-span basis bound or decoder assembly.
+
+## Toolchain and replay
+
+The repository's `formal/lean/lean-toolchain` pins
+`leanprover/lean4:v4.21.0`. The checked sources need that Lean distribution and
+`Init` only; they have no mathlib, external certificate, or package dependency.
+
+From the isolated worktree root, the local cached invocation is:
+
+```sh
+../e8-formal-work/toolchain/lean-4.21.0-darwin_aarch64/bin/lean \
+  --threads=1 -DwarningAsError=true \
+  research/e8-one-coset-deficiency/formal/BinaryCliqueCore.lean
+
+../e8-formal-work/toolchain/lean-4.21.0-darwin_aarch64/bin/lean \
+  --threads=1 -DwarningAsError=true \
+  research/e8-one-coset-deficiency/formal/ConsumerArithmetic.lean
+```
+
+The available cache is a local convenience, not a committed binary bundle. A
+provisioned Lean 4.21.0 binary can run the same sources and flags directly. No
+`lake` command or full build is required. The coordinating agent scheduled the
+recorded replays under a separate 512 MiB RSS watchdog; the commands above alone
+do not provide that external limit. Finish each command before starting the
+next. No Lean jobs were run concurrently.
+
+## Resource-limited drafts
+
+Two exploratory mathlib drafts were preserved privately outside this package
+and are not publication artifacts or formal claims. Their attempted checks
+were stopped before compiler diagnostics by the 1024 MiB RSS watchdog:
+
+| Draft | Result |
+|---|---|
+| Generic independent-transversal/direct-sum/finrank draft | STOPPED, 1033.16 MiB, 3.497 s; default Lean thread count |
+| Generic orthogonal coefficient-detection draft | STOPPED, 1049.67 MiB, 3.266 s; one Lean thread |
+
+These stops establish neither a theorem failure nor successful elaboration.
+The Init-only sources replace their formal coverage in this package. Full Lean
+project verification and clean toolchain provisioning were not run.
diff --git a/research/e8-one-coset-deficiency/PROOF.md b/research/e8-one-coset-deficiency/PROOF.md
new file mode 100644
index 0000000000..89c328853b
--- /dev/null
+++ b/research/e8-one-coset-deficiency/PROOF.md
@@ -0,0 +1,603 @@
+# A uniform one-coset deficiency budget on full E8
+
+Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0.
+This is a written proof with explicit finite integer certificates; its E8
+instantiation is not claimed to be a formally verified theorem.
+
+## 1. Statements and exact model
+
+Let K be any field of characteristic different from two. Let L be the 120
+root lines of E8, choose standard norm-two representatives r_v over Z[1/2],
+and evaluate them in K. Define G and N₀ over K, and define B_d from the
+integer root products before scalar reduction:
+
+```text
+G_Z[v,w] = the integer product of the standard rational roots,
+G = G_Z evaluated in K,            N₀ = G/2,
+B_d[v,w] = (1 + G_Z[v,w]) mod 2.
+```
+
+Thus B_d[v,w] is one exactly when v=w or v is orthogonal to w. The matrix
+B_d is the dense binary COPY table. Orientations of representatives do not
+change B_d. Let C ⊆ K^L be the eight-dimensional scalar root-evaluation code:
+the vectors (r_v·h)_{v∈L}, for h∈K^8. This scalar code is distinct from the
+binary label space Λ defined below.
+
+For X⊆L, write U_X for its binary label span and w(X)=dim_F₂ U_X. For p∈K^L,
+write w(p)=w(supp p) and δ(p)=9−w(p). A term p qᵀ costs
+
+```text
+ρ(supp p,supp q) = rank_F₂ B_d[supp p,supp q].
+```
+
+**Uniform deficiency theorem.** If λ∉C and (p_i) is any finite family of
+pairwise nonproportional nonzero vectors in C+Kλ, then
+
+```text
+Σ_i δ(p_i) ≤ 9.                                             (1)
+```
+
+Every nonzero vector in C has deficiency zero.
+
+**Exact-decoder consequence.** If P,Q∈K^{L×m}, m finite, satisfy
+
+```text
+PQᵀ = N₀,             rank_K P ≤ 9,       rank_K Q ≤ 9,       (2)
+```
+
+then COPY(P,Q)≥72. This floor is sharp in this class. Transposes are ordinary
+transposes, including over the complex numbers. The hypotheses concern the actual factor
+ranks, rather than the number of terms or a choice of presentation.
+The alternative convention PQᵀ=2G=4N₀ has exactly the same result: multiplying
+one factor by four changes neither supports, factor ranks nor COPY.
+
+We prove both statements directly. No catalogue, retraction, or pending
+general masked-realization theorem is a premise.
+
+Sections 2–7 first give the proof in characteristic zero, using a rational
+A8 model. Section 8 transports the finite facts to every characteristic
+different from two and replaces that scalar model by standard K^8. In
+particular the A8 divisions by three are not performed in characteristic three.
+
+## 2. A rational A8 realization and its canonical identification
+
+Until section 8 assume that K has characteristic zero.
+Write ω=(1,…,1)∈K^9 and V={x:Σ_j x_j=0}. Its dot product is nondegenerate:
+V⊥=Kω and ω·ω=9≠0. Use these oriented root representatives:
+
+```text
+r_ij = e_i−e_j                 (0≤i<j≤8),
+r_S  = 1_S−ω/3                (S⊆{0,…,8}, |S|=3).
+```
+
+There are 36+84=120 lines. All have squared norm two. Their integer rows
+R_v=3r_v have respectively entries (3,−3,0,…,0) and entries 2 on S, −1 off S.
+Pair roots already span V. Below R also denotes the 120×9 matrix of these
+integer rows. Its image is C: scaling evaluations by three does not change
+the code, and evaluation restricts to an injective map from V.
+
+Here is an explicit rational isometry to the standard E8 model. In Q^8 take
+the 56 lines e_a±e_b and the 64 half-root lines (±1,…,±1)/2 with an even
+number of minus signs. Choose the eight star roots
+
+```text
+s_j=e_0+e_j   (1≤j≤7),        s_8=(1,…,1)/2.
+```
+
+Their Gram matrix is I₈+J₈, of determinant nine. The eight vectors
+a_j=e_{j−1}−e_8 in V have the same Gram matrix. Therefore the unique rational
+linear map T with T(s_j)=a_j is an isometry. Explicitly, for a standard root x,
+put d_j=x·s_j and D=Σ_{j=1}^8 d_j. Then
+
+```text
+T(x) = (d_1−D/9,…,d_8−D/9,−D/9),
+3T(x) = (3d_1−D/3,…,3d_8−D/3,−D/3).                       (3)
+```
+
+For standard doubled roots A=2x and doubled stars S_j=2s_j,
+d_j=(A·S_j)/4. Enumerate e_a±e_b and the half-roots with first sign positive,
+apply (3), and choose the sign with first nonzero entry positive. The resulting
+120 integer rows are exactly the canonical signs of the rows R above. This
+finite equality is checked explicitly, together with the star Gram identity.
+Thus row permutations and individual row signs transport scalar evaluations,
+supports, and exact Gram factorizations between the two models.
+
+The label model is especially simple in A8 coordinates. Set Λ=F₂^9 with
+β(z,z′)=Σ_j z_j z′_j and assign
+
+```text
+u_ij = ω+e_i+e_j,              u_S = 1_S.                    (4)
+```
+
+All 120 labels are nonzero. They span Λ: differences of triples sharing two
+coordinates generate every e_i+e_j, hence the eight-dimensional even-weight
+space, and a triple adds an odd vector. Direct multiplication gives
+
+```text
+β(u_v,u_w) = (1+r_v·r_w) mod 2 = B_d[v,w].                  (5)
+```
+
+For pair/pair and pair/triple, the parity of the scalar product is the parity
+of the intersection of the indicated index sets; the extra ω contributes
+one. For triple/triple, r_S·r_T=|S∩T|−1, giving (5) as well. This includes
+the diagonal. Isometry (3) transfers the identity to canonical E8 roots.
+Because the labels span Λ and β is nondegenerate, B_d has rank nine.
+Thus (4) realizes the full canonical dense table, including all COPY ranks;
+it is not merely a label convention for a different incidence table.
+
+## 3. The three finite facts and complete profile coverage
+
+For nonzero z∈Λ define
+
+```text
+O_z = {v∈L : β(z,u_v)=1}.
+```
+
+Call distinct nonzero z,z′ **compatible** when the scalar roots indexed by
+O_z∩O_z′ have rank at most seven. For an even-weight vector set
+q(z)=wt(z)/2 mod 2. The required finite facts are:
+
+1. The roots indexed by O_z span V for every nonzero z.
+2. Compatible z,z′ satisfy β(z,z′)=0.
+3. If compatible z,z′ both have even weight, then q(z)≠q(z′).
+
+Fact 1, including its validity in every characteristic different from two,
+was already certified by CubeJerry / PR3095 with power-of-two integer minors.
+The present certificate independently reconstructs that premise together with
+the forbidden-pair witnesses needed for facts 2 and 3.
+
+Only full-rank witnesses are needed to prove these statements. The attached
+[CERTIFICATE.json](CERTIFICATE.json) gives nine single-character witnesses and
+100 forbidden-pair witnesses, each an explicit nonzero integer 8×8 minor
+in standard doubled-root coordinates, with row IDs in the A8 label order.
+Here is the entire reduction from these witnesses to all characters and pairs.
+
+Permutations of nine coordinates act on V, its root lines, and the labels
+(4). A pair root can change orientation; this multiplies a scalar row by −1
+and does not change its binary label. A coordinate permutation σ maps O_z
+to O_{σz} and preserves scalar ranks, β, and q. Nonzero single characters have exactly nine orbits,
+specified by their weight k=1,…,9. The representative z_k has its first k
+bits equal to one, that is integer bitmask 2^k−1 with bit zero first.
+
+For ordered pairs (z,z′), simultaneous coordinate permutation is classified
+completely by the four counts n_ab of coordinates with (z_j,z′_j)=(a,b).
+Two pairs with the same counts are related by a permutation, obtained by
+matching each of the four coordinate classes. There are
+
+```text
+#{(n_00,n_01,n_10,n_11)≥0 : Σ n_ab=9} = binom(12,3)=220.
+```
+
+Delete the profiles with z=0, z′=0, or z=z′. Each condition gives ten
+profiles. Every intersection of two or three conditions is the single
+all-zero pair profile, so their union has 30−3+1=28 profiles. Exactly
+220−28=192 valid ordered profiles remain. For each one use contiguous
+coordinate blocks 00,01,10,11 of their stated lengths to define a,b.
+
+The forbidden predicate on these representatives is precisely
+
+```text
+n_11 odd
+or [wt(a),wt(b) both even and wt(a)/2 ≡ wt(b)/2 (mod 2)].      (6)
+```
+
+Exactly 100 of the 192 profiles satisfy (6). The certificate contains exactly
+this inventory, without omissions or duplicates, and binds each a,b to its
+four counts. For each listed pair it selects eight standard doubled-root
+rows lying in O_a∩O_b with the stated nonzero determinant.
+Thus every forbidden profile has scalar rank eight. Its contrapositive proves
+facts 2 and 3 for all pairs; no assertion that the remaining profiles are
+compatible is required.
+
+For completeness the certificate's nine single-character determinants are
+
+| k | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
+|---|---|---|---|---|---|---|---|---|---|
+| det | −512 | −256 | 512 | −256 | −1024 | −256 | −512 | −256 | 256 |
+
+Rows are indexed from zero: first pair roots in lexicographic order of (i,j),
+then triple roots in lexicographic order of S. Every witness index must be
+distinct, in 0,…,119, and satisfy its stated character conditions. The verifier
+uses (3) to bind each indexed A8 line to its standard eight-dimensional
+doubled-root row. Nonzero determinants give fact 1 and all forbidden
+rank-eight assertions. Every absolute determinant is a power of two,
+belonging to {256,512,1024,2048}; this permits the extension in section 8.
+
+The displayed formulas reconstruct every finite input: enumerate the roots,
+labels, nine singles and 220 four-count tuples; select the 100 tuples by (6);
+check witness membership and recompute every determinant. [verify.py](verify.py)
+enforces these complete inventories. [independent.py](independent.py) separately
+reconstructs the standard D8-plus-half-root model and exhausts all nonzero
+characters and unordered distinct pairs in intrinsic dense-table coordinates.
+
+Every doubled-root entry and every witness determinant is an integer. A nonzero
+integer remains nonzero in every characteristic-zero field. Consequently
+these facts hold for scalar rank over any such K, including fields not
+embedded in R or C. No reduction-mod-prime assumption is used for this
+transfer; modular rank can select a witness, but the exact determinant
+certifies it.
+
+## 4. Every compatibility clique is linearly independent
+
+Credit mightyOil / PR1248's compatible-edge independence argument as the
+method ancestor. Here it is applied to arbitrary compatible cliques, then
+grouped across all support annihilators in section 5.
+
+Let E be a set of distinct pairwise compatible nonzero binary vectors.
+Fact 2 says that its off-diagonal β pairings vanish. For an odd-weight member
+z, β(z,z)=1. Pairing a linear relation among E with z therefore makes its
+coefficient zero. All odd-weight members disappear from any relation.
+
+The remaining members have even weight. By fact 3, any two have opposite
+q values. There are only two values, so there are at most two such members
+in E. A single nonzero vector is independent, and two distinct nonzero
+vectors over F₂ are independent. The remaining relation is therefore zero.
+This proves independence of E, and in particular |E|≤9.
+
+## 5. Annihilator packing proves the uniform theorem
+
+For any scalar vector p define its binary support annihilator
+
+```text
+Z(p) = {z∈Λ : β(z,u_v)=0 for every v∈supp p}.
+```
+
+Nondegeneracy gives dim Z(p)=9−w(p)=δ(p). Equivalently, z∈Z(p) means p
+vanishes on O_z. If 0≠p∈C and 0≠z∈Z(p), the evaluation defining p
+vanishes on roots spanning V by fact 1, forcing p=0. Thus Z(p)=0 for
+every nonzero p∈C.
+
+It remains to consider the members outside C. Each has a unique expression
+p_i=a_i λ+R h_i with a_i≠0 and h_i∈V. Divide by a_i, which preserves support
+and annihilator, and rename h_i to obtain
+
+```text
+p_i = λ+R h_i.
+```
+
+Here Rω=0 because every A8 root row has coordinate sum zero. Together with
+the direct sum K^9=V⊕Kω in characteristic zero and injectivity on V, this
+justifies taking each evaluation representative uniquely in V.
+
+These normalized vectors are distinct: equality would make the original
+members proportional. Thus h_i−h_j≠0 for i≠j. Write Z_i=Z(p_i).
+
+First, Z_i∩Z_j=0. Indeed a common nonzero z would make both vectors vanish
+on O_z. Their difference R(h_i−h_j) would vanish there as well, contradicting
+fact 1 and injectivity of evaluation on V.
+
+Second, every nonzero z∈Z_i and z′∈Z_j with i≠j form a compatible pair.
+They are distinct by the preceding paragraph. Both p_i and p_j vanish on
+O_z∩O_z′. The nonzero linear functional defined by h_i−h_j therefore
+vanishes on every scalar root there. Its kernel in V is a hyperplane, so
+that root set has rank at most seven. This is compatibility by definition.
+
+Pairwise trivial intersection alone would not suffice to add dimensions.
+Here the stronger cross-pair property supplies the missing step. Suppose
+there is a relation Σ_i z_i=0 with z_i∈Z_i. Discard its zero summands. The
+remaining z_i are distinct nonzero vectors, one from each participating
+space, and every two are compatible. Section 4 makes them independent,
+contradicting this nonempty relation. Hence the sum of all Z_i is direct in
+the nine-dimensional Λ, and
+
+```text
+Σ_i δ(p_i) = Σ_i dim Z_i = dim(⊕_i Z_i) ≤ 9.
+```
+
+Members inside C contribute zero, proving (1) for the entire finite family.
+The proof imposes no bound on its cardinality and makes no assumption about
+the weights or support shapes of the individual vectors.
+
+The budget nine is attained. Set λ=0 on pair roots and λ=−2 on triple roots,
+and let p_j=λ+R_column_j for j=0,…,8. The pair roots force λ∉C: a codeword
+vanishing on all pair roots is zero. These nine vectors have different
+supports, hence are nonproportional. Their nonzero triple entries are exactly
+the triples avoiding j; their nonzero pair entries are exactly pairs incident
+to j. All corresponding labels lie in e_j⊥. The triples on the other eight
+coordinates span that eight-dimensional space by the same even-space plus
+odd-vector argument used after (4). Therefore w(p_j)=8 and Σ_j δ(p_j)=9.
+This is sharpness of the family budget, not an exact-decoder fixture.
+
+## 6. Normalization of an exact factorization preserves the needed bounds
+
+Start with (2). Drop any term having a zero factor, since its scalar outer
+product and its COPY cost are both zero. If p_j=μp_i with μ≠0, replace
+
+```text
+p_i q_iᵀ+p_j q_jᵀ  by  p_i(q_i+μq_j)ᵀ.
+```
+
+The new column support is contained in supp q_i∪supp q_j. For a fixed row
+support, binary pairing rank is monotone under restricting columns and
+subadditive under taking their union. Hence the new cost is at most the sum
+of the two old costs. The new columns of either factor lie in its old column
+span, so neither actual factor rank increases. The symmetric operation merges
+proportional q columns. Remove any zero factor created by a merge.
+
+Repeat merges on either side until neither side has a proportional pair.
+Each operation decreases the number of terms, so this terminates. Denote the
+remaining number by m′. Both final families consist of pairwise
+nonproportional nonzero vectors; exactness is preserved and cost has not
+increased. Retain every term with two nonzero factors, even if its binary
+COPY cost is zero: such an outer product can be nonzero and can be necessary
+for exact equality to N₀. There is no deletion of off-mask scalar entries.
+
+The standard root matrix R₀ has full column rank: its rows include the basis
+e_0±e_1,…,e_6±e_7. Thus R₀ is injective and R₀ᵀ is surjective. Their product
+G=R₀R₀ᵀ has rank eight and image C, without requiring R₀ᵀR₀ to be invertible.
+Exactness and its transpose imply
+
+```text
+C = col(N₀) ⊆ col(P),              C ⊆ col(Q).
+```
+
+For the normalized factors their ranks are consequently 8+s and 8+t with
+s,t∈{0,1}. If s=0, all p columns are in C and their total deficiency is zero.
+If s=1, their span is C+Kλ_P for some λ_P∉C; apply (1) to the normalized
+family. The same argument applies on the q side. In both cases,
+
+```text
+Σ_k δ(p_k)≤9s,      Σ_k δ(q_k)≤9t.                         (7)
+```
+
+The values s,t here are the final ranks: normalization can lower a rank,
+and (7) covers (9,9) and every exit into (8,8), (9,8), or (8,9).
+
+## 7. The COPY floor, sharpness, and the boundary of the result
+
+For binary subspaces U,W⊆Λ, the pairing map U→W* has kernel U∩W⊥. Hence
+
+```text
+ρ(U,W)=dim U−dim(U∩W⊥) ≥ dim U+dim W−9.
+```
+
+This also applies to cost-zero terms. Summing it and using (7) gives
+
+```text
+COPY ≥ Σ_k [w(p_k)+w(q_k)−9]
+     = 9m′−Σ_k δ(p_k)−Σ_k δ(q_k)
+     ≥ 9(m′−s−t).                                          (8)
+```
+
+Sylvester's inequality, applied to the normalized exact product, gives
+
+```text
+8=rank(PQᵀ) ≥ rank P+rank Q−m′ = 16+s+t−m′.
+```
+
+For clarity this follows by restricting P:K^{m′}→K^L to im(Qᵀ): its kernel
+has dimension at most m′−rank P. Thus m′≥8+s+t, and (8) is at least 72.
+The original factorization has no smaller cost, proving the consequence.
+
+The one-sided slices are low-dimensional instances of the L120 basis-cost
+programme. If S contains C and dim S=8+s with s in {0,1}, any basis of S is
+nonproportional. The uniform theorem gives total basis deficiency at most 9s,
+so every such basis costs at least 9(8+s)-9s=72. SPARSE-PAIR.md proves the
+specified dimension-ten instance. These statements do not prove L120 for
+arbitrary S; the genuinely two-sided consumer here is the (s,t)=(1,1) cell.
+
+Sharpness requires only the ordinary rank-(8,8) decoder. In standard root
+coordinates use the orthogonal norm-two frame f_k=e_{2a}±e_{2a+1}, a=0,…,3.
+Let X[v,k]=r_v·f_k. Since Σ_k f_k f_kᵀ=2I₈, the factors P=Q=X/2 satisfy
+PQᵀ=G/2. They have rank eight. Every nonzero column is a scalar codeword,
+so its support has label span Λ by section 5. Each of the eight terms
+therefore costs nine, for total 72. No rank-(9,9), ten-term equality fixture
+is needed for this sharpness claim. There is also the following normalized
+two-sided equality construction, retained in [fixtures.py](fixtures.py).
+
+### 7.1. Normalized rank-(9,9), ten-term equality
+
+Write E(h)=(r_x·h)_{x∈L} for scalar evaluation in standard root coordinates.
+Choose v=e_0+e_1 and w=e_0+e_2, so v·w=1, and their root lines a,b. The
+actual oriented representatives at those lines may be ±v and ±w. Use the
+following dual bases; inspection gives h_i·d_j=δ_ij:
+
+```text
+(h_1,…,h_8) = (v, e_1, e_0−e_2, e_3,…,e_7),
+(d_1,…,d_8) = (w, −e_0+e_1−e_2, −e_2, e_3,…,e_7).
+```
+
+Let δ_a,δ_b denote coordinate unit vectors in K^L and define nine terms by
+
+```text
+λ=E(v)_a δ_a,      p_0=λ,             p_j=λ−E(h_j)  (1≤j≤8),
+q_j=−E(d_j)/2      (1≤j≤8),          q_0=−Σ_{j=1}^8 q_j.
+```
+
+Since E(v)_a=±2, λ≠0. It is outside C because its binary support weight is
+one, whereas every nonzero scalar codeword has weight nine. Duality gives
+
+```text
+Σ_{i=0}^8 p_i q_iᵀ
+  = −Σ_{j=1}^8 E(h_j)q_jᵀ
+  = (1/2)Σ_{j=1}^8 E(h_j)E(d_j)ᵀ = G/2.                   (9)
+```
+
+The p columns span C+Kλ: their differences with p_0 give the basis E(h_j).
+They are pairwise nonproportional, since all have the same nonzero quotient
+modulo C and the h_j, together with zero, are distinct. The q_1,…,q_8 are
+a basis of C; q_0 is their negative sum, hence nonzero and nonproportional
+to each of them. This is therefore a normalized rank-(9,8) decoder.
+
+The support of p_1=λ−E(v) is exactly the roots nonorthogonal to v with line
+a omitted. Its labels lie in u_a⊥. Adding label u_a gives the support of
+E(v), whose label span is Λ, so w(p_1)=8. Thus δ(p_0)=8 and δ(p_1)=1.
+The family theorem forces all other p_j to have weight nine. Since each q_i
+is a nonzero codeword, these nine terms have costs (1,8,9,9,9,9,9,9,9).
+
+Now put μ=δ_b and c=N₀[:,b], and replace the nine q columns, adding one term:
+
+```text
+q_i′ = q_i−q_i(b)μ   (0≤i≤8),       (p_9,q_9′)=(c,μ).
+```
+
+Equation (9) implies Σ_i p_i q_i(b)=c, so this changes the product by
+−cμᵀ+cμᵀ=0. The p rank is still nine, since c∈C. The new q columns span
+C+Kμ: μ is present and each old q_i is q_i′+q_i(b)μ. This has dimension
+nine, since the singleton μ is outside C.
+
+All ten terms are normalized. The old p columns are outside C and pairwise
+nonproportional, so none is proportional to the new nonzero c∈C. On the
+other side, a relation q_i′=αq_j′ would give q_i−αq_j∈C∩Kμ=0, contradicting
+the old nonproportionality. No q_i′ is zero or proportional to μ for the same
+reason. Thus neither side admits a proportional merge.
+
+Because d_1=w, q_1′ has exactly the nonorthogonal-to-w support with line b
+omitted. As above its label span is u_b⊥ of dimension eight. Together with
+q_9′=μ of weight one this saturates the q-side deficiency budget nine, so
+all other q_i′ have weight nine. Both p_1 and q_1′ consequently have
+hyperplane label spans. Since v·w=1, equation (5) gives β(u_a,u_b)=0, and
+
+```text
+ρ(p_1,q_1′) = 8−dim_F₂(u_a⊥∩F₂u_b) = 7.
+```
+
+The first and last terms pair a singleton with a full label span and cost
+one each. The seven remaining terms have both label spans full and cost
+nine each. The ten costs are therefore
+
+```text
+(1,7,9,9,9,9,9,9,9,1),                total COPY = 72.
+```
+
+This is an explicit equality example in the strict normalized (9,9), m=10
+class, rather than an enumeration of arbitrary coefficient choices.
+
+### 7.2. Necessary structure of every equality case
+
+Suppose an original factorization in (2) has COPY=72. Any completed
+normalization still costs 72: cost cannot rise, and the proved floor applies
+to its final ranks. For those ranks 8+s,8+t, the two inequalities in section
+7 force
+
+```text
+m′=8+s+t,       Σ_i δ(p_i)=9s,       Σ_i δ(q_i)=9t.
+```
+
+Indeed m′>8+s+t would force COPY≥81; with equality in the term count, any
+unsaturated deficiency budget would make (8) strictly greater than 72.
+Every individual pairing inequality is also an equality, since all their
+nonnegative gaps sum to zero. In annihilator notation this is equivalent to
+
+```text
+Z(q_i) ⊆ U_supp(p_i),   or equivalently β(Z(p_i),Z(q_i))=0.
+```
+
+For either factor with excess one, its annihilators form a β-orthogonal
+direct-sum decomposition of all Λ. Orthogonality follows from fact 2 and
+the cross-compatibility in section 5; their dimensions sum to nine by
+budget saturation. Consequently β restricts nondegenerately to each nonzero
+annihilator: a vector in its radical would be orthogonal to every summand,
+hence all Λ, and would be zero. These are necessary equality conditions;
+they do not classify the scalar coefficient families. The exact fixtures
+check the dimensions, same-side orthogonality, restricted nondegeneracy,
+and matched cross-side orthogonality after every normalization exit.
+
+As a useful unrestricted-rank corollary, every exact ten-term decoder whose
+two factors both leave C costs at least 72. Indeed write their ranks as
+8+s,8+t with s,t≥1. Sylvester gives s+t≤2, so s=t=1 and the theorem applies.
+A cheaper exact decoder with both factors outside C would therefore need at
+least eleven terms. A rank-(10,8) ten-term decoder is outside this result.
+
+The theorem is for the full E8 root set and exact N₀, with dense table B_d.
+It does not prove the general masked P120 floor, a punctured-root floor,
+or an unrestricted floor with a factor of rank ten or more. The separate
+[SPARSE-PAIR.md](SPARSE-PAIR.md) derives a restricted rank-(10,8) extension:
+one factor lies in C and the other in C plus two root-coordinate unit vectors.
+This is a consequence of the one-coset theorem, not a uniform two-direction
+family budget. Singleton padding of a
+punctured decoder can raise the factor ranks beyond nine. Nor does the
+family budget extend to two arbitrary outside directions: over an infinite
+field the vectors δ_a+tδ_b for arbitrarily many distinct nonzero t have support size two,
+are pairwise nonproportional, and all have deficiency seven. There is no
+new κ, physical realization, supplier admission, or multiplication theorem.
+
+## 8. Extension to every scalar field of characteristic different from two
+
+Both the uniform theorem and the exact-decoder COPY floor hold for every
+field K with char K≠2, using the standard E8 roots over Z[1/2]. Define C as
+their scalar evaluation code over K and retain the fixed integer-incidence
+table B_d and the binary labels (4). In particular B_d is defined before
+scalar reduction, rather than by taking parity of a field element.
+
+The 109 standard-coordinate determinant witnesses are powers of two, hence
+remain nonzero in K. To transport their profiles when char K=3, do not reduce
+the rational A8 isometry or its sum-zero scalar space: those were only used
+over Q to index the root lines. Instead use the following integral reflection
+identities. For each adjacent transposition of the nine A8 coordinates, let
+α be the standard doubled E8 root corresponding to that pair root. Its
+reflection is H=I−ααᵀ/4. For N=4I−ααᵀ the verifier checks
+
+```text
+N²=16I,             4u−(u·α)α = ε·4u′    (ε∈{1,−1})
+```
+
+for all 120 standard doubled-root rows u, with u′ the A8-permuted line,
+and checks that its binary label is the same coordinate permutation of u's
+label. These are eight generator checks, 960 signed root-image identities,
+and 512 matrix-entry identities. They hold over Z, so H is an invertible
+root-line permutation over every K of odd characteristic. The generators
+give the full S9 action needed for the nine single and 192 pair profiles.
+Thus the same unit witnesses prove all three finite facts over K, defining
+compatibility by scalar rank over K itself.
+
+In sections 4–7 replace the scalar A8 space V by standard K^8 and its
+evaluation map R₀. Its dot product is nondegenerate, and R₀ has rank eight
+because the orthogonal frame basis has determinant ±16. The annihilator,
+grouped-relation, merge, binary rank and Sylvester arguments are unchanged.
+In particular rank N₀=8 follows from injectivity of R₀ and surjectivity of
+R₀ᵀ, even in characteristics three and five where R₀ᵀR₀=30I is singular.
+The ordinary rank-(8,8) decoder still attains 72. This extension does not
+assert that the nine A8 integer vectors in section 5 retain their stated
+supports after reduction at three, and makes no characteristic-two claim.
+
+The sparse-pair consequence in SPARSE-PAIR.md uses this all-odd-field theorem
+directly; its singleton-ray classification, binary orthogonality and filtered
+basis argument require no further field-transfer premise.
+
+The strict normalized rank-(9,9), ten-term equality construction in section
+7.1 also persists over every such field: its integral dual bases remain bases,
+its quotient-space nonproportionality arguments remain valid, and the two
+distinguished support hyperplanes still saturate the deficiency budgets.
+Their nonzero root pairings are ±1 or ±2, so exactly the same single root
+line is removed on each side in every characteristic different from two.
+
+## 9. Predecessors and proof dependencies
+
+Credit joaqcoo / PR1224 for the all-m projection equations, one-sided
+annihilator constraints and original compatible-pair census; mightyOil /
+PR1248 for the fixed-A8-frame deficiency-nine theorem and compatible-edge
+independence method; adamgall / PR2062 for the fixed A7+A1 family; CubeJerry /
+PR3095 for the single-character rank premise in every odd characteristic;
+and bbMisk / PR1633
+for the sharp factor excess-rank budget and full two-sided ten-term residual
+form. PR717 and PR446 supply the exact-decoder and per-term pairing-rank COPY
+model; PR968 and PR1077 supply earlier exact-root decoder floors. The new
+assembly proves an arbitrary one-coset family budget and its all-m,
+rank-at-most-nine exact-N₀ consumer; the rank and merge arguments are rederived.
+
+The one-sided slices belong to L120, the programme documented in PR3074 and
+PR3154's B-prime node. PR3191's draft completion claim still has an unfilled
+implementation slot at its pinned head; conorholds / PR3166 supplies C7 in
+that programme. None of that conditional chain is a premise here. The
+two-sided (1,1) result addresses PR3154's C-prime node and its requested
+term-count-independent deficiency budget. philippeVV's restricted clean
+lift-family credit-at-most-nine argument in Discussion 1587 is related prior
+work; the arbitrary-family theorem here does not assume its lift hypotheses.
+
+The proof uses only the explicitly constructed root/label model, the 109
+finite rank witnesses and their orbit coverage, and the linear algebra in
+sections 4–7. It imports none of the C1–C5, catalogue, capacity, root-swap,
+or retraction assertions in the later master-floor programme. Reproduction
+and the distinction between executable checks and formal coverage are recorded
+in the package README and verification records. [FORMAL.md](FORMAL.md) describes
+the checked Init-only Lean core for odd-coefficient elimination, the Boolean
+even-color argument, and absence of nonempty zero relations among compatible
+cliques and nonzero grouped choices from trivially intersecting subspaces. It does
+not formalize the E8 finite facts, their geometric instantiation, the connection
+to Mathlib linear independence or finrank, the dimension budget, or the
+exact-factorization COPY consequence. A second Init-only file checks the final
+natural-number implication from the two displayed budget inequalities to
+COPY≥72, with both inequalities left as explicit premises. The first file also
+instantiates the addition and pairing laws on Fin 9→Bool; the E8 geometric
+orthogonality and even-color hypotheses remain explicit premises.
diff --git a/research/e8-one-coset-deficiency/README.md b/research/e8-one-coset-deficiency/README.md
new file mode 100644
index 0000000000..b8d0bcd485
--- /dev/null
+++ b/research/e8-one-coset-deficiency/README.md
@@ -0,0 +1,237 @@
+# Uniform E8 one-coset budget and the two-sided rank-nine COPY floor
+
+The new core result is a uniform deficiency budget for arbitrary finite,
+pairwise nonproportional families in one outside-code direction on full E8.
+It supplies the missing term-count-independent packing step and implies **COPY ≥ 72** for every
+exact decoder `PQᵀ = N₀ = G/2` whose two actual factor ranks are at most nine,
+with any finite number of terms. Both results hold over **every scalar field
+of characteristic different from two**. The binary COPY table is the fixed
+canonical dense table, defined before scalar field reduction.
+
+The genuinely two-sided consumer is the `(s,t)=(1,1)` cell, where both actual
+factor ranks are nine. The one-sided dimension-nine and sparse dimension-ten
+corollaries below are scoped cases of the existing **L120** programme, which
+asks for minimum basis cost at least 72 for every scalar space containing C.
+They are proved here directly, including in odd characteristic, without
+assuming that programme's conditional completion chain.
+
+The floor is attained by the ordinary eight-term frame and by an explicit
+**normalized rank-(9,9), ten-term** decoder. Its per-term costs are
+`(1,7,9,9,9,9,9,9,9,1)`. Thus the result closes the first genuinely two-sided
+ten-term exact-decoder branch, including all proportional-merge exits.
+It does not assert the unrestricted masked P120 floor or change κ.
+
+A further consequence closes a specific **rank-(10,8)** family, over the same
+fields and with any finite term count: if one factor lies in `C` and the other
+in `C + span(δ_a,δ_b)` for two root-coordinate unit vectors, then COPY is at
+least 72. [SPARSE-PAIR.md](SPARSE-PAIR.md) derives this from the uniform theorem
+by classifying all deficient projective rays in those extensions. Weight-at-most-seven
+vectors lie in the two-dimensional coordinate space; weight-at-most-eight
+vectors lie in a four-dimensional space. Every ten-vector basis therefore
+costs at least `1+1+8+8+6·9=72`. A sheared rank-(10,8) equality construction
+is pairwise nonproportional on both sides, so its rank and ten terms survive
+proportional normalization. This is a sparse-pair result, not an arbitrary
+two-direction theorem.
+
+## The theorem and its consumer
+
+Let `C` be the eight-dimensional scalar E8 root-evaluation code. The binary
+root labels span `Λ = F₂⁹`; for a coefficient vector `p`, let `w(p)` be the
+binary rank of the labels on its nonzero support. If `λ ∉ C` and the nonzero
+vectors `p_i ∈ C + Kλ` are pairwise nonproportional, then
+
+```text
+Σ_i (9 − w(p_i)) ≤ 9.
+```
+
+Each nonzero vector in `C` has weight nine. The theorem applies to arbitrary
+families in one extension, rather than a prescribed frame or actual-basis
+catalogue. Its proof uses the annihilators of the binary support spans. Three
+finite E8 rank facts force compatible binary characters to be independent;
+grouping a putative relation by annihilator then proves that all these
+annihilators form a direct sum in a nine-dimensional space.
+
+For the consumer, alternating proportional merges preserve exactness and
+never increase COPY or either factor rank. Only zero-factor terms are
+discarded; nonzero cost-zero atoms are retained. After normalization write
+the ranks as `8+s, 8+t`, with `s,t ∈ {0,1}`. The two deficiency budgets and
+the binary pairing inequality give
+
+```text
+COPY ≥ 9m − 9s − 9t ≥ 72,
+```
+
+where the last step is Sylvester's `m ≥ 8+s+t`. Recomputing the ranks after
+merging includes exits to rank `(9,8)`, `(8,9)` and `(8,8)`.
+
+In particular every exact ten-term decoder whose two factors both leave `C`
+is covered: Sylvester forces both ranks to be nine. A cheaper two-sided exact
+decoder would need at least eleven terms and a factor of rank at least ten.
+
+Every equality case also has necessary rigidity after normalization:
+`m=8+s+t`, both deficiency budgets saturate, and every term's annihilators
+are orthogonal across the two factors. On each rank-nine side, its
+annihilators decompose all `Λ` into mutually orthogonal nondegenerate summands.
+[PROOF.md §7.2](PROOF.md#72-necessary-structure-of-every-equality-case) proves
+these conditions; they do not constitute a scalar coefficient classification.
+
+## Proof, certificates and controls
+
+[PROOF.md](PROOF.md) gives the complete written argument, normalization,
+sharp constructions and field transfer. The finite evidence is separated from
+that universal argument:
+
+| Evidence | What it checks |
+|---|---|
+| [CERTIFICATE.json](CERTIFICATE.json), [geometry.py](geometry.py) | Nine single-character types and 100 forbidden ordered-pair profiles, with 109 explicit integer 8×8 minors. Every determinant is a power of two. |
+| Integral reflection identities | Eight generators implement the full S9 profile action on standard doubled roots over `Z[1/2]`: 960 signed root images and 512 matrix-entry checks. This avoids reducing the rational A8 isometry in characteristic three. |
+| [independent.py](independent.py) | A separately written reconstruction starting from D8 plus half-roots, deriving its own binary labels and checking all 511 characters and 130,305 unordered pairs by modular full-rank witnesses or exact integer elimination. |
+| Complete F3 families | All 6,561 coefficient choices in each of four sparse one-coset families; their total deficiencies are 9, 9, 9 and 7. Also checks weight nine for all 6,560 nonzero scalar codewords. |
+| Model binding | All 120 root lines, 14,400 scalar Gram pairs, and the full binary pairing/quadratic-color transport agree between the two constructions. |
+| [fixtures.py](fixtures.py) | Eight entrywise exact rational factorizations, all costing 72; strict normalized `(9,9)` equality; merges on both sides, cancellation, zero-factor removal and rank drops. The same eight factorizations are checked over F3, F5 and F7. |
+| Semantic controls | Reject omitted terms, wrong target scaling, a changed factor sign, and deletion of a genuinely nonzero cost-zero atom. |
+| [controls.py](controls.py) | Reject 14 certificate corruptions at specified gates, including a valid full-rank minor of determinant 768 that fails the odd-field unit condition; accept a different valid signed minor; separate binary from rational rank; exhibit dependent fake cliques if either binary edge condition is omitted. |
+| Scope controls | Repeated proportional vectors violate the unqualified family bound; six nonproportional rays in two outside directions have total deficiency 42, so doubling the present budget is invalid. |
+| [sparse_pair.py](sparse_pair.py) | Separate dense-table reconstruction; both complete 29,524-ray F3 sparse-pair spaces; exact deficient-ray classifications and weight-filter ranks; planted F5/F7 controls. Six sheared equality fixtures remain rank-(10,8) with zero merges; six original equality fixtures are positive controls that merge twice to rank-(8,8). Omitted reader compensation fails the exact product check. |
+
+The full independent pair-rank histogram is `0:255, 6:3360, 7:35640,
+8:91050`. The certificate supplies sufficient full-rank witnesses, without
+depending on that complete histogram. Failed modular rank never establishes a
+rational deficiency; an explicit rank-drop control exercises that distinction.
+
+These are two internal implementations and AI-assisted source reviews, not
+independent human certification. [FORMAL.md](FORMAL.md) records six checked
+Init-only Lean declarations for the abstract binary clique argument, its
+concrete nine-bit addition/dot-product laws, and the final natural-number
+budget implication. The E8
+instantiation, annihilator/dimension assembly, field transfer and COPY consumer
+remain written mathematics rather than a formal proof-assistant theorem.
+
+## Reproduce
+
+No Python dependencies or compilation are required for the registered replay.
+From the repository root, with CPython 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/e8-one-coset-deficiency --check-only
+python3.12 -B scripts/research_package.py --package research/e8-one-coset-deficiency
+```
+
+Direct replay also works from a source export with the declared inputs present:
+
+```sh
+python3 -I -B research/e8-one-coset-deficiency/verify.py
+```
+
+Normal execution checks the scientific source inventory before loading the
+package modules, authenticates the declared input bytes, recomputes all finite
+evidence and compares it with [RESULT.json](RESULT.json). Package modules are
+compiled from their current source bytes, bypassing stale bytecode. The replay
+uses explicit checks and supports `-O`. It does not rewrite receipts. The
+explicit `--emit` option regenerates both deterministic certificate and result
+after an intentional source change; such a change requires a fresh replay.
+
+The registered Python replay does not invoke Lean. [FORMAL.md](FORMAL.md)
+gives the separate Lean 4.21.0 command and the exact formal boundary. Run
+resource-intensive jobs serially; no whole-project build is needed.
+
+## Relation to prior work and coordination
+
+This answers the uniform compatibility/packing question left by
+[PR1224](https://github.com/CrocSwap/integer-mult-bounds/pull/1224)
+(joaqcoo), rather than just replaying its pair census. It extends
+[PR1248](https://github.com/CrocSwap/integer-mult-bounds/pull/1248)
+(mightyOil)'s fixed A8-frame budget; its compatible-edge independence argument
+is a method ancestor of the clique proof. It also extends the fixed A7+A1 family of
+[PR2062](https://github.com/CrocSwap/integer-mult-bounds/pull/2062) (adamgall).
+[PR1633](https://github.com/CrocSwap/integer-mult-bounds/pull/1633)
+(bbMisk) supplies the factor-excess-rank framework and two-sided ten-term
+normal form; the rank and merge arguments needed here are rederived.
+
+The model and COPY accounting retain the E8 decoder lineage of PR446/PR717
+(DreamingOfClouds), PR968 (themilkman216) and PR1077 (woklerx).
+[PR2854](https://github.com/CrocSwap/integer-mult-bounds/pull/2854)
+is a punctured-P112 rank-nine floor, which does not imply this full-root result.
+The exact-N₀ reduction in
+[PR2832](https://github.com/CrocSwap/integer-mult-bounds/pull/2832)
+does not preserve factor ranks and hence cannot turn this theorem into a
+general masked-realization floor. The special joint-query packing in
+PR3549/PR3569 does not supply this arbitrary-family theorem.
+
+DreamingOfClouds's [PR2816](https://github.com/CrocSwap/integer-mult-bounds/pull/2816)
+already studies singleton root swaps and two coordinate pieces in the P112
+low-excess correction setting; PR2862 gives a historical lift-floor baseline.
+The sparse-pair corollary retains that geometric credit and proves its stated
+full-E8, all-odd-field, all-term contract directly from the uniform budget.
+
+CubeJerry's [PR3095](https://github.com/CrocSwap/integer-mult-bounds/pull/3095)
+already certifies full rank of every full-E8 character complement over every
+characteristic different from two using power-of-two minors (fact 1 here),
+and asks about L120 in odd characteristic. The present finite certificate
+reconstructs that premise and adds the forbidden-pair facts and orbit action;
+fact 1 and its odd-characteristic validity are not claimed as new.
+philippeVV's credit-at-most-nine argument for restricted clean lift families
+in [Discussion 1587](https://github.com/CrocSwap/integer-mult-bounds/discussions/1587)
+is adjacent antecedent work, rather than the arbitrary-family theorem here.
+
+The active two-sided consumer is
+[PR3154](https://github.com/CrocSwap/integer-mult-bounds/pull/3154)'s
+ARCHITECT node C-prime: this closes its exact `(1,1)` cell for every term
+count. Its G2 discussion explicitly requests an “m-free deficiency budget”.
+The one-sided `(1,0)` and `(0,1)` branches and the sparse-pair extension are
+dimension-nine and specified dimension-ten cases of node B-prime / L120.
+For the exact-decoder list in
+[Discussion 1587](https://github.com/CrocSwap/integer-mult-bounds/discussions/1587),
+the coverage is the nine-term P120 item and the ranks-at-most-nine slice of
+`m>=10`; its higher-rank and other realization questions remain open.
+
+The broader characteristic-zero one-sided programme is documented by
+[PR3074](https://github.com/CrocSwap/integer-mult-bounds/pull/3074)'s sufficiency
+of L120 and [draft PR3191](https://github.com/CrocSwap/integer-mult-bounds/pull/3191)'s
+conditional completion claim. At the 2026-10-18 19:29 UTC refresh,
+PR3191 head `9c9e094d0fb665db8a3aaa4f9bce1c95c0c6e14b` still has an
+unfilled implementation slot. conorholds' merged
+[PR3166](https://github.com/CrocSwap/integer-mult-bounds/pull/3166) supplies C7
+within that programme. If its full L120 conclusion is established, it includes
+these one-sided characteristic-zero slices; it does not supply this package's
+arbitrary-family theorem or the two-sided `(1,1)` floor. G2 with one side of
+arbitrary larger rank and C-prime's higher-excess branches remain outside scope.
+This package uses none of the pending catalogue, retraction, C1–C5 or global
+master-floor premises. [SOURCES.json](SOURCES.json) pins the reused proof inputs
+and the historical selected record/catalogue at base `20ecf289`.
+
+The original card and scope change are retained in [TASK.json](TASK.json).
+An overlapping-task search is advisory, not a novelty proof. This candidate
+has been prepared locally under a no-publication instruction; no public claim
+or Discussion reservation was made. Current overlap evidence must be refreshed
+before any authorized submission.
+
+## Limits
+
+The result concerns full E8, fixed dense binary COPY accounting and exact
+`N₀`. It does not cover arbitrary masked realizations, punctured alphabets,
+or arbitrary factors with two outside-code directions. The restricted
+singleton-pair extension is covered by SPARSE-PAIR.md. It does not settle the global
+P120 master floor, unrestricted one-sided ten-term `(10,8)` factorizations,
+supplier admission, physical parking or a multiplication exponent.
+Characteristic two is excluded. The all-odd-field theorem follows from the
+unit minors and reflection identities, rather than inference from three
+finite-field examples. The sparse-pair extension follows from that theorem,
+not extrapolation of its F3 census.
+
+## Open next questions
+
+1. **Two outside directions.** Study an actual rank-(10,9), eleven-term
+   exact identity. This is the next possible cheaper two-sided branch, but
+   the six-ray counterexample prevents replacing nine by eighteen in the
+   present family theorem. A coupled replacement for the direct-sum budget
+   is needed before claiming a generalization.
+2. **Complete formalization.** Instantiate the checked binary clique core
+   with the E8 labels, then connect the certified root spans, annihilators,
+   dimension bound and Sylvester/COPY consumer. These bridges remain open;
+   exploratory broad Mathlib imports exceeded a conservative local memory
+   watchdog. The published formal claim is limited to the checked Init core.
+
+Prepared by conorholds, with substantial OpenAI Codex assistance, including
+GPT-6.1 SOL agents at xHigh. New work is Apache-2.0; predecessor credits are
+retained above. No independent human peer review is claimed.
diff --git a/research/e8-one-coset-deficiency/RESULT.json b/research/e8-one-coset-deficiency/RESULT.json
new file mode 100644
index 0000000000..0605d38388
--- /dev/null
+++ b/research/e8-one-coset-deficiency/RESULT.json
@@ -0,0 +1,1669 @@
+{
+  "actual_factors": {
+    "exact_factorizations": {
+      "canceling_free_atoms": {
+        "copy_cost": 72,
+        "equality_conditions": {
+          "annihilator_dimensions": [
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ],
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ]
+          ],
+          "matched_cross_side_orthogonality": true,
+          "nonzero_excess_summands_nondegenerate": true,
+          "normalized_term_count_tight": true,
+          "same_side_orthogonal_direct_sums": true
+        },
+        "merge_cost_trace": [
+          72,
+          72,
+          72
+        ],
+        "normalized_deficiencies": [
+          0,
+          0
+        ],
+        "normalized_ranks": [
+          8,
+          8
+        ],
+        "normalized_terms": 8,
+        "ranks": [
+          9,
+          9
+        ],
+        "terms": 10
+      },
+      "column_extension": {
+        "copy_cost": 72,
+        "equality_conditions": {
+          "annihilator_dimensions": [
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ],
+            [
+              8,
+              1,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ]
+          ],
+          "matched_cross_side_orthogonality": true,
+          "nonzero_excess_summands_nondegenerate": true,
+          "normalized_term_count_tight": true,
+          "same_side_orthogonal_direct_sums": true
+        },
+        "merge_cost_trace": [
+          72
+        ],
+        "normalized_deficiencies": [
+          0,
+          9
+        ],
+        "normalized_ranks": [
+          8,
+          9
+        ],
+        "normalized_terms": 9,
+        "ranks": [
+          8,
+          9
+        ],
+        "terms": 9
+      },
+      "free_atom_split": {
+        "copy_cost": 72,
+        "equality_conditions": {
+          "annihilator_dimensions": [
+            [
+              8,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              1
+            ],
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ]
+          ],
+          "matched_cross_side_orthogonality": true,
+          "nonzero_excess_summands_nondegenerate": true,
+          "normalized_term_count_tight": true,
+          "same_side_orthogonal_direct_sums": true
+        },
+        "merge_cost_trace": [
+          72,
+          72
+        ],
+        "normalized_deficiencies": [
+          9,
+          0
+        ],
+        "normalized_ranks": [
+          9,
+          8
+        ],
+        "normalized_terms": 9,
+        "ranks": [
+          9,
+          9
+        ],
+        "terms": 10
+      },
+      "free_atom_split_transposed": {
+        "copy_cost": 72,
+        "equality_conditions": {
+          "annihilator_dimensions": [
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ],
+            [
+              8,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              1
+            ]
+          ],
+          "matched_cross_side_orthogonality": true,
+          "nonzero_excess_summands_nondegenerate": true,
+          "normalized_term_count_tight": true,
+          "same_side_orthogonal_direct_sums": true
+        },
+        "merge_cost_trace": [
+          72,
+          72
+        ],
+        "normalized_deficiencies": [
+          0,
+          9
+        ],
+        "normalized_ranks": [
+          8,
+          9
+        ],
+        "normalized_terms": 9,
+        "ranks": [
+          9,
+          9
+        ],
+        "terms": 10
+      },
+      "inside": {
+        "copy_cost": 72,
+        "equality_conditions": {
+          "annihilator_dimensions": [
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ],
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ]
+          ],
+          "matched_cross_side_orthogonality": true,
+          "nonzero_excess_summands_nondegenerate": true,
+          "normalized_term_count_tight": true,
+          "same_side_orthogonal_direct_sums": true
+        },
+        "merge_cost_trace": [
+          72
+        ],
+        "normalized_deficiencies": [
+          0,
+          0
+        ],
+        "normalized_ranks": [
+          8,
+          8
+        ],
+        "normalized_terms": 8,
+        "ranks": [
+          8,
+          8
+        ],
+        "terms": 8
+      },
+      "row_extension": {
+        "copy_cost": 72,
+        "equality_conditions": {
+          "annihilator_dimensions": [
+            [
+              8,
+              1,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ],
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ]
+          ],
+          "matched_cross_side_orthogonality": true,
+          "nonzero_excess_summands_nondegenerate": true,
+          "normalized_term_count_tight": true,
+          "same_side_orthogonal_direct_sums": true
+        },
+        "merge_cost_trace": [
+          72
+        ],
+        "normalized_deficiencies": [
+          9,
+          0
+        ],
+        "normalized_ranks": [
+          9,
+          8
+        ],
+        "normalized_terms": 9,
+        "ranks": [
+          9,
+          8
+        ],
+        "terms": 9
+      },
+      "two_extensions": {
+        "copy_cost": 72,
+        "equality_conditions": {
+          "annihilator_dimensions": [
+            [
+              8,
+              1,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ],
+            [
+              0,
+              1,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              8
+            ]
+          ],
+          "matched_cross_side_orthogonality": true,
+          "nonzero_excess_summands_nondegenerate": true,
+          "normalized_term_count_tight": true,
+          "same_side_orthogonal_direct_sums": true
+        },
+        "merge_cost_trace": [
+          72
+        ],
+        "normalized_deficiencies": [
+          9,
+          9
+        ],
+        "normalized_ranks": [
+          9,
+          9
+        ],
+        "normalized_terms": 10,
+        "ranks": [
+          9,
+          9
+        ],
+        "terms": 10
+      },
+      "zero_factor": {
+        "copy_cost": 72,
+        "equality_conditions": {
+          "annihilator_dimensions": [
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ],
+            [
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0,
+              0
+            ]
+          ],
+          "matched_cross_side_orthogonality": true,
+          "nonzero_excess_summands_nondegenerate": true,
+          "normalized_term_count_tight": true,
+          "same_side_orthogonal_direct_sums": true
+        },
+        "merge_cost_trace": [
+          72,
+          72
+        ],
+        "normalized_deficiencies": [
+          0,
+          0
+        ],
+        "normalized_ranks": [
+          8,
+          8
+        ],
+        "normalized_terms": 8,
+        "ranks": [
+          9,
+          8
+        ],
+        "terms": 9
+      }
+    },
+    "odd_characteristic_actual_controls": {
+      "char5_R_transpose_R_zero_but_Gram_rank_eight": true,
+      "primes": {
+        "3": {
+          "exact_factorizations": {
+            "canceling_free_atoms": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "column_extension": {
+              "copy_cost": 72,
+              "ranks": [
+                8,
+                9
+              ]
+            },
+            "free_atom_split": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "free_atom_split_transposed": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "inside": {
+              "copy_cost": 72,
+              "ranks": [
+                8,
+                8
+              ]
+            },
+            "row_extension": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                8
+              ]
+            },
+            "two_extensions": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "zero_factor": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                8
+              ]
+            }
+          },
+          "target_rank": 8
+        },
+        "5": {
+          "exact_factorizations": {
+            "canceling_free_atoms": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "column_extension": {
+              "copy_cost": 72,
+              "ranks": [
+                8,
+                9
+              ]
+            },
+            "free_atom_split": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "free_atom_split_transposed": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "inside": {
+              "copy_cost": 72,
+              "ranks": [
+                8,
+                8
+              ]
+            },
+            "row_extension": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                8
+              ]
+            },
+            "two_extensions": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "zero_factor": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                8
+              ]
+            }
+          },
+          "target_rank": 8
+        },
+        "7": {
+          "exact_factorizations": {
+            "canceling_free_atoms": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "column_extension": {
+              "copy_cost": 72,
+              "ranks": [
+                8,
+                9
+              ]
+            },
+            "free_atom_split": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "free_atom_split_transposed": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "inside": {
+              "copy_cost": 72,
+              "ranks": [
+                8,
+                8
+              ]
+            },
+            "row_extension": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                8
+              ]
+            },
+            "two_extensions": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                9
+              ]
+            },
+            "zero_factor": {
+              "copy_cost": 72,
+              "ranks": [
+                9,
+                8
+              ]
+            }
+          },
+          "target_rank": 8
+        }
+      }
+    },
+    "semantic_mutations_rejected": [
+      "omit_term",
+      "wrong_N0_scale",
+      "one_factor_sign",
+      "drop_nonzero_cost_zero_atom"
+    ],
+    "sharp_families": {
+      "annihilator_dimensions_eight_and_one": [
+        8,
+        1
+      ],
+      "nine_family_scalar_rank": 9,
+      "nine_weight_eight_vectors": [
+        8,
+        8,
+        8,
+        8,
+        8,
+        8,
+        8,
+        8,
+        8
+      ],
+      "proportional_family_counterexample": {
+        "copies": 6,
+        "total_deficiency": 48
+      },
+      "sharp_total_deficiency": 9,
+      "two_outside_direction_counterexample": {
+        "total_deficiency": 42,
+        "vectors": 6
+      }
+    }
+  },
+  "independent_exhaustion": {
+    "binary_dimension": 9,
+    "canonical_label_weight_counts": {
+      "3": 84,
+      "7": 36
+    },
+    "compatible_pairs": 39255,
+    "controls": {
+      "complementary_normals": 0,
+      "geometry_predicate_mismatch_rejected": true,
+      "modular_rank_drop": {
+        "dispatched_rank": 8,
+        "mod_three_rank": 7,
+        "rational_rank": 8,
+        "used_rational_fallback": true
+      },
+      "nonorthogonal_normals": 8,
+      "orthogonal_coordinate_normals": 7,
+      "orthogonal_even_same_quadratic": 8
+    },
+    "forbidden_pairs_proved_full_rank": 73785,
+    "implementation": "independent standard D8 plus half-root E8 realization",
+    "nonzero_characters": 511,
+    "pair_rank_histogram": {
+      "0": 255,
+      "6": 3360,
+      "7": 35640,
+      "8": 91050
+    },
+    "rank_evaluations": {
+      "exact_rational_fallbacks": 39255,
+      "mod_three_full_rank_witnesses": 91561
+    },
+    "root_lines": 120,
+    "scalar_coordinate_scale": 2,
+    "scalar_dimension": 8,
+    "single_rank_histogram": {
+      "8": 511
+    },
+    "sparse_cosets": {
+      "code_dimension": 8,
+      "codewords_checked": 6561,
+      "families": {
+        "nonorthogonal_11": {
+          "deficiency_histogram": {
+            "0": 6558,
+            "1": 2,
+            "7": 1
+          },
+          "deficiency_sum": 9,
+          "lambda_support_rank": 2,
+          "normalizations_checked": 6561,
+          "sparse_lambda": [
+            [
+              0,
+              1
+            ],
+            [
+              2,
+              1
+            ]
+          ]
+        },
+        "nonorthogonal_12": {
+          "deficiency_histogram": {
+            "0": 6558,
+            "1": 2,
+            "7": 1
+          },
+          "deficiency_sum": 9,
+          "lambda_support_rank": 2,
+          "normalizations_checked": 6561,
+          "sparse_lambda": [
+            [
+              0,
+              1
+            ],
+            [
+              2,
+              2
+            ]
+          ]
+        },
+        "orthogonal_11": {
+          "deficiency_histogram": {
+            "0": 6560,
+            "7": 1
+          },
+          "deficiency_sum": 7,
+          "lambda_support_rank": 2,
+          "normalizations_checked": 6561,
+          "sparse_lambda": [
+            [
+              0,
+              1
+            ],
+            [
+              1,
+              1
+            ]
+          ]
+        },
+        "singleton": {
+          "deficiency_histogram": {
+            "0": 6559,
+            "1": 1,
+            "8": 1
+          },
+          "deficiency_sum": 9,
+          "lambda_support_rank": 1,
+          "normalizations_checked": 6561,
+          "sparse_lambda": [
+            [
+              0,
+              1
+            ]
+          ]
+        }
+      },
+      "field_order": 3,
+      "nonzero_codewords_with_support_rank_nine": 6560
+    },
+    "status": "PASS",
+    "unordered_distinct_nonzero_pairs": 130305
+  },
+  "integrity_and_hypothesis_controls": {
+    "alternative_valid_minor_accepted": true,
+    "binary_vs_scalar_rank_control": {
+      "binary": 2,
+      "rational": 3
+    },
+    "certificate_corruptions_rejected": {
+      "boolean_determinant": "minor determinant type/value",
+      "boolean_normal": "single normal binding",
+      "distinct_valid_rows_with_singular_minor": "integer minor determinant",
+      "duplicate_minor_row": "minor root indices",
+      "duplicate_profile": "unknown/duplicate forbidden profile",
+      "duplicate_single": "duplicate single type",
+      "float_profile_count": "profile counts",
+      "full_rank_minor_not_unit_over_Z_half": "minor is not a unit over Z[1/2]",
+      "incorrect_determinant": "integer minor determinant",
+      "missing_forbidden_profile": "forbidden inventory count",
+      "missing_single": "single inventory count",
+      "negative_root_index": "minor root indices",
+      "valid_minor_bound_to_wrong_profile": "normal/profile binding",
+      "witness_outside_character": "witness support membership"
+    },
+    "weakened_edge_rule_counterexamples": {
+      "omit_even_colour": {
+        "forbidden_pair_rank": 8,
+        "normals": [
+          3,
+          12,
+          15
+        ],
+        "xor": 0
+      },
+      "omit_orthogonality": {
+        "forbidden_pair_rank": 8,
+        "normals": [
+          1,
+          2,
+          4,
+          7
+        ],
+        "xor": 0
+      }
+    }
+  },
+  "live_inputs_authenticated": [
+    "research/a8-simplex-decoder-floor/PROOF.md",
+    "research/decoder-excess-rank/PROOF.md",
+    "research/nine-term-decoder-normal-form-seed42/PROOF.md",
+    "formal/lean/lean-toolchain"
+  ],
+  "model_binding": {
+    "binary_vectors_transported": 512,
+    "even_quadratic_colours_transported": 256,
+    "gram_pairs": 14400,
+    "label_graph_rank": 9,
+    "orthonormal_transport_checks": 81,
+    "root_bijection": 120,
+    "sparse_pair_root_bijection": 120,
+    "sparse_pair_table_entries": 14400
+  },
+  "odd_field_profile_transport": {
+    "adjacent_generators": 8,
+    "denominators_are_powers_of_two": true,
+    "involution_matrix_entries": 512,
+    "root_line_transports": 960
+  },
+  "primary_certificate": {
+    "all_minors_units_over_Z_half": true,
+    "determinants_absolute": [
+      256,
+      512,
+      1024,
+      2048
+    ],
+    "forbidden_pair_profiles": 100,
+    "nonzero_integer_minors": 109,
+    "single_types": 9,
+    "valid_pair_profiles": 192
+  },
+  "profile_orbit_accounting": {
+    "forbidden_ordered_pairs": 147570,
+    "ordered_pairs": 260610
+  },
+  "receipt_type_controls": [
+    "boolean",
+    "float",
+    "string",
+    "wrong_integer"
+  ],
+  "schema_version": 1,
+  "scientific_sha256": {
+    "CERTIFICATE.json": "6c3500ed02a57c1203c9f0eea7f3deee078c5e27f2d95d7f860f580b0984ffbc",
+    "FORMAL.md": "7b6cce9c1157f1ed7cef27f2f55eb79710d37a09eb7905442a0ec2a490b4e154",
+    "PROOF.md": "d3dcc35205225547c13f8bc0ec3175da7aab41e54c7adc06f0c35c86f00b93e4",
+    "README.md": "3f20bd9b8dc51f7d3d05fc87398ae4a1612d5a10123a721ae2fa033f1b7838be",
+    "SOURCES.json": "06d492675838c141b1dc298b977ec3205950066f779719720f245c8e52ff61ab",
+    "SPARSE-PAIR.md": "0a7c82d97837740c00273fc1261a4bfd2037c68ab05cc0e80f8968a19cfa1723",
+    "TASK.json": "e91796c8e9edd97f1ae447e4d5199504e2ca40952ea83cbb131cf9e05a310cb0",
+    "VERIFY.json": "53e5495e35a7e7103ad50b0ab3e2b6556cd4dd2ff0d28b5ea2b281ec3054ec01",
+    "controls.py": "b3b38a8cdd5deda5707e042b9268328a29043b34223808b1756f3ea7a87ef279",
+    "fixtures.py": "62c5e175b203771ed38cda2d5ea4f6258ff00436bbfb605bc898a991defc8d63",
+    "formal/BinaryCliqueCore.lean": "a979ede983a0479da91389747b4085073dadf438ed9f913b8399b4d2d8dbe158",
+    "formal/ConsumerArithmetic.lean": "f71d6e1575655715159a1689811af3d319a37971bbd66eb5ec5a0d0aada98b19",
+    "geometry.py": "c783f6ddaf0bd5381b2345a62fe01f13e3e101ca33d70bc0495c406034782b91",
+    "independent.py": "aca9e8e73e04fc11ee1b33ec498763418900acc7e31dfd52a6deddcc2b7ecf71",
+    "sparse_pair.py": "968f99dd1f1d1a304b78716f4ca71401dcc69fa9e7dc56286a9fca0cdefeec61",
+    "verify.py": "21323d5d9cf3c9d1907dbd2627a454fa07ddeb5ffbac5357153235de07bfc651"
+  },
+  "scope": "finite proof inputs and controls for the written all-m one-coset theorem",
+  "sparse_pair_evidence": {
+    "binary_copy_rank": 9,
+    "code_projective_points": 3280,
+    "controls": {
+      "wrong_hole_factor_two_rejected": true,
+      "wrong_nonorthogonal_branch_rejected": true,
+      "wrong_orthogonal_branch_rejected": true
+    },
+    "f3_cases": [
+      {
+        "classified_projective_rays": 29524,
+        "indices": [
+          0,
+          1
+        ],
+        "minimum_basis_weight": 72,
+        "pair_type": "orthogonal",
+        "prefix_ranks_0_to_8": [
+          0,
+          2,
+          2,
+          2,
+          2,
+          2,
+          2,
+          2,
+          4
+        ],
+        "projective_points": 29524,
+        "weight_histogram": {
+          "1": 2,
+          "2": 2,
+          "8": 2,
+          "9": 29518
+        },
+        "weight_le7_pure_external_rays": 4,
+        "weight_le8_rays_in_H": 6
+      },
+      {
+        "classified_projective_rays": 29524,
+        "indices": [
+          0,
+          2
+        ],
+        "minimum_basis_weight": 72,
+        "pair_type": "nonorthogonal",
+        "prefix_ranks_0_to_8": [
+          0,
+          2,
+          2,
+          2,
+          2,
+          2,
+          2,
+          2,
+          4
+        ],
+        "projective_points": 29524,
+        "weight_histogram": {
+          "1": 2,
+          "2": 2,
+          "8": 6,
+          "9": 29514
+        },
+        "weight_le7_pure_external_rays": 4,
+        "weight_le8_rays_in_H": 10
+      }
+    ],
+    "merge_proof_sharp_fixtures": [
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          1
+        ],
+        "omitted_reader_compensation_mutation_rejected": true,
+        "pair_type": "orthogonal",
+        "pairwise_nonproportional": [
+          true,
+          true
+        ],
+        "prime": 3,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            10,
+            8
+          ],
+          "merges": 0,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            1,
+            1,
+            8,
+            8,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 10,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "merge_proof"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          1
+        ],
+        "omitted_reader_compensation_mutation_rejected": true,
+        "pair_type": "orthogonal",
+        "pairwise_nonproportional": [
+          true,
+          true
+        ],
+        "prime": 5,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            10,
+            8
+          ],
+          "merges": 0,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            1,
+            1,
+            8,
+            8,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 10,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "merge_proof"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          1
+        ],
+        "omitted_reader_compensation_mutation_rejected": true,
+        "pair_type": "orthogonal",
+        "pairwise_nonproportional": [
+          true,
+          true
+        ],
+        "prime": 7,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            10,
+            8
+          ],
+          "merges": 0,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            1,
+            1,
+            8,
+            8,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 10,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "merge_proof"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          2
+        ],
+        "omitted_reader_compensation_mutation_rejected": true,
+        "pair_type": "nonorthogonal",
+        "pairwise_nonproportional": [
+          true,
+          true
+        ],
+        "prime": 3,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            10,
+            8
+          ],
+          "merges": 0,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            1,
+            1,
+            8,
+            8,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 10,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "merge_proof"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          2
+        ],
+        "omitted_reader_compensation_mutation_rejected": true,
+        "pair_type": "nonorthogonal",
+        "pairwise_nonproportional": [
+          true,
+          true
+        ],
+        "prime": 5,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            10,
+            8
+          ],
+          "merges": 0,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            1,
+            1,
+            8,
+            8,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 10,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "merge_proof"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          2
+        ],
+        "omitted_reader_compensation_mutation_rejected": true,
+        "pair_type": "nonorthogonal",
+        "pairwise_nonproportional": [
+          true,
+          true
+        ],
+        "prime": 7,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            10,
+            8
+          ],
+          "merges": 0,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            1,
+            1,
+            8,
+            8,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 10,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "merge_proof"
+      }
+    ],
+    "planted_field_checks": [
+      {
+        "nonzero_coefficient_pairs": 16,
+        "pair_type": "orthogonal",
+        "prime": 5,
+        "singleton_vectors_checked": 16,
+        "two_coset_vectors_checked": 48
+      },
+      {
+        "nonzero_coefficient_pairs": 36,
+        "pair_type": "orthogonal",
+        "prime": 7,
+        "singleton_vectors_checked": 24,
+        "two_coset_vectors_checked": 108
+      },
+      {
+        "nonzero_coefficient_pairs": 16,
+        "pair_type": "nonorthogonal",
+        "prime": 5,
+        "singleton_vectors_checked": 16,
+        "two_coset_vectors_checked": 48
+      },
+      {
+        "nonzero_coefficient_pairs": 36,
+        "pair_type": "nonorthogonal",
+        "prime": 7,
+        "singleton_vectors_checked": 24,
+        "two_coset_vectors_checked": 108
+      }
+    ],
+    "root_lines": 120,
+    "sharp_fixtures": [
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          1
+        ],
+        "pair_type": "orthogonal",
+        "pairwise_nonproportional": [
+          true,
+          false
+        ],
+        "prime": 3,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            8,
+            8
+          ],
+          "merges": 2,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 8,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "collapsing_positive_control"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          1
+        ],
+        "pair_type": "orthogonal",
+        "pairwise_nonproportional": [
+          true,
+          false
+        ],
+        "prime": 5,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            8,
+            8
+          ],
+          "merges": 2,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 8,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "collapsing_positive_control"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          1
+        ],
+        "pair_type": "orthogonal",
+        "pairwise_nonproportional": [
+          true,
+          false
+        ],
+        "prime": 7,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            8,
+            8
+          ],
+          "merges": 2,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 8,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "collapsing_positive_control"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          2
+        ],
+        "pair_type": "nonorthogonal",
+        "pairwise_nonproportional": [
+          true,
+          false
+        ],
+        "prime": 3,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            8,
+            8
+          ],
+          "merges": 2,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 8,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "collapsing_positive_control"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          2
+        ],
+        "pair_type": "nonorthogonal",
+        "pairwise_nonproportional": [
+          true,
+          false
+        ],
+        "prime": 5,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            8,
+            8
+          ],
+          "merges": 2,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 8,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "collapsing_positive_control"
+      },
+      {
+        "all_terms_active": true,
+        "copy": 72,
+        "factor_ranks": [
+          10,
+          8
+        ],
+        "indices": [
+          0,
+          2
+        ],
+        "pair_type": "nonorthogonal",
+        "pairwise_nonproportional": [
+          true,
+          false
+        ],
+        "prime": 7,
+        "product_entries_checked": 14400,
+        "proportional_normalization": {
+          "copy": 72,
+          "factor_ranks": [
+            8,
+            8
+          ],
+          "merges": 2,
+          "pairwise_nonproportional": [
+            true,
+            true
+          ],
+          "product_entries_checked": 14400,
+          "term_copy_costs": [
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9,
+            9
+          ],
+          "terms": 8,
+          "zero_terms_removed": 0
+        },
+        "term_copy_costs": [
+          1,
+          1,
+          8,
+          8,
+          9,
+          9,
+          9,
+          9,
+          9,
+          9
+        ],
+        "variant": "collapsing_positive_control"
+      }
+    ],
+    "status": "PASS_SPARSE_PAIR_FINITE_CONTROLS"
+  }
+}
diff --git a/research/e8-one-coset-deficiency/SOURCES.json b/research/e8-one-coset-deficiency/SOURCES.json
new file mode 100644
index 0000000000..00274991ed
--- /dev/null
+++ b/research/e8-one-coset-deficiency/SOURCES.json
@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/a8-simplex-decoder-floor/PROOF.md",
+      "usage": "input",
+      "git_blob": "4d1d3bcd8799c833dfbb63ed5319af5fe863fa1a",
+      "sha256": "7e3a5407fc535fd9cc7f25f06aab787b0216f09121e571938cccedb383aab3c4"
+    },
+    {
+      "path": "research/decoder-excess-rank/PROOF.md",
+      "usage": "input",
+      "git_blob": "94f7d1737da52b5f52b0154bd501339bb98a67ef",
+      "sha256": "9ef4ef4fc01eaadef9cfb87839346c34b9c03bcd03031ea99257aa976d81fbd7"
+    },
+    {
+      "path": "research/nine-term-decoder-normal-form-seed42/PROOF.md",
+      "usage": "input",
+      "git_blob": "e510fd180a286445fd6fc484057001bfc60f8c9c",
+      "sha256": "0503e07f1764708e9e72c01be88d3dad1b213e73eb3c23397a603032791fd23a"
+    },
+    {
+      "path": "formal/lean/lean-toolchain",
+      "usage": "input",
+      "git_blob": "980709bbbae28702ec58c368b84fdf6638093c63",
+      "sha256": "d24fed434d3b13adfaab57724a0a7f270ea8bf1c818b5ae5cf25cbce24dd685c"
+    },
+    {
+      "path": "research/one-sided-decoders-all-m/README.md",
+      "usage": "provenance",
+      "git_blob": "614ff7397c3510ca740b09bf8846034fef16fa13",
+      "sha256": "7c22a8d73d8e2cf1ec9ce259035fe97be7261b0f71d5555ee50fc4b821872bf8"
+    },
+    {
+      "path": "research/one-sided-padding-audit/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "986e4b9464a5c2d0ec3455c45cd8e5551c5db43d",
+      "sha256": "5b8ef47091aaf09610b66194d834afa6724f0b8cadcf582a25705bc6933c35b7"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/README.md",
+      "usage": "provenance",
+      "git_blob": "094f060a751f6f866a7340fde31fa05bf72f9343",
+      "sha256": "6d9f14b9f666943919d469e14d579acdda317341a02629e8714be820e1ad2846"
+    },
+    {
+      "path": "research/a7-a1-decoder-floor/README.md",
+      "usage": "provenance",
+      "git_blob": "c6f3649af2bb2d91f10127b89eabb3a3c007f166",
+      "sha256": "b05e08146efb393415aad940a7cb4566fa63a9e37138e06ff8e9ea06e04cd476"
+    }
+  ]
+}
diff --git a/research/e8-one-coset-deficiency/SPARSE-PAIR.md b/research/e8-one-coset-deficiency/SPARSE-PAIR.md
new file mode 100644
index 0000000000..c702ce7e33
--- /dev/null
+++ b/research/e8-one-coset-deficiency/SPARSE-PAIR.md
@@ -0,0 +1,284 @@
+# A sharp COPY floor for two singleton outside directions
+
+Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0.
+This is a written corollary of the uniform theorem; full proof-assistant
+verification is not claimed.
+
+## 1. Statement and inputs
+
+Let K be any field of characteristic different from two. Let L be the 120
+standard E8 root lines with oriented norm-two representatives r_x over
+Z[1/2], and retain their fixed binary labels u_x in Lambda=F2^9. Their
+nondegenerate binary pairing beta gives the dense table B_d. Put
+
+```text
+E(h)=(r_x dot h)_{x in L},       C=E(K^8),
+G[x,y]=r_x dot r_y,             N0=G/2,
+U(p)=span_F2{u_x:p(x)!=0},      Z(p)=U(p)^perp,
+w(p)=dim U(p),                 delta(p)=9-w(p).
+```
+
+For distinct lines a,b let delta_a,delta_b be the coordinate unit vectors,
+and set S=C+span_K(delta_a,delta_b).
+
+**Theorem.** For any finite m, if P,Q in K^{L x m} satisfy
+
+```text
+P Q^t=N0,       col(P) subset S,       col(Q) subset C,
+```
+
+then COPY(P,Q)>=72, where each term costs the binary pairing rank
+rho(supp p_i,supp q_i)=rank_F2 B_d[supp p_i,supp q_i]. The floor is sharp,
+including an actual rank-(10,8), ten-term factorization. The transposed
+statement holds as well. Transposes are ordinary transposes over every K.
+
+The inputs are the uniform deficiency theorem and annihilator argument in
+[PROOF.md](PROOF.md)
+section 5, extended to these fields in section 8. Every nonzero codeword
+has weight nine. For any lambda outside C, a finite nonproportional family
+in C+K lambda has total deficiency at most nine. Moreover, for distinct
+normalized outside vectors p=lambda+E(h), p'=lambda+E(h'), their
+annihilators have trivial intersection and are beta-orthogonal: every
+nonzero cross-pair is compatible, so finite fact 2 applies. The root-hole
+support calculation below also occurs in PROOF.md section 7.1.
+
+## 2. Independence and the singleton classification
+
+The evaluation map E is injective: standard roots include the orthogonal
+frame e_0+e_1,e_0-e_1,...,e_6+e_7,e_6-e_7 of determinant plus or minus 16.
+Distinct standard root lines remain nonproportional over K. Pair roots
+have support two and half-roots have support eight. Within either type,
+comparison at a nonzero coordinate forces proportionality scalar +1 or
+-1; odd characteristic preserves all distinct sign patterns. Thus
+E(r_a),E(r_b) are independent. This avoids a Gram-determinant argument,
+which would fail for nonorthogonal roots in characteristic three.
+
+Write u=u_a, v=u_b. Distinct root lines have distinct nonzero binary labels,
+so u!=v and they are independent over F2. Put D=span_K(delta_a,delta_b).
+A nonzero vector in D
+has binary weight one or two, so D intersect C=0 and dim S=10.
+
+Because E(r_a)_a=r_a dot r_a=2, define the singleton hole
+
+```text
+A=delta_a-E(r_a)/2,        B=delta_b-E(r_b)/2.
+```
+
+The support of A is exactly the nonorthogonal-to-r_a roots with line a
+omitted. Its labels lie in u^perp. Adding u restores the support of the
+nonzero codeword E(r_a), whose label span is Lambda. Hence U(A)=u^perp,
+w(A)=8 and Z(A)=F2 u. This calculation survives every characteristic
+different from two: at line a the product r_a dot r_a is 2 and is exactly
+cancelled; at every other nonorthogonal line the product is +1 or -1 and
+remains nonzero. Similarly
+w(B)=8 and Z(B)=F2 v.
+
+The vectors delta_a and A are nonproportional and have deficiencies eight
+and one. They saturate the uniform budget in C+K delta_a. Therefore they
+are the only positive-deficiency projective rays in that extension.
+Likewise delta_b and B are the only such rays in C+K delta_b.
+
+## 3. Classification in a mixed singleton direction
+
+Fix s,t in K nonzero and lambda=s delta_a+t delta_b. Since D intersect C=0,
+lambda is outside C. Its support has label span W=span_F2(u,v), so
+
+```text
+delta(lambda)=7,       Z(lambda)=W^perp.
+```
+
+Consider any other positive-deficiency ray in C+K lambda. It has a unique
+representative p=lambda+E(h), different from lambda; codewords themselves
+have deficiency zero. The annihilator properties in section 1 imply
+
+```text
+Z(p) subset Z(lambda)^perp=W,       Z(p) intersect W^perp=0. (1)
+```
+
+First suppose the scalar root lines a,b are nonorthogonal. Then
+beta(u,v)=0, while beta(u,u)=beta(v,v)=1. Put
+
+```text
+p_a=lambda-(s/2)E(r_a)=sA+t delta_b,
+p_b=lambda-(t/2)E(r_b)=s delta_a+tB.
+```
+
+The first vector vanishes on O_u={x:beta(u,u_x)=1}: its entry at a cancels,
+all other roots there are orthogonal to r_a, and b is not there. Thus
+u belongs to Z(p_a). Similarly v belongs to Z(p_b). Both deficiencies
+are at least one. These vectors and lambda are nonproportional: their
+quotient coefficients modulo C are all one, and E(r_a),E(r_b) are
+independent. Their deficiencies sum to at least 7+1+1=9. The uniform
+theorem forces both new deficiencies to equal one and excludes every
+other positive-deficiency ray in C+K lambda.
+
+Now suppose the root lines are orthogonal, so beta(u,v)=1. On W the
+pairing matrix is [[1,1],[1,1]], with radical F2(u+v)=W intersect W^perp.
+By (1), a nonzero Z(p) must have dimension one and generator u or v.
+Suppose it is u; the other case is symmetric. The vector
+
+```text
+p'=p-sA=t delta_b+E(h+(s/2)r_a)
+```
+
+still vanishes on O_u. It is nonzero and outside C, because t!=0 and
+delta_b is outside C. It is therefore a positive-deficiency vector in
+C+K delta_b and must be proportional to delta_b or B by section 2.
+But delta_b does not vanish on O_u, since beta(u,v)=1; and B has
+annihilator F2 v, which does not contain u. This contradiction proves
+that lambda itself is the only positive-deficiency ray in this case.
+
+## 4. Filtered spans and the basis bound
+
+Every nonzero p in S is a codeword or lies in one of the quotient
+directions just classified. Consequently
+
+```text
+{p in S:w(p)<=7} subset D,
+{p in S:w(p)<=8} subset H=D+span_K(E(r_a),E(r_b)).
+```
+
+The first set spans D, and the second spans H because it contains
+delta_a,delta_b,A,B. Thus these filtered spans have dimensions two and
+four respectively; dim H=4 follows from D intersect C=0 and the root
+independence proved above. The weight-one vectors also span D.
+
+Any ten-vector basis of S therefore contains at most two vectors of
+weight at most seven and at most four of weight at most eight. Nonzero
+vectors have weight at least one. Its ordered weights are bounded below by
+
+```text
+(1,1,8,8,9,9,9,9,9,9),       sum=72.                    (2)
+```
+
+## 5. Every finite exact factorization and sharpness
+
+Delete terms with a zero factor. Each remaining q_i is a nonzero codeword,
+so U(q_i)=Lambda and its term costs exactly w(p_i). Exactness implies
+C=col(N0) subset col(P): the standard root matrix is injective and its
+transpose is surjective, so N0 has rank eight and image C.
+
+If the remaining P has rank at most nine, the rank-at-most-nine
+floor applies, since Q has rank eight. Otherwise its rank is ten and its
+columns span S. Choose a ten-column basis subset. Its weights sum to at
+least 72 by (2); all other costs are nonnegative. This proves the theorem,
+including rank drops caused by deleting zero-reader columns.
+
+### 5.1 Equality survives proportional normalization
+
+The sheared variant below was suggested and computationally checked in the
+local Claude Fable 5.1 AI-assisted audit; this is not human peer review.
+
+Extend h_1=r_a,h_2=r_b to any basis h_1,...,h_8 of K^8, and let d_1,...,d_8
+be its dot-product dual. Such an extension exists also in characteristic three:
+the two root representatives are independent, as proved in section 2; a
+two-root Gram determinant is not needed. Put
+
+```text
+A=delta_a-E(h_1)/2,       B=delta_b-E(h_2)/2,
+y_3=E(h_3)+delta_a,       y_4=E(h_4)+delta_b,
+
+P=(delta_a,delta_b,A,B,y_3,y_4,E(h_5),...,E(h_8)),
+Q=(E(d_1-d_3/2),E(d_2-d_4/2),-E(d_1),-E(d_2),
+   E(d_3)/2,E(d_4)/2,E(d_5)/2,...,E(d_8)/2).
+```
+
+Every P column lies in S=C+span_K(delta_a,delta_b). The unsheared columns
+delta_a,delta_b,A,B,E(h_3),...,E(h_8) form a basis of S: their span contains
+delta_a,delta_b and E(h_1),...,E(h_8), while dim S=10. Adding delta_a to
+E(h_3), and delta_b to E(h_4), are invertible column operations. Hence the
+displayed P has rank ten, all its columns are nonzero, and they are pairwise
+nonproportional.
+
+The two modified columns still have weight nine. By section 2, the only
+positive-deficiency rays in C+K delta_a are delta_a and A. The normal h_3
+is independent of h_1, so y_3 is proportional to neither: comparison modulo
+C would force the proportionality coefficient to be one, and then would
+force h_3=0 or h_3=-h_1/2, respectively, by injectivity of E. Thus w(y_3)=9.
+The same argument with h_4,h_2 gives w(y_4)=9. The full P weight list is
+therefore
+
+```text
+(1,1,8,8,9,9,9,9,9,9),       sum=72.
+```
+
+For the Q columns, use the dual basis as coordinates. Their normal supports
+are respectively
+
+```text
+{1,3}, {2,4}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}.
+```
+
+Every displayed coefficient is nonzero in characteristic different from two.
+These supports are nonempty and distinct, so these normals are nonzero and
+pairwise nonproportional. Injectivity of E gives the same facts for Q. Its
+last eight normals, -d_1,-d_2,d_3/2,...,d_8/2, form a basis, so rank Q=8.
+Every reader is a nonzero codeword and has binary support weight nine.
+Consequently the actual binary pairing rank of each term equals the weight
+of its P column, and COPY=72.
+
+Exactness follows directly by grouping terms:
+
+```text
+PQ^t
+ = (delta_a-A)E(d_1)^t + (delta_b-B)E(d_2)^t
+   + (y_3-delta_a)E(d_3)^t/2
+   + (y_4-delta_b)E(d_4)^t/2
+   + sum_{j=5}^8 E(h_j)E(d_j)^t/2
+ = sum_{j=1}^8 E(h_j)E(d_j)^t/2 = G/2 = N0.
+```
+
+Neither zero-term deletion nor proportional-factor merging on either side
+can change this factorization: all ten terms are active and both factor
+families are pairwise nonproportional. Thus the rank-(10,8) equality example
+already survives that normalization. These statements use no characteristic
+restrictions beyond 2 being invertible and apply to both orthogonal and
+nonorthogonal a,b.
+
+The unsheared fixture retained in `sparse_pair.py` is a useful positive control:
+remove the added units from y_3,y_4 and restore the first readers E(d_1),E(d_2).
+Its two pairs of proportional readers merge to eight code-code terms of ranks
+(8,8), with COPY still 72. The finite verifier retains those six controls
+and adds the sheared construction for both pair types over F3, F5, F7. Each
+new fixture checks all 14,400 product entries, actual binary term ranks,
+scalar factor ranks, active terms, both families' proportionality, and the
+result of an independent proportional normalizer. Omitting the compensating
+changes to the first two readers is explicitly rejected by the product check:
+its product error is
+
+```text
+(delta_a E(d_3)^t + delta_b E(d_4)^t)/2 != 0.
+```
+
+The two nonzero rows lie at distinct coordinates a,b, so the error cannot
+cancel in any permitted characteristic. The finite fixtures do not exhaust
+F5 or F7 or all root pairs; the argument above supplies the universal claim.
+
+The theorem concerns the specific space C+span(delta_a,delta_b) and exact
+N0 on full E8, with fixed B_d. It makes no assertion for arbitrary two
+outside directions, all rank-ten factors, masked identities, punctures,
+or a physical multiplication construction.
+
+## 6. Relation to earlier singleton and root-swap work
+
+DreamingOfClouds's [PR2816](https://github.com/CrocSwap/integer-mult-bounds/pull/2816),
+`research/one-sided-decoders-all-m/README.md` sections 5.2, 6 and 9, already
+analyzes singleton root swaps and `T=span(delta_t,delta_u)` in the P112
+characteristic-zero, low-excess correction programme. Those geometric
+observations are antecedents, not discoveries claimed here. The floor of 68 in PR2862 is a historical
+full-E8 lift baseline, rather than the current status of the one-sided programme. The present statement is full E8, all finite
+term counts and every characteristic different from two, in the explicitly
+restricted coordinate-pair extension. Its proof uses the uniform theorem
+directly, without importing their correction, minimum-basis or survivor-list
+hypotheses. These results do not supply a general one-sided rank-ten floor.
+
+The relevant broader programme is **L120**, the basis-cost bound for every
+scalar space containing C. PR3074 states its sufficiency for the one-sided
+problem, and PR3154 separates that B-prime node from the two-sided C-prime
+node. Draft PR3191 claims completion of its one-sided ledger conditional on
+an implementation slot that remains unfilled at head `9c9e094`; conorholds'
+PR3166 supplies its C7 branch. In characteristic zero a completed L120 proof
+would imply the present sparse-pair corollary. Here this dimension-ten case
+is proved directly, in every characteristic different from two, without that
+conditional chain. The main new theorem of the package is the arbitrary-family
+one-coset budget; its genuinely two-sided application is the rank-(9,9) cell.
diff --git a/research/e8-one-coset-deficiency/TASK.json b/research/e8-one-coset-deficiency/TASK.json
new file mode 100644
index 0000000000..12aae298e1
--- /dev/null
+++ b/research/e8-one-coset-deficiency/TASK.json
@@ -0,0 +1,79 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Uniform deficiency at most nine for arbitrary finite nonproportional families in one outside-code extension of full E8; sharp COPY at least 72 for exact N0 factorizations with both actual factor ranks at most nine, all finite term counts and scalar fields of characteristic different from two. Also proves the sharp one-sided singleton-pair extension floor: Q in C, P in C+span(delta_a,delta_b), any finite exact factorization over the same fields, including rank-(10,8).",
+  "scope_change_reason": "The handoff-first scout identified PR3154 ARCHITECT node C-prime and its request for an m-free deficiency budget. The arbitrary-family theorem closes the two-sided (1,1) exact-P120 cell for all term counts. The one-sided dimension-nine and sparse dimension-ten results are scoped cases of B-prime/L120; they are proved directly rather than assuming the characteristic-zero conditional programme of PR3074/PR3191. No supplier profile is proposed.",
+  "bottleneck_link": "The uniform family theorem eliminates the first unrestricted two-sided ten-term P120 exact-decoder branch, and extends to arbitrary term counts while both ranks stay at most nine. One-sided consequences are L120 subcases, not a new claim to complete that programme. Higher outside ranks and changed physical decoder mechanisms remain available; no selected exponent changes.",
+  "budget_minutes": 120,
+  "stop_rule": "Complete the universal written proof and normalization, independently reconstruct every finite geometric input, retain sharp actual-factor controls, and audit source/export bytes. Pivot on a counterexample or a matching completion found in refreshed overlap.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; CERTIFICATE.json with 109 power-of-two integer minors and eight integral reflection generators; independent.py full 511-character and 130305-pair replay plus four complete 6561-member F3 cosets; fixtures.py eight rational exact factorizations, normalized rank-(9,9) ten-term cost72, normalization exits and necessary equality rigidity, plus 24 controls over F3/F5/F7; controls.py integrity and necessary-hypothesis controls; six Init-only Lean declarations; RESULT.json binds exact package bytes. SPARSE-PAIR.md derives the singleton-pair result directly from the uniform theorem; sparse_pair.py separately exhausts both F3 spaces and checks planted higher-field ray classifications. Audit fixes credit the L120 programme, CubeJerry PR3095, adamgall PR2062, the PR1248 method, conorholds PR3166 and philippeVV lift-family antecedents. Six additional sheared sparse-pair fixtures over F3/F5/F7 remain rank-(10,8), cost72 after zero proportional merges; uncompensated-reader mutations fail exactness. The six original collapsing fixtures remain positive controls.",
+  "author": "conorholds",
+  "ai_assistance": "Substantial OpenAI Codex assistance, including GPT-6.1 SOL agents at xHigh for proof, independent geometry and formal-core work. Internal AI review is not independent human certification.",
+  "open_questions": [
+    {
+      "question": "Can the exact P120 floor be extended to a factor with two outside-code directions?",
+      "why_it_matters": "Any cheaper exact decoder must leave the rank-at-most-nine class; a two-sided one needs at least eleven terms.",
+      "first_step": "Study the actual coupled rank-(10,9), eleven-term identity. The six-ray two-direction counterexample in fixtures.py shows that the present uniform family budget cannot simply be multiplied by two.",
+      "blocked_by": "No multi-direction replacement for the one-coset annihilator direct-sum property is established."
+    },
+    {
+      "question": "Can the full E8 instantiation and factorization assembly be checked in a proof assistant?",
+      "why_it_matters": "The written proof and exact replays do not constitute a formal proof of the complete theorem.",
+      "first_step": "Instantiate the checked abstract binary clique core, then connect certified root spans, annihilators and the COPY/Sylvester consumer in a pinned environment.",
+      "blocked_by": "The scalar/binary geometric bridge and dimension/consumer assembly remain unformalized; broad Mathlib imports exceeded the local conservative memory watchdog."
+    }
+  ],
+  "coordination": "Read-only refresh on 2026-10-18 at 19:29 UTC: main 20ecf289 unchanged; 27 PR updates since 18:40 through PR3747 and fully paginated Discussion1166, plus 1587/3156. No inspected matching completion. PR3701 (petalas) uses the same original card on a different local-word rank question. PR3191 is an open draft at 9c9e094d0fb665db8a3aaa4f9bce1c95c0c6e14b with SLOT-C6-IMPL-C unfilled; PR3154 remains open at 708f0ad8928c383de8294aea3c126e9461d2066d. No public claim or post was made under donor restrictions."
+}
diff --git a/research/e8-one-coset-deficiency/VERIFY.json b/research/e8-one-coset-deficiency/VERIFY.json
new file mode 100644
index 0000000000..51f89a42e2
--- /dev/null
+++ b/research/e8-one-coset-deficiency/VERIFY.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "formal/lean/lean-toolchain",
+    "research/a8-simplex-decoder-floor/PROOF.md",
+    "research/decoder-excess-rank/PROOF.md",
+    "research/nine-term-decoder-normal-form-seed42/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact canonical model, complete 109-minor certificate, separate full E8 reconstruction, actual sharp factorizations, normalization and semantic/integrity controls; read-only receipt comparison. Includes independent sparse-pair ray classifications and filtered-span basis evidence. Includes six sheared normalized rank-(10,8) equality fixtures, six collapsing controls and reader-compensation mutation rejection."
+    }
+  ]
+}
diff --git a/research/e8-one-coset-deficiency/controls.py b/research/e8-one-coset-deficiency/controls.py
new file mode 100644
index 0000000000..d9b7e35de8
--- /dev/null
+++ b/research/e8-one-coset-deficiency/controls.py
@@ -0,0 +1,119 @@
+"""Certificate integrity and necessary-hypothesis controls.
+
+Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0.
+Controls are classified separately from factorization mutations in fixtures.py.
+"""
+
+from copy import deepcopy
+from functools import reduce
+from itertools import combinations
+from operator import xor
+
+
+def run(g, model, certificate):
+    g.check_certificate(model, certificate)
+    # The two ranks in the theorem belong to different fields. This standard
+    # three-vector example separates them, as well as testing zero/full rank.
+    g.require(g.binary_rank([0, 0]) == 0
+              and g.binary_rank([1 << i for i in range(9)]) == 9
+              and g.binary_rank([3, 5, 6]) == 2, "binary rank field controls")
+    g.require(g.rational_rank([[1, 1, 0], [1, 0, 1], [0, 1, 1]]) == 3,
+              "scalar rank field control")
+    cases = []
+
+    def case(name, change, expected):
+        value = deepcopy(certificate)
+        change(value)
+        cases.append((name, value, expected))
+
+    case("missing_single", lambda d: d["single_types"].pop(), "single inventory count")
+    case("missing_forbidden_profile", lambda d: d["forbidden_pairs"].pop(), "forbidden inventory count")
+    case("duplicate_single", lambda d: d["single_types"].__setitem__(1, deepcopy(d["single_types"][0])),
+         "duplicate single type")
+    case("duplicate_profile", lambda d: d["forbidden_pairs"].__setitem__(1, deepcopy(d["forbidden_pairs"][0])),
+         "unknown/duplicate forbidden profile")
+
+    def wrong_binding(data):
+        counts = data["forbidden_pairs"][1]["counts"]
+        data["forbidden_pairs"][1] = deepcopy(data["forbidden_pairs"][0])
+        data["forbidden_pairs"][1]["counts"] = counts
+
+    case("valid_minor_bound_to_wrong_profile", wrong_binding, "normal/profile binding")
+    case("duplicate_minor_row", lambda d: d["single_types"][0]["rows"].__setitem__(
+        -1, d["single_types"][0]["rows"][0]), "minor root indices")
+    case("negative_root_index", lambda d: d["single_types"][0]["rows"].__setitem__(0, -1),
+         "minor root indices")
+    case("incorrect_determinant", lambda d: d["single_types"][0].__setitem__(
+        "determinant", d["single_types"][0]["determinant"] + 1), "integer minor determinant")
+    case("boolean_determinant", lambda d: d["single_types"][0].__setitem__("determinant", True),
+         "minor determinant type/value")
+    case("boolean_normal", lambda d: d["single_types"][0].__setitem__("normal", True),
+         "single normal binding")
+    case("float_profile_count", lambda d: d["forbidden_pairs"][0]["counts"].__setitem__(
+        0, float(d["forbidden_pairs"][0]["counts"][0])), "profile counts")
+    outside = next(i for i, label in enumerate(model["labels"]) if not g.parity(label & 1))
+    case("witness_outside_character", lambda d: d["single_types"][0]["rows"].__setitem__(0, outside),
+         "witness support membership")
+
+    # A full-rank minor can still fail in odd characteristic. These eight
+    # valid star rows have determinant +/-768, so specifically exercise the
+    # unit gate after the membership and exact determinant checks pass.
+    star_indices = [7, 14, 20, 25, 29, 32, 34, 35]
+    scalar_rows = g.standard_binding(model)
+    star_determinant = g.determinant([scalar_rows[i] for i in star_indices])
+    g.require(abs(star_determinant) == 768, "nonunit full-rank control")
+
+    def nonunit(data):
+        data["single_types"][7]["rows"] = star_indices
+        data["single_types"][7]["determinant"] = star_determinant
+
+    case("full_rank_minor_not_unit_over_Z_half", nonunit, "minor is not a unit over Z[1/2]")
+
+    # Eight distinct valid single-character rows whose shared second character
+    # forces rank seven: this must reach the determinant gate, not a shape gate.
+    dependent = [i for i, label in enumerate(model["labels"])
+                 if g.parity(label & 1) and g.parity(label & 2)][:8]
+    g.require(len(dependent) == 8 and g.determinant([scalar_rows[i] for i in dependent]) == 0,
+              "singular distinct-row control is not singular")
+
+    def singular(data):
+        data["single_types"][0]["rows"] = dependent
+        data["single_types"][0]["determinant"] = 1
+
+    case("distinct_valid_rows_with_singular_minor", singular, "integer minor determinant")
+    rejected = {}
+    for name, value, expected in cases:
+        try:
+            g.check_certificate(model, value)
+        except ValueError as error:
+            g.require(expected in str(error), "control failed at wrong gate: " + name)
+            rejected[name] = expected
+        else:
+            raise ValueError("accepted corrupted certificate: " + name)
+
+    alternate = deepcopy(certificate)
+    witness = alternate["single_types"][0]
+    witness["rows"][0], witness["rows"][1] = witness["rows"][1], witness["rows"][0]
+    witness["determinant"] = -witness["determinant"]
+    g.check_certificate(model, alternate)
+
+    def intersection_rank(a, b):
+        return g.rational_rank([row for row, label in zip(model["roots"], model["labels"])
+                                if g.parity(label & a) and g.parity(label & b)])
+
+    # Omitting either binary condition admits a dependent fake clique. At
+    # least one of its edges has actual scalar intersection rank eight.
+    even = [3, 12, 15]
+    odd = [1, 2, 4, 7]
+    g.require(reduce(xor, even, 0) == reduce(xor, odd, 0) == 0, "dependent clique controls")
+    g.require(all(not g.parity(a & b) for a, b in combinations(even, 2)), "even weakened clique")
+    g.require(all(g.parity(a) for a in odd), "odd weakened clique")
+    even_rank = intersection_rank(3, 12)
+    odd_rank = intersection_rank(1, 7)
+    g.require(even_rank == odd_rank == 8, "weakened binary edge rules escaped geometry")
+    return {"certificate_corruptions_rejected": rejected,
+            "binary_vs_scalar_rank_control": {"binary": 2, "rational": 3},
+            "alternative_valid_minor_accepted": True,
+            "weakened_edge_rule_counterexamples": {
+                "omit_even_colour": {"normals": even, "xor": 0, "forbidden_pair_rank": even_rank},
+                "omit_orthogonality": {"normals": odd, "xor": 0, "forbidden_pair_rank": odd_rank}}}
diff --git a/research/e8-one-coset-deficiency/fixtures.py b/research/e8-one-coset-deficiency/fixtures.py
new file mode 100644
index 0000000000..b506577db2
--- /dev/null
+++ b/research/e8-one-coset-deficiency/fixtures.py
@@ -0,0 +1,323 @@
+"""Exact factorization, normalization and sharp-family controls.
+
+Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0.
+These finite controls exercise the universal written argument; they do not
+enumerate arbitrary characteristic-zero coefficient choices.
+"""
+
+from fractions import Fraction as F
+
+
+def add(left, right, scale=1):
+    return tuple(x + scale * y for x, y in zip(left, right))
+
+
+def multiple(left, right):
+    """Return c for left=c*right, or None, for two nonzero factors."""
+    index = next(i for i, x in enumerate(right) if x)
+    value = F(left[index]) / right[index]
+    return value if all(x == value * y for x, y in zip(left, right)) else None
+
+
+def cost(g, model, terms):
+    return sum(g.copy_rank(model, p, q) for p, q in terms)
+
+
+def ranks(g, terms):
+    if not terms:
+        return [0, 0]
+    return [g.rational_rank([list(row) for row in zip(*(term[side] for term in terms))])
+            for side in (0, 1)]
+
+
+def exact(g, model, terms):
+    for i, root in enumerate(model["roots"]):
+        for j, other in enumerate(model["roots"]):
+            value = sum(p[i] * q[j] for p, q in terms)
+            g.require(value == F(g.dot(root, other), 18), "exact N0 factorization fails")
+
+
+def normalized(terms):
+    if any(not any(p) or not any(q) for p, q in terms):
+        return False
+    for side in (0, 1):
+        for i in range(len(terms)):
+            for j in range(i):
+                if multiple(terms[i][side], terms[j][side]) is not None:
+                    return False
+    return True
+
+
+def normalize(g, model, terms):
+    """Literal alternating proportional merges; cost-zero nonzero terms stay."""
+    terms = list(terms)
+    costs = [cost(g, model, terms)]
+    while True:
+        live = [(p, q) for p, q in terms if any(p) and any(q)]
+        if len(live) != len(terms):
+            terms = live
+            costs.append(cost(g, model, terms))
+        merged = False
+        for side in (0, 1):
+            for i in range(len(terms)):
+                for j in range(i):
+                    value = multiple(terms[i][side], terms[j][side])
+                    if value is None:
+                        continue
+                    p, q = terms[j]
+                    if side == 0:
+                        new = (p, add(q, terms[i][1], value))
+                    else:
+                        new = (add(p, terms[i][0], value), q)
+                    terms = [term for k, term in enumerate(terms) if k not in (i, j)] + [new]
+                    costs.append(cost(g, model, terms))
+                    merged = True
+                    break
+                if merged:
+                    break
+            if merged:
+                break
+        if not merged:
+            g.require(normalized(terms), "normalizer did not terminate in normal form")
+            g.require(all(a >= b for a, b in zip(costs, costs[1:])), "merge increased COPY cost")
+            return terms, costs
+
+
+def make_decoders(g, model):
+    roots = tuple(tuple(F(x, 2) for x in row) for row in g.standard_binding(model))
+
+    def code(normal):
+        return tuple(g.dot(root, normal) for root in roots)
+
+    def unit(index, value=1):
+        return tuple(F(value) if i == index else F(0) for i in range(120))
+
+    frame = []
+    for a in range(0, 8, 2):
+        for sign in (1, -1):
+            vector = [0] * 8
+            vector[a], vector[a + 1] = 1, sign
+            column = tuple(x / 2 for x in code(vector))
+            frame.append((column, column))
+
+    # A code basis with first normal v and remaining normals in w-perp.
+    # Its first dual normal is w because v.w=1. This permits an exact,
+    # normalized two-sided cost72 control after adding a column correction.
+    v = (1, 1, 0, 0, 0, 0, 0, 0)
+    w = (1, 0, 1, 0, 0, 0, 0, 0)
+    h = [v, (0, 1, 0, 0, 0, 0, 0, 0), (1, 0, -1, 0, 0, 0, 0, 0)]
+    dual = [w, (-1, 1, -1, 0, 0, 0, 0, 0), (0, 0, -1, 0, 0, 0, 0, 0)]
+    for i in range(3, 8):
+        axis = tuple(int(j == i) for j in range(8))
+        h.append(axis)
+        dual.append(axis)
+    g.require(all(g.dot(a, b) == int(i == j)
+                  for i, a in enumerate(h) for j, b in enumerate(dual)), "dual basis fixture")
+    vi = next(i for i, root in enumerate(roots) if root == v or root == tuple(-x for x in v))
+    wi = next(i for i, root in enumerate(roots) if root == w or root == tuple(-x for x in w))
+    lam = unit(vi, code(v)[vi])
+    p = [lam] + [add(lam, code(normal), -1) for normal in h]
+    q = [tuple(-x / 2 for x in code(normal)) for normal in dual]
+    q = [tuple(-sum(column[i] for column in q) for i in range(120))] + q
+    one_sided = list(zip(p, q))
+
+    # Add the exact N0 column and subtract the corresponding unit column
+    # from every existing reader. Product preservation is checked entrywise.
+    mu = unit(wi)
+    column = tuple(g.dot(root, roots[wi]) / 2 for root in roots)
+    two_sided = [(a, add(b, mu, -b[wi])) for a, b in one_sided] + [(column, mu)]
+
+    # Split a genuinely nonzero cost-zero atom out of the root-swap term.
+    # It must survive until a proportional merge restores the one-sided leaf.
+    free = unit(vi, q[1][vi])
+    g.require(any(free) and g.copy_rank(model, p[1], free) == 0, "free-atom fixture")
+    split = [(a, b) for i, (a, b) in enumerate(one_sided) if i != 1]
+    split += [(p[1], add(q[1], free, -1)),
+              (tuple(2 * x for x in p[1]), tuple(x / 2 for x in free))]
+    zero = tuple(F(0) for _ in range(120))
+    return {
+        "inside": frame,
+        "row_extension": one_sided,
+        "column_extension": [(b, a) for a, b in one_sided],
+        "two_extensions": two_sided,
+        "free_atom_split": split,
+        "free_atom_split_transposed": [(b, a) for a, b in split],
+        "zero_factor": frame + [(unit(vi), zero)],
+        "canceling_free_atoms": frame + [(unit(vi), unit(wi)),
+                                          (unit(vi, -1), unit(wi))],
+    }
+
+
+def family_controls(g, model):
+    lam = tuple(0 if i < 36 else -2 for i in range(120))
+    nine = [tuple(lam[i] + row[j] for i, row in enumerate(model["roots"])) for j in range(9)]
+    first = model["roots"][0]
+    small = tuple(18 if i == 0 else 0 for i in range(120))
+    other = tuple(small[i] - g.dot(row, first) for i, row in enumerate(model["roots"]))
+    weights = [g.support_weight(model, column) for column in nine]
+    pair = [g.support_weight(model, column) for column in (small, other)]
+    g.require(weights == [8] * 9 and pair == [1, 8], "sharp family weights")
+    g.require(g.rational_rank([list(row) for row in zip(*nine)]) == 9, "sharp family scalar rank")
+    # Two outside directions permit an unbounded number of low-weight rays.
+    # This is a failure control for the tempting unrestricted extension.
+    many = [tuple(1 if i == 0 else t if i == 1 else 0 for i in range(120))
+            for t in range(1, 7)]
+    deficits = sum(9 - g.support_weight(model, column) for column in many)
+    g.require(deficits == 42 and deficits > 18, "two-direction scope control")
+    repeated = sum(9 - g.support_weight(model, small) for _ in range(6))
+    g.require(repeated == 48, "proportional-family hypothesis control")
+    return {"nine_weight_eight_vectors": weights, "nine_family_scalar_rank": 9,
+            "annihilator_dimensions_eight_and_one": [9 - x for x in pair],
+            "sharp_total_deficiency": 9,
+            "two_outside_direction_counterexample": {"vectors": 6, "total_deficiency": deficits},
+            "proportional_family_counterexample": {"copies": 6, "total_deficiency": repeated}}
+
+
+def rank_mod(rows, prime):
+    work = [[x % prime for x in row] for row in rows]
+    rank = 0
+    for column in range(len(work[0])):
+        pivot = next((i for i in range(rank, len(work)) if work[i][column]), None)
+        if pivot is None:
+            continue
+        work[rank], work[pivot] = work[pivot], work[rank]
+        inverse = pow(work[rank][column], -1, prime)
+        for i in range(rank + 1, len(work)):
+            factor = work[i][column] * inverse % prime
+            for j in range(column, len(work[0])):
+                work[i][j] = (work[i][j] - factor * work[rank][j]) % prime
+        rank += 1
+        if rank == len(work):
+            break
+    return rank
+
+
+def equality_conditions(g, model, terms, excesses):
+    """Necessary rigidity of sharp normalized decoders, not a classification."""
+    sides = []
+    for side, excess in enumerate(excesses):
+        spaces = []
+        for term in terms:
+            labels = [label for label, value in zip(model["labels"], term[side]) if value]
+            basis = []
+            for z in range(1, 512):
+                if all(not g.parity(z & label) for label in labels):
+                    if g.binary_rank(basis + [z]) > len(basis):
+                        basis.append(z)
+            g.require(len(basis) == 9 - g.support_weight(model, term[side]), "annihilator dimension")
+            if excess:
+                gram = [sum(g.parity(a & b) << j for j, b in enumerate(basis)) for a in basis]
+                g.require(g.binary_rank(gram) == len(basis), "equality annihilator is degenerate")
+            spaces.append(basis)
+        g.require(sum(map(len, spaces)) == 9 * excess, "unsaturated equality budget")
+        for i, left in enumerate(spaces):
+            for right in spaces[i + 1:]:
+                g.require(all(not g.parity(a & b) for a in left for b in right),
+                          "same-side annihilators are not orthogonal")
+        all_normals = [z for basis in spaces for z in basis]
+        g.require(g.binary_rank(all_normals) == 9 * excess, "equality annihilator sum is not direct")
+        sides.append(spaces)
+    g.require(len(terms) == 8 + sum(excesses), "equality normalized term count")
+    for p_space, q_space in zip(*sides):
+        g.require(all(not g.parity(a & b) for a in p_space for b in q_space),
+                  "matched equality annihilators are not orthogonal")
+    return {"normalized_term_count_tight": True,
+            "annihilator_dimensions": [[len(space) for space in side] for side in sides],
+            "same_side_orthogonal_direct_sums": True,
+            "nonzero_excess_summands_nondegenerate": True,
+            "matched_cross_side_orthogonality": True}
+
+
+def finite_field_controls(g, model, decoders):
+    """Small actual field controls; the all-odd-field proof uses unit minors."""
+    standard = g.standard_binding(model)
+    results = {}
+    for prime in (3, 5, 7):
+        def convert(value):
+            value = F(value)
+            return value.numerator * pow(value.denominator, -1, prime) % prime
+
+        target = [[g.dot(a, b) * pow(8, -1, prime) % prime for b in standard] for a in standard]
+        g.require(rank_mod(target, prime) == 8, "odd-field Gram rank")
+        cases = {}
+        for name, original in decoders.items():
+            terms = [(tuple(convert(x) for x in p), tuple(convert(x) for x in q)) for p, q in original]
+            for i in range(120):
+                for j in range(120):
+                    g.require(sum(p[i] * q[j] for p, q in terms) % prime == target[i][j],
+                              "finite-field exact factorization")
+            scalar_ranks = [rank_mod([list(row) for row in zip(*(term[side] for term in terms))], prime)
+                            for side in (0, 1)]
+            g.require(scalar_ranks == ranks(g, original), "finite-field factor ranks")
+            value = cost(g, model, terms)
+            g.require(value == 72, "finite-field sharp COPY cost")
+            if name == "two_extensions":
+                for side in (0, 1):
+                    columns = [term[side] for term in terms]
+                    for i in range(len(columns)):
+                        g.require(any(columns[i]), "finite-field zero normalized factor")
+                        for j in range(i):
+                            k = next(k for k, x in enumerate(columns[j]) if x)
+                            ratio = columns[i][k] * pow(columns[j][k], -1, prime) % prime
+                            g.require(any((x - ratio * y) % prime for x, y in zip(columns[i], columns[j])),
+                                      "finite-field proportional normalized factors")
+            cases[name] = {"ranks": scalar_ranks, "copy_cost": value}
+        results[str(prime)] = {"target_rank": 8, "exact_factorizations": cases}
+    # At characteristic five R^T R=30I vanishes. The rank-eight product
+    # argument must use injectivity/surjectivity rather than invert that matrix.
+    g.require(all(sum(row[i] * row[j] for row in standard) % 5 == 0
+                  for i in range(8) for j in range(8)), "characteristic-five degeneracy control")
+    return {"primes": results, "char5_R_transpose_R_zero_but_Gram_rank_eight": True}
+
+
+def run(g, model):
+    decoders = make_decoders(g, model)
+    expected = {"inside": (8, [8, 8]), "row_extension": (9, [9, 8]),
+                "column_extension": (9, [8, 9]), "two_extensions": (10, [9, 9]),
+                "free_atom_split": (10, [9, 9]),
+                "free_atom_split_transposed": (10, [9, 9]), "zero_factor": (9, [9, 8]),
+                "canceling_free_atoms": (10, [9, 9])}
+    results = {}
+    for name, terms in decoders.items():
+        exact(g, model, terms)
+        scalar_ranks = ranks(g, terms)
+        g.require((len(terms), scalar_ranks) == expected[name], "fixture scalar ranks: " + name)
+        value = cost(g, model, terms)
+        g.require(value == 72, "sharp exact decoder cost: " + name)
+        clean, trace = normalize(g, model, terms)
+        exact(g, model, clean)
+        final_ranks = ranks(g, clean)
+        s, t = final_ranks[0] - 8, final_ranks[1] - 8
+        g.require(s in (0, 1) and t in (0, 1), "normalization rank admission")
+        g.require(len(clean) >= 8 + s + t, "Sylvester fixture bound")
+        row_def = sum(9 - g.support_weight(model, p) for p, _ in clean)
+        col_def = sum(9 - g.support_weight(model, q) for _, q in clean)
+        g.require(row_def <= 9 * s and col_def <= 9 * t, "family budget on actual decoder")
+        g.require(all(g.copy_rank(model, p, q) >=
+                      g.support_weight(model, p) + g.support_weight(model, q) - 9 for p, q in clean),
+                  "binary pairing rank inequality")
+        if name in ("inside", "row_extension", "column_extension", "two_extensions"):
+            g.require(normalized(terms), "advertised normalized fixture")
+        results[name] = {"terms": len(terms), "ranks": scalar_ranks, "copy_cost": value,
+                         "normalized_terms": len(clean), "normalized_ranks": final_ranks,
+                         "normalized_deficiencies": [row_def, col_def], "merge_cost_trace": trace,
+                         "equality_conditions": equality_conditions(g, model, clean, (s, t))}
+
+    # Semantic failures change actual factor matrices, not test bookkeeping.
+    baseline = decoders["two_extensions"]
+    mutations = {"omit_term": baseline[:-1],
+                 "wrong_N0_scale": [(add(p, p), q) for p, q in baseline],
+                 "one_factor_sign": [(tuple(-x for x in p) if i == 1 else p, q)
+                                     for i, (p, q) in enumerate(baseline)],
+                 "drop_nonzero_cost_zero_atom": decoders["free_atom_split"][:-1]}
+    rejected = []
+    for name, terms in mutations.items():
+        try:
+            exact(g, model, terms)
+        except ValueError:
+            rejected.append(name)
+        else:
+            raise ValueError("accepted changed factorization: " + name)
+    return {"exact_factorizations": results, "semantic_mutations_rejected": rejected,
+            "sharp_families": family_controls(g, model),
+            "odd_characteristic_actual_controls": finite_field_controls(g, model, decoders)}
diff --git a/research/e8-one-coset-deficiency/formal/BinaryCliqueCore.lean b/research/e8-one-coset-deficiency/formal/BinaryCliqueCore.lean
new file mode 100644
index 0000000000..b740594151
--- /dev/null
+++ b/research/e8-one-coset-deficiency/formal/BinaryCliqueCore.lean
@@ -0,0 +1,289 @@
+/-
+Copyright (c) 2026 conorholds. All rights reserved.
+Released under Apache 2.0 license as described in the repository LICENSE.
+Prepared with substantial OpenAI Codex assistance.
+-/
+import Init
+
+/-!
+# Binary compatibility cliques have no nonempty zero relation
+
+An Init-only proof of the abstract binary clique argument. The operations and
+their algebraic laws are explicit parameters, not axioms or imported E8 facts.
+No equivalence with Mathlib.LinearIndependent or E8 instantiation is claimed.
+-/
+
+namespace OneCosetDeficiency
+
+universe u
+
+variable {V : Type u}
+
+private theorem bool_three_colors_impossible (a b c : Bool)
+    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : False := by
+  cases a <;> cases b <;> cases c <;>
+    first | exact hab rfl | exact hac rfl | exact hbc rfl
+
+/-- A finite binary relation, with the empty sum explicitly specified. -/
+def binarySum (zero : V) (add : V → V → V) : List V → V
+  | [] => zero
+  | x :: xs => add x (binarySum zero add xs)
+
+/-- A linear Boolean-valued detector vanishes on a sum of vectors which it
+annihilates individually. -/
+theorem detector_sum_zero (zero : V) (add : V → V → V)
+    (β : V → V → Bool)
+    (hzero : ∀ x, β x zero = false)
+    (hadd : ∀ x y z, β x (add y z) = Bool.xor (β x y) (β x z))
+    (x : V) (xs : List V) :
+    (∀ y ∈ xs, β x y = false) → β x (binarySum zero add xs) = false := by
+  induction xs with
+  | nil =>
+      intro _
+      exact hzero x
+  | cons y ys ih =>
+      intro h
+      rw [binarySum, hadd, h y List.mem_cons_self,
+        ih (fun z hz => h z (List.mem_cons_of_mem y hz))]
+      rfl
+
+/-- In a distinct finite family, a detector which is one on a selected vector
+and zero on the other vectors evaluates to one on the whole sum. -/
+theorem detector_sum_selected (zero : V) (add : V → V → V)
+    (β : V → V → Bool)
+    (hzero : ∀ x, β x zero = false)
+    (hadd : ∀ x y z, β x (add y z) = Bool.xor (β x y) (β x z))
+    (x : V) (xs : List V) :
+    xs.Nodup → x ∈ xs → β x x = true →
+    (∀ y ∈ xs, y ≠ x → β x y = false) →
+    β x (binarySum zero add xs) = true := by
+  classical
+  induction xs with
+  | nil =>
+      intro _ hx
+      cases hx
+  | cons y ys ih =>
+      intro hnd hx hdiag hoff
+      have htail := List.nodup_cons.mp hnd
+      by_cases hxy : x = y
+      · subst y
+        have hsumtail : β x (binarySum zero add ys) = false := by
+          apply detector_sum_zero zero add β hzero hadd x ys
+          intro z hz
+          apply hoff z (List.mem_cons_of_mem x hz)
+          intro hzx
+          exact htail.1 (hzx ▸ hz)
+        rw [binarySum, hadd, hdiag, hsumtail]
+        rfl
+      · have hxtail : x ∈ ys := (List.mem_cons.mp hx).resolve_left hxy
+        have hih := ih htail.2 hxtail hdiag
+          (fun z hz hzx => hoff z (List.mem_cons_of_mem y hz) hzx)
+        rw [binarySum, hadd,
+          hoff y List.mem_cons_self (fun hyx => hxy hyx.symm), hih]
+        rfl
+
+/-- Abstract binary clique independence, stated as absence of a nonempty
+distinct zero-sum list. Pairing additivity kills any odd member of a relation.
+Pairwise distinct Boolean colors then allow at most two remaining even members;
+nonzero singleton and characteristic-two cancellation exclude those cases.
+
+`hcancel` is the characteristic-two law `x + y = 0 ↔ x = y`. All required
+algebraic and compatibility facts are premises. -/
+theorem compatible_clique_zero_sum_empty
+    (zero : V) (add : V → V → V) (β : V → V → Bool) (color : V → Bool)
+    (haddzero : ∀ x, add x zero = x)
+    (hcancel : ∀ x y, add x y = zero ↔ x = y)
+    (hβzero : ∀ x, β x zero = false)
+    (hβadd : ∀ x y z, β x (add y z) = Bool.xor (β x y) (β x z))
+    (xs : List V) (hnodup : xs.Nodup)
+    (hnonzero : ∀ x ∈ xs, x ≠ zero)
+    (horth : ∀ x ∈ xs, ∀ y ∈ xs, x ≠ y → β x y = false)
+    (hcolor : ∀ x ∈ xs, ∀ y ∈ xs, x ≠ y →
+      β x x = false → β y y = false → color x ≠ color y)
+    (hsum : binarySum zero add xs = zero) : xs = [] := by
+  have heven : ∀ x ∈ xs, β x x = false := by
+    intro x hx
+    cases hdiag : β x x with
+    | false => rfl
+    | true =>
+        have hdet := detector_sum_selected zero add β hβzero hβadd x xs
+          hnodup hx hdiag
+            (fun y hy hyx => horth x hx y hy (fun hxy => hyx hxy.symm))
+        rw [hsum, hβzero] at hdet
+        cases hdet
+  cases xs with
+  | nil => rfl
+  | cons x rest =>
+      cases rest with
+      | nil =>
+          have hxzero : x = zero := by
+            simpa only [binarySum, haddzero] using hsum
+          exact False.elim (hnonzero x List.mem_cons_self hxzero)
+      | cons y rest =>
+          cases rest with
+          | nil =>
+              have hxy : x = y := (hcancel x y).mp (by
+                simpa only [binarySum, haddzero] using hsum)
+              have hnot := (List.nodup_cons.mp hnodup).1
+              exact False.elim (hnot (List.mem_cons.mpr (Or.inl hxy)))
+          | cons z rest =>
+              have hx : x ∈ x :: y :: z :: rest := List.mem_cons_self
+              have hy : y ∈ x :: y :: z :: rest :=
+                List.mem_cons_of_mem x List.mem_cons_self
+              have hz : z ∈ x :: y :: z :: rest :=
+                List.mem_cons_of_mem x (List.mem_cons_of_mem y List.mem_cons_self)
+              have hnx := (List.nodup_cons.mp hnodup).1
+              have hny := (List.nodup_cons.mp (List.nodup_cons.mp hnodup).2).1
+              have hxy : x ≠ y := by
+                intro h
+                exact hnx (List.mem_cons.mpr (Or.inl h))
+              have hxz : x ≠ z := by
+                intro h
+                exact hnx (List.mem_cons.mpr
+                  (Or.inr (List.mem_cons.mpr (Or.inl h))))
+              have hyz : y ≠ z := by
+                intro h
+                exact hny (List.mem_cons.mpr (Or.inl h))
+              have hcxy := hcolor x hx y hy hxy (heven x hx) (heven y hy)
+              have hcxz := hcolor x hx z hz hxz (heven x hx) (heven z hz)
+              have hcyz := hcolor y hy z hz hyz (heven y hy) (heven z hz)
+              exact False.elim
+                (bool_three_colors_impossible (color x) (color y) (color z) hcxy hcxz hcyz)
+
+/-- The grouped-relation step for a family of binary subspaces, expressed using
+their membership predicates `Z`. A nonzero grouped vector from each selected
+index gives a distinct compatible clique: trivial intersections exclude vector
+collisions. Hence its sum can vanish only when no index was selected.
+
+Closure of `Z i` under binary sums is not needed here: the theorem takes the
+already grouped vectors. No finrank or scalar-field instantiation is asserted. -/
+theorem compatible_transversal_zero_sum_empty {I : Type u}
+    (zero : V) (add : V → V → V) (β : V → V → Bool) (color : V → Bool)
+    (compatible : V → V → Prop) (Z : I → V → Prop)
+    (haddzero : ∀ x, add x zero = x)
+    (hcancel : ∀ x y, add x y = zero ↔ x = y)
+    (hβzero : ∀ x, β x zero = false)
+    (hβadd : ∀ x y z, β x (add y z) = Bool.xor (β x y) (β x z))
+    (horth : ∀ x y, compatible x y → β x y = false)
+    (hcolor : ∀ x y, compatible x y →
+      β x x = false → β y y = false → color x ≠ color y)
+    (hdisjoint : ∀ i j, i ≠ j → ∀ x, Z i x → Z j x → x = zero)
+    (hcompatible : ∀ i j, i ≠ j → ∀ x, Z i x → x ≠ zero →
+      ∀ y, Z j y → y ≠ zero → compatible x y)
+    (indices : List I) (v : I → V) (hindices : indices.Nodup)
+    (hv : ∀ i ∈ indices, Z i (v i))
+    (hnonzero : ∀ i ∈ indices, v i ≠ zero)
+    (hsum : binarySum zero add (indices.map v) = zero) : indices = [] := by
+  have hdistinct : (indices.map v).Nodup := by
+    apply List.pairwise_map.mpr
+    apply List.Pairwise.imp_of_mem (p := hindices)
+    intro i j hi hj hij heq
+    have hzero : v i = zero :=
+      hdisjoint i j hij (v i) (hv i hi) (heq.symm ▸ hv j hj)
+    exact hnonzero i hi hzero
+  have hempty : indices.map v = [] := by
+    apply compatible_clique_zero_sum_empty zero add β color haddzero hcancel hβzero hβadd
+      (indices.map v) hdistinct
+    · intro x hx
+      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hx
+      exact hnonzero i hi
+    · intro x hx y hy hxy
+      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hx
+      obtain ⟨j, hj, rfl⟩ := List.mem_map.mp hy
+      have hij : i ≠ j := fun hij => hxy (congrArg v hij)
+      exact horth _ _ (hcompatible i j hij (v i) (hv i hi) (hnonzero i hi)
+        (v j) (hv j hj) (hnonzero j hj))
+    · intro x hx y hy hxy hxeven hyeven
+      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hx
+      obtain ⟨j, hj, rfl⟩ := List.mem_map.mp hy
+      have hij : i ≠ j := fun hij => hxy (congrArg v hij)
+      exact hcolor _ _ (hcompatible i j hij (v i) (hv i hi) (hnonzero i hi)
+        (v j) (hv j hj) (hnonzero j hj)) hxeven hyeven
+    · exact hsum
+  exact List.eq_nil_of_map_eq_nil hempty
+
+#print axioms detector_sum_zero
+#print axioms detector_sum_selected
+#print axioms compatible_clique_zero_sum_empty
+#print axioms compatible_transversal_zero_sum_empty
+
+namespace BinaryNine
+
+/-- The concrete nine-dimensional binary coordinate space. -/
+abbrev Vector := Fin 9 → Bool
+
+def zero : Vector := fun _ => false
+
+def add (x y : Vector) : Vector := fun i => Bool.xor (x i) (y i)
+
+private def coordinates : List (Fin 9) := [0, 1, 2, 3, 4, 5, 6, 7, 8]
+
+private def pairingOn : List (Fin 9) → Vector → Vector → Bool
+  | [], _, _ => false
+  | i :: is, x, y => Bool.xor (Bool.and (x i) (y i)) (pairingOn is x y)
+
+/-- The usual binary dot product, evaluated over all nine coordinates. -/
+def beta (x y : Vector) : Bool := pairingOn coordinates x y
+
+private theorem xor_zero_iff (a b : Bool) : Bool.xor a b = false ↔ a = b := by
+  cases a <;> cases b <;> simp
+
+private theorem add_zero (x : Vector) : add x zero = x := by
+  funext i
+  change Bool.xor (x i) false = x i
+  cases x i <;> rfl
+
+private theorem add_cancel (x y : Vector) : add x y = zero ↔ x = y := by
+  constructor
+  · intro h
+    funext i
+    exact (xor_zero_iff (x i) (y i)).mp (congrFun h i)
+  · intro h
+    subst y
+    funext i
+    exact Bool.xor_self (x i)
+
+private theorem dot_distribute (a b c r s : Bool) :
+    Bool.xor (Bool.and a (Bool.xor b c)) (Bool.xor r s) =
+      Bool.xor (Bool.xor (Bool.and a b) r) (Bool.xor (Bool.and a c) s) := by
+  cases a <;> cases b <;> cases c <;> cases r <;> cases s <;> rfl
+
+private theorem pairingOn_zero (is : List (Fin 9)) (x : Vector) :
+    pairingOn is x zero = false := by
+  induction is with
+  | nil => rfl
+  | cons i is ih =>
+      change Bool.xor (Bool.and (x i) false) (pairingOn is x zero) = false
+      rw [ih]
+      cases x i <;> rfl
+
+private theorem pairingOn_add (is : List (Fin 9)) (x y z : Vector) :
+    pairingOn is x (add y z) = Bool.xor (pairingOn is x y) (pairingOn is x z) := by
+  induction is with
+  | nil => rfl
+  | cons i is ih =>
+      change Bool.xor (Bool.and (x i) (Bool.xor (y i) (z i)))
+        (pairingOn is x (add y z)) =
+          Bool.xor (Bool.xor (Bool.and (x i) (y i)) (pairingOn is x y))
+            (Bool.xor (Bool.and (x i) (z i)) (pairingOn is x z))
+      rw [ih]
+      exact dot_distribute (x i) (y i) (z i) (pairingOn is x y) (pairingOn is x z)
+
+/-- Concrete binary-nine clique independence. All addition and pairing laws
+are discharged here. Orthogonality and the even-color compatibility condition
+remain explicit geometric premises; no E8 instantiation or finrank is asserted. -/
+theorem clique_zero_sum_empty (color : Vector → Bool) (xs : List Vector)
+    (hnodup : xs.Nodup) (hnonzero : ∀ x ∈ xs, x ≠ zero)
+    (horth : ∀ x ∈ xs, ∀ y ∈ xs, x ≠ y → beta x y = false)
+    (hcolor : ∀ x ∈ xs, ∀ y ∈ xs, x ≠ y →
+      beta x x = false → beta y y = false → color x ≠ color y)
+    (hsum : binarySum zero add xs = zero) : xs = [] :=
+  OneCosetDeficiency.compatible_clique_zero_sum_empty zero add beta color
+    add_zero add_cancel (pairingOn_zero coordinates) (pairingOn_add coordinates)
+    xs hnodup hnonzero horth hcolor hsum
+
+#print axioms clique_zero_sum_empty
+
+end BinaryNine
+
+end OneCosetDeficiency
diff --git a/research/e8-one-coset-deficiency/formal/ConsumerArithmetic.lean b/research/e8-one-coset-deficiency/formal/ConsumerArithmetic.lean
new file mode 100644
index 0000000000..549a3f9b2b
--- /dev/null
+++ b/research/e8-one-coset-deficiency/formal/ConsumerArithmetic.lean
@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 conorholds. All rights reserved.
+Released under Apache 2.0 license as described in the repository LICENSE.
+Prepared with substantial OpenAI Codex assistance.
+-/
+import Init
+
+/-!
+# Arithmetic of the final deficiency consumer
+
+This proves only the natural-number consequence of the two displayed budget
+inequalities. It does not derive either premise from ranks or E8 geometry.
+-/
+
+namespace OneCosetDeficiency
+
+/-- A ninefold budget and deficiency at least eight force at least 72 COPY
+units. Both inequalities are explicit premises; no geometric assembly is
+asserted here. -/
+theorem copy_ge_seventy_two (COPY m s t : Nat)
+    (hbudget : 9 * m ≤ COPY + 9 * s + 9 * t)
+    (hdeficiency : 8 + s + t ≤ m) : 72 ≤ COPY := by
+  have hscaled := Nat.mul_le_mul_left 9 hdeficiency
+  rw [Nat.mul_add, Nat.mul_add] at hscaled
+  change 72 + 9 * s + 9 * t ≤ 9 * m at hscaled
+  have hcombined := Nat.le_trans hscaled hbudget
+  exact Nat.le_of_add_le_add_right (Nat.le_of_add_le_add_right hcombined)
+
+#print axioms copy_ge_seventy_two
+
+end OneCosetDeficiency
diff --git a/research/e8-one-coset-deficiency/geometry.py b/research/e8-one-coset-deficiency/geometry.py
new file mode 100644
index 0000000000..9b4a3844d1
--- /dev/null
+++ b/research/e8-one-coset-deficiency/geometry.py
@@ -0,0 +1,324 @@
+"""Exact A8 model and small witnesses for the one-coset theorem.
+
+Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0.
+The model/deficiency setup credits PR1224 and PR1248; no source code is imported.
+Normal functions are pure and never read or write files.
+"""
+
+from fractions import Fraction
+from itertools import combinations, product
+
+
+OMEGA = 511
+MODEL = "Standard E8 roots scaled by 2; A8 label order"
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def parity(value):
+    return value.bit_count() % 2
+
+
+def dot(left, right):
+    require(len(left) == len(right), "dot-product dimensions differ")
+    return sum(x * y for x, y in zip(left, right))
+
+
+def binary_rank(values):
+    pivots = {}
+    for initial in values:
+        value = initial
+        require(type(value) is int and value >= 0, "binary vector is not a nonnegative integer")
+        while value:
+            pivot = value.bit_length() - 1
+            if pivot in pivots:
+                value ^= pivots[pivot]
+            else:
+                pivots[pivot] = value
+                break
+    return len(pivots)
+
+
+def rational_rank(rows):
+    """Forward Gaussian elimination over Q; not a modular deficiency test."""
+    if not rows:
+        return 0
+    width = len(rows[0])
+    require(all(len(row) == width for row in rows), "ragged rational matrix")
+    work = [[Fraction(x) for x in row] for row in rows]
+    rank = 0
+    for column in range(width):
+        pivot = next((i for i in range(rank, len(work)) if work[i][column]), None)
+        if pivot is None:
+            continue
+        work[rank], work[pivot] = work[pivot], work[rank]
+        for i in range(rank + 1, len(work)):
+            if work[i][column]:
+                factor = work[i][column] / work[rank][column]
+                for j in range(column, width):
+                    work[i][j] -= factor * work[rank][j]
+        rank += 1
+        if rank == len(work):
+            break
+    return rank
+
+
+def determinant(rows):
+    """Bareiss determinant with exact divisions and explicit row swaps."""
+    n = len(rows)
+    require(all(len(row) == n for row in rows), "determinant matrix is not square")
+    if not n:
+        return 1
+    work = [list(row) for row in rows]
+    previous, sign = 1, 1
+    for column in range(n - 1):
+        pivot = next((i for i in range(column, n) if work[i][column]), None)
+        if pivot is None:
+            return 0
+        if pivot != column:
+            work[column], work[pivot] = work[pivot], work[column]
+            sign = -sign
+        value = work[column][column]
+        for i in range(column + 1, n):
+            for j in range(column + 1, n):
+                numerator = value * work[i][j] - work[i][column] * work[column][j]
+                require(numerator % previous == 0, "nonexact Bareiss division")
+                work[i][j] = numerator // previous
+            work[i][column] = 0
+        previous = value
+    return sign * work[-1][-1]
+
+
+def build_model():
+    roots, labels = [], []
+    for i, j in combinations(range(9), 2):
+        row = [0] * 9
+        row[i], row[j] = 3, -3
+        roots.append(tuple(row))
+        labels.append(OMEGA ^ (1 << i) ^ (1 << j))
+    for subset in combinations(range(9), 3):
+        roots.append(tuple(2 if i in subset else -1 for i in range(9)))
+        labels.append(sum(1 << i for i in subset))
+    require(len(roots) == len(set(roots)) == len(set(labels)) == 120, "A8 root inventory")
+    require(binary_rank(labels) == 9, "binary label span is not nine")
+    require(all(sum(row) == 0 and dot(row, row) == 18 for row in roots), "A8 root norm")
+    for i, row in enumerate(roots):
+        for j, other in enumerate(roots):
+            value = dot(row, other)
+            require(value % 9 == 0, "root Gram entry is not integral after rescaling")
+            require(parity(labels[i] & labels[j]) == (1 + value // 9) % 2,
+                    "label/Gram identity")
+            require(parity(labels[i] & labels[j]) == int(i == j or value == 0),
+                    "labels do not represent canonical dense COPY pairing")
+    return {"roots": tuple(roots), "labels": tuple(labels)}
+
+
+def standard_roots():
+    """Standard E8 representatives, with scalar coordinates multiplied by two."""
+    result = []
+    for i, j in combinations(range(8), 2):
+        for sign in (-1, 1):
+            row = [0] * 8
+            row[i], row[j] = 2, 2 * sign
+            result.append(tuple(row))
+    result += [row for row in product((-1, 1), repeat=8)
+               if row[0] == 1 and sum(x < 0 for x in row) % 2 == 0]
+    require(len(result) == len(set(result)) == 120, "standard root inventory")
+    return tuple(result)
+
+
+def canonical(row):
+    return tuple(row) if next(x for x in row if x) > 0 else tuple(-x for x in row)
+
+
+def standard_binding(model):
+    """Rational star isometry; return standard roots in oriented A8 row order."""
+    star = []
+    for j in range(1, 8):
+        row = [0] * 8
+        row[0] = row[j] = 2
+        star.append(tuple(row))
+    star.append((1,) * 8)
+    require(all(dot(x, y) == 4 * (1 + int(i == j))
+                for i, x in enumerate(star) for j, y in enumerate(star)), "star Gram matrix")
+    lookup = {canonical(row): i for i, row in enumerate(model["roots"])}
+    oriented = [None] * 120
+    for root in standard_roots():
+        raw = [dot(root, other) for other in star]
+        require(all(value % 4 == 0 for value in raw), "nonintegral star pairing")
+        inner = [value // 4 for value in raw]
+        total = sum(inner)
+        require(total % 3 == 0, "nonintegral A8 image")
+        image = tuple(3 * value - total // 3 for value in inner) + (-total // 3,)
+        require(canonical(image) in lookup, "standard root missing from A8 alphabet")
+        index = lookup[canonical(image)]
+        sign = 1 if image == model["roots"][index] else -1
+        require(oriented[index] is None, "standard/A8 line map not injective")
+        oriented[index] = tuple(sign * value for value in root)
+    require(all(row is not None for row in oriented), "standard/A8 line map not onto")
+    for i, row in enumerate(oriented):
+        for j, other in enumerate(oriented):
+            require(9 * dot(row, other) == 4 * dot(model["roots"][i], model["roots"][j]),
+                    "standard/A8 isometry scaling")
+    return tuple(oriented)
+
+
+def pair_profiles():
+    for n00 in range(10):
+        for n01 in range(10 - n00):
+            for n10 in range(10 - n00 - n01):
+                n11 = 9 - n00 - n01 - n10
+                a = ((1 << (n10 + n11)) - 1) << (n00 + n01)
+                b = (((1 << n01) - 1) << n00) | (
+                    ((1 << n11) - 1) << (n00 + n01 + n10))
+                if a and b and a != b:
+                    yield (n00, n01, n10, n11), a, b
+
+
+def forbidden(a, b):
+    """Pairs that MUST have scalar intersection rank eight, not an iff edge test."""
+    return bool(parity(a & b) or (
+        parity(a) == parity(b) == 0
+        and (a.bit_count() // 2) % 2 == (b.bit_count() // 2) % 2))
+
+
+def _selected_minor(model, a, b=None):
+    """Use F3 to select standard-coordinate witnesses, then certify over Z."""
+    scalar_rows = standard_binding(model)
+    basis, selected = {}, []
+    for index, (label, row) in enumerate(zip(model["labels"], scalar_rows)):
+        if not parity(label & a) or (b is not None and not parity(label & b)):
+            continue
+        values = [value % 3 for value in row]
+        for pivot, old in sorted(basis.items()):
+            factor = values[pivot]
+            values = [(x - factor * y) % 3 for x, y in zip(values, old)]
+        pivot = next((i for i, value in enumerate(values) if value), None)
+        if pivot is None:
+            continue
+        scale = pow(values[pivot], -1, 3)
+        basis[pivot] = [value * scale % 3 for value in values]
+        selected.append(index)
+        if len(selected) == 8:
+            value = determinant([scalar_rows[i] for i in selected])
+            require(value != 0, "selected minor has zero integer determinant")
+            require(abs(value) & (abs(value) - 1) == 0, "selected minor is not a unit over Z[1/2]")
+            return {"rows": selected, "determinant": value}
+    raise ValueError("no eight-row witness for required character/profile")
+
+
+def make_certificate(model):
+    singles = [{"weight": k, "normal": (1 << k) - 1,
+                **_selected_minor(model, (1 << k) - 1)} for k in range(1, 10)]
+    pairs = [{"counts": list(counts), "a": a, "b": b,
+              **_selected_minor(model, a, b)}
+             for counts, a, b in pair_profiles() if forbidden(a, b)]
+    return {"schema_version": 1, "model": MODEL,
+            "single_types": singles, "forbidden_pairs": pairs}
+
+
+def check_certificate(model, certificate):
+    scalar_rows = standard_binding(model)
+    require(type(certificate) is dict and set(certificate) == {
+        "schema_version", "model", "single_types", "forbidden_pairs"}, "certificate schema")
+    require(type(certificate["schema_version"]) is int and certificate["schema_version"] == 1
+            and certificate["model"] == MODEL, "certificate model/version")
+    singles, pairs = certificate["single_types"], certificate["forbidden_pairs"]
+    require(type(singles) is list and len(singles) == 9, "single inventory count")
+    require(type(pairs) is list and len(pairs) == 100, "forbidden inventory count")
+    expected = {tuple(counts): (a, b) for counts, a, b in pair_profiles() if forbidden(a, b)}
+    require(len(list(pair_profiles())) == 192 and len(expected) == 100, "profile enumeration")
+    seen_single, seen_pair, determinants = set(), set(), []
+    for item, kind in [(row, "single") for row in singles] + [(row, "pair") for row in pairs]:
+        fields = {"weight", "normal", "rows", "determinant"} if kind == "single" else {
+            "counts", "a", "b", "rows", "determinant"}
+        require(type(item) is dict and set(item) == fields, "witness schema")
+        if kind == "single":
+            weight = item["weight"]
+            require(type(weight) is int and 1 <= weight <= 9, "single weight")
+            a, b = item["normal"], None
+            require(type(a) is int and a == (1 << weight) - 1, "single normal binding")
+            require(weight not in seen_single, "duplicate single type")
+            seen_single.add(weight)
+        else:
+            counts = item["counts"]
+            require(type(counts) is list and len(counts) == 4
+                    and all(type(n) is int and 0 <= n <= 9 for n in counts), "profile counts")
+            key = tuple(counts)
+            require(key in expected and key not in seen_pair, "unknown/duplicate forbidden profile")
+            a, b = item["a"], item["b"]
+            require(type(a) is type(b) is int and (a, b) == expected[key], "normal/profile binding")
+            seen_pair.add(key)
+        rows, value = item["rows"], item["determinant"]
+        require(type(rows) is list and len(rows) == 8
+                and all(type(i) is int and 0 <= i < 120 for i in rows)
+                and len(set(rows)) == 8, "minor root indices")
+        require(type(value) is int and value != 0, "minor determinant type/value")
+        for index in rows:
+            label = model["labels"][index]
+            require(parity(label & a) and (b is None or parity(label & b)), "witness support membership")
+        require(determinant([scalar_rows[i] for i in rows]) == value, "integer minor determinant")
+        require(abs(value) & (abs(value) - 1) == 0, "minor is not a unit over Z[1/2]")
+        determinants.append(abs(value))
+    require(seen_single == set(range(1, 10)) and seen_pair == set(expected), "incomplete type coverage")
+    return {"single_types": 9, "valid_pair_profiles": 192,
+            "forbidden_pair_profiles": 100, "nonzero_integer_minors": len(determinants),
+            "determinants_absolute": sorted(set(determinants)),
+            "all_minors_units_over_Z_half": True}
+
+
+def reflection_transport(model):
+    """Check all S9 generators over Z[1/2], without reducing the A8 isometry at3."""
+    scalar = standard_binding(model)
+    lookup = {canonical(row): i for i, row in enumerate(scalar)}
+    root_lookup = {row: i for i, row in enumerate(model["roots"])}
+    for k in range(8):
+        pair = tuple(3 if j == k else -3 if j == k + 1 else 0 for j in range(9))
+        alpha = scalar[root_lookup[pair]]
+        # Numerator of the reflection I - alpha alpha^T / 4.
+        numerator = [[4 * int(i == j) - alpha[i] * alpha[j] for j in range(8)]
+                     for i in range(8)]
+        require(all(sum(numerator[i][t] * numerator[t][j] for t in range(8)) == 16 * int(i == j)
+                    for i in range(8) for j in range(8)), "reflection is not invertible over Z[1/2]")
+        for i, row in enumerate(scalar):
+            product = dot(row, alpha)
+            require(product % 4 == 0, "root reflection quotient is not integral")
+            image = tuple(x - (product // 4) * y for x, y in zip(row, alpha))
+            require(canonical(image) in lookup, "root reflection leaves the fixed alphabet")
+            target = lookup[canonical(image)]
+            label = model["labels"][i]
+            swap = ((label >> k) ^ (label >> (k + 1))) & 1
+            label_image = label ^ ((1 << k) | (1 << (k + 1))) if swap else label
+            require(model["labels"][target] == label_image, "reflection/S9 label action differs")
+            require(all(4 * image[j] == sum(numerator[j][t] * row[t] for t in range(8))
+                        for j in range(8)), "reflection integer transport identity")
+    return {"adjacent_generators": 8, "root_line_transports": 960,
+            "involution_matrix_entries": 512, "denominators_are_powers_of_two": True}
+
+
+def certificate_text(certificate):
+    """Keep each explicit witness on one line so the certificate is reviewable."""
+    import json
+    blocks = ['{', '  "schema_version": 1,', '  "model": ' + json.dumps(MODEL) + ',']
+    for name in ("single_types", "forbidden_pairs"):
+        blocks.append('  ' + json.dumps(name) + ': [')
+        rows = certificate[name]
+        for index, row in enumerate(rows):
+            blocks.append('    ' + json.dumps(row, separators=(',', ':')) + (',' if index + 1 < len(rows) else ''))
+        blocks.append('  ]' + (',' if name == "single_types" else ''))
+    return '\n'.join(blocks + ['}', ''])
+
+
+def support_weight(model, values):
+    require(len(values) == 120, "support vector length")
+    return binary_rank(label for label, value in zip(model["labels"], values) if value)
+
+
+def copy_rank(model, p, q):
+    require(len(p) == len(q) == 120, "factor length")
+    columns = [label for label, value in zip(model["labels"], q) if value]
+    return binary_rank(sum(parity(label & column) << j for j, column in enumerate(columns))
+                       for label, value in zip(model["labels"], p) if value)
diff --git a/research/e8-one-coset-deficiency/independent.py b/research/e8-one-coset-deficiency/independent.py
new file mode 100644
index 0000000000..b0bde92d7b
--- /dev/null
+++ b/research/e8-one-coset-deficiency/independent.py
@@ -0,0 +1,555 @@
+#!/usr/bin/env python3
+"""Independent exact finite replay, using a second realization of E8.
+
+This file does not import the primary verifier or its A8 realization.  It starts
+with the 56 D8 root lines and 64 half-integral root lines in eight coordinates,
+all multiplied by two.  It reconstructs the binary labels from their intrinsic
+orthogonality table and checks every nonzero character and unordered pair.
+
+``build_model()`` (also ``model()``) returns the doubled scalar roots, canonical
+9-bit labels, and binary coordinate-transport data.  ``verify_all()`` (also
+``run()``) returns a JSON-safe summary and writes nothing.  Running this file
+prints PASS and that summary.  Only the Python standard library is required.
+
+Full rank modulo 3 proves rank eight over Q, and hence over every characteristic
+zero scalar field: the witnessing integer minor is nonzero.  A failed modular
+rank is never used to prove deficiency.  In that case primitive integer row
+elimination computes the exact rational rank.  No floating point or assertions
+are used for correctness.
+
+Model lineage: the E8 scalar alphabet and decoder setting in source PRs #1224
+and #1248.  This is a separate AI implementation, not a human review.  Prepared
+by conorholds under Apache-2.0; predecessor attribution belongs in SOURCES.json.
+"""
+
+from itertools import combinations, product
+import json
+from math import gcd
+
+
+DIMENSION = 8
+BINARY_DIMENSION = 9
+OMEGA = (1 << BINARY_DIMENSION) - 1
+
+
+class VerificationError(RuntimeError):
+    """An exact finite identity or required control failed."""
+
+
+def _require(condition, message):
+    if not condition:
+        raise VerificationError(message)
+
+
+def _dot(left, right):
+    return sum(a * b for a, b in zip(left, right))
+
+
+def _parity(value):
+    return value.bit_count() & 1
+
+
+def _even_q(value):
+    _require(_parity(value) == 0, "quadratic form requires an even vector")
+    return (value.bit_count() // 2) & 1
+
+
+def _standard_roots():
+    roots = []
+    for first, second in combinations(range(DIMENSION), 2):
+        for sign in (-1, 1):
+            row = [0] * DIMENSION
+            row[first], row[second] = 2, 2 * sign
+            roots.append(tuple(row))
+    for signs in range(1 << (DIMENSION - 1)):
+        if _parity(signs) == 0:
+            roots.append((1,) + tuple(
+                -1 if signs & (1 << index) else 1
+                for index in range(DIMENSION - 1)
+            ))
+    roots = tuple(roots)
+    _require(len(roots) == len(set(roots)) == 120,
+             "standard E8 construction did not give 120 distinct lines")
+    _require(all(_dot(row, row) == 8 for row in roots),
+             "standard E8 roots have incorrect squared length")
+    _require(all(next(value for value in row if value) > 0 for row in roots),
+             "root-line signs are not canonical")
+    return roots
+
+
+def _intrinsic_table(roots):
+    """One on the diagonal or an orthogonal pair; zero otherwise."""
+    table = []
+    for index, row in enumerate(roots):
+        bits = 0
+        for other_index, other in enumerate(roots):
+            product = _dot(row, other)
+            _require(index == other_index or product in (-4, 0, 4),
+                     "distinct E8 lines have an unexpected scalar product")
+            if index == other_index or product == 0:
+                bits |= 1 << other_index
+        table.append(bits)
+    return tuple(table)
+
+
+def _independent_indices(rows):
+    echelon = {}
+    indices = []
+    for index, initial in enumerate(rows):
+        row = initial
+        while row:
+            pivot = row.bit_length() - 1
+            if pivot in echelon:
+                row ^= echelon[pivot]
+            else:
+                echelon[pivot] = row
+                indices.append(index)
+                break
+    return tuple(indices)
+
+
+def _binary_inverse(rows):
+    size = len(rows)
+    left_mask = (1 << size) - 1
+    work = [row | (1 << (size + index)) for index, row in enumerate(rows)]
+    for column in range(size):
+        pivot = next((index for index in range(column, size)
+                      if work[index] & (1 << column)), None)
+        _require(pivot is not None, "binary Gram matrix is singular")
+        work[column], work[pivot] = work[pivot], work[column]
+        for index in range(size):
+            if index != column and work[index] & (1 << column):
+                work[index] ^= work[column]
+    _require(all((row & left_mask) == 1 << index
+                 for index, row in enumerate(work)),
+             "binary inverse elimination failed")
+    return tuple(row >> size for row in work)
+
+
+def _binary_solve(equations, size):
+    """Solve a required unique system, rejecting inconsistent extra rows."""
+    work = [mask | (right << size) for mask, right in equations]
+    pivot_row = 0
+    for column in range(size):
+        pivot = next((index for index in range(pivot_row, len(work))
+                      if work[index] & (1 << column)), None)
+        _require(pivot is not None, "binary normalization is not uniquely fixed")
+        work[pivot_row], work[pivot] = work[pivot], work[pivot_row]
+        for index in range(len(work)):
+            if index != pivot_row and work[index] & (1 << column):
+                work[index] ^= work[pivot_row]
+        pivot_row += 1
+    mask = (1 << size) - 1
+    _require(all(row & mask or not row >> size for row in work),
+             "binary normalization equations are inconsistent")
+    solution = sum(((work[index] >> size) & 1) << index
+                   for index in range(size))
+    _require(all(_parity(mask & solution) == right
+                 for mask, right in equations),
+             "binary normalization solution failed substitution")
+    return solution
+
+
+def _check_incidence(roots, labels):
+    _require(len(roots) == len(labels) == 120,
+             "root and label counts disagree")
+    for index, root in enumerate(roots):
+        for other_index, other in enumerate(roots):
+            geometric = int(index == other_index or _dot(root, other) == 0)
+            _require(_parity(labels[index] & labels[other_index]) == geometric,
+                     "binary labels disagree with scalar orthogonality")
+
+
+def build_model():
+    """Return independently constructed roots, labels, and exact transport data.
+
+    A raw label records one root's table entries against nine independent root
+    columns.  Its bilinear form is G inverse, not the identity.  The returned
+    labels have been transported to the identity form, then normalized so that
+    the entire root set is exactly the 9-bit vectors of weights three and seven.
+    Thus ordinary bit parity is beta on both labels and normal characters.
+    """
+    roots = _standard_roots()
+    table = _intrinsic_table(roots)
+    indices = _independent_indices(table)
+    _require(len(indices) == BINARY_DIMENSION,
+             "intrinsic binary orthogonality table does not have rank nine")
+    raw_labels = tuple(sum(((row >> selected) & 1) << column
+                           for column, selected in enumerate(indices))
+                       for row in table)
+    gram = tuple(raw_labels[index] for index in indices)
+    inverse = _binary_inverse(gram)
+    matrix_times = tuple(sum(_parity(row & value) << index
+                             for index, row in enumerate(inverse))
+                         for value in range(OMEGA + 1))
+
+    def pairing(left, right):
+        return _parity(left & matrix_times[right])
+
+    for index, left in enumerate(raw_labels):
+        for other_index, right in enumerate(raw_labels):
+            _require(pairing(left, right) == ((table[index] >> other_index) & 1),
+                     "inverse Gram form does not reconstruct the intrinsic table")
+
+    # Choose an orthonormal basis without leaving an alternating residual form.
+    # In an odd nonalternating space the characteristic vector can be a bad first
+    # choice; checking the residual form avoids that binary Gram-Schmidt trap.
+    subspace = list(range(OMEGA + 1))
+    orthonormal = []
+    for remaining in range(BINARY_DIMENSION, 0, -1):
+        selected = None
+        residual = None
+        for candidate in subspace:
+            if not pairing(candidate, candidate):
+                continue
+            complement = [value for value in subspace
+                          if not pairing(candidate, value)]
+            if remaining == 1 or any(pairing(value, value) for value in complement):
+                selected, residual = candidate, complement
+                break
+        _require(selected is not None, "binary orthonormal basis construction failed")
+        orthonormal.append(selected)
+        subspace = residual
+    _require(subspace == [0], "binary orthonormal basis does not span")
+    _require(all(pairing(left, right) == int(i == j)
+                 for i, left in enumerate(orthonormal)
+                 for j, right in enumerate(orthonormal)),
+             "transport basis is not orthonormal")
+    labels = tuple(sum(pairing(label, vector) << index
+                       for index, vector in enumerate(orthonormal))
+                   for label in raw_labels)
+    _check_incidence(roots, labels)
+
+    # On the even subspace, the intrinsic E8 root quadratic form can differ
+    # from wt/2 by a linear form.  Solve for its even representative b.  Since
+    # q(b)=0, x -> x + (x.b)b is an orthogonal transvection correcting that form.
+    equations = [(label ^ OMEGA, 1 ^ _even_q(label ^ OMEGA)) for label in labels]
+    equations.append((OMEGA, 0))
+    correction = _binary_solve(equations, BINARY_DIMENSION)
+    _require(_even_q(correction) == 0,
+             "root quadratic refinement has the wrong isometry type")
+    labels = tuple(label ^ correction if _parity(label & correction) else label
+                   for label in labels)
+    expected = {value for value in range(OMEGA + 1)
+                if value.bit_count() in (3, 7)}
+    _require(set(labels) == expected and len(set(labels)) == 120,
+             "canonical root labels are not exactly the weight-three/seven vectors")
+    _check_incidence(roots, labels)
+    return {
+        "roots": roots,
+        "labels": labels,
+        "pairing_rows": table,
+        "basis_root_indices": indices,
+        "gram_rows": gram,
+        "gram_inverse_rows": inverse,
+        "raw_labels": raw_labels,
+        "orthonormal_basis": tuple(orthonormal),
+        "quadratic_correction": correction,
+        "scalar_coordinate_scale": 2,
+    }
+
+
+model = build_model
+
+
+def _rank_mod_three(support, rows):
+    """Rank in F3; eight is a characteristic-zero certificate, less is not."""
+    basis = [None] * DIMENSION
+    rank = 0
+    while support:
+        bit = support & -support
+        support ^= bit
+        row = list(rows[bit.bit_length() - 1])
+        for column in range(DIMENSION):
+            coefficient = row[column]
+            if not coefficient:
+                continue
+            old = basis[column]
+            if old is None:
+                if coefficient == 2:
+                    for index in range(column, DIMENSION):
+                        row[index] = (2 * row[index]) % 3
+                basis[column] = row
+                rank += 1
+                if rank == DIMENSION:
+                    return rank
+                break
+            for index in range(column + 1, DIMENSION):
+                row[index] = (row[index] - coefficient * old[index]) % 3
+            row[column] = 0
+    return rank
+
+
+def _rank_rational(support, roots):
+    """Exact row rank over Q by primitive integer echelon elimination."""
+    basis = [None] * DIMENSION
+    rank = 0
+    while support:
+        bit = support & -support
+        support ^= bit
+        row = list(roots[bit.bit_length() - 1])
+        for column in range(DIMENSION):
+            coefficient = row[column]
+            if not coefficient:
+                continue
+            old = basis[column]
+            if old is None:
+                content = 0
+                for value in row[column:]:
+                    content = gcd(content, value)
+                if coefficient < 0:
+                    content = -content
+                basis[column] = tuple(value // content for value in row)
+                rank += 1
+                if rank == DIMENSION:
+                    return rank
+                break
+            pivot = old[column]
+            for index in range(column + 1, DIMENSION):
+                row[index] = pivot * row[index] - coefficient * old[index]
+            row[column] = 0
+    return rank
+
+
+def _supports(labels):
+    return tuple(sum(_parity(normal & label) << index
+                     for index, label in enumerate(labels))
+                 for normal in range(OMEGA + 1))
+
+
+def _binary_support_rank(support, labels):
+    basis = [0] * BINARY_DIMENSION
+    rank = 0
+    while support:
+        bit = support & -support
+        support ^= bit
+        row = labels[bit.bit_length() - 1]
+        while row:
+            pivot = row.bit_length() - 1
+            if basis[pivot]:
+                row ^= basis[pivot]
+            else:
+                basis[pivot] = row
+                rank += 1
+                if rank == BINARY_DIMENSION:
+                    return rank
+                break
+    return rank
+
+
+def verify_sparse_cosets(data=None):
+    """Exhaust four sparse outside cosets of the F3 scalar root code.
+
+    Each of the 3**8 vectors h is used once to evaluate the full codeword Rh.
+    The nonzero codewords must have support-label rank nine.  Each chosen lambda
+    has support-label rank at most two, proving it is outside that code.  The
+    histograms exhaust every lambda + Rh, with no random choices or sampling.
+    """
+    if data is None:
+        data = build_model()
+    roots, labels = data["roots"], data["labels"]
+    first = 0
+    orthogonal = next(index for index in range(1, len(roots))
+                      if _dot(roots[first], roots[index]) == 0)
+    nonorthogonal = next(index for index in range(1, len(roots))
+                         if _dot(roots[first], roots[index]) != 0)
+    sparse = {
+        "singleton": ((first, 1),),
+        "nonorthogonal_11": ((first, 1), (nonorthogonal, 1)),
+        "nonorthogonal_12": ((first, 1), (nonorthogonal, 2)),
+        "orthogonal_11": ((first, 1), (orthogonal, 1)),
+    }
+    families = {}
+    for name, entries in sparse.items():
+        rank = _binary_support_rank(sum(1 << index for index, _ in entries), labels)
+        _require(rank == len(entries) < BINARY_DIMENSION,
+                 "sparse lambda support has unexpected binary rank")
+        families[name] = {"sparse_lambda": [list(entry) for entry in entries],
+                          "lambda_support_rank": rank,
+                          "deficiency_histogram": {}, "deficiency_sum": 0}
+    rows = tuple(tuple(value % 3 for value in row) for row in roots)
+    normalizations = 0
+    nonzero_codewords = 0
+    for coefficients in product(range(3), repeat=DIMENSION):
+        evaluations = tuple(sum(a * b for a, b in zip(row, coefficients)) % 3
+                            for row in rows)
+        support = sum(1 << index for index, value in enumerate(evaluations) if value)
+        if any(coefficients):
+            _require(_binary_support_rank(support, labels) == BINARY_DIMENSION,
+                     "a nonzero scalar codeword has deficient binary support")
+            nonzero_codewords += 1
+        else:
+            _require(support == 0, "zero coefficients gave a nonzero codeword")
+        for name, entries in sparse.items():
+            shifted = support
+            for index, value in entries:
+                if bool(evaluations[index]) != bool((evaluations[index] + value) % 3):
+                    shifted ^= 1 << index
+            rank = _binary_support_rank(shifted, labels)
+            _require(rank > 0, "a sparse outside coset contained zero")
+            deficiency = BINARY_DIMENSION - rank
+            family = families[name]
+            histogram = family["deficiency_histogram"]
+            key = str(deficiency)
+            histogram[key] = histogram.get(key, 0) + 1
+            family["deficiency_sum"] += deficiency
+        normalizations += 1
+    _require(normalizations == 6561 and nonzero_codewords == 6560,
+             "scalar code or sparse-coset exhaustion was incomplete")
+    for family in families.values():
+        _require(sum(family["deficiency_histogram"].values()) == normalizations,
+                 "sparse-coset deficiency histogram was incomplete")
+        _require(family["deficiency_sum"] <= BINARY_DIMENSION,
+                 "a sparse outside coset exceeded total deficiency nine")
+        family["normalizations_checked"] = normalizations
+    _require(families["singleton"]["deficiency_sum"] == BINARY_DIMENSION,
+             "singleton outside coset did not attain deficiency nine")
+    return {"field_order": 3, "code_dimension": DIMENSION,
+            "codewords_checked": normalizations,
+            "nonzero_codewords_with_support_rank_nine": nonzero_codewords,
+            "families": families}
+
+
+def _certified_rank(support, roots, rows_mod_three):
+    """Return exact rational rank and whether a full-rank F3 witness sufficed."""
+    modular = _rank_mod_three(support, rows_mod_three)
+    if modular == DIMENSION:
+        return modular, True
+    exact = _rank_rational(support, roots)
+    _require(exact >= modular, "rational rank was smaller than modular rank")
+    return exact, False
+
+
+def _controls(roots, labels, supports):
+    # Two distinct odd orthogonal normals are genuinely compatible; a normal
+    # and its omega-complement have disjoint odd supports.
+    cases = (
+        ("orthogonal_coordinate_normals", 1, 2, 7),
+        ("complementary_normals", 1, OMEGA ^ 1, 0),
+        ("nonorthogonal_normals", 1, 3, 8),
+        ("orthogonal_even_same_quadratic", 3, 12, 8),
+    )
+    results = {}
+    for name, left, right, expected in cases:
+        rank = _rank_rational(supports[left] & supports[right], roots)
+        _require(rank == expected, "geometric control failed: " + name)
+        results[name] = rank
+    _require(_rank_rational(0, roots) == 0, "empty rational rank control failed")
+    _require(_rank_rational(1, roots) == 1, "one-line rational rank control failed")
+    # A determinant divisible by three is nonzero over Q even though it
+    # vanishes modulo three.  Exercise that essential fallback distinction.
+    diagonal = tuple(tuple((3 if index == DIMENSION - 1 else 1)
+                           if index == column else 0
+                           for column in range(DIMENSION))
+                     for index in range(DIMENSION))
+    diagonal_mod_three = tuple(tuple(value % 3 for value in row)
+                               for row in diagonal)
+    diagonal_support = (1 << DIMENSION) - 1
+    modular_rank = _rank_mod_three(diagonal_support, diagonal_mod_three)
+    rational_rank = _rank_rational(diagonal_support, diagonal)
+    dispatched_rank, modular_witness = _certified_rank(
+        diagonal_support, diagonal, diagonal_mod_three)
+    _require(modular_rank == 7 and rational_rank == 8,
+             "modular rank drop was incorrectly treated as rational deficiency")
+    _require(dispatched_rank == 8 and not modular_witness,
+             "rank dispatcher did not use its rational fallback")
+    results["modular_rank_drop"] = {
+        "mod_three_rank": modular_rank,
+        "rational_rank": rational_rank,
+        "dispatched_rank": dispatched_rank,
+        "used_rational_fallback": not modular_witness,
+    }
+    # Replacing one line by its orthogonal neighbour preserves its norm but
+    # invalidates the fixed labels.  Require the geometric predicate to notice.
+    wrong_roots = (roots[1],) + roots[1:]
+    rejected = False
+    try:
+        _check_incidence(wrong_roots, labels)
+    except VerificationError:
+        rejected = True
+    _require(rejected, "deliberate geometry/predicate mismatch was accepted")
+    results["geometry_predicate_mismatch_rejected"] = True
+    return results
+
+
+def verify_all():
+    """Exhaust the finite one-coset rank lemma with bounded, streaming storage."""
+    data = build_model()
+    roots, labels = data["roots"], data["labels"]
+    supports = _supports(labels)
+    rows_mod_three = tuple(tuple(value % 3 for value in row) for row in roots)
+    controls = _controls(roots, labels, supports)
+    single_histogram = {}
+    pair_histogram = {}
+    modular_full_rank = 0
+    rational_fallbacks = 0
+
+    def scalar_rank(support):
+        nonlocal modular_full_rank, rational_fallbacks
+        rank, modular_witness = _certified_rank(support, roots, rows_mod_three)
+        if modular_witness:
+            modular_full_rank += 1
+        else:
+            rational_fallbacks += 1
+        return rank
+
+    for normal in range(1, OMEGA + 1):
+        rank = scalar_rank(supports[normal])
+        single_histogram[str(rank)] = single_histogram.get(str(rank), 0) + 1
+        _require(rank == DIMENSION, "a nonzero character failed to span E8")
+
+    compatible_pairs = 0
+    forbidden_pairs = 0
+    for left in range(1, OMEGA + 1):
+        left_even = not _parity(left)
+        left_q = _even_q(left) if left_even else None
+        for right in range(left + 1, OMEGA + 1):
+            rank = scalar_rank(supports[left] & supports[right])
+            pair_histogram[str(rank)] = pair_histogram.get(str(rank), 0) + 1
+            forbidden = bool(_parity(left & right)) or (
+                left_even and not _parity(right) and left_q == _even_q(right)
+            )
+            if forbidden:
+                forbidden_pairs += 1
+                _require(rank == DIMENSION,
+                         "a deficient pair violated a required binary condition")
+            if rank < DIMENSION:
+                compatible_pairs += 1
+
+    pair_count = OMEGA * (OMEGA - 1) // 2
+    _require(sum(single_histogram.values()) == 511,
+             "single-character exhaustion was incomplete")
+    _require(sum(pair_histogram.values()) == pair_count == 130305,
+             "unordered-pair exhaustion was incomplete")
+    _require(modular_full_rank + rational_fallbacks == 511 + pair_count,
+             "rank-certificate accounting failed")
+    return {
+        "status": "PASS",
+        "implementation": "independent standard D8 plus half-root E8 realization",
+        "scalar_dimension": DIMENSION,
+        "binary_dimension": BINARY_DIMENSION,
+        "root_lines": len(roots),
+        "scalar_coordinate_scale": data["scalar_coordinate_scale"],
+        "canonical_label_weight_counts": {"3": 84, "7": 36},
+        "nonzero_characters": 511,
+        "single_rank_histogram": single_histogram,
+        "unordered_distinct_nonzero_pairs": pair_count,
+        "pair_rank_histogram": pair_histogram,
+        "compatible_pairs": compatible_pairs,
+        "forbidden_pairs_proved_full_rank": forbidden_pairs,
+        "rank_evaluations": {
+            "mod_three_full_rank_witnesses": modular_full_rank,
+            "exact_rational_fallbacks": rational_fallbacks,
+        },
+        "controls": controls,
+        "sparse_cosets": verify_sparse_cosets(data),
+    }
+
+
+run = verify_all
+
+
+if __name__ == "__main__":
+    summary = verify_all()
+    print("PASS_E8_ONE_COSET_DEFICIENCY_INDEPENDENT")
+    print(json.dumps(summary, sort_keys=True))
diff --git a/research/e8-one-coset-deficiency/sparse_pair.py b/research/e8-one-coset-deficiency/sparse_pair.py
new file mode 100644
index 0000000000..eee3e87d1c
--- /dev/null
+++ b/research/e8-one-coset-deficiency/sparse_pair.py
@@ -0,0 +1,381 @@
+"""Independent finite sparse-pair controls, using dense binary COPY ranks.
+
+Prepared by conorholds with substantial AI assistance. Apache-2.0.
+No candidate modules or binary labels are imported. The F3 census is exhaustive;
+the F5/F7 planted checks are controls, not exhaustive proofs over those fields.
+The written argument supplies the extension to every odd characteristic.
+The merge-proof variant was proposed and independently checked by the
+Claude Fable 5.1 AI auditor; this is not human review.
+"""
+from collections import Counter
+from itertools import combinations, product
+import json
+
+
+class VerificationError(ValueError):
+    """An exact finite identity or semantic control failed."""
+
+
+def need(condition, message):
+    if not condition:
+        raise VerificationError(message)
+
+
+def dot(left, right):
+    return sum(x * y for x, y in zip(left, right))
+
+
+def scalar_rank(rows, width, prime=3):
+    basis = {}
+    for initial in rows:
+        row = [x % prime for x in initial]
+        for pivot in range(width):
+            if not row[pivot]:
+                continue
+            if pivot not in basis:
+                scale = pow(row[pivot], -1, prime)
+                basis[pivot] = [scale * x % prime for x in row]
+                break
+            factor = row[pivot]
+            row = [(x - factor * y) % prime for x, y in zip(row, basis[pivot])]
+    return len(basis)
+
+
+def projective_key(column, prime):
+    """Canonical scalar ray, computed without candidate matrix arithmetic."""
+    pivot = next((x % prime for x in column if x % prime), None)
+    if pivot is None:
+        return None
+    scale = pow(pivot, -1, prime)
+    return tuple(scale * x % prime for x in column)
+
+
+def pairwise_nonproportional(columns, prime):
+    keys = [projective_key(column, prime) for column in columns]
+    return all(key is not None for key in keys) and len(set(keys)) == len(keys)
+
+
+def normalize_proportional(P, Q, prime):
+    """Delete inactive terms and merge actual proportional factors on either side."""
+    need(len(P) == len(Q), "normalizer factor lengths")
+    terms = [(tuple(x % prime for x in p), tuple(x % prime for x in q))
+             for p, q in zip(P, Q)]
+    merges = zero_terms_removed = 0
+    while True:
+        active = [term for term in terms if all(any(column) for column in term)]
+        zero_terms_removed += len(terms) - len(active)
+        terms = active
+        merged = False
+        for side in (0, 1):
+            seen = {}
+            for index, term in enumerate(terms):
+                key = projective_key(term[side], prime)
+                if key not in seen:
+                    seen[key] = index
+                    continue
+                previous = seen[key]
+                pivot = next(i for i, x in enumerate(terms[previous][side]) if x)
+                scale = term[side][pivot] * pow(terms[previous][side][pivot], -1, prime) % prime
+                other = 1 - side
+                combined = tuple((x + scale * y) % prime
+                                 for x, y in zip(terms[previous][other], term[other]))
+                replacement = list(terms[previous])
+                replacement[other] = combined
+                terms[previous] = tuple(replacement)
+                del terms[index]
+                merges += 1
+                merged = True
+                break
+            if merged:
+                break
+        if not merged:
+            return ([term[0] for term in terms], [term[1] for term in terms],
+                    {"merges": merges, "zero_terms_removed": zero_terms_removed})
+
+
+def build_model():
+    roots = []
+    for a, b in combinations(range(8), 2):
+        for sign in (-1, 1):
+            row = [0] * 8
+            row[a], row[b] = 2, sign * 2
+            roots.append(tuple(row))
+    roots.extend((1,) + signs for signs in product((-1, 1), repeat=7)
+                 if signs.count(-1) % 2 == 0)
+    need(len(roots) == len(set(roots)) == 120, "root inventory")
+    need(all(dot(root, root) == 8 for root in roots), "doubled root norms")
+    table = tuple(sum(int(i == j or dot(r, s) == 0) << j
+                      for j, s in enumerate(roots)) for i, r in enumerate(roots))
+    return tuple(roots), table
+
+
+def support_weight(support, table, stop_at_nine=True):
+    basis = {}
+    while support:
+        low = support & -support
+        support ^= low
+        row = table[low.bit_length() - 1]
+        while row:
+            pivot = row.bit_length() - 1
+            if pivot in basis:
+                row ^= basis[pivot]
+            else:
+                basis[pivot] = row
+                break
+        if stop_at_nine and len(basis) == 9:
+            return 9
+    return len(basis)
+
+
+def support_bits(column):
+    return sum(int(x != 0) << i for i, x in enumerate(column))
+
+
+def factor_copy_costs(P, Q, table):
+    costs = []
+    for p, q in zip(P, Q):
+        reader_support = support_bits(q)
+        costs.append(support_weight(support_bits(p), tuple(row & reader_support for row in table)))
+    return costs
+
+
+def check_factor_product(P, Q, roots, prime):
+    need(len(P) == len(Q), "sharp product factor lengths")
+    need(all(len(column) == len(roots) for column in P + Q), "sharp product column lengths")
+    eighth = pow(8, -1, prime)
+    for i, root in enumerate(roots):
+        for j, other in enumerate(roots):
+            need(sum(p[i] * q[j] for p, q in zip(P, Q)) % prime
+                 == eighth * dot(root, other) % prime, "sharp entrywise N0 product")
+
+
+def hole(root, coefficient, prime, factor=1):
+    return tuple(-factor * coefficient * x * pow(8, -1, prime) % prime for x in root)
+
+
+def expected_weight(h, s, t, roots, a, b, prime, nonorthogonal, hole_factor=1):
+    if not any(h):
+        return int(bool(s)) + int(bool(t))
+    for coefficient, other, index in ((s, t, a), (t, s, b)):
+        if coefficient and h == hole(roots[index], coefficient, prime, hole_factor):
+            if not other or nonorthogonal:
+                return 8
+    return 9
+
+
+def check_point(h, s, t, roots, table, a, b, prime, nonorthogonal, hole_factor=1):
+    values = [(dot(root, h) + (s if i == a else t if i == b else 0)) % prime
+              for i, root in enumerate(roots)]
+    actual = support_weight(sum(int(x != 0) << i for i, x in enumerate(values)), table)
+    expected = expected_weight(h, s, t, roots, a, b, prime, nonorthogonal, hole_factor)
+    need(actual == expected, "actual support weight contradicts sparse-ray classification")
+    return actual
+
+
+def rejected(action):
+    try:
+        action()
+    except VerificationError:
+        return True
+    return False
+
+
+def inverse(matrix, prime):
+    size = len(matrix)
+    work = [[x % prime for x in row] + [int(i == j) for j in range(size)]
+            for i, row in enumerate(matrix)]
+    for column in range(size):
+        pivot = next((i for i in range(column, size) if work[i][column]), None)
+        need(pivot is not None, "sharp normal basis is singular")
+        work[column], work[pivot] = work[pivot], work[column]
+        scale = pow(work[column][column], -1, prime)
+        work[column] = [scale * x % prime for x in work[column]]
+        for i in range(size):
+            if i != column and work[i][column]:
+                factor = work[i][column]
+                work[i] = [(x - factor * y) % prime for x, y in zip(work[i], work[column])]
+    need(all(row[:size] == [int(i == j) for j in range(size)]
+             for i, row in enumerate(work)), "sharp inverse identity")
+    return [tuple(row[size:]) for row in work]
+
+
+def sharp_fixture(roots, table, a, b, name, prime, merge_proof=False):
+    """Check either the original collapsing control or the sheared sharp fixture."""
+    half = pow(2, -1, prime)
+    scalar_roots = [tuple(half * x % prime for x in root) for root in roots]
+    normals = [scalar_roots[a], scalar_roots[b]]
+    need(scalar_rank(normals, 8, prime) == 2, "sharp pair independence")
+    for coordinate in range(8):
+        axis = tuple(int(i == coordinate) for i in range(8))
+        if scalar_rank(normals + [axis], 8, prime) > len(normals):
+            normals.append(axis)
+    need(len(normals) == 8, "sharp normal basis coverage")
+    dual = inverse(list(zip(*normals)), prime)  # Rows of M^-1 are columns of M^-t.
+    need(all(dot(h, d) % prime == int(i == j)
+             for i, h in enumerate(normals) for j, d in enumerate(dual)), "sharp dot dual")
+
+    def evaluate(normal):
+        return tuple(dot(root, normal) % prime for root in scalar_roots)
+
+    def unit(index):
+        return tuple(int(i == index) for i in range(120))
+
+    units = [unit(a), unit(b)]
+    holes = [tuple((x - half * y) % prime for x, y in zip(unit_column, evaluate(normal)))
+             for unit_column, normal in zip(units, normals[:2])]
+    P = units + holes + [evaluate(h) for h in normals[2:]]
+    readers = [evaluate(d) for d in dual]
+    Q = readers[:2] + [tuple(-x % prime for x in q) for q in readers[:2]]
+    Q += [tuple(half * x % prime for x in q) for q in readers[2:]]
+    if merge_proof:
+        for index in range(2):
+            P[4 + index] = tuple((x + y) % prime for x, y in zip(P[4 + index], units[index]))
+            Q[index] = tuple((x - half * y) % prime
+                             for x, y in zip(readers[index], readers[2 + index]))
+    need(all(any(column) for column in P + Q), "inactive sharp term")
+    ranks = [scalar_rank(zip(*factor), len(factor), prime) for factor in (P, Q)]
+    need(ranks == [10, 8], "sharp factor ranks")
+    weights = [support_weight(support_bits(column), table) for column in P]
+    need(weights == [1, 1, 8, 8] + [9] * 6, "sharp support weights")
+    need(all(support_weight(support_bits(q), table) == 9 for q in Q), "sharp reader weights")
+    costs = factor_copy_costs(P, Q, table)
+    need(costs == weights and sum(costs) == 72, "sharp actual COPY ranks")
+    check_factor_product(P, Q, roots, prime)
+    nonproportional = [pairwise_nonproportional(factor, prime) for factor in (P, Q)]
+    need(nonproportional == [True, merge_proof], "sharp proportionality control")
+
+    clean_P, clean_Q, normalization = normalize_proportional(P, Q, prime)
+    check_factor_product(clean_P, clean_Q, roots, prime)
+    clean_ranks = [scalar_rank(zip(*factor), len(factor), prime) for factor in (clean_P, clean_Q)]
+    clean_costs = factor_copy_costs(clean_P, clean_Q, table)
+    clean_nonproportional = [pairwise_nonproportional(factor, prime) for factor in (clean_P, clean_Q)]
+    need(normalization == {"merges": 0 if merge_proof else 2, "zero_terms_removed": 0},
+         "sharp proportional normalization actions")
+    need(len(clean_P) == (10 if merge_proof else 8), "sharp normalized term count")
+    need(clean_ranks == ([10, 8] if merge_proof else [8, 8]), "sharp normalized ranks")
+    need(clean_nonproportional == [True, True], "sharp normalization did not terminate")
+    need(sum(clean_costs) == 72, "sharp normalization COPY control")
+    if merge_proof:
+        need((clean_P, clean_Q) == (P, Q), "merge-proof factorization was changed by normalization")
+        uncompensated_Q = readers[:2] + Q[2:]
+        need(rejected(lambda: check_factor_product(P, uncompensated_Q, roots, prime)),
+             "omitted reader compensation mutation was accepted")
+    normalization.update({"terms": len(clean_P), "factor_ranks": clean_ranks,
+                          "pairwise_nonproportional": clean_nonproportional,
+                          "term_copy_costs": clean_costs, "copy": sum(clean_costs),
+                          "product_entries_checked": 14400})
+    result = {"prime": prime, "pair_type": name, "indices": [a, b],
+              "variant": "merge_proof" if merge_proof else "collapsing_positive_control",
+              "factor_ranks": ranks, "all_terms_active": True,
+              "pairwise_nonproportional": nonproportional,
+              "term_copy_costs": costs, "copy": sum(costs), "product_entries_checked": 14400,
+              "proportional_normalization": normalization}
+    if merge_proof:
+        result["omitted_reader_compensation_mutation_rejected"] = True
+    return result
+
+
+def run():
+    """Return deterministic finite coverage, classification, and control results."""
+    roots, table = build_model()
+    need(support_weight((1 << 120) - 1, table, False) == 9, "dense COPY rank")
+    a = 0
+    orthogonal = next(i for i in range(1, 120) if dot(roots[a], roots[i]) == 0)
+    nonorthogonal = next(i for i in range(1, 120) if dot(roots[a], roots[i]) != 0)
+    cases = [(orthogonal, "orthogonal", False), (nonorthogonal, "nonorthogonal", True)]
+    code = []
+    for h in product(range(3), repeat=8):
+        first = next((x for x in h if x), 0)
+        if first == 2:
+            continue
+        values = tuple(dot(root, h) % 3 for root in roots)
+        bits = sum(int(x != 0) << i for i, x in enumerate(values))
+        need(support_weight(bits, table) == (9 if first else 0), "codeword support weight")
+        code.append((h, first, values, bits))
+    need(len(code) == 3281, "projective scalar-code coverage")
+    census, planted, fixtures, merge_proof_fixtures = [], [], [], []
+    for b, name, nonorth in cases:
+        need(scalar_rank([root + (int(i == a), int(i == b))
+                          for i, root in enumerate(roots)], 10) == 10, "extension rank")
+        H = [roots[a] + (0, 0), roots[b] + (0, 0),
+             (0,) * 8 + (1, 0), (0,) * 8 + (0, 1)]
+        need(scalar_rank(H, 10) == 4, "four-dimensional low-weight container")
+        low_weight, histogram, pure = [], Counter(), 0
+        for h, first, values, initial in code:
+            cache = {}
+            for s, t in product(range(3), repeat=2):
+                if not first and next((x for x in (s, t) if x), 0) != 1:
+                    continue
+                support = initial
+                for index, value in ((a, s), (b, t)):
+                    if bool(values[index]) != bool((values[index] + value) % 3):
+                        support ^= 1 << index
+                if support not in cache:
+                    cache[support] = support_weight(support, table)
+                w = cache[support]
+                need(w > 0, "nonzero projective vector collapsed")
+                need(w == expected_weight(h, s, t, roots, a, b, 3, nonorth),
+                     "exhaustive F3 sparse-ray classification")
+                histogram[w] += 1
+                if w <= 7:
+                    need(not any(h), "weight at most seven outside pure external plane")
+                    pure += 1
+                if w <= 8:
+                    vector = h + (s, t)
+                    need(scalar_rank(H + [vector], 10) == 4,
+                         "weight at most eight outside H")
+                    low_weight.append((w, vector))
+        count = sum(histogram.values())
+        need(count == 29524, "complete F3 projective extension coverage")
+        prefix = [scalar_rank([v for w, v in low_weight if w <= k], 10) for k in range(9)]
+        need(prefix == [0, 2, 2, 2, 2, 2, 2, 2, 4], "weight-filter rank profile")
+        minimum = sum(10 - rank for rank in prefix)
+        need(minimum == 72, "F3 minimum basis weight")
+        census.append({"pair_type": name, "indices": [a, b], "projective_points": count,
+                       "weight_histogram": {str(k): v for k, v in sorted(histogram.items())},
+                       "prefix_ranks_0_to_8": prefix, "minimum_basis_weight": minimum,
+                       "weight_le7_pure_external_rays": pure,
+                       "weight_le8_rays_in_H": len(low_weight),
+                       "classified_projective_rays": count})
+        for prime in (5, 7):
+            pair_vectors = singleton_vectors = 0
+            for s, t in product(range(1, prime), repeat=2):
+                normals = ((0,) * 8, hole(roots[a], s, prime), hole(roots[b], t, prime))
+                weights = [check_point(h, s, t, roots, table, a, b, prime, nonorth)
+                           for h in normals]
+                need(weights == ([2, 8, 8] if nonorth else [2, 9, 9]),
+                     "planted two-coset deficiencies")
+                pair_vectors += 3
+            for index in (a, b):
+                for coefficient in range(1, prime):
+                    s, t = (coefficient, 0) if index == a else (0, coefficient)
+                    weights = [check_point(h, s, t, roots, table, a, b, prime, nonorth)
+                               for h in ((0,) * 8, hole(roots[index], coefficient, prime))]
+                    need(weights == [1, 8], "planted singleton deficiencies")
+                    singleton_vectors += 2
+            planted.append({"prime": prime, "pair_type": name,
+                            "nonzero_coefficient_pairs": (prime - 1) ** 2,
+                            "two_coset_vectors_checked": pair_vectors,
+                            "singleton_vectors_checked": singleton_vectors})
+        fixtures.extend(sharp_fixture(roots, table, a, b, name, prime) for prime in (3, 5, 7))
+        merge_proof_fixtures.extend(sharp_fixture(roots, table, a, b, name, prime, merge_proof=True)
+                                    for prime in (3, 5, 7))
+    correct_hole = hole(roots[a], 1, 3)
+    controls = {
+        "wrong_nonorthogonal_branch_rejected": rejected(lambda: check_point(
+            correct_hole, 1, 1, roots, table, a, nonorthogonal, 3, False)),
+        "wrong_orthogonal_branch_rejected": rejected(lambda: check_point(
+            correct_hole, 1, 1, roots, table, a, orthogonal, 3, True)),
+        "wrong_hole_factor_two_rejected": rejected(lambda: check_point(
+            hole(roots[a], 1, 3, 2), 1, 0, roots, table, a, nonorthogonal, 3, True, 2)),
+    }
+    need(all(controls.values()), "semantic mutation control was accepted")
+    return {"status": "PASS_SPARSE_PAIR_FINITE_CONTROLS", "root_lines": 120,
+            "binary_copy_rank": 9, "code_projective_points": 3280,
+            "f3_cases": census, "planted_field_checks": planted,
+            "sharp_fixtures": fixtures, "merge_proof_sharp_fixtures": merge_proof_fixtures,
+            "controls": controls}
+
+
+if __name__ == "__main__":
+    print(json.dumps(run(), sort_keys=True))
diff --git a/research/e8-one-coset-deficiency/verify.py b/research/e8-one-coset-deficiency/verify.py
new file mode 100644
index 0000000000..17a61bb5e3
--- /dev/null
+++ b/research/e8-one-coset-deficiency/verify.py
@@ -0,0 +1,229 @@
+#!/usr/bin/env python3
+"""Read-only exact replay of the one-coset theorem's finite inputs and controls.
+
+Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0.
+Use --emit explicitly to replace CERTIFICATE.json and RESULT.json. Normal
+execution writes neither files nor bytecode. This is not an E8 proof assistant.
+"""
+
+import argparse
+from hashlib import sha256
+import json
+from math import factorial
+from pathlib import Path
+import sys
+from types import ModuleType
+
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def canonical_json(value):
+    return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False)
+
+
+def check_receipt(expected, actual):
+    # JSON integer/boolean/float types remain distinct; dict key order does not matter.
+    require(canonical_json(expected) == canonical_json(actual), "RESULT.json differs from replay")
+
+
+def scientific_hashes(certificate_bytes=None):
+    inventory = {}
+    for path in sorted(PACKAGE.rglob("*")):
+        if not path.is_file() or path.name == "RESULT.json" or path.suffix not in (
+                ".py", ".md", ".json", ".lean"):
+            continue
+        require(not path.is_symlink(), "scientific input is a symbolic link")
+        relative = path.relative_to(PACKAGE).as_posix()
+        data = certificate_bytes if relative == "CERTIFICATE.json" and certificate_bytes is not None else path.read_bytes()
+        inventory[relative] = sha256(data).hexdigest()
+    if certificate_bytes is not None:
+        inventory["CERTIFICATE.json"] = sha256(certificate_bytes).hexdigest()
+    return dict(sorted(inventory.items()))
+
+
+def load_source(name):
+    """Execute current source bytes directly; stale .pyc caches cannot replace them."""
+    path = PACKAGE / (name + ".py")
+    module = ModuleType("one_coset_" + name)
+    module.__file__ = str(path)
+    sys.modules[module.__name__] = module
+    exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__)
+    return module
+
+
+def check_sources():
+    sources = json.loads((PACKAGE / "SOURCES.json").read_text())
+    checked = []
+    for row in sources["files"]:
+        if row["usage"] != "input":
+            continue
+        path = ROOT / row["path"]
+        require(sha256(path.read_bytes()).hexdigest() == row["sha256"],
+                "live source pin differs: " + row["path"])
+        checked.append(row["path"])
+    return checked
+
+
+def bind_models(g, first, other):
+    """Match all root lines, scalar orientations and binary label matroids."""
+    standard = g.standard_binding(first)
+    lookup = {g.canonical(row): i for i, row in enumerate(other["roots"])}
+    require(len(lookup) == 120, "independent root lines are not distinct")
+    mapping, signs, basis = [], [], {}
+    for root, label in zip(standard, first["labels"]):
+        key = g.canonical(root)
+        require(key in lookup, "independent root alphabet differs")
+        index = lookup[key]
+        mapping.append(index)
+        signs.append(1 if root == other["roots"][index] else -1)
+        a, b = label, other["labels"][index]
+        while a:
+            pivot = a.bit_length() - 1
+            if pivot in basis:
+                x, y = basis[pivot]
+                a, b = a ^ x, b ^ y
+            else:
+                basis[pivot] = (a, b)
+                break
+        if not a:
+            require(b == 0, "label graph is not a linear map")
+    require(len(set(mapping)) == 120 and len(basis) == 9, "model map is not a full-rank bijection")
+
+    def transport(value):
+        image = 0
+        while value:
+            pivot = value.bit_length() - 1
+            a, b = basis[pivot]
+            value, image = value ^ a, image ^ b
+        return image
+
+    images = [transport(1 << i) for i in range(9)]
+    require(all(g.parity(a & b) == int(i == j) for i, a in enumerate(images)
+                for j, b in enumerate(images)), "label transport does not preserve beta")
+    require(transport(g.OMEGA) == g.OMEGA, "characteristic vector transport")
+    for value in range(512):
+        image = transport(value)
+        require(g.parity(value) == g.parity(image), "parity transport")
+        if not g.parity(value):
+            require((value.bit_count() // 2) % 2 == (image.bit_count() // 2) % 2,
+                    "even quadratic colour transport")
+    for i, root in enumerate(first["roots"]):
+        for j, other_root in enumerate(first["roots"]):
+            product = g.dot(other["roots"][mapping[i]], other["roots"][mapping[j]])
+            require(4 * g.dot(root, other_root) == 9 * signs[i] * signs[j] * product,
+                    "independent scalar Gram isometry")
+    return {"root_bijection": 120, "gram_pairs": 14400, "label_graph_rank": 9,
+            "orthonormal_transport_checks": 81, "binary_vectors_transported": 512,
+            "even_quadratic_colours_transported": 256}
+
+
+def receipt_controls():
+    check_receipt({"count": 1}, {"count": 1})
+    rejected = []
+    for name, value in (("boolean", True), ("float", 1.0), ("string", "1"), ("wrong_integer", 2)):
+        try:
+            check_receipt({"count": value}, {"count": 1})
+        except ValueError:
+            rejected.append(name)
+        else:
+            raise ValueError("receipt type control accepted: " + name)
+    return rejected
+
+
+def run(emit=False):
+    inputs = check_sources()
+    geometry, independent, fixtures, controls, sparse_pair = [
+        load_source(name) for name in ("geometry", "independent", "fixtures", "controls", "sparse_pair")]
+    model = geometry.build_model()
+    if emit:
+        certificate = geometry.make_certificate(model)
+        certificate_bytes = geometry.certificate_text(certificate).encode()
+    else:
+        certificate_bytes = (PACKAGE / "CERTIFICATE.json").read_bytes()
+        certificate = json.loads(certificate_bytes)
+    first = geometry.check_certificate(model, certificate)
+    reflections = geometry.reflection_transport(model)
+    second = independent.run()
+    require(second["single_rank_histogram"] == {"8": 511}, "independent single ranks differ")
+    require(second["pair_rank_histogram"] == {"0": 255, "6": 3360, "7": 35640, "8": 91050},
+            "independent pair ranks differ from the retained census")
+    ordered = forbidden_ordered = 0
+    for counts, a, b in geometry.pair_profiles():
+        orbit = factorial(9)
+        for count in counts:
+            orbit //= factorial(count)
+        ordered += orbit
+        if geometry.forbidden(a, b):
+            forbidden_ordered += orbit
+    require(ordered == 511 * 510 and forbidden_ordered == 2 * second["forbidden_pairs_proved_full_rank"],
+            "profile orbit sizes disagree with the independent exhaustive pairs")
+    other_model = independent.build_model()
+    bound = bind_models(geometry, model, other_model)
+    sparse_roots, sparse_table = sparse_pair.build_model()
+    lookup = {row: i for i, row in enumerate(other_model["roots"])}
+    require(len(sparse_roots) == 120 and set(sparse_roots) == set(lookup),
+            "sparse-pair root alphabet differs from the bound models")
+    mapping = [lookup[row] for row in sparse_roots]
+    for i in range(120):
+        for j in range(120):
+            require(((sparse_table[i] >> j) & 1) == geometry.parity(
+                other_model["labels"][mapping[i]] & other_model["labels"][mapping[j]]),
+                "sparse-pair dense table differs from the bound models")
+    bound["sparse_pair_root_bijection"] = 120
+    bound["sparse_pair_table_entries"] = 14400
+    actual_factors = fixtures.run(geometry, model)
+    fault_controls = controls.run(geometry, model, certificate)
+    result = {
+        "schema_version": 1,
+        "scope": "finite proof inputs and controls for the written all-m one-coset theorem",
+        "live_inputs_authenticated": inputs,
+        "primary_certificate": first,
+        "odd_field_profile_transport": reflections,
+        "independent_exhaustion": second,
+        "profile_orbit_accounting": {"ordered_pairs": ordered, "forbidden_ordered_pairs": forbidden_ordered},
+        "model_binding": bound,
+        "actual_factors": actual_factors,
+        "sparse_pair_evidence": sparse_pair.run(),
+        "integrity_and_hypothesis_controls": fault_controls,
+        "receipt_type_controls": receipt_controls(),
+        "scientific_sha256": scientific_hashes(certificate_bytes if emit else None),
+    }
+    return json.loads(json.dumps(result, sort_keys=True)), certificate_bytes
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--emit", action="store_true", help="explicitly replace both deterministic receipts")
+    args = parser.parse_args()
+    try:
+        expected = None
+        if not args.emit:
+            expected = json.loads((PACKAGE / "RESULT.json").read_text())
+            require(expected["scientific_sha256"] == scientific_hashes(),
+                    "scientific source inventory/hash differs before execution")
+        result, certificate = run(args.emit)
+        if args.emit:
+            (PACKAGE / "CERTIFICATE.json").write_bytes(certificate)
+            (PACKAGE / "RESULT.json").write_text(json.dumps(result, sort_keys=True, indent=2) + "\n")
+        else:
+            check_receipt(expected, result)
+    except (ValueError, RuntimeError, OSError, KeyError, TypeError, IndexError) as error:
+        print("FAIL_E8_ONE_COSET_DEFICIENCY: " + str(error), file=sys.stderr)
+        return 1
+    print("PASS_E8_ONE_COSET_DEFICIENCY minors=109 characters=511 pairs=130305 "
+          "exact_factorizations=8 strict_rank9_equality=72 "
+          "sparse_pair_basis_floor=72 "
+          "normalized_sparse_rank10_equality=72 "
+          "scope=written-proof-inputs-and-controls")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())