diff --git a/research/e7-quadratic-support/README.md b/research/e7-quadratic-support/README.md
new file mode 100644
index 0000000000..5dc8029611
--- /dev/null
+++ b/research/e7-quadratic-support/README.md
@@ -0,0 +1,178 @@
+# Sharp support twelve for trace-zero E7 quadratics
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Result and claim type
+
+**Scoped mathematical proof with an exact finite certificate.** Every nonzero
+rational trace-zero quadratic form on the seven-dimensional orthogonal
+complement of an E8 root is nonzero on at least **twelve** of its 63 root
+lines. Twelve is attained.
+
+This proves the trace-zero replacement for auxiliary statement (2) in
+[JoyboyBrian's released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642).
+The unrestricted statement there needs correction: products of two linear
+forms can have support eleven, as already follows from the 52-line two-flat
+union in DreamingOfClouds's #595 and DaysSky's
+[#897](https://github.com/CrocSwap/integer-mult-bounds/pull/897).
+DreamingOfClouds's open
+[#3045](https://github.com/CrocSwap/integer-mult-bounds/pull/3045)
+also records an E7 intersection of supports of size eleven. The eleven-line
+example first reported in this contribution's progress post is therefore
+credited to that existing coverage, not claimed as an original result.
+The new result is the sharp trace-zero bound and its frame-code certificate.
+
+The arbitrary-deletion quadratic extension in handoff statement (1) remains
+open. This package does not prove the seven-deletion rigidity shortcut.
+
+## Finite certificate
+
+Use doubled E8 roots, with canonical line representatives
+`2e_i +/- 2e_j`, `i < j`, and `(1,s_1,...,s_7)` with an even number of
+negative coordinates. All have squared norm eight. Coordinates run from zero
+through seven. Fix `a=2e_0+2e_4`, and let `R` be the 63 root lines in `a`-perp.
+An orthogonal frame consists of seven mutually orthogonal lines in `R`.
+
+The verifier constructs every frame by an increasing-clique traversal,
+retaining a branch only when enough candidates remain to complete it.
+It finds 135 frames. Their binary incidence matrix `H`, of shape `135 x 63`,
+has rank 36 and kernel dimension 27. The verifier constructs a kernel basis
+with an identity submatrix on its free coordinates, checks every basis vector
+against every row, and enumerates every one of its **134,217,727 nonzero
+vectors**. Their minimum Hamming weight is **12**.
+
+The enumeration uses a Gray traversal. At step `i`, toggling basis vector
+`v_((i & -i).bit_length()-1)` changes the coefficient vector to `i xor (i>>1)`.
+These coefficient vectors visit every nonzero element of `F2^27` once.
+The identity on the free coordinates proves that their images are distinct.
+The finite minimum is recomputed on every registered replay; no saved census
+or external solver is trusted.
+
+## Proof of the rational lower bound
+
+More generally, every nonzero rational function on `R` whose sum on every
+orthogonal frame is zero has support at least twelve. Clear its denominators
+and divide its integer values by their greatest common divisor. The resulting
+primitive integer vector still has zero frame sums, and its reduction modulo
+two is nonzero. That reduction lies in `ker(H)`, and its support is contained
+in the original support. The finite certificate therefore proves the bound.
+
+For a trace-zero quadratic `q`, every frame has zero sum: its seven roots
+are an orthogonal basis of `a`-perp with squared norm eight, so
+`sum(q(r): r in frame) = 8 trace(q) = 0`.
+It remains to check that a nonzero quadratic cannot vanish on all of `R`.
+Here is an elementary injectivity argument.
+
+Write `J={1,2,3,5,6,7}` and `y=x_0=-x_4` on `a`-perp. If a quadratic
+vanishes on every `2e_i +/- 2e_j`, with `i,j` in `J`, subtracting the two
+evaluations kills each mixed coefficient within `J`, and adding them shows
+that every pair of diagonal coefficients sums to zero. Three distinct indices
+then force all six diagonal coefficients to vanish over the rationals.
+The root `2e_0-2e_4` kills the coefficient of `y^2`. Only
+`y sum(b_i x_i: i in J)` remains. The 32 half-root lines have `y=1`, with
+all odd-parity six-sign rows `s`. These rows satisfy `sum(s s^T)=32 I_6`,
+so vanishing on them forces every `b_i=0`. Thus the original quadratic was zero.
+
+This proves the lower bound for the stated rational domain. To transport it
+to any E8 root, the verifier checks nine orthogonal root-set automorphisms:
+seven adjacent coordinate swaps, negation of coordinates zero and one, and
+reflection in `(1,-1,-1,-1,1,-1,-1,-1)`. Their orbit on `a` contains all
+120 root lines. Orthogonal rational transport preserves trace and support.
+
+## A twelve-line attainer
+
+Restrict
+
+\[
+ q_0(x)=x_0^2+x_1^2+x_2^2+x_3^2-x_4^2-x_5^2-x_6^2-x_7^2
+\]
+
+to `a`-perp. The ambient trace is zero and `q_0(a)=0`, so the restricted
+trace is zero. On `R`, the six coordinate-root lines within `{1,2,3}` have
+value `+8`, the six within `{5,6,7}` have value `-8`, and the other 51 lines
+have value zero. Indeed, cross-part coordinate roots cancel, `2e_0-2e_4`
+cancels, and every half-root has four positive and four negative square terms.
+The verifier checks the twelve nonzero values and all 135 literal frame sums.
+
+## Relation to the handoff and limits
+
+The delivered scope repairs the proposed auxiliary support statement by adding
+trace zero. If an ambient trace-zero quadratic vanishes on the pivot, its
+restriction to the pivot's orthogonal complement is trace-zero: in an
+orthonormal basis beginning with the pivot direction, that first diagonal
+entry and the total trace are both zero. The new lemma can therefore supply
+the support step in the handoff's proposed reduction, conditional on its
+separate arbitrary-deletion extension statement and the remaining hypotheses.
+
+The advance claim asked about the unrestricted statement. Semantic overlap
+checking identified the earlier eleven-line coverage before any commit.
+The original contribution delivered here is the trace-zero replacement.
+Neither the earlier flat census nor any predecessor's rigidity result is
+replayed or re-verified as this contribution.
+
+The binary minimum is a complete finite enumeration, not a formal proof-kernel
+certificate. The rational implication and injectivity argument are written
+proofs. Native realization, physical supplier admission, selected cold replay,
+Lean and the complete multiplication theorem are outside scope. No new kappa
+or selected-frontier change is claimed.
+
+## Reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/e7-quadratic-support/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/e7-quadratic-support/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e7-quadratic-support
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e7-quadratic-support --check-source-history
+```
+
+Another CPython 3.12 path can replace the local interpreter path.
+Expected status is `PASS_E7_TRACE_ZERO_SUPPORT`, with 63 lines, 135 frames,
+binary rank 36, dimension 27, 134217727 nonzero codewords, minimum weight 12,
+a quadratic attainer with six positive and six negative values, and 92
+rejecting controls. Normal and optimized modes use explicit checks, not assertions.
+
+The verifier constructs E8 and the intrinsic E7 slice separately and checks the
+root orbit. Omission controls reject every incomplete 63-line domain; basis
+controls reject every one-bit-corrupted basis vector and wrong dimensions.
+It uses bounded traversals, no recursion, and a constant-memory Gray census.
+Python runtime allocation is unavoidable; the stored geometry has only 120
+root lines, 135 frames and 27 kernel vectors. Optional
+`--receipt /absolute/path/outside/the/package.json` writes a generated receipt
+bound to all five package source hashes. Direct replay needs no Git or
+predecessor imports and writes nothing into its source package.
+
+## Open next questions
+
+1. Does every live-frame zero-sum rational function on P112 minus at most
+   seven lines extend to an ambient trace-zero quadratic? This is handoff
+   statement (1) and is the remaining uniform bridge in that reduction.
+   First prove an extension lemma retaining every deletion quantifier.
+   Its existing finite fixtures do not establish that implication.
+2. Which trace-zero quadratics attain support twelve? A classification could
+   identify all possible sparse equality obstructions. First determine the
+   rational kernels on the weight-twelve supports; no equality classification
+   is claimed or required for the present minimum.
+
+## Sources and credit
+
+The immediate question comes from
+[JoyboyBrian's released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642).
+The full-family shortcut and its eight-deletion counterexamples are Josie
+Elliston's [#1668](https://github.com/CrocSwap/integer-mult-bounds/pull/1668),
+following [#1650](https://github.com/CrocSwap/integer-mult-bounds/pull/1650)
+and [#1616](https://github.com/CrocSwap/integer-mult-bounds/pull/1616).
+Andrey Mas's [#1560](https://github.com/CrocSwap/integer-mult-bounds/pull/1560)
+supplies the incidence criterion. Aaron Wang's
+[#1649](https://github.com/CrocSwap/integer-mult-bounds/pull/1649) separates
+the subfamily question. DreamingOfClouds / #595 and #3045 and DaysSky / #897
+retain credit for the earlier unrestricted eleven-line support coverage.
+The retained E8 model and rigidity lineage credit Brett Halligan / #1212,
+themilkman216 / #968, and DreamingOfClouds / #717.
+
+These are motivation and provenance, not mathematical inputs to the new
+self-contained certificate. `SOURCES.json` pins the originating catalogue and
+predecessor notes at canonical main
+`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`.
diff --git a/research/e7-quadratic-support/SOURCES.json b/research/e7-quadratic-support/SOURCES.json
new file mode 100644
index 0000000000..99b379b173
--- /dev/null
+++ b/research/e7-quadratic-support/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/full-family-g-without-d/README.md",
+      "usage": "provenance",
+      "git_blob": "50cb846dc47e238a3f751966555e52aae887f702",
+      "sha256": "4ebf92cebdf400ccd63a89d09376378be86bbe6fdb9f1565b39ddd234958d96c"
+    }
+  ]
+}
diff --git a/research/e7-quadratic-support/TASK.json b/research/e7-quadratic-support/TASK.json
new file mode 100644
index 0000000000..99fcde6b80
--- /dev/null
+++ b/research/e7-quadratic-support/TASK.json
@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 7,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the sharp support bound twelve for every nonzero rational trace-zero quadratic on any E7 complement of an E8 root, using the minimum weight of the binary orthogonal-frame code.",
+  "scope_change_reason": "The released handoff asks for an unrestricted support bound. Before committing, semantic overlap found prior eleven-line coverage in #595/#897/#3045, so that witness is credited rather than claimed. The new result proves the trace-zero replacement sufficient for the proposed support step.",
+  "bottleneck_link": "Scoped algebraic lemma for the seven-deletion rigidity reduction. The trace-zero support step is now proved; arbitrary-deletion quadratic extension and supplier admission remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first original verified implication. Stop after the sharp trace-zero bound and its finite certificate; do not classify equality supports or extend the construction.",
+  "outcome": "completed",
+  "evidence": "Written primitive-integer modulo-two support argument, quadratic injectivity proof and exact full binary code enumeration: 135 x 63 incidence matrix, rank 36, kernel dimension 27, all 134217727 nonzero words, minimum twelve. A diagonal trace-zero quadratic attains twelve. Normal and optimized modes include 92 rejecting controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does every live-frame zero-sum rational function on P112 minus at most seven lines extend to an ambient trace-zero quadratic?",
+      "why_it_matters": "This is the remaining uniform extension bridge in the handoff reduction.",
+      "first_step": "Prove the extension statement with arbitrary-deletion quantifiers retained.",
+      "blocked_by": "Finite fixtures do not establish the uniform extension."
+    },
+    {
+      "question": "Which trace-zero quadratics attain support twelve?",
+      "why_it_matters": "An equality classification could identify all possible sparse obstructions.",
+      "first_step": "Determine rational quadratic kernels on the weight-twelve supports.",
+      "blocked_by": "The minimum proof does not classify equality, and no classification was attempted."
+    }
+  ],
+  "claim_type": "scoped mathematical proof with an exact finite certificate",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146102",
+  "progress_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146143",
+  "handoff_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642",
+  "environment": {
+    "implementation": "CPython",
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "standard library only"
+  },
+  "verification_budget_seconds": {
+    "normal_measured": 10.848847542074509,
+    "optimized_measured": 10.599868249963038,
+    "per_command_timeout": 180,
+    "interpretation": "One local timing per registered command for CI budget planning, not a performance comparison."
+  },
+  "upstream_checkpoint": {
+    "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+    "checked_at_utc": "2026-10-23T13:12:00.026157+00:00",
+    "priority_revision": 7,
+    "guidance_changed_since_base": false,
+    "scientific_base_retained": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c"
+  }
+}
diff --git a/research/e7-quadratic-support/VERIFY.json b/research/e7-quadratic-support/VERIFY.json
new file mode 100644
index 0000000000..7c558c2ec4
--- /dev/null
+++ b/research/e7-quadratic-support/VERIFY.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Full exact 134217727-word binary E7 frame-code census, sharp rational trace-zero quadratic support proof premises, root transitivity, twelve-line attainer and 92 rejecting controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Full exact 134217727-word binary E7 frame-code census, sharp rational trace-zero quadratic support proof premises, root transitivity, twelve-line attainer and 92 rejecting controls with Python assertions disabled."
+    }
+  ]
+}
diff --git a/research/e7-quadratic-support/verify.py b/research/e7-quadratic-support/verify.py
new file mode 100644
index 0000000000..781a074d45
--- /dev/null
+++ b/research/e7-quadratic-support/verify.py
@@ -0,0 +1,262 @@
+#!/usr/bin/env python3
+"""Sharp support twelve for rational trace-zero E7 quadratics. Exact integers."""
+
+import argparse
+from collections import Counter
+import hashlib
+import itertools
+import json
+from pathlib import Path
+import platform
+
+
+PIVOT = (2, 0, 0, 0, 2, 0, 0, 0)
+DIAGONAL = (1, 1, 1, 1, -1, -1, -1, -1)
+N = 63
+DIMENSION = 27
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def dot(left, right):
+    require(len(left) == len(right) == 8, "eight coordinates required")
+    return sum(left[i] * right[i] for i in range(8))
+
+
+def e8_lines():
+    roots = []
+    for i, j in itertools.combinations(range(8), 2):
+        for sign in (-1, 1):
+            root = [0] * 8
+            root[i], root[j] = 2, 2 * sign
+            roots.append(tuple(root))
+    for tail in itertools.product((-1, 1), repeat=7):
+        root = (1,) + tail
+        if root.count(-1) % 2 == 0:
+            roots.append(root)
+    require(len(roots) == len(set(roots)) == 120, "E8 line count")
+    require(all(dot(root, root) == 8 for root in roots), "E8 norms")
+    return tuple(sorted(roots))
+
+
+def intrinsic_e7():
+    roots = []
+    for i, j in itertools.combinations((1, 2, 3, 5, 6, 7), 2):
+        for sign in (-1, 1):
+            root = [0] * 8
+            root[i], root[j] = 2, 2 * sign
+            roots.append(tuple(root))
+    roots.append((2, 0, 0, 0, -2, 0, 0, 0))
+    for signs in itertools.product((-1, 1), repeat=6):
+        if signs.count(-1) % 2 == 1:
+            roots.append((1,) + signs[:3] + (-1,) + signs[3:])
+    return tuple(sorted(roots))
+
+
+def validate_domain(roots):
+    require(len(roots) == len(set(roots)) == N, "63 distinct root lines")
+    require(tuple(sorted(roots)) == intrinsic_e7(), "intrinsic E7 agreement")
+    require(all(dot(PIVOT, root) == 0 for root in roots), "orthogonal slice")
+
+
+def root_transport(root, generator):
+    out = list(root)
+    if generator < 7:
+        out[generator], out[generator + 1] = out[generator + 1], out[generator]
+    elif generator == 7:
+        out[0], out[1] = -out[0], -out[1]
+    else:
+        require(generator == 8, "nine fixed orthogonal generators")
+        normal = (1, -1, -1, -1, 1, -1, -1, -1)
+        inner = dot(root, normal)
+        require(inner % 4 == 0, "integral E8 reflection")
+        out = [root[i] - inner // 4 * normal[i] for i in range(8)]
+    first = next(value for value in out if value)
+    return tuple(value if first > 0 else -value for value in out)
+
+
+def check_root_transitivity():
+    domain = set(e8_lines())
+    for generator, root in itertools.product(range(9), domain):
+        require(root_transport(root, generator) in domain, "root-set automorphism")
+    orbit = {PIVOT}
+    stack = [PIVOT]
+    for _ in range(120):
+        if not stack:
+            break
+        root = stack.pop()
+        for generator in range(9):
+            image = root_transport(root, generator)
+            if image not in orbit:
+                orbit.add(image)
+                stack.append(image)
+    require(not stack and orbit == domain, "all 120 root lines reached")
+    return len(orbit)
+
+
+def orthogonal_frames(roots):
+    adjacency = [{j for j in range(N) if j != i and dot(roots[i], roots[j]) == 0}
+                 for i in range(N)]
+    frames = []
+    stack = [((), tuple(range(N)))]
+    # Each state is an increasing orthogonal subset; 100000 is a fail-closed cap.
+    for _ in range(100000):
+        if not stack:
+            break
+        frame, candidates = stack.pop()
+        if len(frame) == 7:
+            frames.append(frame)
+            continue
+        for offset, j in enumerate(candidates):
+            tail = tuple(k for k in candidates[offset + 1:] if k in adjacency[j])
+            if len(tail) >= 6 - len(frame):
+                stack.append((frame + (j,), tail))
+    else:
+        raise ValueError("frame enumeration exceeded its state cap")
+    require(len(frames) == len(set(frames)) == 135, "135 complete frames")
+    for frame in frames:
+        require(len(frame) == 7 and all(j in adjacency[i] for i, j in
+                itertools.combinations(frame, 2)), "orthogonal frame")
+    return tuple(sorted(frames))
+
+
+def binary_kernel(rows):
+    echelon = {}
+    for row in rows:
+        for pivot in range(N - 1, -1, -1):
+            if row >> pivot & 1:
+                if pivot in echelon:
+                    row ^= echelon[pivot]
+                else:
+                    echelon[pivot] = row
+                    break
+    free = tuple(j for j in range(N) if j not in echelon)
+    basis = []
+    for j in free:
+        vector = 1 << j
+        for pivot in sorted(echelon):
+            if (echelon[pivot] & vector).bit_count() % 2:
+                vector |= 1 << pivot
+        basis.append(vector)
+    require(len(echelon) == 36 and len(free) == DIMENSION, "binary rank 36")
+    validate_basis(rows, basis, free)
+    return tuple(basis), free
+
+
+def validate_basis(rows, basis, free):
+    require(len(basis) == len(free) == DIMENSION, "complete kernel dimension")
+    require(len(set(free)) == DIMENSION, "distinct free coordinates")
+    for index, vector in enumerate(basis):
+        require(0 < vector < 1 << N, "bounded nonzero kernel vector")
+        require(all((vector & row).bit_count() % 2 == 0 for row in rows),
+                "every frame parity vanishes")
+        require(tuple(vector >> j & 1 for j in free) ==
+                tuple(int(k == index) for k in range(DIMENSION)),
+                "identity on free coordinates proves independence")
+
+
+def full_weight_census(basis):
+    word = 0
+    minimum = N
+    visited = 0
+    for index in range(1, 1 << DIMENSION):
+        word ^= basis[(index & -index).bit_length() - 1]
+        weight = word.bit_count()
+        require(weight != 0, "independent basis cannot revisit zero")
+        if weight < minimum:
+            minimum = weight
+        visited += 1
+    require(visited == 134217727, "every nonzero binary kernel vector visited")
+    require(minimum == 12, "binary frame code has minimum weight twelve")
+    return visited, minimum
+
+
+def check_witness(roots, frames):
+    values = tuple(sum(DIAGONAL[i] * root[i] ** 2 for i in range(8))
+                   for root in roots)
+    require(sum(DIAGONAL) == 0, "ambient quadratic has trace zero")
+    require(sum(DIAGONAL[i] * PIVOT[i] ** 2 for i in range(8)) == 0,
+            "pivot diagonal entry vanishes, so restricted trace is zero")
+    require(Counter(values) == {0: 51, 8: 6, -8: 6}, "twelve-line attainer")
+    require(all(sum(values[j] for j in frame) == 0 for frame in frames),
+            "literal rational frame sums vanish")
+    # Odd-parity six-sign rows span all six remaining coordinates. Together
+    # with coordinate +/- pairs and e0-e4, this proves quadratic injectivity.
+    signs = [tuple(root[j] for j in (1, 2, 3, 5, 6, 7))
+             for root in roots if root[0] == 1]
+    require(len(signs) == 32, "all odd-parity sign rows")
+    for i, j in itertools.product(range(6), repeat=2):
+        require(sum(row[i] * row[j] for row in signs) == 32 * int(i == j),
+                "sign-row Gram identity")
+    return values
+
+
+def rejection_controls(roots, rows, basis, free):
+    rejected = 0
+    for j in range(N):
+        try:
+            validate_domain(roots[:j] + roots[j + 1:])
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("incomplete root domain accepted")
+    for j in range(DIMENSION):
+        changed = list(basis)
+        changed[j] ^= 1
+        try:
+            validate_basis(rows, changed, free)
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("non-kernel basis accepted")
+    for changed in (basis[:-1], basis + (basis[0],)):
+        try:
+            validate_basis(rows, changed, free)
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("wrong kernel dimension accepted")
+    require(rejected == 92, "all 92 omission and basis controls executed")
+    return rejected
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--receipt", type=Path, help="write generated receipt outside package")
+    args = parser.parse_args()
+    orbit_size = check_root_transitivity()
+    roots = tuple(root for root in e8_lines() if dot(root, PIVOT) == 0)
+    validate_domain(roots)
+    frames = orthogonal_frames(roots)
+    rows = tuple(sum(1 << j for j in frame) for frame in frames)
+    basis, free = binary_kernel(rows)
+    values = check_witness(roots, frames)
+    controls = rejection_controls(roots, rows, basis, free)
+    visited, minimum = full_weight_census(basis)
+    package = Path(__file__).resolve().parent
+    files = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+    receipt = {
+        "status": "PASS_E7_TRACE_ZERO_SUPPORT", "e7_lines": len(roots),
+        "pivot_orbit": orbit_size,
+        "frames": len(frames), "binary_rank": N - len(basis),
+        "binary_kernel_dimension": len(basis), "nonzero_codewords": visited,
+        "minimum_binary_weight": minimum, "quadratic_support": sum(v != 0 for v in values),
+        "positive_values": sum(v > 0 for v in values),
+        "negative_values": sum(v < 0 for v in values), "rejecting_controls": controls,
+        "python": platform.python_version(),
+        "source_sha256": {name: hashlib.sha256((package / name).read_bytes()).hexdigest()
+                          for name in files},
+    }
+    serialized = json.dumps(receipt, indent=2, sort_keys=True) + "\n"
+    if args.receipt is not None:
+        require(not args.receipt.resolve().is_relative_to(package),
+                "receipt must be outside the source package")
+        args.receipt.write_text(serialized, encoding="utf-8")
+    print(serialized, end="")
+
+
+if __name__ == "__main__":
+    main()