diff --git a/research/complex-rank8-rigidity-p104-admissible/PROOF.md b/research/complex-rank8-rigidity-p104-admissible/PROOF.md
new file mode 100644
index 0000000000..8e6fd5a9f5
--- /dev/null
+++ b/research/complex-rank8-rigidity-p104-admissible/PROOF.md
@@ -0,0 +1,95 @@
+# Rank-8 rigidity on the admissible P104 units
+
+Notation, equations (E), (1), (2), (E0), (E2), (E4) and Lemmas 2–8 are those of PR1212
+(`research/complex-rank8-decoder-rigidity/PROOF.md` at head `57099cb5`). Finite facts marked
+**[X]** are recomputed by this package's `verify.py` (check id `X`). Facts marked **[1212: X]** are
+PR1212's checks, which `verify.py --pr1212-dir` replays from blob-pinned files.
+
+**Theorem.** Let L be one of the 896 admissible P104 units: P112 minus a frame of type (1,…,1) relative to
+FRAME0. Let K be an L × L matrix over a field of characteristic 0 with rank K ≤ 8 that satisfies (E). Then
+K = D (2 G_L) D⁻¹ for an invertible diagonal D.
+
+**Corollary.** In the E-graph model, every decoder with exactly eight costly terms on an admissible P104 unit
+has cst ≥ 56. This is PR968's floor at p = 16, reached through PR1212's §8 verbatim. PR717's P104 decoders,
+which lie in this orbit **[1212: G.pr717-p104-orbit]**, attain it.
+
+By PR1212 §10 transport, the stabiliser of FRAME0 is transitive on the 896 admissible frames
+**[1212: G.frame-orbits]**. It therefore suffices to treat PR1212's representative, P112 minus the frame
+`DEAD` with pivot `PIVOT` (both listed as root vectors in `verify.py`) **[unit.live, unit.admissible-type,
+pr1212.unit-vectors]**.
+
+## Inputs that already hold
+
+Relative to this pivot there are 22 complete live classes, four classes with two live rows, and two empty
+classes **[unit.class-profile]**. PR1212 §10 records that three of its four finite inputs hold here:
+
+- **(I2)** zero exclusion (Lemma 8) **[1212: G.P104-11111111.zero-exclusion]**;
+- **(I3)** the Lemma 5 group witnesses for every complete class **[lemma5.group-witnesses;
+  1212: G.P104-11111111.class-witnesses]**;
+- **(I4)** every block carries a complete live class **[lemma6.blocks-and-gluing]**.
+
+Only (I1) fails: eight live lines lie in two-row classes, and there Lemma 5 leaves a one-parameter family
+**[control.in-class-not-forced]**.
+
+## Step 1: the complete classes
+
+Lemma 5 applies to each of the 22 complete classes. It needs only (I2), (I3) and the class's own
+equations. Lemma 6 applies to the set of complete classes. Its proof uses only complete classes:
+
+- the gluing equation (5) between complete classes C, C′ in distinct blocks through {k, k′};
+- for two classes in the same block, a complete class in one of the two other blocks through {k, k′};
+- the cocycle in the block of each triple.
+
+All three exist by (I4) **[lemma6.blocks-and-gluing]**. Lines outside the complete classes play no role. So there are nonzero
+g_f (f ∈ F) and d′_j such that for every line j in a complete class and f ∈ T_j:
+
+    a_jf = d′_j ε_jf g_f,      b_jf = 4 (d′_j g_f)⁻¹ ε_jf.                                  (6)
+
+## Step 2: Lemma 9 (propagation)
+
+**Lemma 9.** Let i be a live non-pivot line with support T = T_i. Call a pair {k, k′} ⊂ T *witnessed* if
+some line j of a complete class has G_ij = 0 and T_i ∩ T_j = {k, k′}. If the witnessed pairs connect T,
+then for a nonzero λ_i
+
+    a_if = λ_i ε_if g_f,      b_if = 4 (λ_i g_f)⁻¹ ε_if      (f ∈ T).
+
+*Proof.* Let j witness {k, k′}. Rule (3) with G_ij = 0 gives ε_ik ε_jk = −ε_ik′ ε_jk′
+**[lemma9.propagation-connected]**. Equation (E2) in the order a_i · b_j, with b_j from (6), reads
+
+    (4 / d′_j) (a_ik ε_jk / g_k + a_ik′ ε_jk′ / g_k′) = 0.
+
+Multiply by ε_ik ε_jk d′_j / 4 and use the sign identity:
+
+    a_ik ε_ik / g_k = a_ik′ ε_ik′ / g_k′.
+
+So a_if ε_if / g_f is constant along witnessed pairs, and hence on T. Call the constant λ_i. Then
+a_if = λ_i ε_if g_f, and λ_i ≠ 0 because (E0) needs a_i ≠ 0.
+
+In the order a_j · b_i, with a_j from (6), the same steps give b_ik ε_ik g_k = b_ik′ ε_ik′ g_k′. So
+b_if = μ_i ε_if / g_f. Finally (E0) gives 4 λ_i μ_i = 16. ∎
+
+The proof needs no zero exclusion for i, no in-class equation and no witness inside i's own class. Each
+witnessed pair costs one linear equation, so connectivity is exactly what is needed. With every witness at
+one column of T removed, a 2-dimensional family survives **[control.disconnected-not-forced]**. As an
+algebra cross-check, `verify.py` builds the witnessed equations (E2) from (6) for random rational g, d′. On
+both a_i|T and b_i|T they have rank 3, with kernels ε_i ∘ g and ε_i / g **[lemma9.solution-line]**.
+
+**Finite input.** On this unit all eight two-row lines have all six pairs of T witnessed, with 40 witnesses
+each **[lemma9.propagation-connected]**. The non-gauge two-row solution of the control satisfies every
+in-class condition. It fails 28 of the 40 witnessed equations for one of its rows
+**[control.cross-block-rejects]**.
+
+## Assembly
+
+Steps 1 and 2 put every live non-pivot line into PR1212 §7's form, with d′_i = λ_i for the two-row lines.
+PR1212 §7 then applies verbatim and gives K = D (2G) D⁻¹. An exact rational control checks the assembly on
+all 104 live lines **[assembly-control, control.perturbed-fails]**. ∎
+
+## Remarks
+
+- Lemma 9 is more general than the use made of it here. It needs only a set of lines already in form (6)
+  that witnesses a connected pair graph, whatever their classes. It can be iterated, since propagated lines
+  become witnesses. The work on another unit is in Step 1, which needs (6) on enough classes to fix g.
+- Lemma 9 is linear in a_i and b_i. The only field facts it uses are division by 4 and by the nonzero
+  g_f, d′_j. Step 1 inherits PR1212's argument, which holds over any field of characteristic 0
+  (PR1212 §9).
diff --git a/research/complex-rank8-rigidity-p104-admissible/README.md b/research/complex-rank8-rigidity-p104-admissible/README.md
new file mode 100644
index 0000000000..9852ca5a3a
--- /dev/null
+++ b/research/complex-rank8-rigidity-p104-admissible/README.md
@@ -0,0 +1,94 @@
+# Rank-8 masked decoders are gauge-rigid on the 896 admissible P104 units (no new κ)
+
+**Status: scoped structural result. No κ claim, no construction.** It extends PR1212 (burntout76,
+`research/complex-rank8-decoder-rigidity/`, open, head `57099cb5`) and depends on that PR's zero-exclusion
+lemma. It is independent of PR1389, the type-(4,4) and P111 cases.
+
+PR1212 proves the following in PR717's E-graph (masked) model. Every rank-≤8 solution K of
+`K_ii = 4, K_ij = 0` on orthogonal live pairs, with odd entries free, is `D(2G)D⁻¹`. As a result, decoders
+with exactly eight costly terms keep PR968's floor. Its PROOF.md §10 leaves the **896 admissible P104 units**
+open (PR717's P104 among them). On its pivot there, four classes keep only two live rows, and Lemma 5 then
+leaves a one-parameter family inside each.
+
+This package closes that gap ([PROOF.md](PROOF.md)) with one new lemma:
+
+- **Lemma 9 (propagation).** Lemmas 5–6 already fix the global scaling `g` on the 22 complete classes, since
+  all 14 blocks carry one. A two-row line `i` then needs no in-class argument. Each witness `j` in a complete
+  class with `T_i ∩ T_j = {k, k′}` turns (E2) into `a_ik ε_ik / g_k = a_ik′ ε_ik′ / g_k′`, and the reverse
+  order gives the same for `b`. If the witnessed pairs connect `T_i`, then `a_i ∝ ε_i ∘ g` and `b_i ∝ ε_i / g`,
+  and (E0) fixes the product. On this unit every two-row line has all six pairs witnessed, with 40 witnesses
+  per line.
+
+**Consequence.** In the E-graph model, every decoder with exactly eight costly terms has `cst ≥ 56` on every
+admissible P104 unit. PR717's P104 decoders attain it.
+
+Together with PR1212 (336 type-(2,2,2,2) units) and PR1389 (28 type-(4,4) units), this covers all 1260 P104
+frame complements. That combination is conditional on PR1389, which is unmerged and unreviewed.
+
+## Reproduce
+
+From the repository root, Python 3.10+, standard library only, about 0.1 s:
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-p104-admissible/verify.py
+```
+
+Expected final line:
+
+```text
+PASS_COMPLEX_RANK8_RIGIDITY_P104_ADMISSIBLE: checks 15; classes 22 complete + 4 two-row; 8 two-row lines propagated; floor 56; zero exclusion cited from PR1212
+```
+
+To also replay PR1212's zero exclusion for this unit (about 15 s), first make a checkout of PR1212's head.
+The verifier checks the git blobs of its `verify.py` and `proof-P104-11111111.drup`. It then runs PR1212's
+verifier and matches the unit and pivot by root vectors:
+
+```sh
+git fetch origin pull/1212/head && git worktree add --detach /tmp/pr1212 57099cb5
+python3 -I -B research/complex-rank8-rigidity-p104-admissible/verify.py --pr1212-dir /tmp/pr1212
+```
+
+The last line then ends `... replayed from PR1212` with 22 checks. The replay covers
+`G.P104-11111111.zero-exclusion`, `G.P104-11111111.class-witnesses`, `G.frame-orbits` and
+`G.pr717-p104-orbit`.
+
+The verifier is independent of PR1212's code: it has its own E8 model, classes, witnesses, gluing and
+propagation. It recomputes the orbit type of the punctured frame. It cross-checks Lemma 9's algebra on
+the actual (E2) equations (rank 3, with the gauge vector as kernel). The four controls show that:
+
+- the in-class conditions admit a non-gauge two-row solution;
+- witnessed cross-block equations reject that solution (28 of 40 fail);
+- removing the witnesses at one column leaves a 2-dimensional family;
+- a perturbed entry breaks (2).
+
+## Not covered
+
+- **Nine or more costly terms**, including PR717's mixed-β problem. Rank-8 rigidity says nothing about
+  rank-≥9 solutions of (E).
+- **The intermediate punctures P105–P110.**
+- **Zero exclusion** is PR1212's DRUP result, replayed but not re-derived. The flat classification premise
+  (F6) inherited through PR968 is unchanged.
+- The written proof has had no independent human review. There is no construction and no κ change, and
+  every condition of the selected record is unchanged.
+
+## Open next questions
+
+**Intermediate punctures P105–P110.** This matters because, with this package, PR1212 and PR1389, rigidity
+holds on P120, P112, P111 and every P104 frame complement. The units in between are the remaining
+eight-term gap in the masked model. A feasible first step: enumerate the FRAME0-stabiliser orbits of 2–7
+line punctures of P112. For each orbit, pick a pivot and test (I3) and (I4) on the complete classes, then
+Lemma 9 connectivity for the other live lines. Lemma 9 needs no in-class equations, so incomplete classes
+cost nothing once `g` is fixed. The blocker: zero exclusion is a separate DRUP certificate per unit
+(PR1212's CNF builder plus python-sat), and the orbit count is not yet known. See [TASK.json](TASK.json).
+
+## Credit
+
+- **burntout76 / Brett Halligan (PR1212):** the theorem, the proof skeleton and every lemma reused here,
+  zero exclusion and its DRUP certificate for this unit, the transport, the pivot, and the §10 record of
+  this gap.
+- **themilkman216 (PR968):** the eight-term floor.
+- **DreamingOfClouds (PR717):** the E-graph model and the P104 decoders.
+- **Navinor (PR1292):** local rigidity on all P104 units.
+
+Prepared by JosieElliston with substantial assistance from Claude Opus 5.5 (Anthropic) via Claude Code,
+covering the proof, verifier and write-up. Apache-2.0.
diff --git a/research/complex-rank8-rigidity-p104-admissible/SOURCES.json b/research/complex-rank8-rigidity-p104-admissible/SOURCES.json
new file mode 100644
index 0000000000..43693ebc24
--- /dev/null
+++ b/research/complex-rank8-rigidity-p104-admissible/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    }
+  ]
+}
diff --git a/research/complex-rank8-rigidity-p104-admissible/TASK.json b/research/complex-rank8-rigidity-p104-admissible/TASK.json
new file mode 100644
index 0000000000..14ee70294d
--- /dev/null
+++ b/research/complex-rank8-rigidity-p104-admissible/TASK.json
@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-masked-decoder",
+  "priority_revision": 2,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "original_card": {
+    "id": "complex-masked-decoder",
+    "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?",
+    "starting_points": [
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md"
+    ],
+    "methods": [
+      "Synthesize a decoder with exact coefficients and fully priced helper endpoints.",
+      "Bound the best possible budget for a fixed support alphabet before synthesis."
+    ],
+    "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-decoder-field-extension-seed44/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44",
+      "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.",
+    "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.",
+    "allowed_variations": [
+      "Select a specific masked or overcomplete family with exact labels and supports."
+    ],
+    "scope_change_triggers": [
+      "Repeating the exact eight-term all-pairs search inside its proved scope."
+    ],
+    "overlap_terms": [
+      "masked decoder",
+      "overcomplete",
+      "eight-term"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Proof obligation inside the masked (E-graph) model: does every rank-<=8 solution of PR1212's system (E) on the 896 admissible (type (1,...,1)) P104 units equal D(2G)D^-1, so that decoders with exactly eight costly terms keep PR968's floor 56 there?",
+  "scope_change_reason": "The card asks whether a masked decoder can beat the floor. PR1212 answered it for exactly eight costly terms on P112, P120 and the type-(2,2,2,2) units, and PR1389 on P111 and type (4,4); both list the admissible P104 units as open (PR1212 PROOF.md section 10, PR1389 open question). This closes that gap; it does not construct a decoder.",
+  "bottleneck_link": "Side result on the binding complex supplier: the admissible units are where PR968's 7/13 ratio is attained (PR717's P104/56). This rules out masked eight-costly-term decoders below the floor there, so the remaining masked escape routes are nine or more costly terms or deeper/other punctures.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the admissible P104 orbit; nine or more costly terms and P105-P110 punctures are left as handoffs.",
+  "outcome": "completed",
+  "evidence": "verify.py: 11 exact checks plus 4 controls (about 0.1 s); --pr1212-dir replays PR1212's zero-exclusion DRUP proof for this unit, its class witnesses and the orbit transport from blob-pinned files (7 more checks).",
+  "author": "JosieElliston (with Claude Opus 5.5 via Claude Code)",
+  "ai_assistance": "Claude Opus 5.5 via Claude Code: proof, verifier and write-up. Submitted by the account holder.",
+  "open_questions": [
+    {
+      "question": "Does rank-8 rigidity of (E), and with it the eight-costly-term floor, hold on the intermediate punctures P105-P110 (P112 minus 2-7 lines)?",
+      "why_it_matters": "With this package, PR1212 and PR1389, rigidity holds on P120, P112, P111 and every P104 frame complement. The intermediate punctures are the remaining eight-term gap in the masked model between those depths.",
+      "first_step": "Enumerate the FRAME0-stabiliser orbits of 2-7 line punctures of P112, pick a pivot per orbit, and test (I3), (I4) on the complete classes plus Lemma 9 witness connectivity for every other live line. Lemma 9 uses no in-class equations, so incomplete classes cost nothing once g is fixed.",
+      "blocked_by": "Zero exclusion is a separate DRUP certificate per unit (PR1212's CNF builder and python-sat), and the number of orbits is not yet known."
+    }
+  ]
+}
diff --git a/research/complex-rank8-rigidity-p104-admissible/VERIFY.json b/research/complex-rank8-rigidity-p104-admissible/VERIFY.json
new file mode 100644
index 0000000000..0e5c842841
--- /dev/null
+++ b/research/complex-rank8-rigidity-p104-admissible/VERIFY.json
@@ -0,0 +1,19 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "11 exact structural checks on PR1212's admissible P104 representative (unit and orbit type, D4 blocks, class profile, Lemma 5 group witnesses, Lemma 6 blocks and gluing, Lemma 9 propagation connectivity and solution line, assembly) and 4 negative controls. PR1212 zero exclusion is cited; replay it with --pr1212-dir."
+    }
+  ]
+}
diff --git a/research/complex-rank8-rigidity-p104-admissible/verify.py b/research/complex-rank8-rigidity-p104-admissible/verify.py
new file mode 100644
index 0000000000..465a45e1dc
--- /dev/null
+++ b/research/complex-rank8-rigidity-p104-admissible/verify.py
@@ -0,0 +1,433 @@
+#!/usr/bin/env python3
+"""Finite inputs for extending PR1212's rank-8 rigidity theorem to the 896 admissible (type (1,...,1)) P104 units.
+
+Independent implementation (own E8 model, classes, witnesses and propagation); nothing is imported from
+PR1212.  Zero exclusion on this unit (PR1212 Lemma 8) and the orbit transport are cited.  With --pr1212-dir
+they are also replayed by running PR1212's own verifier from a checkout whose files match the pinned git blobs.
+
+    python3 -I -B research/complex-rank8-rigidity-p104-admissible/verify.py [--pr1212-dir DIR] [--out FILE]
+
+Standard library only.  Exact integer / rational arithmetic throughout.
+"""
+import argparse
+import hashlib
+import itertools
+import json
+import os
+import subprocess
+import sys
+from fractions import Fraction
+
+FAILS = []
+NCHECK = 0
+
+
+def check(tag, cond, info=''):
+    global NCHECK
+    NCHECK += 1
+    print(('PASS ' if cond else 'FAIL ') + tag + (' | ' + info if info else ''))
+    if not cond:
+        FAILS.append(tag)
+    return bool(cond)
+
+
+# ------------------------------------------------------------------ E8 model (doubled coordinates)
+def lines_e8():
+    """One representative per root line, roots in doubled coordinates (norm 8), canonical sign:
+    the first nonzero coordinate is positive."""
+    out = set()
+    for i, j in itertools.combinations(range(8), 2):
+        for sj in (2, -2):
+            v = [0] * 8
+            v[i], v[j] = 2, sj
+            out.add(tuple(v))
+    for s in itertools.product((1, -1), repeat=7):
+        v = (1,) + s
+        if v.count(-1) % 2 == 0:
+            out.add(v)
+    return sorted(out)
+
+
+LINES = lines_e8()
+IDX = {v: n for n, v in enumerate(LINES)}
+NL = len(LINES)
+
+
+def canon(v):
+    v = tuple(v)
+    first = next(a for a in v if a)
+    return v if first > 0 else tuple(-a for a in v)
+
+
+def ip(x, y):
+    d = sum(a * b for a, b in zip(x, y))
+    assert d % 4 == 0
+    return d // 4
+
+
+G = [[ip(LINES[i], LINES[j]) for j in range(NL)] for i in range(NL)]
+
+
+def lid(v):
+    return IDX[canon(v)]
+
+
+def frame_lines(vs):
+    return [lid(v) for v in vs]
+
+
+# PR1212's FRAME0 and its admissible representative unit P112 minus DEAD with pivot PIVOT, as root vectors
+# (from PR1212 head 57099cb5 verify.py `extension_units()`, unit 'P104-11111111'; --pr1212-dir rechecks the
+# correspondence through PR1212's own line numbering).
+FRAME0 = [(2, 2, 0, 0, 0, 0, 0, 0), (2, -2, 0, 0, 0, 0, 0, 0), (0, 0, 2, 2, 0, 0, 0, 0), (0, 0, 2, -2, 0, 0, 0, 0),
+          (0, 0, 0, 0, 2, 2, 0, 0), (0, 0, 0, 0, 2, -2, 0, 0), (0, 0, 0, 0, 0, 0, 2, 2), (0, 0, 0, 0, 0, 0, 2, -2)]
+DEAD = [(2, 0, 2, 0, 0, 0, 0, 0), (0, 2, 0, 0, 2, 0, 0, 0), (0, 0, 0, 2, 0, 0, 2, 0), (0, 0, 0, 0, 0, 2, 0, 2),
+        (1, 1, -1, 1, -1, 1, -1, -1), (1, 1, -1, -1, -1, -1, 1, 1), (1, -1, -1, 1, 1, -1, -1, 1), (1, -1, -1, -1, 1, 1, 1, -1)]
+PIVOT = [(2, 0, 0, 0, 0, 0, 0, 2), (2, 0, 0, 0, 0, 0, 0, -2), (0, 2, 0, 0, 0, 0, 2, 0), (0, 2, 0, 0, 0, 0, -2, 0),
+         (0, 0, 2, 0, 0, 2, 0, 0), (0, 0, 2, 0, 0, -2, 0, 0), (0, 0, 0, 2, 2, 0, 0, 0), (0, 0, 0, 2, -2, 0, 0, 0)]
+PR1212 = {
+    'head': '57099cb5684f38877f31d149d598801671a633db',
+    'dir': 'research/complex-rank8-decoder-rigidity',
+    'blobs': {'verify.py': 'c3707b0993d04b78e20c5d3512d370495690df8b',
+              'proof-P104-11111111.drup': 'e71c3c93deeb43a08772614fc439bd4b7bd08a24'},
+    'pass_lines': ['PASS G.P104-11111111.zero-exclusion', 'PASS G.P104-11111111.class-witnesses',
+                   'PASS G.frame-orbits', 'PASS G.pr717-p104-orbit'],
+    'unit_line': ('PASS G.P104-11111111.unit', 'P112 minus the frame (2, 18, 40, 52, 77, 86, 107, 112)',
+                  'pivot [12, 13, 22, 23, 30, 31, 36, 37]'),
+    'dead_idx': [2, 18, 40, 52, 77, 86, 107, 112],
+    'pivot_idx': [12, 13, 22, 23, 30, 31, 36, 37],
+}
+
+
+def is_frame(S):
+    return len(S) == 8 and all(G[a][b] == 0 for a in S for b in S if a != b)
+
+
+# ------------------------------------------------------------------ exact linear algebra
+def rank_q(rows):
+    M = [[Fraction(x) for x in r] for r in rows]
+    if not M:
+        return 0
+    r = 0
+    for c in range(len(M[0])):
+        p = next((i for i in range(r, len(M)) if M[i][c] != 0), None)
+        if p is None:
+            continue
+        M[r], M[p] = M[p], M[r]
+        for i in range(len(M)):
+            if i != r and M[i][c] != 0:
+                f = M[i][c] / M[r][c]
+                M[i] = [a - f * b for a, b in zip(M[i], M[r])]
+        r += 1
+    return r
+
+
+def lcg(seed):
+    x = seed
+    while True:
+        x = (6364136223846793005 * x + 1442695040888963407) % (1 << 64)
+        yield x >> 33
+
+
+def rand_nonzero(rng):
+    while True:
+        n = next(rng) % 17 - 8
+        d = next(rng) % 7 + 1
+        if n:
+            return Fraction(n, d)
+
+
+# ------------------------------------------------------------------ structure relative to a pivot
+def relative(F, lines):
+    """line -> (T, eps): T the pivot lines (in pivot order) the line is odd to, eps the signs G_if."""
+    out = {}
+    for i in lines:
+        if i in F:
+            continue
+        T = tuple(f for f in F if G[i][f] != 0)
+        out[i] = (T, tuple(G[i][f] for f in T))
+    return out
+
+
+def parity(eps):
+    return sum(1 for s in eps if s < 0) % 2
+
+
+def classes_of(rel):
+    cl = {}
+    for i, (T, eps) in rel.items():
+        cl.setdefault((T, parity(eps)), []).append(i)
+    return cl
+
+
+def connected(nodes, edges):
+    nodes = list(nodes)
+    if not nodes:
+        return False
+    seen, todo = {nodes[0]}, [nodes[0]]
+    while todo:
+        x = todo.pop()
+        for p, q in edges:
+            for y in ((q,) if p == x else (p,) if q == x else ()):
+                if y not in seen:
+                    seen.add(y)
+                    todo.append(y)
+    return len(seen) == len(nodes)
+
+
+def gauge_form(rel, F, g, dd):
+    """a_i = d'_i eps_i g, b_i = 4 (d'_i g)^-1 eps_i on T_i (PR1212 section 7), pivots a_f = b_f = 4 e_f."""
+    a = {i: {f: (dd[i] * G[i][f] * g[f] if f in rel[i][0] else Fraction(0)) for f in F} for i in rel}
+    b = {i: {f: (4 / (dd[i] * g[f]) * G[i][f] if f in rel[i][0] else Fraction(0)) for f in F} for i in rel}
+    for f in F:
+        a[f] = {h: Fraction(4 if h == f else 0) for h in F}
+        b[f] = {h: Fraction(4 if h == f else 0) for h in F}
+    return a, b
+
+
+def system_holds(a, b, live, F, rows=None):
+    """Equations (2) of PR1212: a_i . b_j = 16 [i = j] on the diagonal and on orthogonal live pairs."""
+    rows = live if rows is None else rows
+    return all(sum(a[i][f] * b[j][f] for f in F) == (16 if i == j else 0)
+               for i in rows for j in live if i == j or G[i][j] == 0)
+
+
+def analyse(cert):
+    print('== unit')
+    F0 = frame_lines(FRAME0)
+    P112 = [i for i in range(NL) if i not in F0]
+    dead = frame_lines(DEAD)
+    live = [i for i in P112 if i not in dead]
+    F = frame_lines(PIVOT)
+    check('unit.live', is_frame(dead) and set(dead) <= set(P112) and len(live) == 104
+          and is_frame(F) and set(F) <= set(live), 'P112 minus a frame inside P112; live 104; pivot is a live frame')
+
+    # Type of the punctured frame relative to FRAME0: how many of its lines fall in each FRAME0 class.
+    cl0 = classes_of(relative(F0, range(NL)))
+    hits = sorted((sum(1 for i in v if i in dead) for v in cl0.values()), reverse=True)
+    check('unit.admissible-type', hits[:8] == [1] * 8 and sum(hits) == 8,
+          'the punctured frame meets 8 distinct FRAME0 classes once each: type (1,...,1), the 896-orbit (PR968 admissible)')
+
+    # Lemma 2 facts used below, recomputed relative to the pivot.
+    rel_all = relative(F, range(NL))
+    rel = relative(F, live)
+    blocks = sorted({T for T, _ in rel_all.values()})
+    ok_a = all(len(T) == 4 and all(abs(s) == 1 for s in e) for T, e in rel_all.values())
+    steiner = len(blocks) == 14 and all(sum(1 for B in blocks if set(t) <= set(B)) == 1
+                                        for t in itertools.combinations(F, 3))
+    cl_all = classes_of(rel_all)
+    had = len(cl_all) == 28 and all(
+        len(v) == 4 and all(G[i][j] == 0 for i in v for j in v if i != j)
+        and all(sum(x * y for x, y in zip(rel_all[i][1], rel_all[j][1])) == (4 if i == j else 0) for i in v for j in v)
+        for v in cl_all.values())
+    rule = True
+    for i, j in itertools.combinations(rel_all, 2):
+        Ti, ei = rel_all[i]
+        Tj, ej = rel_all[j]
+        s = sum(ei[Ti.index(f)] * ej[Tj.index(f)] for f in set(Ti) & set(Tj))
+        rule &= (2 * G[i][j] == s)
+    check('unit.d4-structure', ok_a and steiner and had and rule,
+          '112 non-pivot lines odd to 4 pivot lines; 14 blocks = S(3,4,8); 28 Hadamard 4-frame classes; 2G_ij = sum of sign products')
+
+    cl = classes_of(rel)
+    sizes = {}
+    for key in cl_all:
+        n = len(cl.get(key, []))
+        sizes[n] = sizes.get(n, 0) + 1
+    check('unit.class-profile', sizes == {0: 2, 2: 4, 4: 22}, f'live rows per class -> count: {dict(sorted(sizes.items()))}')
+    complete = {k: v for k, v in cl.items() if len(v) == 4}
+    known = {i for v in complete.values() for i in v}
+    rest = [i for i in rel if i not in known]
+
+    # (I3) Lemma 5 step 1: every live group of every complete class has a live witness in another block.
+    wit_ok, nwit = True, 0
+    for (T, _), rows in complete.items():
+        for c, c2 in itertools.combinations(range(4), 2):
+            for i, i2 in itertools.combinations(rows, 2):
+                if rel[i][1][c] * rel[i][1][c2] != rel[i2][1][c] * rel[i2][1][c2]:
+                    continue
+                nwit += 1
+                wit_ok &= any(set(Tj) & set(T) == {T[c], T[c2]} and G[j][i] == 0 and G[j][i2] == 0
+                              for j, (Tj, _) in rel.items())
+    check('lemma5.group-witnesses', wit_ok and nwit == 22 * 12,
+          f'{nwit} live groups (22 complete classes x 6 column pairs x 2 groups) each have a live witness')
+
+    # (I4) Lemma 6: every block carries a complete live class, and for complete classes C, C' in distinct
+    # blocks meeting in {k, k'}, every row j of C' is orthogonal to exactly two rows of C.
+    cblocks = {T for (T, _) in complete}
+    pair_ok, npair = True, 0
+    for c1, c2 in itertools.permutations(complete, 2):
+        if c1[0] == c2[0] or len(set(c1[0]) & set(c2[0])) != 2:
+            continue
+        npair += 1
+        pair_ok &= all(sum(1 for i in complete[c1] if G[i][j] == 0) == 2 for j in complete[c2])
+    check('lemma6.blocks-and-gluing', len(cblocks) == 14 and pair_ok,
+          f'14/14 blocks carry a complete class; {npair} ordered class pairs through a pivot pair glue')
+
+    # Lemma 9 (propagation) input: for every live line i outside the complete classes, the column pairs
+    # {k, k'} of T_i witnessed by a line j of a complete class with G_ij = 0 and T_i n T_j = {k, k'}
+    # connect T_i.  Also checked: every such witness has eps_ik eps_jk = -eps_ik' eps_jk', the identity
+    # the derivation uses.
+    prop_ok, sign_ok, prop = True, True, {}
+    for i in rest:
+        T, ei = rel[i]
+        edges, nw = [], 0
+        for c, c2 in itertools.combinations(range(4), 2):
+            ws = [j for j in known if G[i][j] == 0 and set(rel[j][0]) & set(T) == {T[c], T[c2]}]
+            for j in ws:
+                ej = rel[j][1]
+                Tj = rel[j][0]
+                sign_ok &= ei[c] * ej[Tj.index(T[c])] == -ei[c2] * ej[Tj.index(T[c2])]
+            if ws:
+                edges.append((c, c2))
+            nw += len(ws)
+        prop[i] = (edges, nw)
+        prop_ok &= connected(range(4), edges)
+    full = all(len(e) == 6 for e, _ in prop.values())
+    check('lemma9.propagation-connected', len(rest) == 8 and prop_ok and sign_ok,
+          f'{len(rest)} two-row lines: witnessed column pairs connect T_i'
+          + (' (all 6 pairs witnessed for every line)' if full else ''))
+
+    # Lemma 9 algebra, cross-checked on the actual equations rather than the simplified ratio form: with the
+    # complete classes in gauge form for random rational g, d', the witnessed equations (E2) in the order
+    # a_i . b_j are linear in the 4 unknowns a_i|T and have a 1-dimensional solution space spanned by eps_i o g;
+    # in the order a_j . b_i the same holds for b_i with eps_i / g.
+    rng = lcg(1212)
+    g = {f: rand_nonzero(rng) for f in F}
+    dd = {i: rand_nonzero(rng) for i in rel}
+    alg_ok = True
+    for i in rest:
+        T, ei = rel[i]
+        wit = [j for j in known if G[i][j] == 0 and len(set(rel[j][0]) & set(T)) == 2]
+        rows_a = [[4 / (dd[j] * g[f]) * G[j][f] for f in T] for j in wit]   # b_j|T coefficients
+        rows_b = [[dd[j] * G[j][f] * g[f] for f in T] for j in wit]         # a_j|T coefficients
+        va = [ei[n] * g[f] for n, f in enumerate(T)]
+        vb = [ei[n] / g[f] for n, f in enumerate(T)]
+        alg_ok &= rank_q(rows_a) == 3 and all(sum(r[n] * va[n] for n in range(4)) == 0 for r in rows_a)
+        alg_ok &= rank_q(rows_b) == 3 and all(sum(r[n] * vb[n] for n in range(4)) == 0 for r in rows_b)
+    check('lemma9.solution-line', alg_ok,
+          'witnessed (E2) equations have rank 3 on a_i|T and on b_i|T, kernel spanned by eps_i o g and eps_i / g')
+
+    # Assembly control (PR1212 section 7 on this unit): gauge forms satisfy (2) and assemble to D (2G) D^-1.
+    a, b = gauge_form(rel, F, g, dd)
+    D = {i: dd[i] / 2 for i in rel}
+    D.update({f: 1 / g[f] for f in F})
+    asm_ok = system_holds(a, b, live, F) and all(
+        sum(a[i][f] * b[j][f] for f in F) / 4 == 2 * G[i][j] * D[i] / D[j] for i in live for j in live)
+    check('assembly-control', asm_ok, 'gauge forms satisfy (2) on all 104 live lines and assemble to D (2G) D^-1 exactly')
+    cert.update({'live': len(live), 'dead_frame': DEAD, 'pivot': PIVOT, 'class_profile': sizes,
+                 'two_row_lines': {str(LINES[i]): {'support': [LINES[f] for f in rel[i][0]],
+                                                   'witnessed_pairs': len(prop[i][0]), 'witnesses': prop[i][1]}
+                                   for i in rest},
+                 'group_witnesses': nwit, 'glued_class_pairs': npair, 'floor': 56})
+    return live, F, rel, complete, known, rest, g, dd
+
+
+def controls(data):
+    print('== controls')
+    live, F, rel, complete, known, rest, g, dd = data
+    # C1: inside a two-row class, every in-class condition (E0, E4 both ways, Lemma 5 step-1 parallelism on the
+    # one live group, for a and for b) admits a non-gauge solution.  Rows 1, 2 have eps_1 o eps_2 = s (1,1,-1,-1)
+    # in the column order where they form a group; u_1 = (1,1,1,1), u_2 = (1,1,t,t), v_1 = (8t,8t,8,8)/(t+1),
+    # v_2 = 8 (1,1,1,1)/(t+1), with a = eps o u, b = eps o v.  For t = 2 it is not of gauge form.
+    i1 = rest[0]
+    T, e1 = rel[i1]
+    i2 = next(j for j in rest if j != i1 and rel[j][0] == T and parity(rel[j][1]) == parity(e1))
+    e2 = rel[i2][1]
+    p = [e1[n] * e2[n] for n in range(4)]
+    grp = next((c, c2) for c, c2 in itertools.combinations(range(4), 2) if p[c] == p[c2])
+    oth = tuple(n for n in range(4) if n not in grp)
+    t = Fraction(2)
+    u1 = [Fraction(1)] * 4
+    u2 = [t if n in oth else Fraction(1) for n in range(4)]
+    v1 = [8 * (t if n in grp else 1) / (t + 1) for n in range(4)]
+    v2 = [Fraction(8) / (t + 1)] * 4
+    A = {i1: [e1[n] * u1[n] for n in range(4)], i2: [e2[n] * u2[n] for n in range(4)]}
+    B = {i1: [e1[n] * v1[n] for n in range(4)], i2: [e2[n] * v2[n] for n in range(4)]}
+
+    def dot(x, y):
+        return sum(x[n] * y[n] for n in range(4))
+    in_class = (dot(A[i1], B[i1]) == 16 and dot(A[i2], B[i2]) == 16 and dot(A[i1], B[i2]) == 0
+                and dot(A[i2], B[i1]) == 0 and G[i1][i2] == 0)
+    par = all(X[i1][c] * X[i2][c2] == X[i1][c2] * X[i2][c] for X in (A, B) for c, c2 in (grp, oth))
+    gauge = rank_q([[A[i1][n] * e1[n] for n in range(4)], [A[i2][n] * e2[n] for n in range(4)]]) == 1
+    check('control.in-class-not-forced', in_class and par and not gauge,
+          'a non-gauge two-row solution satisfies every in-class condition (PR1212: one-parameter family)')
+    # C2: the same rows fail a witnessed cross-block equation (E2) once the complete classes are in gauge form
+    # (any scaling: here g = 1 on T, matching u_1, so row 1 passes and row 2 must fail).
+    g1 = {f: Fraction(1) for f in F}
+    _, bg = gauge_form(rel, F, g1, dd)
+    wit = [j for j in known if G[i2][j] == 0 and len(set(rel[j][0]) & set(T)) == 2]
+    fails = [j for j in wit if sum(A[i2][n] * bg[j][f] for n, f in enumerate(T)) != 0]
+    check('control.cross-block-rejects', len(fails) > 0,
+          f'{len(fails)}/{len(wit)} witnessed (E2) equations reject the non-gauge row')
+    # C3: the connectivity input is necessary for the conclusion: dropping every witness at one column of T_i
+    # leaves a 2-dimensional solution space for a_i|T.
+    i = rest[0]
+    T, _ = rel[i]
+    wit = [j for j in known if G[i][j] == 0 and len(set(rel[j][0]) & set(T)) == 2 and T[0] not in rel[j][0]]
+    rows_a = [[4 / (dd[j] * g[f]) * G[j][f] for f in T] for j in wit]
+    check('control.disconnected-not-forced', 4 - rank_q(rows_a) == 2,
+          'without witnesses at one column the propagation equations leave 2 free directions')
+    # C4: tripling one entry of a two-row line in an exact gauge solution breaks (2).
+    a, b = gauge_form(rel, F, g, dd)
+    a[i][T[0]] *= 3
+    check('control.perturbed-fails', not system_holds(a, b, live, F, rows=[i]), 'tripling one a-entry of a two-row line violates (2)')
+
+
+def git_blob_sha1(path):
+    data = open(path, 'rb').read()
+    return hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest()
+
+
+def replay_pr1212(root, cert):
+    print('== PR1212 replay (zero exclusion, witnesses, transport)')
+    pkg = os.path.join(root, PR1212['dir'])
+    blobs = {f: git_blob_sha1(os.path.join(pkg, f)) for f in PR1212['blobs']}
+    if not check('pr1212.blobs', blobs == PR1212['blobs'], f'files match head {PR1212["head"][:8]}'):
+        return
+    out = subprocess.run([sys.executable, '-I', '-B', os.path.join(pkg, 'verify.py')], capture_output=True, text=True,
+                         cwd=root).stdout
+    lines = out.splitlines()
+    for p in PR1212['pass_lines']:
+        check('pr1212.' + p.split()[1], any(l.startswith(p + ' ') or l == p for l in lines), p)
+    head, unit, piv = PR1212['unit_line']
+    check('pr1212.unit-line', any(l.startswith(head) and unit in l and piv in l for l in lines), f'{unit}; {piv}')
+    code = ('import sys,json; sys.path.insert(0, sys.argv[1]); import verify as V; '
+            'print(json.dumps({"lines": V.LINES}))')
+    vec = json.loads(subprocess.run([sys.executable, '-I', '-B', '-c', code, pkg], capture_output=True, text=True).stdout)
+    same = (sorted(canon(vec['lines'][i]) for i in PR1212['pivot_idx']) == sorted(canon(v) for v in PIVOT)
+            and sorted(canon(vec['lines'][i]) for i in PR1212['dead_idx']) == sorted(canon(v) for v in DEAD))
+    check('pr1212.unit-vectors', same, 'same punctured frame and pivot as root vectors')
+    cert['pr1212_replayed'] = True
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument('--pr1212-dir', help='checkout of PR1212 head 57099cb5 (repo root); replays its zero-exclusion checks')
+    ap.add_argument('--out', help='write certificate JSON (must not exist)')
+    args = ap.parse_args()
+    cert = {'pr1212_head': PR1212['head'], 'pr1212_replayed': False}
+    print('== model')
+    check('model.lines', NL == 120 and {abs(G[i][j]) for i in range(NL) for j in range(NL) if i != j} == {0, 1},
+          '120 lines, Gram off-diagonal in {0,+-1}')
+    check('model.frame0', is_frame(frame_lines(FRAME0)), 'FRAME0 is a frame')
+    data = analyse(cert)
+    controls(data)
+    if args.pr1212_dir:
+        replay_pr1212(args.pr1212_dir, cert)
+    else:
+        print('NOTE zero exclusion and orbit transport cited from PR1212 (not replayed; pass --pr1212-dir)')
+    if args.out:
+        with open(args.out, 'x') as fh:
+            json.dump(cert, fh, indent=1, default=list)
+    if FAILS:
+        print('FAILED: ' + ', '.join(FAILS))
+        sys.exit(1)
+    print(f'PASS_COMPLEX_RANK8_RIGIDITY_P104_ADMISSIBLE: checks {NCHECK}; classes 22 complete + 4 two-row; '
+          f'8 two-row lines propagated; floor 56; zero exclusion '
+          + ('replayed from PR1212' if cert['pr1212_replayed'] else 'cited from PR1212'))
+
+
+if __name__ == '__main__':
+    main()