diff --git a/research/dn-unrestricted-root-code-floor/DEPENDENCY.json b/research/dn-unrestricted-root-code-floor/DEPENDENCY.json
new file mode 100644
index 0000000000..977947e004
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/DEPENDENCY.json
@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "repository": "CrocSwap/integer-mult-bounds",
+  "files": [
+    {
+      "head": "5ccad6aa04409ee2805d5638aa0fc84c76bbb881",
+      "author": "Aaron Wang with opencode",
+      "pr": 2518,
+      "path": "research/polar-law-t7-overcomplete-screen/search.py",
+      "retained": "references/PR2518-search.py",
+      "sha256": "c0335db5753be6535b25ece1dc14ed61e7688f20ce17180a4316a172e23d47fd",
+      "git_blob": "019540d5a75b17a606007131cb87e6181934fad5"
+    },
+    {
+      "head": "5ccad6aa04409ee2805d5638aa0fc84c76bbb881",
+      "author": "Aaron Wang with opencode",
+      "pr": 2518,
+      "path": "research/polar-law-t7-overcomplete-screen/README.md",
+      "retained": "references/PR2518-README.md",
+      "sha256": "ed9c61d8616fa4bc86a9d28d66f49aa774ef25fe56a4e3c895b69bf784e7880f",
+      "git_blob": "3d7a42855310f5251452bdb003300275b538efc3"
+    },
+    {
+      "head": "ca7f99921f03398d303bba90245d3ee2e38e95c3",
+      "author": "DreamingOfClouds",
+      "pr": 2277,
+      "path": "research/overcomplete-and-realisation-floors/README.md",
+      "retained": "references/PR2277-README.md",
+      "sha256": "1a11f33a8d358479cae0f39018fa9ebd3d439790cd1872de91d109fd4d23a088",
+      "git_blob": "02660b10d4f48cd39db3416def50cd944aef4ac9"
+    }
+  ]
+}
diff --git a/research/dn-unrestricted-root-code-floor/README.md b/research/dn-unrestricted-root-code-floor/README.md
new file mode 100644
index 0000000000..21f57857e1
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/README.md
@@ -0,0 +1,244 @@
+# Full D_n root-code decoders cannot beat n(n-1)
+
+For every n >= 4, over every field K of characteristic other than two,
+the full dense D_n root-code Gram decoder has minimum algebraic rank cost
+**n(n-1)**, even when an arbitrary finite number of rank-one terms is allowed.
+The coordinate Gram expansion attains the floor. Every optimal expansion
+has exactly n nonzero terms. This does not classify its possible bases.
+
+The decision is to retire attempts to improve the coordinate bill by adding
+terms in this precise full-root-code model. Sparse pairings, punctures,
+factors outside the root code and different realizations change the premise.
+This is a written uniform proof with finite cross-checks, not a new physical
+decoder, Lean theorem, supplier or multiplication bound.
+
+## Priority and exact source contract
+
+DreamingOfClouds's [PR2228](https://github.com/CrocSwap/integer-mult-bounds/pull/2228)
+already settles D4 and D6 at every term count, and establishes the support
+deficiency method. Their [PR2277](https://github.com/CrocSwap/integer-mult-bounds/pull/2277)
+at `ca7f99921f03398d303bba90245d3ee2e38e95c3` settles D5 at every term count
+and supplies the overcomplete coupling lemma used below. Those individual
+floors and the coupling lemma retain that priority. Aaron Wang's
+[PR2518](https://github.com/CrocSwap/integer-mult-bounds/pull/2518) at
+`5ccad6aa04409ee2805d5638aa0fc84c76bbb881` gives the exact D generator and
+bounded overcomplete searches. Its generator uses twice the roots below;
+this common nonzero scale changes neither supports nor the argument.
+
+Our earlier [PR2659](https://github.com/CrocSwap/integer-mult-bounds/pull/2659)
+addresses only a fixed-coordinate one-extra update family. The present
+result allows arbitrary factors and arbitrary finite term counts in every
+dimension n >= 4. PR2582's uniform B_n/C_n proof concerns different roots;
+we do not count those floors again. The new contribution is the uniform
+D_n support classification and its all-term conclusion, including the
+odd-dimensional case where an unmatched axis term is cheaper.
+
+Original PR2277 and PR2518 READMEs and the unchanged PR2518 generator are
+retained with exact head, blob and SHA-256 pins in `DEPENDENCY.json`.
+Authentication precedes extracting only the source's canon/lines/D functions.
+No modified upstream file or selected record is used.
+
+Let R have one row r_(ij,+)=e_i+e_j and r_(ij,-)=e_i-e_j for every i<j.
+There are v=n(n-1) rows. The fixed binary matrix B has a one on its diagonal
+and between orthogonal real root lines, and zero elsewhere. This definition
+uses the integer root pattern even if K has positive characteristic.
+An allowed expansion is
+
+    R R^T = sum_j (R x_j) (R y_j)^T,    x_j,y_j in K^n,
+    cost = sum_j rank_F2 B[supp(R x_j), supp(R y_j)].
+
+The transpose is bilinear, not Hermitian. Zero outer factors may be removed;
+m always counts nonzero terms. Since 2 is invertible, the two signs on an
+edge span its coordinate axes, so R has full column rank. Left and right
+inverses show that exactness is equivalent to sum_j x_j y_j^T=I_n.
+The same theorem holds after fixed invertible diagonal scaling of the rows
+and the corresponding Gram matrix. Neither arbitrary non-root-code factors
+nor a changed binary mask is covered.
+
+## Binary support classification
+
+Both signs on an edge have the same B row. Deleting repeated rows/columns
+preserves binary rank. Put
+
+    E = {s in F2^n : sum_i s_i=0},  L=F2 direct-sum E,
+    u_ij=(1,e_i+e_j),  Omega((a,s),(b,t))=a b+s dot t.
+
+Then B is the Omega Gram matrix of the edge labels: its entry is one for
+equal/disjoint edges and zero for distinct edges sharing one vertex.
+The labels span L: the sum of a triangle's three labels is (1,0), and
+adding that vector to each label gives (0,e_i+e_j), which span E.
+The radical of Omega on L is zero for odd n, and is generated by
+(0,(1,...,1)) for even n. Consequently
+
+    h=rank_F2 B = n (n odd), or n-1 (n even).
+
+Work in the nondegenerate quotient V=L/rad(Omega). Its binary code consists
+of c_(a,s)(ij,+)=c_(a,s)(ij,-)=a+s_i+s_j with s in E, modulo the radical.
+For a root-code support S, let delta(S) be the dimension of codewords
+vanishing on S. Equivalently it is the codimension in V of span{u_e:e in S}.
+
+For x nonzero, a codeword c vanishes on supp(Rx) precisely when every edge
+with c(e)=1 has both x_i+x_j=0 and x_i-x_j=0. These equations force
+x_i=x_j=0. Thus every nonzero coordinate of x must be an isolated vertex
+of the graph whose edges satisfy c(e)=1.
+
+Suppose vertex i is isolated. For j != i, s_j=a+s_i. If a=0 then all s_j
+are equal and c is the zero codeword. If a=1 then c is the complete graph
+on the other n-1 vertices, with i its unique isolated vertex. The condition
+s in E permits this exactly when n is odd: it forces s_i=0 and all other
+s_j=1. (For even n the parity is always one.) Therefore
+
+* Even n: delta(supp(Rx))=0 for every nonzero x.
+* Odd n: delta(supp(Rx))=1 exactly when x is a nonzero coordinate-axis
+  vector; it is zero otherwise. For each axis the deficient code space
+  has exactly one nonzero word.
+
+For two supports S,T, nondegeneracy gives
+
+    rank B[S,T] >= h-delta(S)-delta(T).
+
+Indeed the left-label span has dimension h-delta(S); the kernel of its
+pairing with the right-label span lies in the latter's annihilator, of
+dimension delta(T). This also proves that when both deficiencies are zero
+the rectangle has rank h.
+
+For odd n the exact term costs are:
+
+| x,y | rank cost |
+|---|---:|
+| Neither is an axis | n |
+| Exactly one is an axis | n-1 |
+| Both lie on the same axis | n-1 |
+| They lie on distinct axes | n-2 |
+
+An axis support compresses to its n-1 incident edges. Its principal
+rectangle is I_(n-1), giving the first relevant upper bound and same-axis
+value. For two distinct axes, put their common edge first. The rectangle
+is 1 direct-sum (I_(n-2)+J_(n-2)). When n is odd, n-2 is odd, and the
+second block has precisely the all-ones kernel. This gives n-2. For even
+n every nonzero term instead has rank n-1 by the zero-deficiency result.
+
+## All numbers of terms
+
+Rank of the exact sum forces m>=n. Even n is immediate: every nonzero term
+costs n-1, so the total is m(n-1), strictly above the floor if m>n.
+
+Now let n be odd, hence n>=5. Call a term *cheap* when its cost is n-2.
+The table says these are exactly x_i=alpha_i e_(a_i),
+y_i=beta_i e_(b_i), with a_i != b_i and both scalars nonzero.
+
+If m=n, write X=[x_1 ... x_n] and Y=[y_1 ... y_n]. Exactness gives
+X Y^T=I, hence Y^T X=I. In particular y_i dot x_i=1, excluding cheap
+terms. The total is at least n(n-1).
+
+If m=n+1, use the credited overcomplete coupling lemma from PR2277:
+for K=Y^T X there are column vectors u,w such that
+
+    I-K=u w^T,  w^T u=1.
+
+For completeness, K is idempotent of rank n: X K=X and X has rank n.
+Thus I-K has rank one. A nonzero column factors it as u w^T, and its
+idempotence implies w^T u=1. For a cheap index i, K_ii=0, so u_i w_i=1.
+For distinct cheap indices i,j this forces K_ij=-u_i w_j != 0. But
+K_ij=y_i dot x_j is nonzero only if b_i=a_j. Three cheap indices i,j,k
+would give a_j=b_i=a_k and a_i=b_j=a_k, making a_i=b_i, a contradiction.
+There are therefore at most two cheap terms. Every other term costs at
+least n-1, and the total is at least
+
+    (n+1)(n-1)-2 = n^2-3 > n(n-1).
+
+If m>=n+2, even the crude per-term floor gives
+
+    m(n-2) >= (n+2)(n-2) = n^2-4 > n(n-1).
+
+Finally, x_i=y_i=e_i gives n principal star rectangles I_(n-1), attaining
+n(n-1). All inequalities for m>n are strict, as claimed. The one-extra
+bound n^2-3 is only a sufficient lower bound, not an asserted exact minimum.
+The n>=4 restriction matters to this proof: for n=3 its last displayed
+count is only 5<6. No counterexample or all-term statement for D3 is claimed.
+
+## Evidence and falsification
+
+The written proof establishes arbitrary dimension, field and term count.
+`RESULT.json` records bounded, exact checks of the actual source-generated
+roots, binary label/radical and support ranks, and exact Gram expansions.
+The checks enumerate every label codeword for n=4..12, compare 583,115
+support pairs over Q, F3 and F5 for n=4..7, and replay 366 exact expansions
+for n=4..9. These include nonintegral reciprocal factor scalings, mixed
+bases, cancelling cheap terms, and actual one-extra words with two cheap
+terms. The independent checker covers 1,482 axis rectangles for n=4..16
+and 208,348 possible cheap-triple extensions for n=3..16.
+The primary checker uses bit-vector binary elimination and actual root
+evaluations. The independent checker constructs the mask directly from
+edge intersections and uses a separate matrix elimination routine; it also
+enumerates the necessary axis relations for hypothetical cheap triples.
+Neither treats a finite search as proof of the uniform theorem.
+
+Controls demonstrate that characteristic two destroys the root-code
+injection, sparse identity masks change the term tariff, unmatched axes
+really are cheaper, an inexact cheap term does not supply I, and the
+small-dimensional counting boundary cannot be silently generalized.
+Export tests check optimized Git-free replay, source corruption rejection,
+typed receipt mismatch and refusal to overwrite an existing output.
+
+From the repository root, standard-library Python 3.12:
+
+```sh
+python3 -I -B scripts/research_package.py --package research/dn-unrestricted-root-code-floor
+python3 -I -B scripts/research_package.py --package research/dn-unrestricted-root-code-floor --check-only
+```
+
+Default verification compares the complete typed receipt and writes no
+files. `python3 -I -B research/dn-unrestricted-root-code-floor/verify.py
+--output NEW.json` creates a new receipt and refuses an existing path.
+The package works without Git when exported with its declared input.
+No Lean replay, native circuit replay or selected full cold replay is claimed.
+
+## Family decision and obligation ledger
+
+The priority-5 picker first selected P104-side-correction on main
+`6bd33bc0b87a01e9c9d8b1c01576f3ddbcaee850`; its binding baseline passed.
+`TASK.json` records the changed assignment to the suggested decoder-bound
+track after crowded P104 obligations were checked. The precise question
+is an all-dimension/full-code rejection, not another seeded search.
+
+The final checkpoint fetched canonical main `c3c94c2ea2ebcd5d69d1e51b5fe8a36bf79819f5`;
+guidance, family gate and selected record were unchanged. Both scientific
+predecessor heads above were rechecked unchanged. Overlap coverage included
+767 open PRs at 18:06Z and 1,239 Discussion records at 15:22Z on 2026-10-15,
+plus the newest 100 open PRs checked at 18:16Z and retained local notes.
+Later Discussion claims and arbitrary code diffs are not covered; absence
+of a search match is not a novelty certificate. Coordination is recorded
+on [PR2277](https://github.com/CrocSwap/integer-mult-bounds/pull/2277#issuecomment-6198818270).
+
+**Decision: reject improvements inside this full dense root-code family.**
+The floor already equals the number of ports. Overcomplete factors cannot
+save its algebraic rank mass. Stop larger searches in this same family;
+reopen only with a stated changed mask, root set, factor space or realization.
+
+| Obligation | Status |
+|---|---|
+| Exact root-code Gram identity | The hypothesis sum xy^T=I is necessary and sufficient |
+| Every term's binary rank charge | Proved uniformly; no omitted zero/cheap terms |
+| Arbitrary finite term count | Proved; nonzero optimum uses exactly n terms |
+| Source generator and predecessor binding | Pinned and authenticated |
+| Physical frames, dirty restoration, hosting, precision, all-size budget | Not supplied; unknown, not zero |
+| Changed global kappa or selected frontier | None |
+
+The next consumer is a researcher considering dense-root-code synthesis:
+use this result to rule out that family before paying for a larger census.
+The algebraic result alone makes no runtime or physical allocation claim.
+
+## Open next questions
+
+Which specific punctured or sparse D_n pairing changes this floor enough
+to survive a fully charged decoder/hosting budget? First identify a mask
+outside the full dense theorem and a complete intended consumer; do not
+reuse its full-mask tariff after removing constraints. Physical admissibility
+and the complete downstream cost remain unresolved here.
+
+Prepared for ywz65 with substantial OpenAI Codex assistance. DreamingOfClouds
+retains priority for the deficiency method, overcomplete coupling lemma and
+the D4/D5/D6 all-term results; Aaron Wang with opencode retains credit for
+the PR2518 generator and finite screens. Copied artifacts retain their
+original attribution and Apache-2.0 provenance.
diff --git a/research/dn-unrestricted-root-code-floor/RESULT.json b/research/dn-unrestricted-root-code-floor/RESULT.json
new file mode 100644
index 0000000000..a4d328ce5a
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/RESULT.json
@@ -0,0 +1,3442 @@
+{
+  "status": "PASS_DN_UNRESTRICTED_ROOT_CODE_FLOOR",
+  "binary_code_checks": [
+    {
+      "n": 4,
+      "roots": 12,
+      "binary_rank": 3,
+      "codewords": 8,
+      "isolated_classes": 0
+    },
+    {
+      "n": 5,
+      "roots": 20,
+      "binary_rank": 5,
+      "codewords": 32,
+      "isolated_classes": 5
+    },
+    {
+      "n": 6,
+      "roots": 30,
+      "binary_rank": 5,
+      "codewords": 32,
+      "isolated_classes": 0
+    },
+    {
+      "n": 7,
+      "roots": 42,
+      "binary_rank": 7,
+      "codewords": 128,
+      "isolated_classes": 7
+    },
+    {
+      "n": 8,
+      "roots": 56,
+      "binary_rank": 7,
+      "codewords": 128,
+      "isolated_classes": 0
+    },
+    {
+      "n": 9,
+      "roots": 72,
+      "binary_rank": 9,
+      "codewords": 512,
+      "isolated_classes": 9
+    },
+    {
+      "n": 10,
+      "roots": 90,
+      "binary_rank": 9,
+      "codewords": 512,
+      "isolated_classes": 0
+    },
+    {
+      "n": 11,
+      "roots": 110,
+      "binary_rank": 11,
+      "codewords": 2048,
+      "isolated_classes": 11
+    },
+    {
+      "n": 12,
+      "roots": 132,
+      "binary_rank": 11,
+      "codewords": 2048,
+      "isolated_classes": 0
+    }
+  ],
+  "support_pair_checks": [
+    {
+      "n": 4,
+      "field": "Q",
+      "supports": 52,
+      "pairs": 2704
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "supports": 33,
+      "pairs": 1089
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "supports": 52,
+      "pairs": 2704
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "supports": 137,
+      "pairs": 18769
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "supports": 67,
+      "pairs": 4489
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "supports": 137,
+      "pairs": 18769
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "supports": 253,
+      "pairs": 64009
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "supports": 118,
+      "pairs": 13924
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "supports": 253,
+      "pairs": 64009
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "supports": 422,
+      "pairs": 178084
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "supports": 191,
+      "pairs": 36481
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "supports": 422,
+      "pairs": 178084
+    }
+  ],
+  "factorizations": [
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "Q",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F3",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 4,
+      "cheap_terms": 0,
+      "cost": 12
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 15
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 18
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 4,
+      "field": "F5",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 20
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 20
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 20
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 22
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 22
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 25
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 26
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 25
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 28
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 29
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 31
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 32
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 33
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 32
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 34
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 36
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 36
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 37
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 38
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 20
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 20
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 20
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 21
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 23
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 25
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 25
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 27
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 26
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 27
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 32
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 32
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 33
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 1,
+      "cost": 34
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 36
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 38
+    },
+    {
+      "n": 5,
+      "field": "F3",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 36
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 20
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 20
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 20
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 22
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 5,
+      "cheap_terms": 0,
+      "cost": 22
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 25
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 26
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 26
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 27
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 26
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 32
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 32
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 36
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 37
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 36
+    },
+    {
+      "n": 5,
+      "field": "F5",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 38
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "Q",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F3",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 6,
+      "cheap_terms": 0,
+      "cost": 30
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 35
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 40
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 6,
+      "field": "F5",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 45
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 44
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 44
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 49
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 50
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 50
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 51
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 52
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 57
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 57
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 59
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 58
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 64
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 64
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 66
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 67
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 43
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 44
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 49
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 49
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 50
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 51
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 52
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 57
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 58
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 57
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 59
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 64
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 65
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 66
+    },
+    {
+      "n": 7,
+      "field": "F3",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 65
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 42
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 7,
+      "cheap_terms": 0,
+      "cost": 43
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 49
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 50
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 51
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 51
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 53
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 58
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 59
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 60
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 64
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 65
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 66
+    },
+    {
+      "n": 7,
+      "field": "F5",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 67
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "Q",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F3",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 8,
+      "cheap_terms": 0,
+      "cost": 56
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 63
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 70
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 8,
+      "field": "F5",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 77
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 73
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 81
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 82
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 82
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 83
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 84
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 90
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 91
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 92
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 92
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 94
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 99
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 100
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 101
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 102
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 103
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 73
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 73
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 81
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 82
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 82
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 84
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 85
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 90
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 91
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 92
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 93
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 93
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 99
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 100
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 101
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 102
+    },
+    {
+      "n": 9,
+      "field": "F3",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 102
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 0,
+      "shears": 0,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 0,
+      "shears": 1,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 0,
+      "shears": 2,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 0,
+      "shears": 3,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 72
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 0,
+      "shears": 4,
+      "nonzero_terms": 9,
+      "cheap_terms": 0,
+      "cost": 74
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 1,
+      "shears": 0,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 81
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 1,
+      "shears": 1,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 82
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 1,
+      "shears": 2,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 82
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 1,
+      "shears": 3,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 83
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 1,
+      "shears": 4,
+      "nonzero_terms": 10,
+      "cheap_terms": 0,
+      "cost": 84
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 2,
+      "shears": 0,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 90
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 2,
+      "shears": 1,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 91
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 2,
+      "shears": 2,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 92
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 2,
+      "shears": 3,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 93
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 2,
+      "shears": 4,
+      "nonzero_terms": 11,
+      "cheap_terms": 0,
+      "cost": 92
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 3,
+      "shears": 0,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 99
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 3,
+      "shears": 1,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 100
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 3,
+      "shears": 2,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 101
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 3,
+      "shears": 3,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 102
+    },
+    {
+      "n": 9,
+      "field": "F5",
+      "extra": 3,
+      "shears": 4,
+      "nonzero_terms": 12,
+      "cheap_terms": 0,
+      "cost": 102
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "fixture": "cancelling_unmatched_axes",
+      "nonzero_terms": 7,
+      "cheap_terms": 2,
+      "cost": 26
+    },
+    {
+      "n": 5,
+      "field": "Q",
+      "fixture": "one_extra_two_cheap",
+      "nonzero_terms": 6,
+      "cheap_terms": 2,
+      "cost": 23
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "fixture": "cancelling_unmatched_axes",
+      "nonzero_terms": 9,
+      "cheap_terms": 2,
+      "cost": 52
+    },
+    {
+      "n": 7,
+      "field": "Q",
+      "fixture": "one_extra_two_cheap",
+      "nonzero_terms": 8,
+      "cheap_terms": 2,
+      "cost": 47
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "fixture": "cancelling_unmatched_axes",
+      "nonzero_terms": 11,
+      "cheap_terms": 2,
+      "cost": 86
+    },
+    {
+      "n": 9,
+      "field": "Q",
+      "fixture": "one_extra_two_cheap",
+      "nonzero_terms": 10,
+      "cheap_terms": 2,
+      "cost": 79
+    }
+  ],
+  "controls": [
+    "characteristic_two_root_kernel",
+    "unmatched_axis_cheaper",
+    "matched_axis_not_cheap",
+    "sparse_mask_changes_tariff",
+    "inexact_cheap_term",
+    "wrong_parity_rank",
+    "n3_count_boundary"
+  ],
+  "scope": "finite cross-checks of written all-n>=4, all-finite-m root-code theorem; no native or formal verification"
+}
diff --git a/research/dn-unrestricted-root-code-floor/SOURCES.json b/research/dn-unrestricted-root-code-floor/SOURCES.json
new file mode 100644
index 0000000000..d26a3d9a39
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "6bd33bc0b87a01e9c9d8b1c01576f3ddbcaee850",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6",
+      "git_blob": "889b95d936746df124872133ae1e7cc339adcb92"
+    },
+    {
+      "path": "docs/research/research-family-status.md",
+      "usage": "provenance",
+      "sha256": "c37c7e0f6a1134983990e1b3efef55e65239b38be780e8a4cc10f5aefdaf2df5",
+      "git_blob": "1a2195004c5d681679279f0095b7964fb14a01e6"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11"
+    }
+  ]
+}
diff --git a/research/dn-unrestricted-root-code-floor/TASK.json b/research/dn-unrestricted-root-code-floor/TASK.json
new file mode 100644
index 0000000000..1dd6d7e47d
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/TASK.json
@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "p104-side-correction",
+  "priority_revision": 5,
+  "base_commit": "6bd33bc0b87a01e9c9d8b1c01576f3ddbcaee850",
+  "original_card": {
+    "id": "p104-side-correction",
+    "question": "Which unresolved physical correction, endpoint transport or hosting obligation in a pinned P104 follow-up can be closed or decisively rejected?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/p104-native-channel/README.md",
+      "research/p104-native-channel/PROOF.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct one side-correction word at an explicit chronological cut with the needed frames still available.",
+      "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget."
+    ],
+    "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the P104 row in research-family-status.md and its exact pending source heads before choosing a task. #1991 is the reviewed channel; #2586 is a pending physical dual with explicit added transport costs, not an admitted supplier.",
+      "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."
+    },
+    "first_experiment": "Check live claims, pin the chosen follow-up and reproduce only the evidence needed for one unresolved obligation. Compare its complete correction/transport/hosting invoice with the target budget; test legal chronological access. Do not rebuild #1991 or assume #2586 has solved global admission.",
+    "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.",
+    "allowed_variations": [
+      "One correction factorization, one chronological cut, or one explicit hosting obstruction.",
+      "A changed correction schedule with an updated full bill and native frame contract."
+    ],
+    "scope_change_triggers": [
+      "Recompiling the already certified low-rank channel without closing a new obligation.",
+      "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.",
+      "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation."
+    ],
+    "overlap_terms": [
+      "P104",
+      "I-G/2",
+      "side correction",
+      "native channel",
+      "1972",
+      "1991",
+      "2586",
+      "endpoint transport",
+      "physical dual",
+      "relay composition"
+    ]
+  },
+  "picker_nonce": "bf095ac9ae4e910ba34716fd4e7bc7f8",
+  "scope_status": "changed",
+  "actual_scope": "Prove the full dense D_n root-code algebraic cost floor uniformly for every n>=4, arbitrary characteristic-not-two field and arbitrary finite term count.",
+  "scope_change_reason": "After reproducing the binding baseline and checking crowded P104 corrections, narrowed the suggested decoder-bound track to the missing uniform D_n support classification and all-term floor. This is a rejection result, not a new physical construction.",
+  "bottleneck_link": "Stops larger overcomplete searches inside a full root-code family whose exact rank mass can never beat its coordinate bill; any renewed construction must change a stated premise.",
+  "budget_minutes": 90,
+  "stop_rule": "Stop after the uniform proof, source-pinned finite cross-checks and effective counterexamples; do not extend to punctures or physical supplier admission.",
+  "outcome": "completed",
+  "evidence": "README proof; RESULT.json; separate edge-intersection/cheap-triple checker and Git-free controls.",
+  "author": "ywz65",
+  "ai_assistance": "Substantial OpenAI Codex assistance; DreamingOfClouds and Aaron Wang with opencode retain predecessor priority and credit.",
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/2277#issuecomment-6198818270",
+  "open_questions": [
+    {
+      "question": "Which explicit changed mask/root set/factor space escapes the uniform D_n floor with a complete favorable bill?",
+      "why_it_matters": "The full dense root-code model cannot save algebraic rank mass.",
+      "first_step": "Specify a pinned changed premise and intended physical consumer before searching.",
+      "blocked_by": "No changed candidate with physical frames/restoration/hosting and full budget is supplied."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "c3c94c2ea2ebcd5d69d1e51b5fe8a36bf79819f5",
+    "checked_utc": "2026-10-15T18:16:18Z",
+    "relevant_changes": "Guidance, family gate, selected record and both scientific predecessor heads unchanged; actual start base retained."
+  },
+  "overlap": {
+    "open_pr_records": 767,
+    "open_pr_fetched_utc": "2026-10-15T18:06:42Z",
+    "discussion_records": 1239,
+    "discussion_fetched_utc": "2026-10-15T15:22:22Z",
+    "targeted_rest": "Latest100 open PRs at18:16Z; PR2277/2518 heads rechecked unchanged.",
+    "limits": "Later Discussion claims and arbitrary code diffs not covered; no-match is not novelty proof."
+  }
+}
diff --git a/research/dn-unrestricted-root-code-floor/VERIFY.json b/research/dn-unrestricted-root-code-floor/VERIFY.json
new file mode 100644
index 0000000000..5fb80680c9
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/VERIFY.json
@@ -0,0 +1,39 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Authenticate original roots/READMEs; actual binary support ranks, exact Gram factorizations and semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent edge-intersection mask and dense elimination, coordinate attainment and cheap-triple relations."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/exportchecks.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Optimized Git-free read-only replay; source mutation, typed receipt and existing-output failures."
+    }
+  ]
+}
diff --git a/research/dn-unrestricted-root-code-floor/exportchecks.py b/research/dn-unrestricted-root-code-floor/exportchecks.py
new file mode 100644
index 0000000000..bedc39249e
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/exportchecks.py
@@ -0,0 +1,54 @@
+#!/usr/bin/env python3
+"""Git-free, optimized and failure-path public CLI controls."""
+import hashlib
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+
+HERE=Path(__file__).resolve().parent
+
+
+def require(x,message):
+    if not x:raise ValueError(message)
+
+
+def snapshot(root):
+    return {str(p.relative_to(root)):hashlib.sha256(p.read_bytes()).hexdigest()
+            for p in root.rglob('*') if p.is_file()}
+
+
+def run(package,*extra):
+    return subprocess.run([sys.executable,'-I','-B','-O',str(package/'verify.py'),*extra],
+                          cwd=package.parent,capture_output=True,text=True,timeout=300)
+
+
+def main():
+    with tempfile.TemporaryDirectory(prefix='dn-unrestricted-export-') as tmp:
+        root=Path(tmp)
+        package=root/'research'/HERE.name
+        shutil.copytree(HERE,package)
+        before=snapshot(root)
+        result=run(package)
+        require(result.returncode==0 and 'PASS_DN_UNRESTRICTED_ROOT_CODE_FLOOR' in result.stdout,'optimized Git-free replay: '+result.stderr)
+        require(snapshot(root)==before,'read-only export')
+        result=run(package,'--output',str(package/'RESULT.json'))
+        require(result.returncode!=0 and 'output already exists' in result.stderr,'overwrite rejection')
+        source=package/'references/PR2518-search.py'
+        saved=source.read_bytes();source.write_bytes(saved+b'\nraise RuntimeError("must not execute")\n')
+        result=run(package)
+        require(result.returncode!=0 and 'source SHA256:' in result.stderr and 'must not execute' not in result.stderr,'source fails before extraction')
+        source.write_bytes(saved)
+        receipt=package/'RESULT.json';saved=receipt.read_bytes();bad=json.loads(saved)
+        bad['binary_code_checks'][0]['binary_rank']=float(bad['binary_code_checks'][0]['binary_rank'])
+        receipt.write_text(json.dumps(bad),encoding='utf-8')
+        result=run(package)
+        require(result.returncode!=0 and 'typed receipt mismatch' in result.stderr,'typed receipt rejection')
+        receipt.write_bytes(saved)
+        require(snapshot(root)==before,'mutants restored')
+    print('PASS_DN_GITFREE_EXPORT: optimized read-only; source, typed receipt and overwrite controls')
+
+
+if __name__=='__main__':main()
diff --git a/research/dn-unrestricted-root-code-floor/independent.py b/research/dn-unrestricted-root-code-floor/independent.py
new file mode 100644
index 0000000000..19de587c44
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/independent.py
@@ -0,0 +1,69 @@
+#!/usr/bin/env python3
+"""Separate dense-elimination checks, without importing the primary checker."""
+from itertools import combinations, permutations
+
+
+def require(x, message):
+    if not x:
+        raise ValueError(message)
+
+
+def rank2(matrix):
+    rows = [list(row) for row in matrix]
+    if not rows:
+        return 0
+    n = len(rows[0])
+    pivot = 0
+    for col in range(n):
+        candidates = [i for i in range(pivot, len(rows)) if rows[i][col]]
+        if not candidates:
+            continue
+        i = candidates[0]
+        rows[pivot], rows[i] = rows[i], rows[pivot]
+        for j in range(len(rows)):
+            if j != pivot and rows[j][col]:
+                rows[j] = [(a + b) % 2 for a, b in zip(rows[j], rows[pivot])]
+        pivot += 1
+        if pivot == len(rows):
+            break
+    return pivot
+
+
+def main():
+    rectangles = 0
+    for n in range(4, 17):
+        edges = list(combinations(range(n), 2))
+        mask = [[int(len(set(e).intersection(f)) != 1) for f in edges] for e in edges]
+        require(rank2(mask) == n - int(n % 2 == 0), 'edge mask rank')
+        for a in range(n):
+            s = [i for i, edge in enumerate(edges) if a in edge]
+            for b in range(n):
+                t = [j for j, edge in enumerate(edges) if b in edge]
+                actual = [[mask[i][j] for j in t] for i in s]
+                want = n - 1 - int(n % 2 == 1 and a != b)
+                require(rank2(actual) == want, 'axis rectangle')
+                rectangles += 1
+        bill = sum(rank2([[mask[i][j] for j, f in enumerate(edges) if a in f]
+                          for i, e in enumerate(edges) if a in e]) for a in range(n))
+        require(bill == n * (n - 1), 'coordinate expansion attainment')
+    # Enumerate all possible cheap first/second terms and force the coordinates
+    # of a third from the required nonzero cross pairings. No support-rank code.
+    triple_attempts = 0
+    for n in range(3, 17):
+        axes = list(permutations(range(n), 2))
+        for a, b in axes:
+            for c, d in axes:
+                if b != c or d != a:
+                    continue
+                for e, f in axes:
+                    triple_attempts += 1
+                    require(not (b == e and f == a and d == e and f == c), 'three cheap axes falsely compatible')
+    # Detect realistic broken independent implementations.
+    require(rank2([[1, 1], [1, 1]]) == 1, 'binary duplicate-row control')
+    require(rank2([[0, 1, 1], [1, 0, 1], [1, 1, 0]]) == 2, 'odd I+J kernel control')
+    require(rank2([[0, 1], [1, 0]]) == 2, 'even I+J invertibility control')
+    print('PASS_DN_INDEPENDENT_EDGE_PROOF_CHECKS', rectangles, 'rectangles;', triple_attempts, 'cheap-triple attempts; 3 controls')
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/dn-unrestricted-root-code-floor/references/PR2277-README.md b/research/dn-unrestricted-root-code-floor/references/PR2277-README.md
new file mode 100644
index 0000000000..02660b10d4
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/references/PR2277-README.md
@@ -0,0 +1,190 @@
+# Dense-pairing floors for overcomplete root-code decoders (E6 36, D5 20, every m) and for every rank-T realisation (E8 72, E7 49, D6 30, D4 12, P104 56), with a correction to Conjecture ID (a) (no κ claim)
+
+> **Scope, stated first.** This package is about the **algebraic cost** `Σ_j rank_F2 B[R_j, A_j]` of exact decoders of root units (and punctured root units) in the model of #446 / #595 / #1590 / #2111 / #2125 / #2228. It proves lower bounds **in stated classes** and one **correction** to a conjecture of ours. It contains **no κ claim, no window closed, no new supplier, no copy / hosting / restoration cost**, and it says nothing about decoders whose factors leave the column space of the realisation, about realisations of rank above T, or (except where a SAT statement says so) about pairings B other than the dense one. Every statement carries one of the labels below; every scope is spelled out in §2.
+>
+> **Labels.** **PROVEN** (full proof in this README); **CHECKED** (recomputed by `verify.sh`, exact integer / `Fraction` / bit arithmetic, or SAT with a DRAT proof that `drat-trim` verifies); **RECORDED** (a number of another PR or of the author's working notes, or a solver verdict whose proof is not shipped, not re-run here; for SAT items, "RECORDED: DRAT-verified at generation" means `verify.sh` regenerates the CNFs and checks their sha256 hashes and the recorded verdicts, while the DRAT proofs themselves are regenerable with `sat/run.py solve` but are not shipped); **OPEN**.
+>
+> **Correction (read this first).** Conjecture ID of #2228 §6, branch (a), says that for an *odd geometry* (an integral normalisation with unit diagonal exists) the optimal cost is `v`. **That branch is false when the number of terms is unbounded**: the 120-line unit "all lines pairwise orthogonal" with `M = I` has an exact decoder of cost **72 < 120** (§3, **PROVEN + CHECKED**). The values of Conjecture ID for the nine even root units are untouched, and #2228's Theorem 1 and Corollary 2.2 are not contradicted (their hypothesis is that all lines survive); but "odd geometry ⇒ cost* = v" and the framing of "geometry" as an invariant of the cost are wrong in the any-number-of-terms model. §3 gives the repaired statement `cost*(U) = min over admissible B of c(B)`.
+
+## 0. Reading this package
+
+```sh
+bash research/overcomplete-and-realisation-floors/verify.sh /fresh/output/dir     # from a checkout or `git archive`; Python >= 3.11, standard library only
+DRAT_TRIM=/path/to/drat-trim bash research/overcomplete-and-realisation-floors/verify.sh /fresh/output/dir   # additionally re-checks the shipped DRAT proofs
+```
+
+`verify.sh` first checks every file against `MANIFEST.sha256` and every pin of `SOURCES.json` (stops with exit 1 on mismatch), then runs six check scripts that print one `PASS` / `FAIL` line per assertion (`SKIP` for the DRAT re-check when `drat-trim` is neither on `PATH`, nor in `$DRAT_TRIM`, nor buildable from the vendored `research/p111-minrank-proof-reconciliation/vendor/drat-trim/drat-trim.c` with `cc`). One core, a few minutes (57 PASS lines including step 0's two, with `drat-trim`). No solver is needed for verification; `kissat` is only needed to *re-solve* (optional, `KISSAT_RESOLVE=n`).
+
+| script | what it recomputes |
+|---|---|
+| `checks/c1_overcomplete_d5.py` | Lemma OC on 120 exact random decompositions; D5: deficient directions, pair ranks 3 / 4, the combinatorial core of the D5 theorem |
+| `checks/c2_free_terms_frame120.py` | the 6,728-term exact decoder of the 120-line frame unit, `M = I`, cost 72 |
+| `checks/c3_realisation_free_floors.py` | frame-intersection certificate on D4, D5, D6, E6, E7, E8, P104, P112, E7 minus a 7-frame (all 2^h − 1 label classes of each); P104 / P112 pair-rank tables |
+| `checks/c4_e6_overcomplete.py` | E6: 27 deficient directions, 432 + 297 pair ranks, 1-dimensional bilinear-form space, transitivity of W(E6) on the 432 rank-5 pairs, exhaustive search over **5,504,660** seven-sets |
+| `checks/c5_known_decoders.py` | the decoders that attain the floors: E8 72, E7 49, D6 30, D4 12, P112 64, P104 56 (and the trivial decoders for E6 / D5) |
+| `checks/c6_sat_replay.py` | regenerates all 1,473 SAT instances, compares DIMACS hashes, checks SAT models clause by clause, re-checks the shipped DRAT proofs |
+
+**Prior work this builds on.** The model, the dense pairing and the root-code floor: **#446** (cost model, Theorem C), **#595 / #1590** (merged; two lemmas and an erratum), **#2111**, **#2125** (T² threshold, E7 first gain), **#2162** (T = 3 side), **#2228** (the dense polar law, Theorem 4 root-code floors, **Conjecture ID**, which this package corrects in one branch), **#2244** (the Lagrangian bound for line systems; unrelated to the statements here but the same model). The E8 / P112 / P104 floors for exactly 8 terms or for factors in the live root code: **#968** (merged, frame-pair decoders), **#1077**, **#1180** (merged; overcomplete factor-linear E8 decoders retain the puncture floor, and the 9-term example *outside* the root code that marks the boundary of this package), **#1224** (merged, joaqcoo: for E8 with live roots spanning `R^8`, factors split as `D = RA + N₁`, `T = RB + N₂` with exactness `ABᵀ = 2I`, `N₁Bᵀ = 0`, …; nine-term decoders are one-sided overcomplete representations), **#1633** (merged, bbMisk: for exact overcomplete E8 decoders the ranks of the two factors outside the live root code satisfy `s + t ≤ m − 8`), **#1212** (merged; rank-8 decoders are gauge-rigid), **#1236**, **#1744**, **#1815** (merged; unit diagonals and required zeros force `N = R Rᵀ`, `B = U Uᵀ` for P112 — the same mechanism as our Lemma 7.1 for E6 / D5). Forced minors: **#2176**, **#2206**. Independent E6 screens: **#2137** (1337isnot1337: the orthogonal-zero constraints on the 36 coordinates of a bilinear form `L` have rank 35, kernel `Q·G`; this is our §7 check `c4.nspace` / `c1.d5nspace`, found independently), **#2232**, **#2240** (one-extra frame screen, minimum 40 over its alphabet), **#2247** (sheared one-extra screen, 330,486 support cells, minimum 37 and none below 36): these are RECORDED, scoped to their finite families, and agree with §7 below, which closes the E6 seven-term question **for the whole root-code class**. Swarm discussion of the minrank / shadow viewpoint: #2232, #2240, #2247. **Free terms are not new.** Zero-cost corrections supported on zero-pairing rectangles ("free rectangles") are the mechanism of **#1331** (Arham-Tahir64: one free P112 rectangle cannot improve a coordinate COPY term; sharp whole-decoder floor 64) and **#1375** (commdata2338: two-coordinate mixing with small free rectangles keeps COPY 64), followed by **#1460** (bbMisk: pair (4,6), arbitrary free rectangles), **#1468** (bitplane: arbitrary one-column corrections) and **#1591** (Arham-Tahir64: all nine-factor singleton completions, COPY ≥ 64); all are scoped negative results for P112. Proposition 3.1 is the same move applied to whole units; what is new here is its use against Conjecture ID (a). The Shadow Lemma is Lemma CR2 / `hadamard_diag_rank_sum` of #2162 (`lean/DecoderDuality.lean`), with a rectangular Lean form in #2267; only `Overcomplete.lean` is shipped (§4). The repository helper `scripts/find_overlap.py --refresh` was run before submission (it also searches discussions: it surfaced discussion 1316, the free-rectangle line of #1331, and discussion 1622 = #1633, already cited; nothing else new).
+
+## 1. Setting and notation
+
+* A **unit** `U` is a list of `v` pairwise non-proportional vectors `r_t ∈ Q^n` ("lines"); `t ⊥ s` means `r_t · r_s = 0`. `V := span{r_t}`, `T := dim V`. All units here are root systems or punctures of E8: `D4, D5, D6, E6, E7, E8` and `P112 = E8 minus an 8-frame`, `P104 = E8 minus two 8-frames`, `E7-frame = E7 minus a 7-frame`; `lib/roots.py` builds them (E8 in doubled integer coordinates, E7 / E6 as orthogonal complements of one resp. two roots, D_n from `±e_i ± e_j`).
+* A **realisation** of `U` over a field `K ⊇ Q` is a matrix `M ∈ K^{v×v}` with `M_tt ≠ 0` and `M_ts = 0` whenever `t ⊥ s` (other entries arbitrary, possibly 0). A **decoder** is `M = Σ_{j=1..m} p_j q_jᵀ` (`p_j, q_j ∈ K^v`) together with an **admissible pairing** `B ∈ F2^{v×v}`: `B_tt = 1`, and `B_ts = 1` (`t ≠ s`) only if `t ⊥ s`. Then `B̃ ∘ M = diag(M_tt)` holds automatically. `R_j = supp p_j`, `A_j = supp q_j`, and
+  **cost = Σ_j rank_{F2} B[R_j, A_j]**.
+  The factors are *unrestricted* unless a theorem says otherwise. Terms with `p_j = 0` or `q_j = 0` contribute nothing and are dropped.
+* The **dense pairing** is `B_d := J + Ā`, i.e. `B_ts = 1` iff `t = s` or `t ⊥ s`; it depends on the orthogonality pattern only. `h := rank_F2 B_d` (D4 3, D5 5, D6 5, E6 7, E7 7, E8 9, P104 9, P112 9, E7-frame 7). It is symmetric.
+* **Label classes.** Let `C := col(B_d) ⊆ F2^v` (dimension `h`). A **class** is the support of a nonzero vector `w ∈ C` (`2^h − 1` of them, counted by vector). For `R ⊆ [v]` put `Def(R) := {w ∈ C : supp w ∩ R = ∅}` (a subspace of `C`) and `δ(R) := dim Def(R)`. In the notation of #2228, the classes are the sets `O_z = {t : Ω(u_t, z) = 1}`.
+* **Root-code decoders** (the class of #2228 Theorem 4). For a unit with line matrix `R ∈ Q^{v×n}`: `p_j = D₁ R x_j`, `q_j = D₂ R y_j` with `x_j, y_j ∈ V_K` and `D₁, D₂` invertible diagonal. Then `R(x) := supp(D₁Rx) = {t : r_t · x ≠ 0}`.
+* **Frames.** A **T-frame** is a set of `T` pairwise orthogonal lines; `α_⊥` is the size of a largest orthogonal set. If `U` has a `T`-frame `F`, every realisation `M` has `M[F,F]` diagonal and invertible, so **every realisation has rank ≥ α_⊥** (PROVEN, one line).
+
+## 2. Results at a glance
+
+| # | statement | label | exact scope | where |
+|---|---|---|---|---|
+| ID-a | Conjecture ID branch (a) (odd geometry ⇒ cost* = v) is false: the 120-line frame unit has an exact decoder of cost 72 | **PROVEN + CHECKED** | model with an unbounded number of terms; `M = I`; `B = J + Ā_E8`; 6,728 terms | §3, `c2` |
+| Mono | `orth(U') ⊆ orth(U)` on the same lines ⇒ `cost*(U) ≤ cost*(U')`; and `cost*(U) = min over admissible B of c(B)`, `c(B)` = cost of the unit whose orthogonality relation is `supp B` | **PROVEN** | any number of terms, any field of characteristic 0 | §3 |
+| OC | `Σ_{j≤m} x_j y_jᵀ = id_V` ⇔ `K = (⟨y_i,x_j⟩)` is an idempotent of rank `T`; `m = T` ⇒ biorthogonal; `m = T+1` ⇒ `I − K` has rank one, off-diagonal of `K` is rank one; criterion for prescribed directions | **PROVEN** (idempotency, traces, square case: **Lean**, no `sorry`); spot-checked on 120 exact instances (`c1`) | any field of characteristic 0; factors in `V` | §4 |
+| E6 | every root-code decoder of E6 (scaled-Gram realisation), dense `B`, **every** number of terms `m`, costs **≥ 36** | **PROVEN** from **CHECKED** data (`c4`: 5,504,660 seven-sets, exact integers) | factors in `col M`; realisations `D₁ G D₂`; dense `B`; char 0 | §7 |
+| D5 | same for D5: **≥ 20** | **PROVEN** from **CHECKED** data (`c1`) | same | §7 |
+| 4′ | Theorem 4′: the root-code floor `cost ≥ Σ_j (h − δ(R_j) − δ(A_j))` holds for **every realisation** `M` of rank `T`, deficiency being a property of the label class in that realisation | **PROVEN** | col P ⊆ col M, col Q ⊆ row M (all square decoders; any `m` otherwise); dense `B`; rank of `M` exactly `T` | §5 |
+| 3.3 | frame-intersection certificate: a class is non-deficient in **every** rank-`T` realisation if it contains a `T`-frame, or (clause (c)) if a `T`-frame contains the parts `F_i ∖ O` of frames with empty common intersection | **PROVEN** | rank-`T` realisations of units with a `T`-frame | §5 |
+| 3.4 | for every rank-`T` realisation and every decoder with col P ⊆ col M, col Q ⊆ row M, dense `B`: **E8 ≥ 72, E7 ≥ 49, D6 ≥ 30, D4 ≥ 12, P104 ≥ 56, P112 ≥ 56**; E8, E7, D6, D4, P104 are attained (P112: 64 attained, 56 proven here), see `c5` | **PROVEN** from **CHECKED** tables (`c3`) | as in 4′ | §5 |
+| – | E6 / D5 have no `T`-frame (`α_⊥ = 4`), so §5 gives nothing; the realisation-free statement for E6 / D5 is open | **OPEN** | | §8 |
+| SAT-1 | `min over admissible B of rank_F2 B` on E6 equals **7** (UNSAT at 5 and 6, each under three symmetry-breaking cliques; SAT at 7) | **CHECKED** (kissat 4.0.4 + DRAT, drat-trim VERIFIED) | all 36 lines | §9.1 |
+| SAT-2 | char-2 shadow minranks: `mr₂(Γ_E6) ≥ 7`, `mr₂(Γ_E7) ≥ 8` (UNSAT at 6 resp. 7, two cliques each) ⇒ a B-independent F2 shadow cannot certify all lines with `T` terms | **RECORDED**: DRAT-verified at generation (E7 part: shipped proof, **CHECKED**); `verify.sh` checks the CNF hashes and recorded verdicts for the E6 part, whose proofs are regenerable, not shipped ⇒ **PROVEN** consequence given those | over `F2` only | §9.2 |
+| SAT-3 | per-term drops are real: an E6 deficient pair of dense rank 6 has fitting minrank 4; E8 root blocks: 9, 9, ≤ 8 | **CHECKED** (DRAT / model) | single blocks, any `B` | §9.3 |
+| SAT-4 | the known optimal decoders are `B`-robust: every term of the E8 frame decoder (8), E8 coordinate decoder (terms 0, 7), E7 frame decoder (7), P112 removed-frame decoder (8), P104 frame-pair decoder (8) has fitting minrank equal to its dense rank (UNSAT at dense − 1) | **CHECKED** (DRAT) | those specific terms, any `B` | §9.4 |
+| SAT-5 | a shared `B` never brings any of **26** E6 square decoders below 36: **1,262** instances (every cap vector with `c_j ≥ fr_j`, `Σ c_j = 35`), all UNSAT, plus 156 floor instances | **RECORDED**: DRAT-verified at generation; `verify.sh` checks CNF hashes and recorded verdicts (proofs regenerable with `sat/run.py solve`, not shipped); decoder exactness is **CHECKED** (`c6.decoders`) | those 26 decoders (`data/e6_square_decoders.json`), every admissible `B` | §9.5 |
+
+**What is *not* proven here.** Arbitrary admissible `B` for a whole unit (only SAT-1..5 above); decoders with `col P ⊄ col M` (e.g. the 9-term example of #1180); realisations of rank `> T`; the E6 / D5 statements for realisations other than `D₁ G D₂`; P112 `≥ 64` for every realisation; any bound for `T = 3`.
+
+## 3. A correction to Conjecture ID (a), and the shape of cost*
+
+Free terms are the point (the "free rectangle" of #1331 / #1375). A term whose block `B[R_j, A_j]` is zero costs nothing, and a single-entry term `c e_t e_sᵀ` is free whenever `B_ts = 0`.
+
+**Proposition 3.1 (monotonicity) — PROVEN.** If `orth(U') ⊆ orth(U)` on the same `v` lines (patterns of required zeros, possibly directed) then `cost*(U) ≤ cost*(U')`.
+*Proof.* Take an optimal decoder `(M', P', Q', B')` of `U'`. Its `B'` is admissible for `U` (its off-diagonal ones lie in `orth(U') ⊆ orth(U)`). For every `(t,s) ∈ orth(U) ∖ orth(U')` add the term `−M'_ts e_t e_sᵀ`; its block is `B'_ts = 0`, so it is free. The new `M` vanishes on `orth(U)`, its diagonal is unchanged. ∎
+
+**Proposition 3.2 (reformulation) — PROVEN.** `cost*(U) = min over B admissible for U of c(B)`, where `c(B)` is the optimal cost, with the fixed pairing `B`, of decoders whose realisation `M` has `M_tt ≠ 0` and `M_ts = 0` exactly where required by the pattern `S(B) := {(t,s) : t ≠ s, B_ts = 1}` (a directed pattern if `B` is not symmetric; nothing else is asked of `M`).
+*Proof.* "≤": Proposition 3.1 with `U'` the `B`-unit. "≥": take a decoder of `U` with pairing `B`. Every line has `M_tt ≠ 0`, so some term covers `(t,t)`, and its block contains `B_tt = 1`; hence free terms never touch a diagonal entry. The paid terms (nonzero block) sum to a matrix `N` with the same diagonal as `M`, and `N_ts = 0` wherever `B_ts = 1`, `t ≠ s` (there every free term contributes 0 and `B̃ ∘ M = Δ`). So the paid part is a decoder of the `B`-unit of the same cost. ∎
+
+**Proposition 3.3 (the 120-line frame unit costs at most 72) — PROVEN + CHECKED (`c2`).** Let `F_120` be the unit of 120 lines, all pairs orthogonal; it admits every `B` with unit diagonal, and `M = I` (unit diagonal, "odd geometry") is a realisation. Take the E8 lines `r_t` (norm 2), `B = J + Ā_{E8}` (dense pairing of E8), and the terms
+ * `j = 1..8`: `p_j(t) = r_t[j]/2`, `q_j(s) = r_s[j]` (coordinate `j` of the E8 lines in the standard coordinates), whose sum is `½ G` (`G` the E8 Gram matrix);
+ * one **free term** `p = −(G_ts/2) e_t`, `q = e_s` for each of the 6,720 ordered non-orthogonal E8 pairs `(t,s)`.
+Then `Σ p q^T = ½G − ½(G − 2I) = I` exactly (`G_tt = 2`, the free terms cancel the off-diagonal part), `B̃ ∘ I = I`, the 8 coordinate terms have `F2`-rank 9 each (the 78 lines with a nonzero coordinate `j`; computed), and every free term has block `B_ts = 0` (the pair is non-orthogonal in E8), i.e. rank 0. Total cost **72 < 120 = v**. `c2` recomputes the sum `M = I` over 6,728 exact `Fraction` terms and the 8 + 6,720 ranks. ∎
+
+*Consequences, stated plainly.* (i) Conjecture ID (a) ("odd geometry ⇒ cost* = v") fails for `F_120`; the "odd geometry" property (an integral normalisation with unit diagonal) is not an invariant of cost* in the model where the number of terms is unbounded. F_120 (and F_104) are degenerate (`T = v`); no counterexample to (a) with `T < v` is known, and the only non-degenerate odd-geometry row of #2228 (Eisenstein, 40) still satisfies (a) by #2017. (ii) The correct way to read the frame unit is Proposition 3.2: the unit allows every `B`, and `c(B_dense(E8)) ≤ 72`. In this reading the search for good units is a search for **admissible pairings `B` with small `c(B)/v`**. (iii) #2228's Theorem 1 is *not* contradicted: it bounds the cost below by the number of lines whose leading 2-adic terms survive, and #2228 Corollary 2.2 derives "cost ≥ v" only for decoders in which all lines survive for some prime and shift; the decoder above has cost 72 < 120, so by Theorem 1 not all lines survive in it. (We have not recomputed the count of surviving lines for this decoder.) (iv) The theorems of §§5–7 are *not* affected: they assume `col P ⊆ col M`, `col Q ⊆ row M`, and a single-entry term `e_t e_sᵀ` lies outside `col M` as soon as `rank M < v`. (v) Scope: the decoder needs more than `T` terms; with the number of terms capped at the rank of the realisation, free terms are not available. The same move gives `cost*(F_104) ≤ 56` from the known P104 decoder; we did not re-run that and do not claim it.
+
+## 4. Lemma OC (overcomplete coupling)
+
+*Relation to #1224.* For E8 with `R` the matrix of live roots, #1224 Theorem A contains the identity `A Bᵀ = 2I` for the root-code parts; Lemma OC below is the same identity written as a statement about the cross matrix `K = YᵀX`, which (i) is basis-free, (ii) holds for any unit and any field (it is used here for E6 and D5, where a root basis does not have a dual basis of roots), and (iii) gives the idempotent / rank-one-off-diagonal structure used in §7. It is elementary and we claim nothing deeper.
+
+**Lemma OC — PROVEN.** Let `V = 𝕜^T` (`𝕜` a field of characteristic 0, or any field), `x_1..x_m ∈ V`, `y_1..y_m ∈ V*`, and `Σ_j x_j ⊗ y_j = id_V` (absorb coefficients into `y_j`). Put `K_ij := ⟨y_i, x_j⟩` (an `m × m` matrix). Then **`K` is idempotent of rank `T`**, so `Π := I_m − K` is idempotent of rank `m − T` and `trace Π = m − T`. Conversely, if `rank(x_j) = rank(y_j) = T` and `K² = K`, then `Σ_j x_j ⊗ y_j = id_V`.
+*Proof.* With `X = [x_j]`, `Y = [y_j]` (`T × m`): `XYᵀ = I_T`, so `K = YᵀX` satisfies `K² = Yᵀ(XYᵀ)X = K`, and `rank K = rank X = T` (`Yᵀ` is injective since `XYᵀ = I`). Conversely `K² = K` reads `Yᵀ(XYᵀ − I)X = 0`; `Yᵀ` is injective (rank `T`) and `X` surjective (rank `T`). ∎
+**Lean:** `lean/Overcomplete.lean` proves `oc_idempotent` (`(Yᵀ X)² = Yᵀ X`), `oc_trace` (`tr(Yᵀ X) = T`), `oc_complement_idempotent`, `oc_complement_trace` (`tr(1 − YᵀX) = m − T`) and `oc_square` (`m = T` ⇒ `Yᵀ X = 1`), with `#print axioms` showing only `propext, Classical.choice, Quot.sound`, no `sorry`. The rank statements, the converse and the consequences below are written proofs (not formalised).
+
+**Consequences — PROVEN.**
+ (a) `m = T`: `Π = 0`, so `⟨y_i, x_j⟩ = δ_ij` (biorthogonality; this is also `oc_square`).
+ (b) `m = T + 1`: `Π = u wᵀ` with `wᵀ u = 1` (rank-one idempotent), so `⟨y_i, x_j⟩ = −u_i w_j` for `i ≠ j`: **the cross matrix agrees off the diagonal with the rank-one matrix `−u wᵀ`**, and `⟨y_i, x_i⟩ = 1 − u_i w_i`.
+ (c) A term with `⟨y_i, x_i⟩ = 0` has `Π_ii = 1`.
+ (d) (**criterion for prescribed directions**) Let `m = T + 1 ≥ 3`, prescribed lines `x̂_j, ŷ_j` with `rank[x̂_j] = rank[ŷ_j] = T` and `Λ_ij := ⟨ŷ_i, x̂_j⟩ ≠ 0` for `i ≠ j`. There are scalars with `Σ_j (s_j x̂_j) ⊗ (t_j ŷ_j) = id` **iff** `Λ = D + a bᵀ` with `D` diagonal and invertible.
+ *Proof of (d).* "⇒": by the Lemma, `K = diag(t) Λ diag(s) = I − u wᵀ` for some `u, w` (the scalars `s_j, t_i` multiply `x̂_j, ŷ_i`; and `Π := I − K` is idempotent of rank `m − T = 1`, hence `Π = u wᵀ`), so `Λ = diag(1/t) (I − u wᵀ) diag(1/s)` has the form `D + a bᵀ` with `D = diag(1/(t_i s_i))` invertible. "⇐": given `Λ = D + a bᵀ`, choose `s_i t_i = 1/D_ii`, `u_i = −t_i a_i`, `w_j = s_j b_j`. Then `K := diag(t) Λ diag(s) = I − u wᵀ`. Since `rank Λ ≤ T < m`, `det Λ = 0`, i.e. `det(I + D⁻¹ a bᵀ) = 0`, i.e. `1 + Σ a_i b_i / D_ii = 0`, i.e. `wᵀ u = −Σ s_i t_i a_i b_i = 1`. So `Π = uwᵀ` is idempotent, `K² = K`, and the converse of the Lemma gives `Σ = id`. ∎
+ (e) A term-count consequence: at least `T` terms have `x_j ≠ 0 ≠ y_j`.
+
+## 5. Theorem 4′ and the frame-intersection certificate (realisation-free floors)
+
+Fix a unit with a `T`-frame and a realisation `M` of rank exactly `T` (so `T = α_⊥` is the minimum possible rank). Write `M = P₀ N Q₀ᵀ` with `P₀, Q₀ ∈ K^{v×T}` bases of `col M`, `col Mᵀ` and `N ∈ GL_T(K)`; `π(t)` (resp. `κ(s)`) is row `t` of `P₀` (row `s` of `Q₀`). Consider decoders with `p_j = P₀ x_j`, `q_j = Q₀ y_j` (`col P ⊆ col M`, `col Q ⊆ row M`); **every square decoder (`m = T`) is of this form** (`rank M = T ≤ rank P ≤ m`). Then `N = Σ_j x_j y_jᵀ` (as `P₀, Q₀` are injective), so at least `T` terms are nonzero.
+
+**Lemma 5.1 (support-only bound) — PROVEN.** For any `R, A ⊆ [v]`: `rank_F2 B_d[R, A] ≥ h − δ(R) − δ(A)`, and `rank B_d[R,A]` depends only on the two subspaces `Def(R), Def(A) ⊆ C`.
+*Proof.* Choose a rank factorisation `B_d = X Yᵀ` with `X, Y ∈ F2^{v×h}` of full column rank; `col X = col Y = C` (`B_d` is symmetric). `ker X_R = {z : X_R z = 0} ≅ {w ∈ C : w|_R = 0} = Def(R)` (via `w = Xz`), so `rank X_R = h − δ(R)`; likewise `rank Y_A = h − δ(A)`. Sylvester: `rank(X_R Y_Aᵀ) ≥ rank X_R + rank Y_A − h`. If `X_R` and `X_{R'}` have the same kernel they have the same row space `W`, and `X_R = S W` with `S` of full column rank, so `rank(X_R Y_Aᵀ) = rank(W Y_Aᵀ)`; the same on the other side. ∎
+
+**Theorem 4′ — PROVEN.** In the setting above and with the dense pairing `B_d`,
+  **cost ≥ Σ_{j : x_j,y_j ≠ 0} ( h − δ(R(x_j)) − δ(A(y_j)) ),** where `R(x) = {t : π(t)·x ≠ 0}`, `A(y) = {s : κ(s)·y ≠ 0}`.
+Call a class `O` **π-deficient** if `π(O)` lies in a hyperplane of `K^T` (**κ-deficient** analogously). If `w ∈ Def(R(x))` then `supp w ∩ R(x) = ∅`, i.e. `π(supp w) ⊆ x^⊥`: the class `supp w` is π-deficient. **If no class is π-deficient or κ-deficient, every term costs ≥ h and cost ≥ T·h.**
+*Proof.* Lemma 5.1 and the count of nonzero terms (§5, last sentence of the setting). ∎
+This is #2228 Theorem 4 (which already allows `M = D₁ R N Rᵀ D₂` with arbitrary `N`, for factors in the scaled root code) extended to rank-`T` realisations whose column space is not a scaled root code (`col M ≠ D₁·RV`); in the Gram case `π = κ = ` coordinates of the line.
+
+**Lemma 5.2 (frame-intersection certificate) — PROVEN.** Let `M` be a rank-`T` realisation and `O ⊆ [v]` with `π(O) ⊆ ker c` for a nonzero functional `c`. Then
+ (a) `O` contains no `T`-frame;
+ (b) for every `T`-frame `F`, `c ∈ span σ(F ∖ O)`, where `σ(s) := N κ(s)ᵀ`;
+ (c) if a `T`-frame `E` contains the sets `F_1∖O, …, F_k∖O` of `T`-frames `F_i` whose intersection `∩_i (F_i ∖ O)` is empty, then `c = 0`, a contradiction.
+Hence **a class that contains a `T`-frame, or satisfies (c), is not π-deficient in any rank-`T` realisation.** Replacing `M` by `Mᵀ` (a realisation of the same pattern) gives the same for κ.
+*Proof.* For a `T`-frame `F`, `M[F,F] = P₀[F] N Q₀[F]ᵀ` is diagonal (all pairs orthogonal) with nonzero diagonal, hence invertible, so `{π(f)}_{f∈F}` is a basis of `K^T`, and `π(f)·σ(f') = 0` for `f ≠ f'`, `≠ 0` for `f = f'`: `{σ(f)}` is the dual basis up to scalars, and **σ(f) depends on the line `f` only, not on the frame**. (a): `F ⊆ O` would give `c ⟂ π(F)`, a basis. (b): expand `c = Σ_{f∈F} λ_f σ(f)`; then `π(f')·c = λ_{f'} π(f')·σ(f')`, which is 0 for `f' ∈ F ∩ O`. (c): by (b), `c ∈ ∩_i span σ(F_i∖O)`; all `F_i ∖ O ⊆ E` and `σ(E)` is a basis, so these spans are coordinate subspaces and their intersection is `span σ(∩_i F_i∖O) = 0`. ∎
+
+**Corollary 5.3 (realisation-free floors) — PROVEN from the CHECKED tables of `c3`.** (`c3` enumerates, for each unit, all maximal cliques of the orthogonality graph (frames = cliques of size `T`), all `2^h − 1` classes, and decides for each class: contains a `T`-frame / certified by (c) / uncertified.)
+
+| unit | v | T | h | α_⊥ | T-frames | classes (2^h−1) | contain a T-frame | certified by (c) | uncertified | 2-dim subspace of uncertified? |
+|---|---|---|---|---|---|---|---|---|---|---|
+| D4 | 12 | 4 | 3 | 4 | 3 | 7 | 7 | – | 0 | – |
+| D6 | 30 | 6 | 5 | 6 | 15 | 31 | 16 | 15 | 0 | – |
+| E7 | 63 | 7 | 7 | 7 | 135 | 127 | 64 | 63 | 0 | – |
+| E8 | 120 | 8 | 9 | 8 | 2025 | 511 | 391 | 120 | 0 | – |
+| P104 | 104 | 8 | 9 | 8 | 759 | 511 | 375 | 104 | 32 (size 52) | no |
+| P112 | 112 | 8 | 9 | 8 | 1260 | 511 | 383 | 112 | 16 (size 56) | no |
+| E7-frame | 56 | 7 | 7 | 7 | 64 | 127 | 57 | 56 | 14 (sizes 24, 32) | yes |
+| E6 | 36 | 6 | 7 | 4 | 0 | 127 | 0 | 0 | 127 | yes |
+| D5 | 20 | 5 | 5 | 4 | 0 | 31 | 0 | 0 | 31 | yes |
+
+(The classes without a `T`-frame are exactly the neighbourhoods `N(α) = {t ≠ α : r_t · r_α ≠ 0}` — `c3.N.*`; in E8 every frame not through `α` meets `N(α)` in exactly 4 lines, which is why clause (c) is needed — `c3.e8meet`.) Consequently, for **every realisation of rank `T`** and **every decoder with `col P ⊆ col M`, `col Q ⊆ row M`** (all square decoders, any number of terms otherwise), dense `B`:
+ * **E8 ≥ 72, E7 ≥ 49, D6 ≥ 30, D4 ≥ 12** (no class is deficient, every term has rank `h`, `T` terms at least);
+ * **P104 ≥ 56** and **P112 ≥ 56**: the uncertified classes contain no 2-dimensional subspace, so `δ(R), δ(A) ≤ 1` for every term (a `Def(R)` consists of π-deficient, hence uncertified, classes and is a subspace), each uncertified class has deficiency exactly 1 (`c3.pairs.*`), and the rank of a term depends only on `(Def(R), Def(A))` (Lemma 5.1); over the `(uncertified or none)²` pairs the computed ranks are `{7: 640, 8: 448, 9: 1}` (P104) and `{7: 192, 8: 96, 9: 1}` (P112), minimum 7, so `8 · 7 = 56`.
+**Sharpness (CHECKED, `c5`).** The decoders of `c5` attain E8 72, E7 49, D6 30, D4 12 (frame decoders with `M = G`), P112 64 (removed-frame decoder) and P104 56 (the eight frame-pair terms of #968; `M = R N Rᵀ` with `N` not the Gram form). For P112 the gap between the realisation-free 56 and the attained 64 is **OPEN** (§8); in the Gram realisation 64 is #2228 Theorem 4 (RECORDED, not re-run). The E6 and D5 values are covered in §7.
+
+*How this relates to earlier work.* For the E8 / P112 / P104 values with factors in the live root code, the statement is #1180 and #2228 Theorem 4; for exactly 8 terms, #968 / #1077 / #1212. What Theorem 4′ adds to #2228 Theorem 4 is the case `col M ≠ D₁·(root code)`: Lemma 5.2 shows that *no realisation of rank `T`* can make a class deficient, so the floors hold for every rank-`T` realisation (the hypothesis `col P ⊆ col M`, `col Q ⊆ row M` remains). We do not claim priority for the E8 value itself.
+
+## 6. The cap on what is proven: realisations of rank above T
+
+If `rank M = ρ > T`, a `T`-frame no longer spans `K^ρ` and Lemma 5.2 fails. Theorem 4′ still gives `cost ≥ Σ_j (h − δ_j − δ'_j)` with at least `ρ` terms, but `δ` is no longer controlled by frames. This is **OPEN** (§8).
+
+## 7. E6 and D5 for every number of terms (scaled-Gram realisations)
+
+**The class.** `p_j = D₁ R x_j`, `q_j = D₂ R y_j`, `x_j, y_j ∈ V_K`, any `m`, dense `B`. Then `M = D₁ R N Rᵀ D₂` with `N = Σ x_j y_jᵀ ∈ V ⊗ V`.
+
+**Lemma 7.1 — CHECKED (`c4.nspace`, `c1.d5nspace`).** For E6 and for D5 the space `𝒩 = {N ∈ V ⊗ V : r_tᵀ N r_s = 0 for all orthogonal t, s}` is **one-dimensional**, spanned by the metric (identity in orthonormal coordinates). (Exact rational rank of the constraint system on the `T²` unknowns; #2137 computes the same kernel for E6 in its coordinates.) Hence `N = c·Id_V`, `c ≠ 0` (the diagonal of `M` is nonzero), and after absorbing `c`: **`Σ_j x_j ⊗ y_j = id_V`**, so Lemma OC applies with `T = 6` (E6) resp. `5` (D5), and `m ≥ T`.
+
+**Lemma 7.2 — CHECKED (`c4.dirs`, `c4.pairranks`, `c4.cross`, `c1.d5dirs`, `c1.d5ranks`).** Over `Q`, the classes of E6 (127) with `rank π(O) < 6` are exactly 27, each with a one-dimensional annihilator; the 27 annihilators are 27 distinct lines (the minuscule weights). Call a direction `x ∈ V_K` **deficient** if it lies on one of them; for a deficient `x`, `δ(R(x)) = 1`, for every other `x`, `δ(R(x)) = 0` (a class sits inside `x^⊥` iff `x` spans its annihilator, and the map class ↦ direction is injective). The same holds on the column side with the same 27 lines (`B_d` is symmetric). Dense-pairing ranks of terms (Lemma 5.1 and the table): both deficient: **5** (432 ordered pairs) or **6** (297 pairs); exactly one deficient: 6; none: 7. **All 27 × 27 cross products `⟨y, x⟩` of deficient directions are nonzero.** For D5 the deficient directions are the five axes `e_1..e_5`; both deficient: rank **4** if matched (`e_a, e_a`), **3** if `a ≠ b` (20 pairs); one deficient: 4; none: 5.
+
+**Theorem 7.3 (E6 ≥ 36 for every `m`) — PROVEN from CHECKED data (Lemmas 7.1, 7.2 and `c4.transitive`, `c4.nodes`, `c4.noleaf`).** Every root-code decoder of E6 with dense `B` has cost `≥ 36`.
+*Proof.* By Lemma 7.1 `Σ x_j y_jᵀ = id`. Suppose a decoder of cost `c₀` exists and take one of cost `≤ c₀` with the fewest terms. Two terms with proportional `x` and proportional `y` have the same supports and can be merged into one term of the same rank (or both vanish), contradicting minimality; so the ordered pairs of lines `([x_j],[y_j])` are pairwise distinct (and terms with a zero factor are absent). Every term costs `≥ 5` (Lemma 7.2).
+ *`m ≥ 8`*: cost `≥ 40`.
+ *`m = 6`* (square, `m = T`): by OC(a), `⟨y_i, x_j⟩ = δ_ij`. Let `k` (resp. `l`) be the number of deficient `x_j` (resp. `y_j`). If `y_j` is deficient, every `x_i`, `i ≠ j`, is non-deficient — otherwise `⟨y_j, x_i⟩ = 0` for two deficient directions, contradicting Lemma 7.2. Hence `l ≥ 1` forces `k ≤ 1`, and `k ≥ 2` forces `l = 0`. By Lemma 5.1 each term costs `≥ 7 − [x_j def] − [y_j def]`, so cost `≥ 42 − k − l`. If `k ≥ 2` then `l = 0`, cost `≥ 42 − 6 = 36`; symmetrically for `l ≥ 2`; if `k, l ≤ 1`, cost `≥ 40`.
+ *`m = 7`*: cost `≤ 35` forces all seven terms to have rank 5 (`7 · 5 = 35`), i.e. seven distinct pairs from the 432 rank-5 pairs. By OC(b) the off-diagonal of `Λ_ij = ⟨y_i, x_j⟩` has rank one (rescaling rows and columns by the nonzero scalars `s_j, t_i` does not change this), and `rank[x_j] = rank[y_j] = 6`. W(E6) is transitive on the 432 rank-5 pairs (`c4.transitive`: the orbit of one pair under the 36 reflections has 432 elements), and it permutes the lines and so preserves everything, so one pair may be fixed. `c4` then enumerates **all** 7-sets containing that pair whose `Λ` has rank-one off-diagonal (exact integer cross-multiplication, no floating point): there are 27,250 triples, 206,275 / 898,460 / 2,502,409 / **5,504,660** sets of sizes 4 / 5 / 6 / 7 (`c4.nodes`; these numbers reproduce the node counts of an independent floating-point search of the working notes, which used `numpy`), and **none** of the 5,504,660 has both its row directions and its column directions spanning `V` — in fact none has `≥ 6` distinct row directions and `≥ 6` distinct column directions (`c4.noleaf`). So no 7-term decomposition exists.
+ Since `m = 6, 7` and `m ≥ 8` exhaust the possibilities (`m ≥ 6` is needed for `Σ x_j y_jᵀ = id`), cost `≥ 36` in all cases. ∎
+ *Remarks.* The value 36 is attained by the trivial decoder (`c5.E6`, `M = I`, a different realisation). (RECORDED, not re-run: the working notes' floating-point search found 5,208 exact 7-term decompositions with deficient `x_j, y_j`, the best of cost 40, consistent with the above; #2240 / #2247 report minimum 40 / 37 for their finite alphabets.)
+
+**Theorem 7.4 (D5 ≥ 20 for every `m`) — PROVEN from CHECKED data (Lemmas 7.1, 7.2 for D5).** Every root-code decoder of D5 with dense `B` costs `≥ 20`.
+*Proof.* Each term has rank `≥ 3`, with equality iff `x_j = e_a`, `y_j = e_b` with `a ≠ b` (both deficient, unmatched); all other terms have rank `≥ 4`. Let `n₃` be the number of rank-3 terms. Cost `≤ 19` needs `3 n₃ + 4(m − n₃) ≤ 19`, i.e. `n₃ ≥ 4m − 19`; with `n₃ ≤ m` this gives `m ≤ 6`, and `m ≥ 5` is forced. *`m = 5`* (square): `n₃ ≥ 1` is impossible, since a rank-3 term has `⟨y_i, x_i⟩ = ⟨e_b, e_a⟩ = 0`, contradicting `⟨y_i, x_i⟩ = 1`. *`m = 6`*: `n₃ ≥ 5`. By OC(b), `Π = u wᵀ`; a rank-3 term `i` has `⟨y_i,x_i⟩ = 0`, so `u_i w_i = 1` (OC(c)), and for two rank-3 terms `i ≠ j`, `⟨y_i, x_j⟩ = −u_i w_j ≠ 0`, i.e. `b_i = a_j`. Three rank-3 terms `i, j, k` then give `a_j = b_i = a_k` and `a_i = b_j = a_k`, so `a_i = b_i`, a contradiction (`c1.d5core` checks that no three pairs `(a_i, b_i)`, `a_i ≠ b_i`, satisfy `b_i = a_j` for all `i ≠ j`); so `n₃ ≤ 2 < 5`. ∎ The value 20 is attained by the trivial decoder (`c5.D5`). An independent counting proof for D5 is in the working notes (RECORDED).
+
+## 8. Open next questions (ranked by what they would buy)
+
+1. **Arbitrary `B`, E8.** A per-term census of fitting minranks `fr(R_x, A_y)` over pairs of maximal-flat normals (E8 has 8 orbits of normals; only root × root is done, §9.3) plus a coupling argument (Lemma OC bounds how many terms with `fr = 8` can occur) would give E8 `≥ 72` for root-code decoders and arbitrary `B`.
+2. **P112.** Exclude the extra 8 of the 16 uncertified classes in every rank-8 realisation (a stronger certificate than (c), e.g. two-step propagation); this gives P112 `≥ 64` for every rank-8 realisation.
+3. **Rank `> T` realisations and factors outside `col M`** (the 9-term decoder of #1180 is the test case): the supports are hyperplane sections of a lifted configuration in `K^{dim col P}` and Lemma 5.2 does not apply. For E8-type units with live roots spanning `R^8`, #1224 and #1633 give structure (one-sided nine-term decoders are overcomplete representations; `s + t ≤ m − 8`), but no cost floor outside the root code is known to us; Lemma OC generalises to idempotents of the lifted configuration, but no cost bound is derived.
+4. **E6 / D5 realisation-free.** Neither has a `T`-frame; a rank-5 realisation of E6 would give dense cost `≤ 35`. No such realisation is known; rigidity of the Gram point and global uniqueness at rank `T` are open. (A floating-point search of the working notes found none; not reproduced, not claimed.)
+5. **A human proof of `mr₂(Γ̄_E6) = 7`** (SAT-1 is a DRAT certificate, not an argument; a 16-line sub-configuration already needs rank 7 in the working notes' minimisation), and the exact values of `mr₂(Γ_E6)`, `mr₂(Γ_E7)` (only lower bounds 7, 8 are proved), over `F2` and over larger fields of characteristic 2.
+6. **A B-dependent proof.** SAT-2 says a B-independent shadow cannot certify E6 / E7 with `T` terms, and SAT-5 says a shared `B` defeats every per-term drop on 26 decoders; an argument that explains the second by using that one `B` serves all terms is missing.
+7. **Does a sparser admissible `B` ever beat the dense value for a whole unit?** All evidence here (SAT-1, SAT-4, SAT-5) says no for the nine test units; Proposition 3.2 says this is exactly the question of whether `min_B c(B)` is attained at the dense `B`.
+
+## 9. SAT evidence (arbitrary pairings)
+
+Everything in this section is about **all admissible B** (not just the dense one). Standard facts used: (i) `rank_F2 X ≤ r` iff `X = U Vᵀ` with `U, V` having `r` columns; this is encoded with an AND per entry and an XOR chain (`lib/satgen.py`). (ii) **Symmetry breaking** is valid: if `C` is a set of rows/columns with `X[C,C] = I` (a clique of pairwise *non-orthogonal* lines for fitting problems, where `X_tt = 1`, `X_ts = 0`; a clique of pairwise *orthogonal* lines for the `Γ` problems), then `U[C]` has rank `|C|` and a change of basis `U ↦ UA`, `V ↦ VA^{-T}` of `F2^r` makes `U[C] = [I | 0]` (and `V[C] = [I | 0]` when `r = |C|`). Any clique may be chosen; we use several. (iii) Every UNSAT is a **DRAT proof** checked by `drat-trim` (built from the upstream source vendored in `research/p111-minrank-proof-reconciliation/vendor/drat-trim/`); every SAT answer is a **model** checked clause by clause. (iv) **Controls** (SAT at the known feasible rank, so the encoding is not vacuously unsatisfiable): E6 at rank 7, E8 / P104 / E7 frame blocks at their dense ranks, three E6 shared-B instances at the dense ranks (`jointctrl_d00/07/18`).
+Solver: kissat 4.0.4 only. Every instance is regenerated by `sat/instances.py` (deterministic); `sat/results.jsonl` and `sat/joint_results.jsonl` record the sha256 of its DIMACS text, the status, and the DRAT verdict; `c6` regenerates all 1,473 and compares. Proof files: the 44 DRAT proofs of the primary instances other than the two E6 `Γ` ones are shipped (`sat/proofs/*.drat.xz`, 2 MB compressed), with all 55 primary CNFs (`sat/cnf/*.cnf.xz`) and the 9 SAT models (`sat/models/`); the two E6 `Γ` proofs (about 90 MB each) and the 1,418 shared-B / floor proofs (about 600 MB in total, each ≤ 2.5 MB) are **not** shipped: regenerate with `python3 sat/run.py solve OUT NAME...` (`kissat` and `drat-trim` on `PATH`; sub-second per shared-B instance) and verify with `drat-trim OUT/NAME.cnf OUT/NAME.drat`. All of them were solved and DRAT-verified by the author (`seconds` and `proof_bytes` in the results files).
+
+### 9.1 SAT-1: the smallest rank of an admissible B on E6 is 7 — CHECKED
+`e6glob_r5_c{0,1,2}`, `e6glob_r6_c{0,1,2}`: UNSAT (three different 5-cliques of pairwise non-orthogonal lines); `e6glob_r7_c0`: SAT (model checked). So **every** admissible `B` on the 36 E6 lines has rank `≥ 7` (the 5-clique already forces `≥ 5`), and the dense `B` attains 7. Note `ω(Γ) = 5 < 7`, so this is not a clique bound. Meaning: a decoder cannot lower its cost below `m · 7` by using a globally low-rank `B` (the bound "cost ≤ m · rank B" is useless below 42 for `m = 6`).
+
+### 9.2 SAT-2: B-independent shadows cannot certify E6 or E7 — E7 CHECKED (shipped DRAT), E6 RECORDED (DRAT-verified at generation), consequence PROVEN
+**Shadow Lemma — PROVEN** (this is Lemma CR2 / `hadamard_diag_rank_sum` of #2162, `lean/DecoderDuality.lean`; rectangular Lean form in #2267; cited, not shipped). For any field `L ⊇ F2`, `x_j, y_j ∈ L^v` with `supp x_j ⊆ R_j`, `supp y_j ⊆ A_j`, and `N := Σ_j x_j y_jᵀ`: for every admissible `B`, **cost ≥ rank_L(B ∘ N)**. *Proof:* `B ∘ N = Σ_j D(x_j) B D(y_j)` and each summand factors through `B[R_j, A_j]`, so has rank `≤ rank_F2 B[R_j,A_j]` (rank is invariant under field extension); rank is subadditive. If moreover `N` vanishes on every orthogonal pair, `B ∘ N` is diagonal (a non-orthogonal pair has `B_ts = 0`), so **cost ≥ #{t : N_tt ≠ 0} for every B**.
+A shadow `N` certifying all `v` lines with `m` terms is a matrix of rank `≤ m` over `L` with nonzero diagonal vanishing on orthogonal pairs. Over `L = F2` this is a matrix of rank `≤ m` with unit diagonal and zeros on orthogonal pairs: its minimum rank is `mr₂(Γ)`. **E6 RECORDED** (DRAT-verified at generation; the two ~90 MB proofs are not shipped, `verify.sh` checks the CNF hashes and verdicts) **and E7 CHECKED:** `gamma_E6_r6_c{0,1}` UNSAT (so `mr₂(Γ_E6) ≥ 7 > 6 = T`) and `gamma_E7_r7_c{0,1}` UNSAT (`mr₂(Γ_E7) ≥ 8 > 7 = T`); symmetry-breaking cliques of pairwise orthogonal lines (E6 has `α_⊥ = 4`). **PROVEN consequence:** for square decoders (`m = T`) no **F2-valued, B-independent** Shadow-Lemma certificate certifies all lines of E6 or of E7. Larger fields of characteristic 2 are not covered (OPEN, §8.5). The E-type floors for arbitrary `B`, if true, need an argument using that one `B` is shared.
+
+### 9.3 SAT-3: per-term drops — CHECKED
+`e6term_r4` (SAT) and `e6term_r3` (UNSAT): a pair of deficient directions with dense rank 6 and `|R ∩ A| = 8` has fitting minrank exactly 4 over all admissible `B`. E8 root blocks (`e8blk_*`, any `B`): `fr(R_α, R_α) ≥ 9` and `fr(R_α, R_β) ≥ 9` for non-orthogonal `α, β` (UNSAT at 8); `fr(R_α, R_β) ≤ 8` for orthogonal `α, β` (SAT). So per-term monotonicity in `B` fails (a sparser `B` can lower a *single* term) — which is what makes SAT-5 informative.
+
+### 9.4 SAT-4: the known optimal decoders are B-robust — CHECKED
+For each of the following terms the F2-fitting minrank over all admissible `B` equals the dense rank (UNSAT at dense − 1; SAT at the dense rank for the controls): E8 frame-normal decoder, 8 terms (dense 9); E8 coordinate decoder, terms 0 and 7 (78 lines each; dense 9; the other coordinates are equivalent under coordinate permutations of E8); E7 frame decoder, 7 terms (dense 7); P112 removed-frame decoder, 8 terms (dense 8); P104 frame-pair decoder, 8 terms (dense 7). So **no admissible `B` lowers the cost of these decoders** (72, 49, 64, 56), i.e. the sharp dense values are also robust to the choice of `B` *for these decoders*. (This is a statement about those decoders, not a lower bound for the unit.)
+
+### 9.5 SAT-5: a shared B does not rescue per-term drops on E6 — RECORDED (DRAT-verified at generation; CNF hashes and verdicts checked by verify.sh)
+`data/e6_square_decoders.json` lists 26 square (`m = 6`) root-code decoders of E6 (found by hill climbing over bases of normals of maximal flats; dense costs 38 to 41). For each decoder `d` and term `j` let `lo_j` be the F2-fitting minrank of `B[R_j, A_j]` over all admissible `B` (computed with kissat from the dense rank downwards; each `lo_j > 1` is backed by an UNSAT instance `floor_dXX_tY` at rank `lo_j − 1`, DRAT-verified; 156 of them). Every admissible `B` has `rank B[R_j,A_j] ≥ lo_j`, and `Σ_j lo_j ≤ 35` for all 26 decoders. If some `B` had total cost `≤ 35`, then with `c_j := rank B[R_j,A_j] ≥ lo_j` and `Σ c_j ≤ 35` we may enlarge the `c_j` to reach `Σ = 35`; `B` then satisfies `rank B[R_j,A_j] ≤ c_j` for **a** cap vector `c ≥ lo` with `Σ c = 35`. So it suffices to refute each such cap vector with the shared variables (`B` entries on orthogonal pairs shared by all six blocks): **1,262 instances** (`joint_dXX_c1-…-c6`; 1, 6, 21, 56, 126 or 252 per decoder), **all UNSAT, all DRAT-verified**. Controls: with the dense ranks as caps the instances are SAT (`jointctrl_*`). So **no admissible `B` brings any of these 26 decoders to cost `≤ 35`**, although the sums of their per-term floors are as low as 30. Scope: those 26 decoders only.
+
+## 10. What was *not* reproduced, and discrepancies
+`verify.sh` reproduces every CHECKED number above. Items quoted from other PRs or from the working notes are marked RECORDED in place and are not claimed. The earlier helper `mrsub.py` of the working notes reports solver timeouts as SAT and was **not** used; all SAT / UNSAT verdicts here come from `sat/run.py`, which records `UNKNOWN` / `TIMEOUT` separately (there are none).
diff --git a/research/dn-unrestricted-root-code-floor/references/PR2518-README.md b/research/dn-unrestricted-root-code-floor/references/PR2518-README.md
new file mode 100644
index 0000000000..3d7a428553
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/references/PR2518-README.md
@@ -0,0 +1,227 @@
+# Polar-law screens at T >= 7 and a small-T overcomplete census
+
+**Scoped negative results; no new kappa.** The dense-polar small-T screen of
+[PR 2272](https://github.com/CrocSwap/integer-mult-bounds/pull/2272) left three obligations open: the T^2
+threshold law at T >= 7, overcomplete (m = T + 1) decoders, and pairing minima on its 1,023 cost = v ties.
+This package attacks the first two. No configuration at T = 7 or T = 8 outside the already-checked E7/E8
+gains has dense-polar cost below v under the checked decoders, and no overcomplete decoder in the one-extra
+rank-one family of [PR 2240](https://github.com/CrocSwap/integer-mult-bounds/pull/2240) beats v on any of
+144,953 exhaustively censused punctures at T <= 4 or on any of 13 full sets at T <= 5.
+
+Model, as in [PR 2125](https://github.com/CrocSwap/integer-mult-bounds/pull/2125) / PR 2272: a configuration
+is a list of root lines `t = 1..v` with vectors `p(t) = q(t)` in `Q^T`. The full-orthogonal-pattern pairing
+`B0` has unit diagonal and `B_ts = 1` exactly where `dot(p(t), p(s)) = 0`. An exact coordinate Gram decoder
+`M = sum_j p_j q_j^T = Gram` is priced `cost = sum_j rank_F2 B[R_j, A_j]` (Theorem C without the floor),
+where `R_j = supp p_j` and `A_j = supp q_j`. A gain is `cost < v`. All arithmetic is exact (integers,
+rationals, F2 bitsets), standard library only.
+
+## 1. Positive control: the checked table reproduces exactly
+
+The engine re-derives the root systems, the exact coordinate decoders and the F2 block ranks independently;
+PR 2125's `data/e6_best.json` is pinned read-only (SHA-256 in `SOURCES.json`) and supplies only the E6
+stored basis and stored pairing. Before any new number was computed, the controls reproduced PR 2272's
+checked table (PR 2125 values) exactly:
+
+| unit | v | T | cost | expected | status |
+|---|---:|---:|---:|---:|---|
+| D4 (standard coords, B0) | 12 | 4 | 12 | 12 | CHECKED |
+| D5 (standard coords, B0) | 20 | 5 | 20 | 20 | CHECKED |
+| D6 (standard coords, B0) | 30 | 6 | 30 | 30 | CHECKED |
+| E6 (stored basis, stored B) | 36 | 6 | 36 | 36 | CHECKED |
+| E6 (first-independent basis, B0) | 36 | 6 | 37 | 37 | CHECKED |
+| E7 (first-independent basis, B0) | 63 | 7 | 49 | 49 | CHECKED |
+| E8 (first-independent basis, B0) | 120 | 8 | 72 | 72 | CHECKED |
+
+The A4/A5/A6 first-independent-basis values 16/25/36 reproduce as well, and the mutation controls
+(replace B by the identity) change the cost on D5 and E7, so the pricing is sensitive to the pairing.
+
+## 2. Exact full-system screens at T = 7 and T = 8
+
+Twelve systems, same rigor as PR 2272's full-system table (exact coordinate Gram decoder, B0). The
+B/C/D families use standard coordinates, A7/A8 and E7/E8 the first-independent span basis, matching
+PR 2272's conventions. Width is the decoder width (= span dimension); T^2 in the last column is width^2.
+
+| unit | v | width | cost | cost - v | gain | v > T^2 |
+|---|---:|---:|---:|---:|---|---|
+| A7 | 28 | 7 | 49 | +21 | no | no |
+| B7 | 49 | 7 | 49 | 0 | no | no (v = T^2 exactly) |
+| C7 | 49 | 7 | 49 | 0 | no | no (v = T^2 exactly) |
+| D7 | 42 | 7 | 42 | 0 | no | no |
+| E7 | 63 | 7 | 49 | -14 | yes | yes |
+| {0,+/-1}^7 | 1093 | 7 | 4501 | +3408 | no | yes |
+| A8 | 36 | 8 | 64 | +28 | no | no |
+| B8 | 64 | 8 | 64 | 0 | no | no (v = T^2 exactly) |
+| C8 | 64 | 8 | 64 | 0 | no | no (v = T^2 exactly) |
+| D8 | 56 | 8 | 56 | 0 | no | no |
+| E8 | 120 | 8 | 72 | -48 | yes | yes |
+| {0,+/-1}^8 | 3280 | 8 | 15760 | +12480 | no | yes |
+
+Findings:
+
+1. **No new T >= 7 gain.** The only systems with cost below v are E7 and E8, both already inside
+   PR 2272's checked table. Every other T = 7/8 system ties or exceeds v under the checked decoder.
+2. **The law's necessary condition survives T = 7 and T = 8.** Both gains have v above T^2
+   (63 > 49 and 120 > 64); every system with v at or below T^2 has no gain. The B family sits exactly
+   on the boundary: v = T^2 = cost at both T = 7 and T = 8. The {0,+/-1}^T sets again show that
+   v above T^2 is not sufficient for a gain (cost - v = 3408 and 12480 under the checked decoder),
+   extending PR 2272's T = 4/5/6 observation (40/121/364 lines).
+3. The A family costs T^2 strictly above v at both T = 7 and T = 8 (49 and 64), continuing the
+   A4-A6 pattern 16/25/36.
+
+## 3. Bounded falsification searches at T = 7 and T = 8 (seeded 20261015)
+
+Basis pivots (300 seeded random span bases each, exact recomputation of supports) and seeded
+greedy/random puncture searches (12 restarts x 250 steps plus 200 random subsets, minimum size 2).
+These are bounded searches, not exhaustive: no claim outside the recorded domains.
+
+| unit | search | best cost | v of best | min(cost - v) |
+|---|---|---:|---:|---:|
+| A7 | basis pivots | 46 | 28 | +18 |
+| B7 | basis pivots | 49 | 49 | 0 |
+| D7 | basis pivots | 44 | 42 | +2 |
+| E7 | basis pivots | 49 | 63 | -14 |
+| A8 | basis pivots | 64 | 36 | +28 |
+| B8 | basis pivots | 66 | 64 | +2 |
+| D8 | basis pivots | 56 | 56 | 0 |
+| A7 | punctures | 2 | 2 | 0 |
+| B7 | punctures | 10 | 10 | 0 |
+| D7 | punctures | 22 | 22 | 0 |
+
+No puncture or basis pivot produced cost below v at T = 7 or T = 8 (E7's -14 is the already-known
+in-table gain). The std coordinate decoder remains the best known for D7 (42) and B7 (49); the
+random pivot search did not find it (minima 44 and 49).
+
+## 4. Overcomplete (m = T + 1) decoders: one-extra rank-one census
+
+The identity of PR 2240 with T + 1 terms (exact for every nonzero direction `a` and rational
+`lambda != 0`, verified exactly in the replay):
+
+```text
+p_i = X e_i                      q_i = X(H e_i - lambda a_i a),  i = 1..T
+p_{T+1} = X a                    q_{T+1} = lambda X a
+```
+
+Here `X` is the exact coordinate matrix of the lines in the declared basis and `H` the basis Gram, so
+`sum_j p_j q_j^T = G = X H X^T`. The census enumerates every projective `{-1,0,1}^T` direction plus
+every configuration line as direction, and for each direction every rational lambda support cell
+(each open interval between consecutive breakpoints of the linear forms `p(t) . q_i` and each
+breakpoint itself). Supports and F2 block ranks are constant between breakpoints, so the census is
+exact on the declared family and alphabet, with B = B0 fixed.
+
+Full sets (13 configurations, T = 3..5):
+
+| unit | v | T | directions | cells | min cost | min - v |
+|---|---:|---:|---:|---:|---:|---:|
+| A3 | 6 | 3 | 13 | 102 | 9 | +3 |
+| B3 | 9 | 3 | 22 | 120 | 9 | 0 |
+| {0,+/-1}^3 | 13 | 3 | 13 | 88 | 18 | +5 |
+| A4 | 10 | 4 | 40 | 340 | 16 | +6 |
+| B4 | 16 | 4 | 56 | 320 | 16 | 0 |
+| C4 | 16 | 4 | 56 | 320 | 16 | 0 |
+| D4 | 12 | 4 | 52 | 288 | 12 | 0 |
+| F4 | 24 | 4 | 56 | 416 | 36 | +12 |
+| {0,+/-1}^4 | 40 | 4 | 40 | 360 | 84 | +44 |
+| A5 | 15 | 5 | 121 | 1086 | 25 | +10 |
+| B5 | 25 | 5 | 146 | 856 | 25 | 0 |
+| C5 | 25 | 5 | 146 | 856 | 25 | 0 |
+| D5 | 20 | 5 | 141 | 804 | 20 | 0 |
+
+Exhaustive puncture censuses at T <= 4 (every nonempty subset of lines, family restricted to the
+subset; the per-subset live-count prefilter is validated against unfiltered exact minima on five
+deterministic subsets per configuration):
+
+| unit | subsets | directions | members per subset | min(cost - v) | gains | ties |
+|---|---:|---:|---:|---:|---:|---:|
+| A3 | 63 | 13 | 102 | 0 | 0 | 13 |
+| B3 | 511 | 22 | 120 | 0 | 0 | 91 |
+| {0,+/-1}^3 | 8191 | 13 | 88 | 0 | 0 | 95 |
+| A4 | 1023 | 40 | 340 | 0 | 0 | 37 |
+| B4 | 65535 | 56 | 320 | 0 | 0 | 1279 |
+| C4 | 65535 | 56 | 320 | 0 | 0 | 1279 |
+| D4 | 4095 | 52 | 288 | 0 | 0 | 183 |
+
+Finding: **no overcomplete decoder in this family beats v anywhere in the declared domain.** The
+minimum over the family equals v exactly on every B/C/D-family full set and on 2,977 punctures
+(counted ties), and exceeds v elsewhere. In particular, within this family no D5 decoder with
+m = 6 terms reaches the requested cost 18 (minimum 20 = v), and no D4 or {0,+/-1}^3 puncture
+admits an m = T + 1 factorization with cost below its v. Total: 144,953 subsets censused with
+zero gains.
+
+## Scope and limitations
+
+- Cost is that of the declared factorizations priced with B = B0 (or the stored E6 pairing in the
+  control). A gain found here would be a true gain, but the negative excludes only these
+  decoder/pairing pairs: a sparser admissible B could price below the B0 values, so pairing
+  minimization (PR 2272's open question 2, its 1,023 D5 ties) remains open.
+- The overcomplete census covers exactly one factorization family: the one-extra rank-one identity
+  above with the p_i = X e_i frame fixed, over the declared direction alphabet (all projective
+  ternary directions in the declared basis plus all configuration lines). Unrestricted (m = T + 1)
+  factorizations with moving frames are not covered; the finite support-cell reduction over Q for
+  arbitrary factorizations is the recorded blocker.
+- E6 is not in the overcomplete family census (PR 2240 and the transvection extension of
+  [comment 18938558](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18938558)
+  cover it in the pinned basis, with family minima 40 and 37 against the 35 target; the
+  unrestricted seven-term E6 question stays open).
+- D5 punctures (2^20 - 1 subsets) and all T >= 7 punctures are not enumerated (compute); the D5
+  full set and the T = 7/8 full systems are covered exactly.
+- Basis pivots are seeded (300 per unit) and bounded; no claim over all GL_T(Q) bases. The
+  E7 basis question (is 49 the minimum over bases?) is open, mirroring PR 2272's E6 36-vs-37 question.
+- The greedy/random puncture searches at T = 7/8 are seeded and bounded as recorded in
+  CERTIFICATE.json. No kappa, supplier, paid-profile or selected-frontier change is claimed.
+
+## Open next questions
+
+1. **Pairing minima on ties.** On the tied D7/B7/A7 punctures (cost = v at B0), is the minimum over
+   admissible pairings B exactly v, or can a sparser B price below v? That is PR 2272's open
+   question 2 now at T = 7. First step: exact branch-and-bound over B on the largest tied punctures.
+   Blocker: rank_F2 B[R, A] is not monotone in B, so no monotone relaxation is known.
+2. **Unrestricted overcomplete factorizations at T = 3.** Does any (m = 4)-term exact factorization
+   of the {0,+/-1}^3 Gram matrix with a moving frame beat v = 13? First step: a two-direction
+   correction family (two independent extra frames) with its own exact support-cell reduction.
+   Blocker: no finite support-cell reduction over Q is known for arbitrary (p_j, q_j) tuples.
+3. **E7 basis minimum.** Is the B0 cost of E7 at least 49 over all GL_7(Q) bases (the T = 7 analogue
+   of PR 2272's 36-vs-37 E6 question)? First step: deterministic basis descent with exact
+   recomputation of supports. Blocker: support patterns are not continuous in the basis.
+
+## Reproduce
+
+From the repository root, with Python 3.12 or newer and only the standard library:
+
+```sh
+python3 -B research/polar-law-t7-overcomplete-screen/verify.py
+```
+
+Expected final line `PASS_POLAR_T7_OVERCOMPLETE_SCREEN` (about 316 s on this host). The registered
+replay was run locally under Python 3.12; `make` is not installed on this host, so
+`scripts/research_package.py` was used directly:
+
+```sh
+python3 scripts/research_package.py --package research/polar-law-t7-overcomplete-screen --check-only
+```
+
+prints `PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)`. To regenerate the
+certificate after changing the search, run each stage with `--emit`, e.g.
+`python3 -B research/polar-law-t7-overcomplete-screen/search.py --stage t7t8 --emit`.
+Obligations not checked: host CI replay (queued), human review, and everything listed under
+Scope and limitations.
+
+## Credit and links
+
+Model, cost formula and the threshold question: DreamingOfClouds,
+[PR 2125](https://github.com/CrocSwap/integer-mult-bounds/pull/2125),
+[PR 2228](https://github.com/CrocSwap/integer-mult-bounds/pull/2228),
+[PR 2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111), requests
+[comment 18934590](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18934590)
+item 3 and
+[comment 18936173](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18936173)
+Q1. Small-T screen, checked table and the three open obligations: Aaron Wang with help from opencode,
+[PR 2272](https://github.com/CrocSwap/integer-mult-bounds/pull/2272). One-extra rank-one identity,
+support-cell method and E6 family minima: 1337isnot1337,
+[PR 2240](https://github.com/CrocSwap/integer-mult-bounds/pull/2240) and
+[comment 18938558](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18938558).
+Prior lattice work
+[PR 446](https://github.com/CrocSwap/integer-mult-bounds/pull/446),
+[PR 595](https://github.com/CrocSwap/integer-mult-bounds/pull/595),
+[PR 1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590). The E6 stored basis and pairing
+are PR 2125's `data/e6_best.json`, pinned by SHA-256 in `SOURCES.json`. Prepared by Aaron Wang with
+help from opencode (substantial AI assistance; no independent human review claimed). Apache-2.0.
diff --git a/research/dn-unrestricted-root-code-floor/references/PR2518-search.py b/research/dn-unrestricted-root-code-floor/references/PR2518-search.py
new file mode 100644
index 0000000000..019540d5a7
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/references/PR2518-search.py
@@ -0,0 +1,785 @@
+"""Dense-polar threshold screens at T >= 7 and an overcomplete (m = T + 1) census.
+
+Model (DreamingOfClouds, PR 2125 / PR 2228 / PR 2111; screen convention of
+PR 2272): a configuration is a list of root lines t = 1..v with vectors
+p(t) = q(t) in Q^T. The full-orthogonal-pattern pairing B0 has unit diagonal
+and B_ts = 1 exactly where dot(p(t), p(s)) = 0. An exact coordinate Gram
+decoder M = sum_j p_j q_j^T = Gram is priced
+cost = sum_j rank_F2 B[R_j, A_j] (Theorem C without the floor w), where
+R_j = supp p_j and A_j = supp q_j. A gain is cost < v.
+
+Stages:
+  controls   - positive control: reproduce PR 2272's checked table
+               D4/D5/D6 = 12/20/30, E6 = 36/37, E7 = 49, E8 = 72.
+  t7t8       - exact full-system screens at T = 7 and T = 8.
+  searches   - seeded bounded basis pivots and puncture searches at T = 7/8.
+  overfull   - overcomplete one-extra rank-one family on full sets (small T).
+  overpunc   - overcomplete one-extra rank-one family on every puncture of the
+               declared small-T configurations (shardable).
+
+Everything is exact integer / rational / F2 arithmetic, standard library only.
+Independent reimplementation; predecessor heads are recorded in SOURCES.json.
+"""
+import itertools
+import json
+import os
+import random
+import sys
+from fractions import Fraction as F
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+E6_BEST_PATH = os.path.join(HERE, "sources", "e6_best.json")
+
+# ---------------------------------------------------------------- root lines
+
+def canon(r):
+    f = next(x for x in r if x)
+    return tuple(r) if f > 0 else tuple(-x for x in r)
+
+
+def lines(R):
+    seen, out = set(), []
+    for r in R:
+        c = canon(r)
+        if c not in seen:
+            seen.add(c)
+            out.append(c)
+    return out
+
+
+def A(n):
+    R = []
+    for i in range(n + 1):
+        for j in range(i + 1, n + 1):
+            v = [0] * (n + 1)
+            v[i], v[j] = 2, -2
+            R.append(v)
+    return lines(R)
+
+
+def D(n):
+    R = []
+    for i in range(n):
+        for j in range(i + 1, n):
+            for s in (2, -2):
+                v = [0] * n
+                v[i], v[j] = 2, s
+                R.append(v)
+    return lines(R)
+
+
+def Bn(n):
+    R = []
+    for i in range(n):
+        v = [0] * n
+        v[i] = 2
+        R.append(v)
+        for j in range(i + 1, n):
+            for s in (2, -2):
+                w = [0] * n
+                w[i], w[j] = 2, s
+                R.append(w)
+    return lines(R)
+
+
+def Cn(n):
+    R = []
+    for i in range(n):
+        v = [0] * n
+        v[i] = 4
+        R.append(v)
+        for j in range(i + 1, n):
+            for s in (2, -2):
+                w = [0] * n
+                w[i], w[j] = 2, s
+                R.append(w)
+    return lines(R)
+
+
+def F4():
+    R = []
+    for i in range(4):
+        v = [0] * 4
+        v[i] = 2
+        R.append(v)
+        for j in range(i + 1, 4):
+            for s in (2, -2):
+                w = [0] * 4
+                w[i], w[j] = 2, s
+                R.append(w)
+    for sg in itertools.product((1, -1), repeat=4):
+        R.append(list(sg))
+    return lines(R)
+
+
+def E8():
+    R = [list(r) for r in D(8)]
+    for sg in itertools.product((1, -1), repeat=8):
+        if sg.count(-1) % 2 == 0:
+            R.append(list(sg))
+    return lines(R)
+
+
+def dot(a, b):
+    return sum(x * y for x, y in zip(a, b))
+
+
+def E7():
+    return [r for r in E8() if sum(r) == 0]
+
+
+def E6():
+    r1 = [2, -2, 0, 0, 0, 0, 0, 0]
+    r2 = [0, 2, -2, 0, 0, 0, 0, 0]
+    return [r for r in E8() if dot(r, r1) == 0 and dot(r, r2) == 0]
+
+
+def pm1_lines(T):
+    """All lines with coordinates in {0, +1, -1}, canonical sign."""
+    R = []
+    for r in itertools.product((1, 0, -1), repeat=T):
+        if any(r):
+            R.append(list(r))
+    return lines(R)
+
+
+# ------------------------------------------------------------ F2 machinery
+
+def rank2(rows):
+    piv = []
+    for x in rows:
+        for p in piv:
+            x = min(x, x ^ p)
+        if x:
+            piv.append(x)
+            piv.sort(reverse=True)
+    return len(piv)
+
+
+def b0_rows(L):
+    """Full orthogonal pattern as bitset rows: unit diagonal + orth pairs."""
+    v = len(L)
+    out = []
+    for t in range(v):
+        bits = 1 << t
+        for s in range(v):
+            if s != t and dot(L[t], L[s]) == 0:
+                bits |= 1 << s
+        out.append(bits)
+    return out
+
+
+def supports(P):
+    """Column supports of the coefficient matrix P (nonzero test over Q)."""
+    v = len(P)
+    T = len(P[0]) if P else 0
+    return [frozenset(t for t in range(v) if P[t][j] != 0) for j in range(T)]
+
+
+def cost_from_supports(Brows, RS, AS):
+    out = []
+    for R, A in zip(RS, AS):
+        if not R or not A:
+            out.append(0)
+            continue
+        amask = 0
+        for s in A:
+            amask |= 1 << s
+        rows = [Brows[t] & amask for t in R]
+        out.append(rank2(rows))
+    return out
+
+
+def cost_from_masks(Brows, RS, AS):
+    """Same cost with supports given as bitmasks."""
+    out = []
+    n = len(Brows)
+    for R, A in zip(RS, AS):
+        if not R or not A:
+            out.append(0)
+            continue
+        rows = [Brows[t] & A for t in range(n) if (R >> t) & 1]
+        out.append(rank2(rows))
+    return out
+
+
+def sup_mask(S):
+    m = 0
+    for s in S:
+        m |= 1 << s
+    return m
+
+
+# ------------------------------------------------- exact coordinate decoder
+
+def solve_coords(basis, r):
+    n = len(basis)
+    m = len(r)
+    M = [[F(basis[i][k]) for i in range(n)] + [F(r[k])] for k in range(m)]
+    piv, row = [], 0
+    for c in range(n):
+        p = next((i for i in range(row, m) if M[i][c] != 0), None)
+        if p is None:
+            raise ValueError("dependent basis")
+        M[row], M[p] = M[p], M[row]
+        inv = M[row][c]
+        M[row] = [x / inv for x in M[row]]
+        for i in range(m):
+            if i != row and M[i][c] != 0:
+                f = M[i][c]
+                M[i] = [a - f * b for a, b in zip(M[i], M[row])]
+        row += 1
+    return [M[i][n] for i in range(n)]
+
+
+def frac_rank(rows):
+    M = [[F(x) for x in r] for r in rows]
+    rk = 0
+    if not M:
+        return 0
+    for c in range(len(M[0])):
+        p = next((i for i in range(rk, len(M)) if M[i][c] != 0), None)
+        if p is None:
+            continue
+        M[rk], M[p] = M[p], M[rk]
+        for i in range(rk + 1, len(M)):
+            if M[i][c] != 0:
+                f = M[i][c] / M[rk][c]
+                M[i] = [a - f * b for a, b in zip(M[i], M[rk])]
+        rk += 1
+    return rk
+
+
+def first_basis(L):
+    idx, cur = [], []
+    for i, r in enumerate(L):
+        if frac_rank(cur + [r]) > len(cur):
+            idx.append(i)
+            cur.append(r)
+    return idx
+
+
+def decoder_std(L):
+    return [[F(x) for x in r] for r in L], [[F(x) for x in r] for r in L]
+
+
+def decoder_basis(L, bidx):
+    basis = [L[i] for i in bidx]
+    n = len(basis)
+    C = [[dot(basis[i], basis[k]) for k in range(n)] for i in range(n)]
+    P = [solve_coords(basis, r) for r in L]
+    Q = [[sum(P[t][i] * C[i][k] for i in range(n)) for k in range(n)] for t in range(len(L))]
+    return P, Q
+
+
+def config_cost(L, P, Q, Brows=None):
+    if Brows is None:
+        Brows = b0_rows(L)
+    RS, AS = supports(P), supports(Q)
+    br = cost_from_supports(Brows, RS, AS)
+    return sum(br), br
+
+
+# ------------------------------------------------------ one-extra rank-one
+
+def ternary_dirs(T):
+    """All projective directions a in Q^T with entries in {0, +1, -1}."""
+    out = set()
+    for r in itertools.product((1, 0, -1), repeat=T):
+        if any(r):
+            out.add(tuple(F(x) for x in canon(list(r))))
+    return sorted(out)
+
+
+def one_extra_cells(X, H, a):
+    """All exact lambda support cells of PR 2240's identity for direction a.
+
+    p_i = X e_i, q_i = X(H e_i - lambda a_i a), i = 1..T
+    p_{T+1} = X a, q_{T+1} = lambda X a.
+    Returns a list of tuples (cell_id, [term supports (R_j, A_j) masks]).
+    Supports are constant on each cell; cells are the open intervals between
+    consecutive breakpoints plus the breakpoints themselves (lambda != 0).
+    """
+    T = len(X[0])
+    n = len(X)
+    alpha = [dot(X[t], a) for t in range(n)]           # p(t) . a
+    beta = [[dot(X[t], [H[i][k] for k in range(T)]) for i in range(T)] for t in range(n)]
+    # p(t) . q_i = beta[t][i] - lambda * a[i] * alpha[t]
+    brk = set()
+    for t in range(n):
+        for i in range(T):
+            ai = a[i]
+            if ai != 0 and alpha[t] != 0:
+                brk.add(F(beta[t][i], 1) / (F(ai) * F(alpha[t])))
+    brk = sorted(b for b in brk if b != 0)
+    samples = [("at", b) for b in brk]
+    cuts = sorted(set([F(0)] + brk))
+    # Open cells between consecutive cut points, plus the two unbounded cells.
+    edges = [None] + cuts + [None]
+    for lo, hi in zip(edges, edges[1:]):
+        if lo is None and hi is None:
+            continue
+        if lo is None:
+            samples.append(("in", hi - 1))
+        elif hi is None:
+            samples.append(("in", lo + 1))
+        else:
+            samples.append(("in", (lo + hi) / 2))
+    S = [sup_mask(t for t in range(n) if X[t][i] != 0) for i in range(T)]
+    Ta = sup_mask(t for t in range(n) if alpha[t] != 0)
+    out = []
+    for cid, lam in samples:
+        AS = []
+        for i in range(T):
+            if a[i] == 0:
+                c = [H[i][k] for k in range(T)]
+            else:
+                c = [F(H[i][k]) - F(lam) * F(a[i]) * F(a[k]) for k in range(T)]
+            AS.append(sup_mask(t for t in range(n) if dot(X[t], c) != 0))
+        terms = [(S[i], AS[i]) for i in range(T)] + [(Ta, Ta)]
+        out.append((cid, lam, terms))
+    return out
+
+
+def verify_identity(X, H, a, lam):
+    """Exact check that the one-extra identity sums to G = X H X^T at (a, lam),
+    and that the recorded supports match the constructed p_j, q_j."""
+    T = len(X[0])
+    n = len(X)
+    G = [[sum(X[t][i] * H[i][k] * X[s][k] for i in range(T) for k in range(T))
+          for s in range(n)] for t in range(n)]
+    P, Q = [], []
+    for i in range(T):
+        pi = [X[t][i] for t in range(n)]
+        qi = [sum(X[t][k] * (F(H[i][k]) - F(lam) * F(a[i]) * F(a[k])) for k in range(T))
+              for t in range(n)]
+        P.append(pi)
+        Q.append(qi)
+    P.append([sum(X[t][k] * F(a[k]) for k in range(T)) for t in range(n)])
+    Q.append([F(lam) * sum(X[t][k] * F(a[k]) for k in range(T)) for t in range(n)])
+    for t in range(n):
+        for s in range(n):
+            lhs = sum(P[j][t] * Q[j][s] for j in range(T + 1))
+            if lhs != G[t][s]:
+                return False, "identity mismatch at (%d,%d)" % (t, s)
+    for t in range(n):
+        if G[t][t] == 0:
+            return False, "zero diagonal at %d" % t
+    return True, "ok"
+
+
+def one_extra_census_full(L, X, H, dirs, label):
+    """Exact census of the one-extra rank-one family on one full configuration."""
+    n = len(L)
+    T = len(X[0])
+    Brows = b0_rows(L)
+    best = None
+    hist = {}
+    cells_total = 0
+    ident_ok = 0
+    for a in dirs:
+        cells = one_extra_cells(X, H, a)
+        for k, (cid, lam, terms) in enumerate(cells):
+            cells_total += 1
+            if k in (0, len(cells) // 2, len(cells) - 1):
+                ok, why = verify_identity(X, H, a, lam)
+                if not ok:
+                    raise AssertionError("identity failed for %s dir=%s cell=%s: %s" % (label, a, cid, why))
+                ident_ok += 1
+            br = cost_from_masks(Brows, [R for R, _ in terms], [A for _, A in terms])
+            c = sum(br)
+            hist[c] = hist.get(c, 0) + 1
+            if best is None or c < best[0]:
+                best = (c, list(a), cid, str(lam))
+    return {
+        "label": label,
+        "v": n,
+        "T": T,
+        "directions": len(dirs),
+        "cells": cells_total,
+        "identity_checks": ident_ok,
+        "min_cost": best[0],
+        "min_cost_minus_v": best[0] - n,
+        "min_witness": {"dir": [str(x) for x in best[1]], "cell": best[2], "lambda": str(best[3])},
+        "hist": {str(k): hist[k] for k in sorted(hist)},
+    }
+
+
+def one_extra_punctures(L, X, H, dirs, label, mask_range=None):
+    """Exhaustive puncture census: every nonempty subset U of lines, with the
+    family restricted to U (supports and B0 intersected with U).
+
+    The per-subset live-count prefilter is validated against unfiltered exact
+    minima on a deterministic sample of subsets (brute_masks)."""
+    n = len(L)
+    T = len(X[0])
+    Brows = b0_rows(L)
+    # Precompute the global family term-support tuples once.
+    fam = []
+    for a in dirs:
+        for cid, lam, terms in one_extra_cells(X, H, a):
+            fam.append([(R, A) for R, A in terms])
+    lo, hi = (1, (1 << n) - 1) if mask_range is None else mask_range
+    brute_masks = {lo, hi, lo + 1, hi - 1, (lo + hi) // 2}
+    brute_mismatches = []
+    gains = []
+    best = None
+    ties = 0
+    checked = 0
+    for mask in range(lo, hi + 1):
+        vs = mask.bit_count()
+        checked += 1
+        cache = {}
+
+        def block_rank(R, A):
+            key = (R & mask, A & mask)
+            v = cache.get(key)
+            if v is None:
+                k, l = key
+                if not k or not l:
+                    v = 0
+                else:
+                    rows = [Brows[t] & l for t in range(n) if (k >> t) & 1]
+                    v = rank2(rows)
+                cache[key] = v
+            return v
+
+        best_u = None
+        for terms in fam:
+            live = 0
+            for R, A in terms:
+                k, l = R & mask, A & mask
+                if not k or not l:
+                    continue
+                for t in range(n):
+                    if (k >> t) & 1 and Brows[t] & l:
+                        live += 1
+                        break
+            if best_u is not None and live >= best_u:
+                continue
+            c = sum(block_rank(R, A) for R, A in terms)
+            if best_u is None or c < best_u:
+                best_u = c
+            if best_u == 0:
+                break
+        d = best_u - vs
+        if mask in brute_masks:
+            brute = min(sum(block_rank(R, A) for R, A in terms) for terms in fam)
+            if brute != best_u:
+                brute_mismatches.append((mask, best_u, brute))
+        if best is None or d < best[0]:
+            best = (d, mask, vs, best_u)
+        if best_u < vs:
+            gains.append((mask, vs, best_u))
+        elif best_u == vs:
+            ties += 1
+    return {
+        "label": label,
+        "lines": n,
+        "subsets_checked": checked,
+        "directions": len(dirs),
+        "family_members_per_subset": len(fam),
+        "min_cost_minus_v": best[0],
+        "best_mask": best[1],
+        "best_v": best[2],
+        "best_cost": best[3],
+        "gain_count": len(gains),
+        "gains": gains[:10],
+        "tie_count": ties,
+        "brute_masks_checked": sorted(m for m in brute_masks if lo <= m <= hi),
+        "brute_mismatches": brute_mismatches,
+    }
+
+
+# ------------------------------------------------------------------ controls
+
+def expect(name, got, want, fails):
+    ok = got == want
+    print("CTRL %-42s got=%s want=%s %s" % (name, got, want, "OK" if ok else "MISMATCH"))
+    if not ok:
+        fails.append((name, got, want))
+    return ok
+
+
+def stage_controls(fails, cert):
+    """Positive control: PR 2272's checked table (PR 2125 values)."""
+    tab = {}
+    for nm in ("D4", "D5", "D6"):
+        L = {"D4": D(4), "D5": D(5), "D6": D(6)}[nm]
+        P, Q = decoder_std(L)
+        c, br = config_cost(L, P, Q)
+        tab[nm] = {"v": len(L), "T": len(L[0]), "cost": c, "block_ranks": br}
+        expect("%s std B0 cost" % nm, c, {"D4": 12, "D5": 20, "D6": 30}[nm], fails)
+    L6 = E6()
+    with open(E6_BEST_PATH, encoding="utf-8") as f:
+        e6 = json.load(f)
+    P6, Q6 = decoder_basis(L6, e6["basis"])
+    Bstored = [e6["rows"][t] for t in range(len(L6))]
+    cs, brs = config_cost(L6, P6, Q6, Bstored)
+    expect("E6 stored basis + stored B cost", cs, 36, fails)
+    expect("E6 stored cost matches e6_best.json", cs, e6["cost"], fails)
+    cb, brb = config_cost(L6, P6, Q6)
+    P6f, Q6f = decoder_basis(L6, first_basis(L6))
+    cf, brf = config_cost(L6, P6f, Q6f)
+    expect("E6 first-basis B0 cost", cf, 37, fails)
+    tab["E6"] = {"v": 36, "T": 6, "cost": cs, "block_ranks": brs}
+    tab["E6_firstB0"] = {"v": 36, "T": 6, "cost": cf, "block_ranks": brf}
+    tab["E6_storedB0"] = {"v": 36, "T": 6, "cost": cb, "block_ranks": brb}
+    L7, L8 = E7(), E8()
+    P7, Q7 = decoder_basis(L7, first_basis(L7))
+    c7, br7 = config_cost(L7, P7, Q7)
+    expect("E7 first-basis B0 cost", c7, 49, fails)
+    tab["E7"] = {"v": len(L7), "T": 7, "cost": c7, "block_ranks": br7}
+    P8, Q8 = decoder_basis(L8, first_basis(L8))
+    c8, br8 = config_cost(L8, P8, Q8)
+    expect("E8 first-basis B0 cost", c8, 72, fails)
+    tab["E8"] = {"v": len(L8), "T": 8, "cost": c8, "block_ranks": br8}
+    for nm, want in (("A4", 16), ("A5", 25), ("A6", 36)):
+        L = {"A4": A(4), "A5": A(5), "A6": A(6)}[nm]
+        P, Q = decoder_basis(L, first_basis(L))
+        c, br = config_cost(L, P, Q)
+        tab[nm + "_firstBasis"] = {"v": len(L), "T": len(P[0]), "cost": c, "block_ranks": br}
+        expect("%s first-basis B0 cost" % nm, c, want, fails)
+    # mutation control: B = identity must change the cost on D5 and E7
+    L5 = D(5)
+    P5, Q5 = decoder_std(L5)
+    ci, _ = config_cost(L5, P5, Q5, [1 << t for t in range(len(L5))])
+    expect("D5 mutated B=I cost differs from 20", ci != 20, True, fails)
+    ci7, _ = config_cost(L7, P7, Q7, [1 << t for t in range(len(L7))])
+    expect("E7 mutated B=I cost differs from 49", ci7 != 49, True, fails)
+    cert["controls"] = tab
+    return tab
+
+
+# ------------------------------------------------------------- T = 7, 8
+
+def stage_t7t8(cert):
+    full = {}
+    jobs = (("A7", A(7), "first"), ("B7", Bn(7), "std"), ("C7", Cn(7), "std"),
+            ("D7", D(7), "std"), ("E7", E7(), "first"),
+            ("pm1_T7", pm1_lines(7), "std"),
+            ("A8", A(8), "first"), ("B8", Bn(8), "std"), ("C8", Cn(8), "std"),
+            ("D8", D(8), "std"), ("E8", E8(), "first"),
+            ("pm1_T8", pm1_lines(8), "std"))
+    for nm, L, kind in jobs:
+        if kind == "std":
+            P, Q = decoder_std(L)
+        else:
+            P, Q = decoder_basis(L, first_basis(L))
+        c, br = config_cost(L, P, Q)
+        v = len(L)
+        width = len(P[0])
+        full[nm] = {"v": v, "T_width": width, "ambient": len(L[0]), "cost": c,
+                    "cost_minus_v": c - v, "gain": c < v,
+                    "v_over_Tsq": v > width * width, "block_ranks": br}
+        print("T78 %-8s v=%4d width=%d ambient=%d cost=%5d cost-v=%+d gain=%s v>T^2=%s"
+              % (nm, v, width, len(L[0]), c, c - v, c < v, v > width * width))
+    cert["t7t8_full"] = full
+
+
+def stage_searches(cert):
+    rng = random.Random(20261015)
+    out = {}
+    jobs = (("A7", A(7)), ("B7", Bn(7)), ("D7", D(7)), ("E7", E7()),
+            ("A8", A(8)), ("B8", Bn(8)), ("D8", D(8)))
+    for nm, L in jobs:
+        T = frac_rank(L)
+        best = None
+        idxs = list(range(len(L)))
+        for _ in range(300):
+            rng.shuffle(idxs)
+            pick, cur = [], []
+            for i in idxs:
+                if len(pick) >= T:
+                    break
+                if frac_rank(cur + [L[i]]) > len(cur):
+                    pick.append(i)
+                    cur.append(L[i])
+            if len(pick) != T:
+                continue
+            try:
+                P, Q = decoder_basis(L, pick)
+            except ValueError:
+                continue
+            c, _ = config_cost(L, P, Q)
+            if best is None or c < best[0]:
+                best = (c, list(pick))
+        stdc, _ = config_cost(L, *decoder_std(L)) if frac_rank(L) == len(L[0]) else (None, None)
+        out[nm + "_basis_pivot"] = {"trials": 300, "min_cost": best[0], "v": len(L),
+                                    "min_cost_minus_v": best[0] - len(L),
+                                    "std_cost": stdc, "basis": best[1]}
+        print("PIV %-8s bases=300 min=%d v=%d min-v=%+d" % (nm, best[0], len(L), best[0] - len(L)))
+    # seeded greedy/random puncture searches at T = 7/8 (small systems only)
+    for nm, L in (("A7", A(7)), ("B7", Bn(7)), ("D7", D(7))):
+        P, Q = decoder_std(L) if frac_rank(L) == len(L[0]) else decoder_basis(L, first_basis(L))
+        n = len(L)
+        Brows = b0_rows(L)
+        T = len(P[0])
+        Pnz = [frozenset(j for j in range(T) if P[t][j] != 0) for t in range(n)]
+        Qnz = [frozenset(j for j in range(T) if Q[t][j] != 0) for t in range(n)]
+
+        def cost_of(mask):
+            br = 0
+            for j in range(T):
+                rows = [Brows[t] & mask for t in range(n) if (mask >> t) & 1 and j in Pnz[t]]
+                cols = sup_mask(s for s in range(n) if (mask >> s) & 1 and j in Qnz[s])
+                br += rank2([rw & cols for rw in rows]) if rows else 0
+            return br
+
+        best = None
+        for _ in range(12):
+            vs = rng.randint(2, n)
+            mask = 0
+            for t in rng.sample(range(n), vs):
+                mask |= 1 << t
+            cur = cost_of(mask) - mask.bit_count()
+            if best is None or cur < best[0]:
+                best = (cur, mask)
+            for _ in range(250):
+                t = rng.randrange(n)
+                cand = mask ^ (1 << t)
+                if cand.bit_count() < 2:
+                    continue
+                d = cost_of(cand) - cand.bit_count()
+                if d <= cur:
+                    mask, cur = cand, d
+                    if d < best[0]:
+                        best = (d, mask)
+        for _ in range(200):
+            vs = rng.randint(2, n)
+            mask = 0
+            for t in rng.sample(range(n), vs):
+                mask |= 1 << t
+            d = cost_of(mask) - mask.bit_count()
+            if d < best[0]:
+                best = (d, mask)
+        out[nm + "_puncture_search"] = {"greedy_restarts": 12, "greedy_steps": 250,
+                                        "random_trials": 200, "min_cost_minus_v": best[0],
+                                        "mask": best[1], "v": best[1].bit_count(),
+                                        "cost": best[0] + best[1].bit_count()}
+        print("SRCH %-8s min(cost-v)=%+d (v=%d)" % (nm, best[0], best[1].bit_count()))
+    cert["t7t8_searches"] = out
+
+
+# ------------------------------------------------------------ overcomplete
+
+def configs_smallT():
+    """(label, L, X, H) for the overcomplete census.
+
+    Uses standard coordinates (H = I) where the line span is the full ambient
+    space (D/B/C/F4/{0,+/-1} families, the PR 2125 D-series convention) and the
+    first-independent span basis otherwise (A family)."""
+    out = []
+    for nm, L in (("A3", A(3)), ("B3", Bn(3)), ("pm1_T3", pm1_lines(3)),
+                  ("A4", A(4)), ("B4", Bn(4)), ("C4", Cn(4)), ("D4", D(4)), ("F4", F4()),
+                  ("pm1_T4", pm1_lines(4)),
+                  ("A5", A(5)), ("B5", Bn(5)), ("C5", Cn(5)), ("D5", D(5))):
+        if frac_rank(L) == len(L[0]):
+            P, Q = decoder_std(L)
+            H = [[1 if i == k else 0 for k in range(len(L[0]))] for i in range(len(L[0]))]
+        else:
+            bidx = first_basis(L)
+            P, Q = decoder_basis(L, bidx)
+            basis = [L[i] for i in bidx]
+            T = len(basis)
+            H = [[dot(basis[i], basis[k]) for k in range(T)] for i in range(T)]
+        out.append((nm, L, P, H))
+    return out
+
+
+def stage_overfull(cert):
+    res = {}
+    for nm, L, X, H in configs_smallT():
+        T = len(X[0])
+        dirs = sorted(set(ternary_dirs(T)) | set(canon([x for x in r]) for r in X))
+        dirs = [tuple(F(x) for x in a) for a in dirs]
+        r = one_extra_census_full(L, X, H, dirs, nm)
+        res[nm] = r
+        print("OVF %-8s v=%3d T=%d dirs=%d cells=%d min=%d min-v=%+d"
+              % (nm, r["v"], r["T"], r["directions"], r["cells"], r["min_cost"], r["min_cost_minus_v"]))
+    cert["overcomplete_full"] = res
+
+
+def stage_overpunc(cert, only=None, mask_range=None):
+    res = {}
+    for nm, L, X, H in configs_smallT():
+        if only is not None and nm not in only:
+            continue
+        if nm not in ("A3", "B3", "pm1_T3", "A4", "B4", "C4", "D4"):
+            continue
+        T = len(X[0])
+        dirs = sorted(set(ternary_dirs(T)) | set(canon([x for x in r]) for r in X))
+        dirs = [tuple(F(x) for x in a) for a in dirs]
+        r = one_extra_punctures(L, X, H, dirs, nm, mask_range=mask_range)
+        if r["brute_mismatches"]:
+            raise AssertionError("prefilter mismatch on %s: %s" % (nm, r["brute_mismatches"]))
+        res[nm] = r
+        print("OVP %-8s subsets=%d dirs=%d members=%d min(cost-v)=%+d gains=%d ties=%d"
+              % (nm, r["subsets_checked"], r["directions"], r["family_members_per_subset"],
+                 r["min_cost_minus_v"], r["gain_count"], r["tie_count"]))
+    cert.setdefault("overcomplete_punctures", {}).update(res)
+
+
+# ----------------------------------------------------------------- driver
+
+def compute(stage, fails, cert, only=None, mask_range=None):
+    if stage == "controls":
+        stage_controls(fails, cert)
+    elif stage == "t7t8":
+        stage_t7t8(cert)
+    elif stage == "searches":
+        stage_searches(cert)
+    elif stage == "overfull":
+        stage_overfull(cert)
+    elif stage == "overpunc":
+        stage_overpunc(cert, only=only, mask_range=mask_range)
+    else:
+        raise SystemExit("unknown stage: " + stage)
+
+
+def main(argv):
+    sys.stdout.reconfigure(encoding="utf-8")
+    args = argv[1:]
+    emit = "--emit" in args
+    args = [a for a in args if a != "--emit"]
+    stage = "all"
+    only = None
+    mask_range = None
+    if "--stage" in args:
+        stage = args[args.index("--stage") + 1]
+    if "--only" in args:
+        only = set(args[args.index("--only") + 1].split(","))
+    if "--mask-range" in args:
+        lo, hi = args[args.index("--mask-range") + 1].split(":")
+        mask_range = (int(lo), int(hi))
+    fails = []
+    cert_path = os.path.join(HERE, "CERTIFICATE.json")
+    cert = {"screen": "polar-law T >= 7 threshold screens and small-T overcomplete census",
+            "model": "full-orthogonal-pattern pairing B0, exact coordinate Gram decoder(s), cost = sum_j rank_F2 B[R_j, A_j]",
+            "python": sys.version.split()[0]}
+    stages = ["controls", "t7t8", "searches", "overfull", "overpunc"] if stage == "all" else [stage]
+    for st in stages:
+        print("== stage %s ==" % st)
+        compute(st, fails, cert, only=only, mask_range=mask_range)
+    cert["control_failures"] = fails
+    if emit:
+        # Merge with any existing certificate so shard runs accumulate.
+        if os.path.exists(cert_path):
+            old = json.load(open(cert_path, encoding="utf-8"))
+            for k, v in cert.items():
+                if k in ("overcomplete_punctures", "overcomplete_full", "t7t8_full", "t7t8_searches") and isinstance(v, dict):
+                    merged = dict(old.get(k, {}))
+                    merged.update(v)
+                    old[k] = merged
+                else:
+                    old[k] = v
+            cert = old
+        with open(cert_path, "w", encoding="utf-8") as f:
+            json.dump(cert, f, indent=1, sort_keys=True)
+        print("CERTIFICATE:", cert_path)
+    print("CONTROL_FAILURES:", len(fails))
+    return 1 if fails else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main(sys.argv))
diff --git a/research/dn-unrestricted-root-code-floor/verify.py b/research/dn-unrestricted-root-code-floor/verify.py
new file mode 100644
index 0000000000..91a5a439f6
--- /dev/null
+++ b/research/dn-unrestricted-root-code-floor/verify.py
@@ -0,0 +1,299 @@
+#!/usr/bin/env python3
+"""Finite checks for the uniform written D_n root-code floor.
+
+ywz65 with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+import ast
+import hashlib
+import itertools as it
+import json
+from fractions import Fraction as Q
+from pathlib import Path
+import random
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def need(value, message):
+    if not value:
+        raise ValueError(message)
+
+
+def canonical(x):
+    return json.dumps(x, sort_keys=True, separators=(',', ':'), allow_nan=False)
+
+
+def authenticate():
+    dependency = json.loads((HERE / 'DEPENDENCY.json').read_bytes())
+    for row in dependency['files']:
+        raw = (HERE / row['retained']).read_bytes()
+        need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256: ' + row['retained'])
+        need(hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == row['git_blob'], 'source blob')
+    sources = json.loads((HERE / 'SOURCES.json').read_bytes())
+    for row in sources['files']:
+        if row['usage'] != 'input':
+            continue
+        raw = (ROOT / row['path']).read_bytes()
+        need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'input source SHA256')
+        need(hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == row['git_blob'], 'input source blob')
+    # Use only these three authenticated, pure source functions, not its search.
+    path = HERE / 'references/PR2518-search.py'
+    tree = ast.parse(path.read_bytes(), filename=str(path))
+    nodes = [x for x in tree.body if isinstance(x, ast.FunctionDef) and x.name in ('canon', 'lines', 'D')]
+    need([x.name for x in nodes] == ['canon', 'lines', 'D'], 'source D generator inventory')
+    scope = {}
+    exec(compile(ast.Module(body=nodes, type_ignores=[]), str(path), 'exec'), scope)
+    return scope['D']
+
+
+def binary_rank(rows):
+    pivots = {}
+    for row in rows:
+        while row:
+            pivot = row.bit_length() - 1
+            if pivot in pivots:
+                row ^= pivots[pivot]
+            else:
+                pivots[pivot] = row
+                break
+    return len(pivots)
+
+
+def rank(matrix, prime=None):
+    a = [[Q(x) if prime is None else int(x) % prime for x in row] for row in matrix]
+    if not a:
+        return 0
+    pos = 0
+    for c in range(len(a[0])):
+        pivot = next((r for r in range(pos, len(a)) if a[r][c]), None)
+        if pivot is None:
+            continue
+        a[pos], a[pivot] = a[pivot], a[pos]
+        inv = 1 / a[pos][c] if prime is None else pow(a[pos][c], -1, prime)
+        a[pos] = [v * inv if prime is None else v * inv % prime for v in a[pos]]
+        for r in range(pos + 1, len(a)):
+            q = a[r][c]
+            a[r] = [v - q * w if prime is None else (v - q * w) % prime for v, w in zip(a[r], a[pos])]
+        pos += 1
+        if pos == len(a):
+            break
+    return pos
+
+
+def dot(x, y, prime=None):
+    value = sum(a * b for a, b in zip(x, y))
+    return value if prime is None else value % prime
+
+
+def roots(n):
+    return [tuple((1 if k == i else s if k == j else 0) for k in range(n))
+            for i in range(n) for j in range(i + 1, n) for s in (1, -1)]
+
+
+def pairing(rr):
+    return [sum(1 << j for j, y in enumerate(rr) if i == j or dot(x, y) == 0)
+            for i, x in enumerate(rr)]
+
+
+def support(rr, x, prime=None):
+    return sum(1 << i for i, r in enumerate(rr) if dot(r, x, prime))
+
+
+def rectangle(bb, s, t):
+    return binary_rank([row & t for i, row in enumerate(bb) if s >> i & 1])
+
+
+def axis(x):
+    indices = [i for i, v in enumerate(x) if v]
+    return indices[0] if len(indices) == 1 else None
+
+
+def expected_term(n, x, y):
+    if n % 2 == 0:
+        return n - 1
+    a, b = axis(x), axis(y)
+    if a is None and b is None:
+        return n
+    return n - 2 if a is not None and b is not None and a != b else n - 1
+
+
+def patterns(n):
+    out = set()
+    for size in (1, 2, 3):
+        for indices in it.combinations(range(n), size):
+            for values in it.product((-1, 1, 2), repeat=size):
+                x = [0] * n
+                for i, v in zip(indices, values):
+                    x[i] = v
+                out.add(tuple(x))
+    out.add(tuple(range(1, n + 1)))
+    out.add((1,) * n)
+    return sorted(out)
+
+
+def finite_support_checks(source_d):
+    reports = []
+    for n in range(4, 13):
+        rr = roots(n)
+        need(source_d(n) == [tuple(2 * x for x in r) for r in rr], 'source root binding')
+        bb = pairing(rr)
+        h = n if n % 2 else n - 1
+        need(binary_rank(bb) == h, 'full binary rank parity')
+        need(rank(rr) == n, 'rational root injection')
+        # Every codeword in the label description, with radical duplicates removed.
+        words = set()
+        isolated = []
+        for a in (0, 1):
+            for s in range(1 << n):
+                if s.bit_count() % 2:
+                    continue
+                word = 0
+                for k, r in enumerate(rr):
+                    i, j = [i for i, v in enumerate(r) if v]
+                    if a ^ (s >> i & 1) ^ (s >> j & 1):
+                        word |= 1 << k
+                words.add(word)
+        need(len(words) == 1 << h, 'full code cardinality')
+        for word in words - {0}:
+            touched = {i for k, r in enumerate(rr) if word >> k & 1 for i, v in enumerate(r) if v}
+            missing = sorted(set(range(n)) - touched)
+            need(not missing or (n % 2 and len(missing) == 1), 'isolated vertex classification')
+            if missing:
+                isolated.extend(missing)
+            if n <= 8:
+                need(rank([r for k, r in enumerate(rr) if word >> k & 1], 3) == len(touched), 'actual F3 zero-root rank')
+        need(sorted(isolated) == (list(range(n)) if n % 2 else []), 'exact deficient axis classes')
+        reports.append({'n': n, 'roots': len(rr), 'binary_rank': h, 'codewords': len(words), 'isolated_classes': len(isolated)})
+    # All distinct supports of the bounded vector list, over three exact fields.
+    pairs = []
+    for n in range(4, 8):
+        rr, bb = roots(n), pairing(roots(n))
+        for prime in (None, 3, 5):
+            representatives = {}
+            for x in patterns(n):
+                v = x if prime is None else tuple(a % prime for a in x)
+                representatives.setdefault(support(rr, v, prime), v)
+            count = 0
+            for s, x in representatives.items():
+                for t, y in representatives.items():
+                    need(rectangle(bb, s, t) == expected_term(n, x, y), 'exact support tariff')
+                    count += 1
+            pairs.append({'n': n, 'field': 'Q' if prime is None else f'F{prime}', 'supports': len(representatives), 'pairs': count})
+    return reports, pairs
+
+
+def factor_fixtures():
+    rng = random.Random(22772518)
+    reports = []
+    for n in range(4, 10):
+        rr, bb = roots(n), pairing(roots(n))
+        for prime in (None, 3, 5):
+            for extra in range(4):
+                for trial in range(5):
+                    # X=[I,A], Y^T=[I-A B;B] is exact at arbitrary term counts.
+                    a = [[rng.randrange(-2, 3) for _ in range(extra)] for _ in range(n)]
+                    b = [[rng.randrange(-2, 3) for _ in range(n)] for _ in range(extra)]
+                    xrows = [[int(i == j) for j in range(n)] + a[i] for i in range(n)]
+                    yt = [[int(i == j) - sum(a[i][k] * b[k][j] for k in range(extra)) for j in range(n)]
+                          for i in range(n)] + b
+                    xs = [list(col) for col in zip(*xrows)]
+                    ys = [list(row) for row in yt]
+                    # Simultaneous inverse-transpose shear preserves identity,
+                    # and exposes factors beyond the fixed coordinate family.
+                    for _ in range(trial):
+                        u, v = rng.sample(range(n), 2)
+                        scalar = rng.choice((-2, -1, 1, 2))
+                        for x, y in zip(xs, ys):
+                            x[u] += scalar * x[v]
+                            y[v] -= scalar * y[u]
+                    if prime is not None:
+                        xs = [[v % prime for v in x] for x in xs]
+                        ys = [[v % prime for v in y] for y in ys]
+                    else:
+                        # Nonintegral reciprocal term scaling preserves each
+                        # outer product but tests actual rational supports.
+                        for k in range(len(xs)):
+                            scale = Q((-1) ** k * (k + 2), k + 3)
+                            xs[k] = [scale * v for v in xs[k]]
+                            ys[k] = [v / scale for v in ys[k]]
+                    terms = [(x, y) for x, y in zip(xs, ys) if any(x) and any(y)]
+                    actual = [[sum(x[i] * y[j] for x, y in terms) for j in range(n)] for i in range(n)]
+                    if prime:
+                        actual = [[v % prime for v in row] for row in actual]
+                    need(actual == [[int(i == j) for j in range(n)] for i in range(n)], 'exact Gram factorization')
+                    bill = sum(rectangle(bb, support(rr, x, prime), support(rr, y, prime)) for x, y in terms)
+                    m = len(terms)
+                    cheap = sum(expected_term(n, x, y) == n - 2 for x, y in terms) if n % 2 else 0
+                    need(bill >= n * (n - 1), 'all-term floor')
+                    need(m == n or bill > n * (n - 1), 'overcomplete strictness')
+                    need(not (n % 2 and m == n + 1) or cheap <= 2, 'one-extra cheap bound')
+                    reports.append({'n': n, 'field': 'Q' if prime is None else f'F{prime}', 'extra': extra,
+                                    'shears': trial, 'nonzero_terms': m, 'cheap_terms': cheap, 'cost': bill})
+    # Explicit cancelling off-diagonal pair: exercises two cheap terms in an
+    # exact, overcomplete word rather than relying on generic random fixtures.
+    for n in (5, 7, 9):
+        es = [[int(i == j) for i in range(n)] for j in range(n)]
+        terms = list(zip(es, es)) + [(es[0], es[1]), (es[0], [-a for a in es[1]])]
+        bb, rr = pairing(roots(n)), roots(n)
+        bill = sum(rectangle(bb, support(rr, x), support(rr, y)) for x, y in terms)
+        need(bill == n * (n - 1) + 2 * (n - 2), 'actual cancelling cheap terms')
+        reports.append({'n': n, 'field': 'Q', 'fixture': 'cancelling_unmatched_axes', 'nonzero_terms': n + 2, 'cheap_terms': 2, 'cost': bill})
+        # I_2=E_12+E_21+(e_1-e_2)(e_1-e_2)^T, giving an
+        # actual one-extra fixture with two cheap terms, the proved cap.
+        u = [a - b for a, b in zip(es[0], es[1])]
+        terms = [(es[0], es[1]), (es[1], es[0]), (u, u)] + list(zip(es[2:], es[2:]))
+        need([[sum(x[i] * y[j] for x, y in terms) for j in range(n)] for i in range(n)] ==
+             [[int(i == j) for j in range(n)] for i in range(n)], 'two-cheap one-extra exact identity')
+        bill = sum(rectangle(bb, support(rr, x), support(rr, y)) for x, y in terms)
+        need(bill == n * n - 2, 'two-cheap one-extra actual bill')
+        reports.append({'n': n, 'field': 'Q', 'fixture': 'one_extra_two_cheap', 'nonzero_terms': n + 1, 'cheap_terms': 2, 'cost': bill})
+    return reports
+
+
+def controls():
+    rr, bb = roots(5), pairing(roots(5))
+    x, y = (1, 0, 0, 0, 0), (0, 1, 0, 0, 0)
+    sx, sy = support(rr, x), support(rr, y)
+    need(support(rr, (1,) * 5, 2) == 0 and rank(rr, 2) < 5, 'char-two injection control')
+    need(rectangle(bb, sx, sy) == 3 < 4, 'unmatched axis is really cheaper')
+    need(rectangle(bb, sx, sx) == 4 != 3, 'matched axis is not cheap')
+    sparse = [1 << i for i in range(len(rr))]
+    need(rectangle(sparse, sx, sx) == 8 != 4, 'mask change affects actual cost')
+    need(rank([[a * b for b in y] for a in x]) == 1 != 5, 'single cheap term fails exact identity')
+    need(binary_rank(bb) == 5 != 4, 'wrong parity rank rejected')
+    need((3 + 2) * (3 - 2) == 5 < 3 * (3 - 1), 'excluded small dimension count')
+    return ['characteristic_two_root_kernel', 'unmatched_axis_cheaper', 'matched_axis_not_cheap',
+            'sparse_mask_changes_tariff', 'inexact_cheap_term', 'wrong_parity_rank', 'n3_count_boundary']
+
+
+def run():
+    source_d = authenticate()
+    code, pairs = finite_support_checks(source_d)
+    factors = factor_fixtures()
+    return {'status': 'PASS_DN_UNRESTRICTED_ROOT_CODE_FLOOR', 'binary_code_checks': code,
+            'support_pair_checks': pairs, 'factorizations': factors, 'controls': controls(),
+            'scope': 'finite cross-checks of written all-n>=4, all-finite-m root-code theorem; no native or formal verification'}
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--output', type=Path)
+    args = parser.parse_args()
+    if args.output is not None and args.output.exists():
+        raise ValueError('output already exists')
+    result = run()
+    if args.output:
+        with args.output.open('x', encoding='utf-8') as stream:
+            json.dump(result, stream, indent=2, allow_nan=False)
+            stream.write('\n')
+    else:
+        need(canonical(result) == canonical(json.loads((HERE / 'RESULT.json').read_bytes())), 'typed receipt mismatch')
+    print(result['status'])
+    print('support pairs:', sum(row['pairs'] for row in result['support_pair_checks']),
+          'exact factorizations:', len(result['factorizations']), 'controls:', len(result['controls']))
+
+
+if __name__ == '__main__':
+    main()