diff --git a/research/p112-overcomplete-factor-spaces/CERTIFICATE.json b/research/p112-overcomplete-factor-spaces/CERTIFICATE.json
new file mode 100644
index 0000000000..03b42e132f
--- /dev/null
+++ b/research/p112-overcomplete-factor-spaces/CERTIFICATE.json
@@ -0,0 +1,985 @@
+{
+  "attainer": {
+    "COPY": 64,
+    "M": [
+      [
+        1,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        1,
+        -1,
+        0,
+        -1,
+        0,
+        0,
+        -1,
+        0
+      ],
+      [
+        0,
+        0,
+        1,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        1,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        1
+      ]
+    ],
+    "N": [
+      [
+        1,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        1,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        1,
+        1,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        1,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        1,
+        0,
+        0,
+        1,
+        0,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        0,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        0
+      ],
+      [
+        0,
+        1,
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0
+      ],
+      [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        1
+      ]
+    ],
+    "ranks": [
+      8,
+      7,
+      8,
+      8,
+      8,
+      8,
+      8,
+      8,
+      1
+    ]
+  },
+  "character_kernels": {
+    "left": {
+      "characters": 511,
+      "distinct_nonzero_kernels": 10,
+      "kernels": [
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1,
+            0
+          ],
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1,
+            0,
+            0
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            1,
+            0,
+            0,
+            0
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            1,
+            0,
+            0,
+            0,
+            0
+          ],
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            1,
+            0,
+            0,
+            0,
+            0,
+            0
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            1,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0
+          ],
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            1,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0
+          ],
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            1,
+            1,
+            0,
+            1,
+            0,
+            0,
+            1,
+            -4
+          ]
+        ],
+        [
+          [
+            1,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0
+          ]
+        ]
+      ],
+      "nullity_histogram": {
+        "0": 251,
+        "1": 256,
+        "2": 4
+      },
+      "ordered_character_kernel_sha256": "37c4b8c55f0314e06aa423158d51de55ca4c8ba324621e69e717da6250a31c08"
+    },
+    "right": {
+      "characters": 511,
+      "distinct_nonzero_kernels": 11,
+      "kernels": [
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1,
+            0
+          ],
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1,
+            0,
+            0
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            1,
+            0,
+            0,
+            0
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            0,
+            1,
+            0,
+            0,
+            0,
+            0
+          ],
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            0,
+            1,
+            0,
+            0,
+            0,
+            0,
+            0
+          ]
+        ],
+        [
+          [
+            0,
+            0,
+            1,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0
+          ],
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            1,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0
+          ],
+          [
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            1
+          ]
+        ],
+        [
+          [
+            0,
+            1,
+            1,
+            0,
+            1,
+            0,
+            0,
+            -1,
+            -4
+          ]
+        ],
+        [
+          [
+            0,
+            1,
+            1,
+            0,
+            1,
+            0,
+            0,
+            1,
+            0
+          ]
+        ],
+        [
+          [
+            1,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0,
+            0
+          ]
+        ]
+      ],
+      "nullity_histogram": {
+        "0": 378,
+        "1": 129,
+        "2": 4
+      },
+      "ordered_character_kernel_sha256": "bb77bcadfa1f37186d8f0b958e7701300d1882d06fc4dfcde8bdd8cdfc43306d"
+    }
+  },
+  "majorization": {
+    "P": [
+      8,
+      8,
+      8,
+      8,
+      8,
+      8,
+      8,
+      7,
+      1
+    ],
+    "P_partials": [
+      8,
+      16,
+      24,
+      32,
+      40,
+      48,
+      56,
+      63,
+      64
+    ],
+    "many_mixed_surrogate": [
+      8,
+      7,
+      7,
+      7,
+      7,
+      7,
+      7,
+      7,
+      7
+    ],
+    "many_partials": [
+      8,
+      15,
+      22,
+      29,
+      36,
+      43,
+      50,
+      57,
+      64
+    ],
+    "two_cost7": [
+      8,
+      8,
+      8,
+      8,
+      8,
+      8,
+      7,
+      7,
+      2
+    ],
+    "two_cost7_partials": [
+      8,
+      16,
+      24,
+      32,
+      40,
+      48,
+      55,
+      62,
+      64
+    ]
+  },
+  "matrix": {
+    "K_sha256": "dc18cf0af21df0331f9ec261670c61ace0b9a81c71b25c935294f70cf2870114",
+    "ports": 112,
+    "rank_L": 9,
+    "rank_R": 9,
+    "s": [
+      0,
+      1,
+      1,
+      0,
+      1,
+      0,
+      0,
+      1
+    ],
+    "s_dot_s": 4,
+    "s_dot_t": 2,
+    "t": [
+      0,
+      1,
+      1,
+      0,
+      1,
+      0,
+      0,
+      -1
+    ]
+  },
+  "negative_controls": [
+    "altered physical factor rejected",
+    "omitted compensation rejected",
+    "V/V undercharge rejected",
+    "source-byte mutation rejected",
+    "changed character premise rejected",
+    "Hermitian-transpose substitution rejected"
+  ],
+  "outside_right_space": {
+    "extended_right_space_rank": 10,
+    "rank_R_e": 10,
+    "rank_R_f": 10,
+    "ranks": [
+      8,
+      8,
+      8,
+      8,
+      8,
+      8,
+      8,
+      8,
+      0,
+      0
+    ],
+    "terms": 10
+  },
+  "overcomplete_in_space": {
+    "added_coefficient_pairs": [
+      [
+        [
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          1
+        ],
+        [
+          0,
+          1,
+          1,
+          0,
+          1,
+          0,
+          0,
+          1,
+          0
+        ]
+      ],
+      [
+        [
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          -1
+        ],
+        [
+          0,
+          1,
+          1,
+          0,
+          1,
+          0,
+          0,
+          1,
+          0
+        ]
+      ]
+    ],
+    "ranks": [
+      8,
+      7,
+      8,
+      8,
+      8,
+      8,
+      8,
+      8,
+      1,
+      0,
+      0
+    ],
+    "terms": 11
+  },
+  "pairing_ranks": {
+    "E0": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 8,
+      "U": 8,
+      "V": 8,
+      "W": 2
+    },
+    "E1": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 8,
+      "U": 7,
+      "V": 7,
+      "W": 2
+    },
+    "E2": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 8,
+      "U": 7,
+      "V": 7,
+      "W": 2
+    },
+    "E3": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 8,
+      "U": 8,
+      "V": 8,
+      "W": 2
+    },
+    "E4": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 8,
+      "U": 7,
+      "V": 7,
+      "W": 2
+    },
+    "E5": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 8,
+      "U": 8,
+      "V": 8,
+      "W": 2
+    },
+    "E6": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 8,
+      "U": 8,
+      "V": 8,
+      "W": 2
+    },
+    "E7": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 8,
+      "U": 7,
+      "V": 7,
+      "W": 2
+    },
+    "F": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 9,
+      "U": 8,
+      "V": 8,
+      "W": 2
+    },
+    "V": {
+      "E0": 8,
+      "E1": 7,
+      "E2": 7,
+      "E3": 8,
+      "E4": 7,
+      "E5": 8,
+      "E6": 8,
+      "E7": 7,
+      "F": 8,
+      "U": 7,
+      "V": 8,
+      "W": 1
+    },
+    "Z": {
+      "E0": 1,
+      "E1": 1,
+      "E2": 1,
+      "E3": 1,
+      "E4": 1,
+      "E5": 1,
+      "E6": 1,
+      "E7": 1,
+      "F": 1,
+      "U": 1,
+      "V": 0,
+      "W": 1
+    }
+  },
+  "positive_controls": [
+    "11-term zero-COPY cancellation",
+    "ordinary transpose nonreal phase",
+    "outside-right-space boundary"
+  ],
+  "schema_version": 1,
+  "source_sha256": "327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f",
+  "support_span_dimensions": {
+    "left": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 9,
+      "V": 8,
+      "Z": 1
+    },
+    "right": {
+      "E0": 8,
+      "E1": 8,
+      "E2": 8,
+      "E3": 8,
+      "E4": 8,
+      "E5": 8,
+      "E6": 8,
+      "E7": 8,
+      "F": 9,
+      "U": 8,
+      "V": 8,
+      "W": 2
+    }
+  }
+}
diff --git a/research/p112-overcomplete-factor-spaces/PROOF.md b/research/p112-overcomplete-factor-spaces/PROOF.md
new file mode 100644
index 0000000000..f364bd1632
--- /dev/null
+++ b/research/p112-overcomplete-factor-spaces/PROOF.md
@@ -0,0 +1,274 @@
+# Arbitrarily many terms inside the two minimal factor spaces
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+
+This extends the **term-count scope** of Hanhong Zhao's [PR #2321](https://github.com/CrocSwap/integer-mult-bounds/pull/2321),
+head `0665be26c2db1bd7f393d829e786698b34b626e4`. Its support catalogue and
+attainer are credited premises reconstructed here from the root prototype.
+The new argument is Sections 3–5: termwise coefficient duality is unavailable
+for an overcomplete decomposition. Zero-COPY nonzero terms are allowed.
+
+## 1. Statement and conventions
+
+Remove the first eight frame rows from the pinned 120-root prototype. Write
+`X` for the resulting 112-by-8 matrix and `lambda_i` for its 112 binary labels
+in `F_2^9`. Set `B_ij = lambda_i dot lambda_j` over `F_2`.
+The checker binds this convention to `(X_i dot X_j / 2 + 1) mod 2`.
+Let `e=e_0`, `f=e_1`, `s=X[0,:]^T`, `t=X[1,:]^T`, and define
+
+```
+G = X X^T
+K = G - (G e - 4 e)e^T + e f^T
+L = [X, e]                         (112 by 9)
+R = [(I - e e^T)X, 4e + f]         (112 by 9).
+```
+
+The exact finite checks give `K=L R^T`, `rank(L)=rank(R)=9`, and `K_ij=G_ij`
+on every required pair `B_ij=1`. All transposes in this note are **ordinary**
+transposes over `C`, never conjugate transposes. In particular,
+
+```
+s = (0,1,1,0,1,0,0,1),    t = (0,1,1,0,1,0,0,-1),
+s^T s = 4,                s^T t = 2.
+```
+
+**Theorem.** Consider any finite decomposition
+
+```
+K = sum_i D_i T_i^T,       D_i in col_C(L), T_i in col_C(R).
+```
+
+For each term separately charge
+`rho_i = rank_F2 B[supp(D_i), supp(T_i)]`. For every real `0<q<=1`,
+
+```
+                 sum_i rho_i^q >= 7*8^q + 7^q + 1.              (1)
+```
+
+The minimum is attained by the same rational nine-term factorization for
+every `q`. Thus COPY has sharp minimum 64. For `0<q<1`, the minimum is strictly
+greater than `8*8^q`.
+
+This theorem requires **both** factor-space inclusions and separate billing.
+It does not bound all factorizations of `K`, shared physical COPY work, or a
+completed recursive supplier. Section 7 gives an exact ten-term factorization
+outside the right space that violates (1) for every `0<q<1`.
+
+## 2. Complete finite support premises
+
+Because `L,R` have full column rank, write uniquely
+`D_i=L m_i`, `T_i=R n_i`, with `m_i=(a_i,c_i)` and `n_i=(b_i,d_i)`, where
+`a_i,b_i` are eight-dimensional. Left inverses of `L,R` give the equivalence
+
+```
+K = sum_i D_i T_i^T     iff     sum_i m_i n_i^T = I_9.          (2)
+```
+
+Terms with a zero physical factor contribute zero and may be removed. We do
+**not** remove a nonzero term merely because its COPY rank is zero. Call a
+remaining term *mixed* when both `a_i` and `b_i` are nonzero; otherwise call
+it *pure*. This terminology concerns coefficient projections, not COPY rank.
+
+Here is the fixed support catalogue from PR #2321. Put
+`z=(0^8,1)`, `l=(s,-4)`, `v=(s,0)`, `u=(t,-4)`.
+
+| Side/class | Coefficient vectors | Dimension of binary support span |
+|---|---|---:|
+| left Z | nonzero multiples of z | 1 |
+| left E_r | alpha e_r + beta z, alpha nonzero; beta=0 if s_r=0 | 8 |
+| left V | nonzero multiples of l | 8 |
+| left F | all other nonzero vectors | 9 |
+| right W | nonzero multiples of z | 2 |
+| right E_r | alpha e_r + beta z, alpha nonzero; beta=0 if s_r=0 | 8 |
+| right V | nonzero multiples of v | 8 |
+| right U | nonzero multiples of u | 8 |
+| right F | all other nonzero vectors | 9 |
+
+The eight left/right E classes have binary support span perpendicular to
+the corresponding removed-frame label. Left V and right V have span
+`lambda_0^perp`; right U has span `lambda_1^perp`. Left Z spans `lambda_0`,
+and right W spans `lambda_0,lambda_1`.
+
+For completeness, the checker computes the exact rational kernel of the
+rows of `L` (respectively `R`) indexed by `h dot lambda_i=1`, for **all 511
+nonzero characters h on each side**. These are precisely the coefficient
+vectors whose physical support annihilates `h`. It checks every kernel against
+the displayed model spaces, and verifies that distinct nonzero kernels
+intersect only in zero or the line `Cz`. Therefore a non-pure vector in a
+proper binary support span has exactly one nonzero annihilator, so that span
+has dimension eight. Every remaining nonzero coefficient vector has full
+binary support span. Rational kernel identities extend to `C`; this is a
+classification of all complex coefficients, including cancellations, rather
+than a sampling of rational representatives.
+
+The nullity histograms are `{0:251,1:256,2:4}` on the left and
+`{0:378,1:129,2:4}` on the right. There are respectively 10 and 11 distinct
+nonzero kernels. Once support spans are fixed, their bilinear pairing rank
+is fixed. The complete 11-by-12 table in `CERTIFICATE.json` is recomputed by
+two elimination methods, on actual supports and on their binary spans. Its
+consequences used below are:
+
+1. Every mixed term costs at least 7. A mixed term of cost 7 must have left
+   class V, right class V, or right class U. Left V/right V costs 8.
+2. The only zero-COPY class pair is left Z/right V.
+3. Left Z costs 1 against every right class except V.
+4. Right W costs 1 against left Z or V, and 2 against every left E or F.
+
+These finite premises are inherited and rechecked. Sections 3–5 are the
+extension to arbitrary term count.
+
+## 3. Nine or more mixed terms: a rank bound
+
+The top-left block of (2) is
+
+```
+                       sum_i a_i b_i^T = I_8.                 (3)
+```
+
+Only mixed terms contribute. Hence their number `n` is at least eight.
+Partition all mixed cost-7 terms among the three possible types in item 1,
+assigning a term satisfying multiple types to any one type. Their aggregate
+contribution to (3) has the form
+
+```
+                       s x^T + y s^T + w t^T
+```
+
+for some eight-dimensional vectors `x,y,w`; its rank is at most three.
+If `h` other mixed terms remain, each contributes a rank-one matrix and costs
+at least eight. Rank subadditivity applied to (3) gives `8<=3+h`, so `h>=5`.
+When `n>=9`, the mixed power bill is therefore at least
+
+```
+                         5*8^q + 4*7^q.                     (4)
+```
+
+This dominates the bill of `Q_many=(8,7,7,7,7,7,7,7,7)` term by term.
+The desired profile `P=(8,8,8,8,8,8,8,7,1)` majorizes `Q_many`:
+both sum to 64 and every descending partial sum of `P` is at least the
+corresponding partial sum of `Q_many`. Concavity of `x^q` for `0<q<=1`
+gives `sum Q_many^q >= sum P^q`, proving (1) in this case. Pure terms have
+nonnegative bills and cannot lower it.
+
+## 4. Exactly eight mixed terms: projection duality and compensation
+
+Index the eight mixed terms by `1,...,8` and put their projections in square
+matrices `A=[a_1 ... a_8]`, `B'=[b_1 ... b_8]`. Equation (3) gives
+`A B'^T=I_8`, hence
+
+```
+                         b_i^T a_j = delta_ij.               (5)
+```
+
+This is **eight-dimensional projection duality**, not the generally false
+nine-dimensional claim `n_i^T m_j=delta_ij`. Both projected sets are bases.
+There is at most one left V projection (the line `Cs`), at most one right V
+projection (`Cs`), and at most one right U projection (`Ct`). If a left V
+occurs at index `j`, any right V or U must occur at the same index: otherwise
+(5) contradicts `s^T s=4` or `s^T t=2`. As left V/right V costs eight, there
+is then at most one cost-7 mixed term. If no left V occurs, at most the two
+right exceptional lines can provide cost seven. Thus there are at most two
+cost-7 mixed terms in all cases.
+
+**Compensation costs at least one.** Suppose all pure terms cost zero.
+By item 2 each is a multiple of `z v^T` in coefficient coordinates, and
+contributes zero to the top-right and bottom-right blocks of (2). The
+top-right block then says `A d=0`, where `d=(d_1,...,d_8)^T` lists the mixed
+last coordinates. Thus `d=0`. The mixed contribution to the bottom-right
+entry is also zero, contradicting that this entry of `I_9` is one.
+Consequently the integer sum of the pure COPY ranks is at least one, and
+its power bill is at least one.
+
+**If two mixed terms cost seven, compensation costs at least two.** Suppose
+instead the pure COPY sum is at most one. The previous paragraph makes it
+exactly one: there is exactly one positive-COPY pure term, costing one,
+and all other pure terms have type Z/V. The positive term has one of the
+following forms by items 3–4:
+
+- **Left Z.** Every pure term then has `a=0`. The top-right equation still
+  gives `A d=0`, hence all mixed `d_i=0`. Mixed right U is impossible,
+  since its last coordinate is nonzero. The remaining cost-7 possibilities,
+  left V or right V, yield at most one such term by (5) and the V/V cost.
+- **Left V/right W.** Its top-right contribution is `eta s` for some
+  nonzero `eta`. All zero-COPY pure terms contribute zero there. Thus
+  `A d=-eta s`, and (5) gives `d_i=-eta b_i^T s`. A mixed right V would
+  have `b_i=gamma s`, `gamma!=0`, and `d_i=0`, contradicting
+  `d_i=-4 eta gamma`. Hence right V is absent. Only left V and right U
+  can give cost seven; if both occur they must share one index by (5) and
+  `s^T t=2`. Again at most one mixed term costs seven.
+
+Both alternatives contradict two cost-7 mixed terms. Therefore in that
+case the pure COPY sum is at least two. Subadditivity of `x^q` gives
+`sum_pure rho_i^q >= (sum_pure rho_i)^q >= 2^q`. This allows arbitrarily
+many pure terms, including arbitrarily many nonzero zero-COPY terms.
+
+## 5. Exhausting the eight-mixed-term cases
+
+According as there are zero, one, or two cost-7 mixed terms, Section 4 gives
+one of the following lower bills:
+
+```
+8*8^q + 1,
+7*8^q + 7^q + 1,
+6*8^q + 2*7^q + 2^q.
+```
+
+The first dominates (1) and the second equals it. For the third, set
+`Q_two=(8,8,8,8,8,8,7,7,2)`. The descending partial sums are
+
+```
+P:      8,16,24,32,40,48,56,63,64
+Q_two:  8,16,24,32,40,48,55,62,64.
+```
+
+Thus `P` majorizes `Q_two`, and concavity again gives the desired lower bound.
+Together with Section 3 this exhausts all finite term counts. The verifier
+checks the integer partial sums; no numerical sampling of real `q` is used.
+
+## 6. Attainment and a genuine overcomplete fixture
+
+As in PR #2321, let `N` be `I_9` with column 1 replaced by `v=(s,0)`.
+Since `s_1=1`, it is invertible. Set `M=N^(-T)`, `D=L M`, `T=R N`.
+The checker reconstructs these rational matrices and verifies all 12,544
+entries of `D T^T=K` and the actual support ranks
+
+```
+                         (8,7,8,8,8,8,8,8,1).
+```
+
+For an eleven-term in-space example, append the coefficient pairs
+`(z,v)` and `(-z,v)`. They are nonzero, cancel exactly, and both cost zero.
+This attains the same bill and shows why excluding every zero-COPY term
+by nine-term diagonal duality would be an invalid proof here. It also
+shows that the result is not restricted to minimal-length decompositions.
+For `0<q<1`, strict subadditivity gives `7^q+1>8^q`, proving the strict
+comparison with eight rank-eight terms. At `q=1`, both totals are 64.
+
+## 7. The right-space hypothesis is essential
+
+The defining identity for `K` already gives ten terms:
+
+```
+K = sum_{r=0}^7 X[:,r] X[:,r]^T + (4e-G e)e^T + e f^T.       (6)
+```
+
+All ten left factors lie in `col(L)`. The two additional terms have COPY
+rank zero, and the eight original terms have rank eight. Thus the profile
+is `(8,8,8,8,8,8,8,8,0,0)`, whose power bill `8*8^q` is below (1) for
+`0<q<1`. The checker verifies (6) entry by entry and computes
+`rank([R,e])=rank([R,f])=10`. The two added right factors are outside
+`col(R)`. All right factors of (6) lie in the single extra dimension
+`col(R)+Ce`, since `f=(4e+f)-4e` and `X[:,r]=R[:,r]+s_r e`; the checker
+also verifies that the combined right space has dimension ten. This is a boundary control derived from the predecessor matrix,
+not a new physical decoder or an improved total COPY bound.
+
+## Evidence status and remaining obligations
+
+The result is a scoped written proof supported by exact finite algebra.
+The support catalogue and nine-term witness are predecessor work; the new
+contribution is the arbitrary-length rank/compensation argument and its
+explicit scope controls. No Lean proof, independent human review, or
+external-agent review is claimed. The verification program checks finite
+premises and fixtures; it does not mechanically certify the written universal
+argument. Native frames, arbitrary-dirty realization, shared costs, precision,
+reserve, chronological hosting, and all-size transfer remain unaddressed.
diff --git a/research/p112-overcomplete-factor-spaces/README.md b/research/p112-overcomplete-factor-spaces/README.md
new file mode 100644
index 0000000000..b5667eda07
--- /dev/null
+++ b/research/p112-overcomplete-factor-spaces/README.md
@@ -0,0 +1,111 @@
+# P112: extra terms inside the minimal factor spaces do not lower the COPY-power minimum
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+
+For the fixed PR #2021 two-column P112 completion with `(j,k)=(0,1)` and
+coefficient `+1`, the sharp separately billed minimum over **any finite number
+of complex rank-one terms**, with both factors inside the matrix's minimal
+nine-dimensional column and row spaces, is
+
+```
+min sum_i rho_i^q = 7*8^q + 7^q + 1,        0 < q <= 1.
+```
+
+Here `rho_i` is the actual binary support-pairing rank of term `i`. COPY has
+minimum 64. For `0<q<1`, this exceeds the eight-rank-eight bill `8*8^q`.
+The result extends [PR #2321](https://github.com/CrocSwap/integer-mult-bounds/pull/2321)
+from exactly nine terms to arbitrary finite length **under the two stated
+factor-space inclusions**. In the nine-term setting those inclusions follow
+automatically from rank; in the overcomplete setting they are restrictions.
+Zero-COPY nonzero terms are allowed.
+
+[PROOF.md](PROOF.md) gives the new rank/compensation argument. It reconstructs
+PR #2321's finite support classification and credits its nine-term attaining
+profile `(8,8,8,8,8,8,8,7,1)`. With exactly eight mixed projections, projected
+duality controls the exceptional cost-seven terms. With more mixed terms,
+the aggregate cost-seven contribution has rank at most three.
+
+An exact ten-term boundary control leaves the right factor space and attains
+`(8,8,8,8,8,8,8,8,0,0)`. Thus the theorem cannot be applied to arbitrary
+factorizations of this matrix. This is a scoped obstruction, not a completed
+supplier or an improvement of the selected multiplication exponent.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -I -B scripts/research_package.py --package research/p112-overcomplete-factor-spaces --check-only
+python3 -I -B scripts/research_package.py --package research/p112-overcomplete-factor-spaces
+```
+
+The registered verifier reports:
+
+```
+PASS_P112_OVERCOMPLETE_FACTOR_SPACES kernels=1022 class_pairs=132 entries=12544 COPY=64 controls=7
+```
+
+It binds the live prototype to its SHA256 and Gram/binary convention, recomputes
+all character kernels over the rationals, checks their intersections and all
+class pairings, and uses two binary rank elimination methods. It verifies the
+nine-term attainer, an eleven-term in-space zero-COPY cancellation fixture,
+and the ten-term out-of-space boundary, with all-entry matrix multiplication.
+It checks integer majorization premises for all real `q` in the stated interval.
+Meaningful rejection controls cover altered physical factors, omitted
+compensation, a V/V undercharge, changed source bytes, a changed character
+kernel, a Hermitian-transpose substitution, and an undercharged certificate.
+An exact nonreal phase fixture checks the ordinary-transpose convention.
+
+[CERTIFICATE.json](CERTIFICATE.json) records the deterministic finite evidence,
+including the coefficient witness and complete rank table. Normal replay is
+read-only and compares the entire certificate. `verify.py --write NEW_FILE`
+regenerates evidence into a new file exclusively; it refuses to overwrite.
+No predecessor program or pending PR checkout is needed for replay. The
+universal argument is written mathematics; the checker certifies its finite
+premises, not a formalization of that argument.
+
+## Task, overlap and scope
+
+[TASK.json](TASK.json) records the original `complex-new-helper-inventory` card,
+priority revision 4, the selection nonce and explicit scope change to the
+more-terms handoff in [discussion #2006](https://github.com/CrocSwap/integer-mult-bounds/discussions/2006#discussioncomment-18940755).
+The claim is in [discussion #2006](https://github.com/CrocSwap/integer-mult-bounds/discussions/2006#discussioncomment-18942846). This algebraic side result
+screens whether additional terms alone can improve one fixed masked decoder's
+power bill; it does not pass the original physical-inventory acceptance gate.
+
+The fixed completion is from this account's merged
+[PR #2021](https://github.com/CrocSwap/integer-mult-bounds/pull/2021), head
+`9943467c4b24d2050275a202e3866cfc522afbe7`. PR #2321 at
+`0665be26c2db1bd7f393d829e786698b34b626e4` proves the exactly-nine-term result.
+A concurrent coefficient-family investigation varies the completion coefficient
+while retaining nine terms; this package fixes coefficient `+1` and changes
+term count. It does not vary ports or audit PR #2308's shared-plane completion.
+[SOURCES.json](SOURCES.json) pins the main-branch prototype and records
+predecessor proof provenance. Pending predecessor code is not a runtime dependency.
+
+## Open next questions
+
+- What is the sharp power minimum for this same matrix when factors may leave
+  either minimal factor space? The explicit ten-term boundary already beats
+  the in-space minimum for `q<1`. A useful first step is to classify the explicit
+  one-dimensional extension `col(R)+Ce_0` of the right space and seek a lower bill than
+  `8*8^q`. The present character catalogue does not cover that extension.
+- Can a concrete physical implementation share COPY work across terms?
+  Separate support billing is a theorem premise. A useful next step is one
+  legal sharing construction with its frames, restoration, precision and
+  reserve fully charged; no such realization is supplied here.
+
+## Credit
+
+The completion and COPY65 predecessor are from commdata2338's PR #2021.
+Hanhong Zhao (@Hope7Happiness), PR #2321, supplied the complete support catalogue,
+sharp nine-term theorem and rational attainer. This package independently
+reconstructs those finite premises and extends the proof to arbitrary length
+within both minimal spaces. Related support/compensation lineage includes
+Arham Tahir (PR #1591), Gareth Davidson (@bitplane, PR #1652),
+woklerx (PR #1077/#1447), DreamingOfClouds (PR #717), and themilkman216
+(PR #968), together with the PR #845 root-geometry lineage.
+
+New work is Apache-2.0. OpenAI Codex performed the derivation, implementation,
+checking and writing. No independent human review or formal verification is
+claimed. See [TASK.json](TASK.json) for the assistance disclosure.
diff --git a/research/p112-overcomplete-factor-spaces/SOURCES.json b/research/p112-overcomplete-factor-spaces/SOURCES.json
new file mode 100644
index 0000000000..1ec73b7961
--- /dev/null
+++ b/research/p112-overcomplete-factor-spaces/SOURCES.json
@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "path": "research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json",
+      "usage": "input",
+      "git_blob": "9efe30ee107b9c67f15f1c726e1a1cb5cef03929",
+      "sha256": "327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f"
+    }
+  ],
+  "predecessor_references": [
+    {
+      "commit": "0665be26c2db1bd7f393d829e786698b34b626e4",
+      "path": "research/p112-two-column-copy-optimum/PROOF.md",
+      "git_blob": "1dab3ed3cff24dd356ad2294fda7f470b8db7860",
+      "sha256": "09ec847df2ed516e050aab005b515cad5a0ba6ad2f677aed9d256acf93bdb46d",
+      "role": "Credited support catalogue, nine-term theorem and attainer; not imported or required at runtime."
+    },
+    {
+      "commit": "9943467c4b24d2050275a202e3866cfc522afbe7",
+      "path": "research/p112-two-column-completion/README.md",
+      "git_blob": "3317a04a7aa4d6ac4fc1a2a7c51b4c2afa8d0271",
+      "sha256": "fbec870913799a7d750ba77b043fd0b3e64cec3a84e0f40df459495d1c5ebaeb",
+      "role": "Fixed completion and COPY65 predecessor; not a runtime input."
+    }
+  ]
+}
diff --git a/research/p112-overcomplete-factor-spaces/TASK.json b/research/p112-overcomplete-factor-spaces/TASK.json
new file mode 100644
index 0000000000..bce43a3ca9
--- /dev/null
+++ b/research/p112-overcomplete-factor-spaces/TASK.json
@@ -0,0 +1,111 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?",
+    "starting_points": [
+      "research/complex-local-word-ceiling/README.md",
+      "research/heterogeneous-owner-assembly/README.md",
+      "certificates/selected-result.json",
+      "research/selected-k8-unrestricted-ends/README.md"
+    ],
+    "methods": [
+      "Propose a changed helper inventory and derive an optimistic exact moment.",
+      "Design a small completed instance and independently verify its endpoint and rank bill."
+    ],
+    "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.",
+    "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.",
+    "allowed_variations": [
+      "Narrow to one changed boundary or helper type with explicit counts.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Mixing only providers already inside the pinned catalogue.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013."
+    ],
+    "overlap_terms": [
+      "helper inventory",
+      "heterogeneous-owner",
+      "mutable leaver"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp separately billed COPY-power minimum for arbitrarily many complex rank-one terms of the fixed PR2021 (0,1), coefficient +1 completion, with both factors constrained to its minimal nine-dimensional spaces.",
+  "scope_change_reason": "Takes the explicit more-terms handoff in discussion #2006 / PR2321 after overlap ruled out the initial central candidate. The selected helper-inventory suggestion is narrowed to an algebraic screen for overcomplete inventory. This side result does not meet the original physical-inventory acceptance gate.",
+  "bottleneck_link": "Closes the extra-terms-only escape within both minimal factor spaces for this one masked decoder: the power bill remains above eight rank-eight children for 0<q<1. No native physical supplier or selected exponent improvement follows.",
+  "budget_minutes": 60,
+  "stop_rule": "One fixed completion and its complete finite support classification; stop after proving or refuting the arbitrary-term extension and checking scope controls. No coefficient, port, supplier or sharing search.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md gives the arbitrary-length rank and compensation argument. CERTIFICATE.json and verify.py reconstruct 1022 character kernels, 132 class pairings, exact attainer and boundary fixtures, integer majorization and seven rejection controls.",
+  "author": "commdata2338",
+  "ai_assistance": "Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. OpenAI Codex (GPT-6 Astra) did the derivation, implementation, checking and writing. No independent human review, external-agent review or formal verification is claimed.",
+  "open_questions": [
+    {
+      "question": "What is the sharp power minimum when factors may leave either minimal factor space?",
+      "why_it_matters": "The explicit ten-term boundary already beats the in-space minimum for q<1.",
+      "first_step": "Classify col(R)+Ce_0, the explicit one-dimensional extension containing the boundary witness, and test whether it permits a bill below 8*8^q.",
+      "blocked_by": "The present support classification applies only inside the two fixed nine-dimensional spaces."
+    },
+    {
+      "question": "Can a legal physical implementation share COPY work across terms?",
+      "why_it_matters": "The proof bills actual support ranks separately for each term.",
+      "first_step": "Specify one sharing construction and charge its frames, restoration, precision and reserve.",
+      "blocked_by": "No physical realization or complete native invoice is supplied."
+    }
+  ],
+  "selection": {
+    "nonce": "b839c7d51965d70bcac5d0fde27becf6",
+    "track": "complex-mechanisms",
+    "scope_key": "f3b0895a4f9f1cc62e75",
+    "draw": "original draw; no reroll",
+    "suggestions": [
+      "complex-new-helper-inventory",
+      "p104-side-correction",
+      "complex-rank-shape-decoder"
+    ],
+    "override": "Explicit more-terms handoff from PR2321 in discussion #2006; fixed-completion overcomplete-factor-space screen.",
+    "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2006#discussioncomment-18940755",
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2006#discussioncomment-18942846"
+  },
+  "predecessors": [
+    {
+      "pr": 2021,
+      "head": "9943467c4b24d2050275a202e3866cfc522afbe7",
+      "role": "fixed masked completion; main-branch mathematical predecessor"
+    },
+    {
+      "pr": 2321,
+      "head": "0665be26c2db1bd7f393d829e786698b34b626e4",
+      "role": "credited nine-term proof, support catalogue and attainer; no runtime dependency"
+    }
+  ],
+  "unresolved_obligations": [
+    "factors outside either minimal space",
+    "shared physical COPY billing",
+    "native frames and arbitrary-dirty realization",
+    "precision and reserve",
+    "chronological hosting and all-size transfer",
+    "formal proof verification"
+  ],
+  "refresh_checkpoint": {
+    "utc": "2026-10-15T07:11:22Z",
+    "main_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+    "priority_revision": 4,
+    "changed_files": [],
+    "decision": "Continue on unchanged base, guidance, selected record and scientific input. PR2321 head also unchanged at 0665be26c2db1bd7f393d829e786698b34b626e4."
+  }
+}
diff --git a/research/p112-overcomplete-factor-spaces/VERIFY.json b/research/p112-overcomplete-factor-spaces/VERIFY.json
new file mode 100644
index 0000000000..4d763e2c6e
--- /dev/null
+++ b/research/p112-overcomplete-factor-spaces/VERIFY.json
@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact source-bound support catalogue, both rank algorithms, all-entry attainer and scope fixtures, integer majorization and seven rejection controls."
+    }
+  ]
+}
diff --git a/research/p112-overcomplete-factor-spaces/verify.py b/research/p112-overcomplete-factor-spaces/verify.py
new file mode 100644
index 0000000000..7b66e5b044
--- /dev/null
+++ b/research/p112-overcomplete-factor-spaces/verify.py
@@ -0,0 +1,361 @@
+#!/usr/bin/env python3
+"""Exact finite premises and controls for the theorem in PROOF.md (stdlib only)."""
+from __future__ import annotations
+import argparse
+from collections import Counter
+from fractions import Fraction as Q
+from hashlib import sha256
+import json
+from math import gcd, lcm
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parent.parent
+SOURCE = 'research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json'
+SOURCE_SHA = '327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f'
+
+
+def require(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def transpose(a):
+    return [list(x) for x in zip(*a)]
+
+
+def product(a, b):
+    return [[sum(x*y for x, y in zip(row, col)) for col in transpose(b)] for row in a]
+
+
+def primitive(row):
+    denominator = 1
+    for x in row:
+        if isinstance(x, Q):
+            denominator = lcm(denominator, x.denominator)
+    row = [int(x*denominator) for x in row]
+    g = 0
+    for x in row:
+        g = gcd(g, x)
+    if not g:
+        return row
+    g *= 1 if next(x for x in row if x) > 0 else -1
+    return [x//g for x in row]
+
+
+def echelon(rows, width):
+    """Integer fraction-free elimination; retained rows span the exact Q row space."""
+    basis = {}
+    for original in rows:
+        row = primitive(original)
+        for p, b in sorted(basis.items()):
+            if row[p]:
+                c, d = row[p], b[p]
+                row = primitive([d*x-c*y for x, y in zip(row, b)])
+        p = next((j for j, x in enumerate(row) if x), None)
+        if p is not None:
+            basis[p] = primitive(row)
+        if len(basis) == width:
+            break
+    return sorted(basis.items())
+
+
+def rank(rows):
+    return len(echelon(rows, len(rows[0]))) if rows else 0
+
+
+def canonical(rows, width=9):
+    b = [(p, list(map(Q, row))) for p, row in echelon(rows, width)]
+    for i in range(len(b)-1, -1, -1):
+        p, row = b[i]
+        pivot = row[p]
+        row[:] = [x/pivot for x in row]
+        for _, previous in b[:i]:
+            c = previous[p]
+            previous[:] = [x-c*y for x, y in zip(previous, row)]
+    return [row for _, row in b]
+
+
+def kernel(rows, width):
+    b = canonical(rows, width)
+    pivots = [next(j for j, x in enumerate(row) if x) for row in b]
+    result = []
+    for free in sorted(set(range(width))-set(pivots)):
+        v = [Q(0)]*width
+        v[free] = Q(1)
+        for p, row in zip(pivots, b):
+            v[p] = -row[free]
+        result.append(v)
+    return result
+
+
+def inverse(a):
+    n = len(a)
+    augmented = [list(map(Q, row))+[Q(i == j) for j in range(n)] for i, row in enumerate(a)]
+    for p in range(n):
+        k = next(i for i in range(p, n) if augmented[i][p])
+        augmented[p], augmented[k] = augmented[k], augmented[p]
+        c = augmented[p][p]
+        augmented[p] = [x/c for x in augmented[p]]
+        for i in range(n):
+            if i != p:
+                c = augmented[i][p]
+                augmented[i] = [x-c*y for x, y in zip(augmented[i], augmented[p])]
+    return [row[n:] for row in augmented]
+
+
+def gf2_basis(values):
+    basis = {}
+    for value in values:
+        while value:
+            p = value.bit_length()-1
+            if p in basis:
+                value ^= basis[p]
+            else:
+                basis[p] = value
+                break
+    return [basis[p] for p in sorted(basis)]
+
+
+def gf2_rank_low(values):
+    """Independent elimination direction, also used on the unreduced support matrix."""
+    rows = list(values)
+    r = 0
+    width = max((x.bit_length() for x in rows), default=0)
+    for p in range(width):
+        k = next((i for i in range(r, len(rows)) if (rows[i] >> p) & 1), None)
+        if k is None:
+            continue
+        rows[r], rows[k] = rows[k], rows[r]
+        for i in range(r+1, len(rows)):
+            if (rows[i] >> p) & 1:
+                rows[i] ^= rows[r]
+        r += 1
+    return r
+
+
+def pairing_rows(left, right):
+    return [sum(((a & b).bit_count() % 2) << j for j, b in enumerate(right)) for a in left]
+
+
+def charge(d, t, labels):
+    dl = [labels[i] for i, x in enumerate(d) if x != 0]
+    tl = [labels[i] for i, x in enumerate(t) if x != 0]
+    reduced = len(gf2_basis(pairing_rows(gf2_basis(dl), gf2_basis(tl))))
+    direct = gf2_rank_low(pairing_rows(dl, tl))
+    require(reduced == direct, 'binary rank algorithms disagree')
+    return direct
+
+
+def serial(value):
+    if isinstance(value, Q):
+        return int(value) if value.denominator == 1 else str(value)
+    if isinstance(value, dict):
+        return {str(k): serial(v) for k, v in value.items()}
+    if isinstance(value, (list, tuple)):
+        return [serial(x) for x in value]
+    return value
+
+
+def digest(value):
+    return sha256(json.dumps(serial(value), sort_keys=True, separators=(',', ':')).encode()).hexdigest()
+
+
+def identity(n):
+    return [[int(i == j) for j in range(n)] for i in range(n)]
+
+
+def exact_factor_check(d, t, target, labels):
+    require(product(d, transpose(t)) == target, 'all-entry factor identity failed')
+    return [charge(a, b, labels) for a, b in zip(transpose(d), transpose(t))]
+
+
+def majorizes(p, r):
+    p, r = sorted(p, reverse=True), sorted(r, reverse=True)
+    return sum(p) == sum(r) and all(sum(p[:i]) >= sum(r[:i]) for i in range(1, len(p)+1))
+
+
+def reject(action, reason):
+    try:
+        action()
+    except ValueError:
+        return reason
+    raise ValueError('negative control accepted: '+reason)
+
+
+def build():
+    raw = (ROOT/SOURCE).read_bytes()
+    require(sha256(raw).hexdigest() == SOURCE_SHA, 'live prototype hash mismatch')
+    src = json.loads(raw)
+    roots, all_labels = src['root_lines'], src['binary_ports']
+    require(roots[:8] == [[2*int(i == j) for j in range(8)] for i in range(8)], 'frame binding')
+    x, labels, frame = roots[8:], all_labels[8:], all_labels[:8]
+    require(len(x) == 112 and len(set(labels)) == 112, 'source dimensions')
+    s, t = x[0], x[1]
+    z = [0]*8+[1]
+    l, v, u = s+[-4], s+[0], t+[-4]
+    require(sum(a*a for a in s) == 4 and sum(a*b for a, b in zip(s, t)) == 2, 'projection pairings')
+    require([j for j in range(8) if s[j]] == [j for j in range(8) if t[j]] == [1, 2, 4, 7], 'coordinate support')
+    g = product(x, transpose(x))
+    require(all(g[i][i] == 4 for i in range(112)), 'root norm')
+    require(all(g[i][j] % 2 == 0 and ((g[i][j]//2+1) % 2) == ((labels[i]&labels[j]).bit_count()%2)
+                for i in range(112) for j in range(112)), 'Gram/binary convention binding')
+    left = [row+[int(i == 0)] for i, row in enumerate(x)]
+    right = [([0]*8 if i == 0 else row)+[4*int(i == 0)+int(i == 1)] for i, row in enumerate(x)]
+    target = [[g[i][j]-(g[i][0]-4*int(i == 0))*int(j == 0)+int(i == 0 and j == 1)
+               for j in range(112)] for i in range(112)]
+    require(rank(left) == rank(right) == 9 and product(left, transpose(right)) == target, 'rank-nine binding')
+    require(all(target[i][j] == g[i][j] for i in range(112) for j in range(112)
+                if ((labels[i]&labels[j]).bit_count()%2)), 'masked completion changed a required entry')
+
+    # Complete support theorem: every nonzero binary annihilator is inspected.
+    kernel_evidence = {}
+    for side, matrix in [('left', left), ('right', right)]:
+        found, unique, histogram = [], {}, Counter()
+        for h in range(1, 512):
+            rows = [row for row, lab in zip(matrix, labels) if (h & lab).bit_count()%2]
+            got = canonical(kernel(rows, 9))
+            if h in frame:
+                r = frame.index(h)
+                expected = [identity(9)[r]]+([z] if s[r] else [])
+            elif h == labels[0]:
+                expected = [l if side == 'left' else v]
+            elif side == 'right' and h == labels[1]:
+                expected = [u]
+            elif (h&labels[0]).bit_count()%2 == 0 and (side == 'left' or (h&labels[1]).bit_count()%2 == 0):
+                expected = [z]
+            else:
+                expected = []
+            require(got == canonical(expected), f'{side} character {h}: kernel mismatch')
+            require(all(sum(a*b for a, b in zip(row, vec)) == 0 for row in rows for vec in got), 'kernel residual')
+            histogram[len(got)] += 1
+            found.append([h, got])
+            if got:
+                unique[digest(got)] = got
+        spaces = list(unique.values())
+        require(len(spaces) == (10 if side == 'left' else 11), 'distinct character-kernel count')
+        for i, a in enumerate(spaces):
+            for b in spaces[i+1:]:
+                intersection_dimension = len(a)+len(b)-rank(a+b)
+                common_z = rank(a+[z]) == len(a) and rank(b+[z]) == len(b)
+                require(intersection_dimension == int(common_z), 'unexpected character-kernel intersection')
+        expected_hist = {0:251, 1:256, 2:4} if side == 'left' else {0:378, 1:129, 2:4}
+        require(dict(histogram) == expected_hist, 'nullity histogram')
+        kernel_evidence[side] = {'characters':511, 'nullity_histogram': dict(histogram),
+                                'distinct_nonzero_kernels': len(spaces), 'kernels': sorted(serial(spaces), key=str),
+                                'ordered_character_kernel_sha256': digest(found)}
+
+    eclasses = {'E'+str(r): identity(9)[r] for r in range(8)}
+    lc = {'Z':z, **eclasses, 'V':l, 'F':[2**j for j in range(9)]}
+    rc = {'W':z, **eclasses, 'V':v, 'U':u, 'F':[2**j for j in range(9)]}
+    physical_left = {name:[sum(a*b for a, b in zip(row, coeff)) for row in left] for name, coeff in lc.items()}
+    physical_right = {name:[sum(a*b for a, b in zip(row, coeff)) for row in right] for name, coeff in rc.items()}
+    span_dims = {}
+    for side, columns, pure in [('left', physical_left, 'Z'), ('right', physical_right, 'W')]:
+        span_dims[side] = {name:len(gf2_basis([labels[i] for i, value in enumerate(col) if value])) for name, col in columns.items()}
+        for name, dim in span_dims[side].items():
+            expected_dim = (1 if side == 'left' else 2) if name == pure else (9 if name == 'F' else 8)
+            require(dim == expected_dim, 'class support dimension')
+    table = {a:{b:charge(da, tb, labels) for b, tb in physical_right.items()} for a, da in physical_left.items()}
+    for a in lc:
+        for b in rc:
+            r = table[a][b]
+            require((r == 0) == (a == 'Z' and b == 'V'), 'zero-cost catalogue')
+            if a != 'Z' and b != 'W':
+                require(r >= 7 and (r != 7 or a == 'V' or b in ('V', 'U')), 'mixed cost catalogue')
+            if a == 'Z' and b != 'V':
+                require(r == 1, 'left-pure catalogue')
+            if b == 'W':
+                require(r == (1 if a in ('Z', 'V') else 2), 'right-pure catalogue')
+    require(table['V']['V'] == 8, 'V/V charge')
+
+    n = identity(9)
+    for i in range(9):
+        n[i][1] = v[i]
+    m = transpose(inverse(n))
+    require(product(m, transpose(n)) == identity(9), 'attainer coefficients')
+    d, tt = product(left, m), product(right, n)
+    attained = exact_factor_check(d, tt, target, labels)
+    require(attained == [8, 7, 8, 8, 8, 8, 8, 8, 1], 'attaining profile')
+
+    # Genuine overcomplete in-space fixture: two nonzero cancelling zero-COPY terms.
+    mc, nc = transpose(m)+[z, [-a for a in z]], transpose(n)+[v, v]
+    require(product(transpose(mc), nc) == identity(9), 'overcomplete coefficients')
+    over_d, over_t = product(left, transpose(mc)), product(right, transpose(nc))
+    over = exact_factor_check(over_d, over_t, target, labels)
+    require(over == attained+[0, 0], 'zero-cost overcomplete fixture')
+    require(sum(a*b for a, b in zip(mc[-1], nc[-1])) == 0, 'termwise duality control')
+
+    # Boundary control: removing the right-space restriction admits a ten-term bill64.
+    e, f = [int(i == 0) for i in range(112)], [int(i == 1) for i in range(112)]
+    correction = [-g[i][0]+4*e[i] for i in range(112)]
+    bd = transpose(transpose(x)+[correction, e])
+    bt = transpose(transpose(x)+[e, f])
+    boundary = exact_factor_check(bd, bt, target, labels)
+    require(boundary == [8]*8+[0, 0], 'outside-space boundary profile')
+    require(rank([a+[b] for a, b in zip(left, correction)]) == 9, 'boundary left-space membership')
+    re, rf = rank([a+[b] for a, b in zip(right, e)]), rank([a+[b] for a, b in zip(right, f)])
+    require(re == rf == 10, 'boundary factors must be outside right space')
+    require(rank([a+b for a, b in zip(right, bt)]) == 10, 'one-dimensional right-space extension')
+
+    p, two_sevens, many = [8]*7+[7, 1], [8]*6+[7, 7, 2], [8]+[7]*8
+    require(majorizes(p, two_sevens) and majorizes(p, many), 'concavity integer partial sums')
+    partials = lambda a: [sum(sorted(a, reverse=True)[:j]) for j in range(1, len(a)+1)]
+
+    controls = []
+    bad = [row[:] for row in d]
+    bad[0][0] += 1
+    controls.append(reject(lambda: exact_factor_check(bad, tt, target, labels), 'altered physical factor rejected'))
+    missing = [row[:-1] for row in d]
+    controls.append(reject(lambda: exact_factor_check(missing, [row[:-1] for row in tt], target, labels), 'omitted compensation rejected'))
+    controls.append(reject(lambda: require(table['V']['V'] == 7, 'bad tariff'), 'V/V undercharge rejected'))
+    controls.append(reject(lambda: require(sha256(raw+b' ').hexdigest() == SOURCE_SHA, 'bad hash'), 'source-byte mutation rejected'))
+    bad_kernel = [row[:] for row in left]
+    bad_kernel[0][8] += 1
+    h = labels[0]
+    controls.append(reject(lambda: require(canonical(kernel([row for row, lab in zip(bad_kernel, labels) if (h&lab).bit_count()%2], 9)) == canonical([l]), 'bad kernel'), 'changed character premise rejected'))
+    # Exact Gaussian integer phases, with no floating-point tolerance.
+    require(all(Q(value).denominator == 1 for row in d+tt for value in row), 'phase fixture uses integer coefficients')
+    cd = [[complex(value) for value in row] for row in d]
+    ct = [[complex(value) for value in row] for row in tt]
+    for row in cd:
+        row[0] *= 1j
+    for row in ct:
+        row[0] *= -1j
+    require(exact_factor_check(cd, ct, target, labels) == attained, 'ordinary transpose phase fixture')
+    controls.append(reject(lambda: exact_factor_check(cd, [[x.conjugate() for x in row] for row in ct], target, labels), 'Hermitian-transpose substitution rejected'))
+    # Every Gaussian-integer value and sum here is below 2**53; complex arithmetic is exact.
+    require(max(abs(x.real)+abs(x.imag) for row in cd+ct for x in row) < 100, 'phase exactness range')
+
+    return serial({'schema_version':1, 'source_sha256':SOURCE_SHA, 'matrix':{'ports':112, 'rank_L':9, 'rank_R':9,
+        's':s, 't':t, 's_dot_s':4, 's_dot_t':2, 'K_sha256':digest(target)},
+        'character_kernels':kernel_evidence, 'support_span_dimensions':span_dims, 'pairing_ranks':table,
+        'attainer':{'M':m, 'N':n, 'ranks':attained, 'COPY':sum(attained)},
+        'overcomplete_in_space':{'terms':11, 'ranks':over, 'added_coefficient_pairs':[[z, v], [[-a for a in z], v]]},
+        'outside_right_space':{'terms':10, 'ranks':boundary, 'rank_R_e':re, 'rank_R_f':rf, 'extended_right_space_rank':10},
+        'majorization':{'P':p, 'two_cost7':two_sevens, 'many_mixed_surrogate':many,
+                        'P_partials':partials(p), 'two_cost7_partials':partials(two_sevens), 'many_partials':partials(many)},
+        'negative_controls':controls, 'positive_controls':['11-term zero-COPY cancellation', 'ordinary transpose nonreal phase', 'outside-right-space boundary']})
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--write', type=Path, help='create a new certificate exclusively; never overwrite')
+    args = parser.parse_args()
+    actual = build()
+    if args.write:
+        with args.write.open('x') as stream:
+            json.dump(actual, stream, indent=2, sort_keys=True)
+            stream.write('\n')
+        print('WROTE_P112_OVERCOMPLETE_CERTIFICATE')
+    else:
+        expected = json.loads((HERE/'CERTIFICATE.json').read_text())
+        require(actual == expected, 'certificate differs from exact recomputation')
+        altered = json.loads(json.dumps(expected))
+        altered['attainer']['ranks'][0] -= 1
+        reject(lambda: require(actual == altered, 'altered certificate'), 'certificate undercharge rejected')
+        print('PASS_P112_OVERCOMPLETE_FACTOR_SPACES kernels=1022 class_pairs=132 entries=12544 COPY=64 controls=7')
+
+
+if __name__ == '__main__':
+    main()