diff --git a/research/rank-three-closed-completion/PROOF.md b/research/rank-three-closed-completion/PROOF.md
new file mode 100644
index 0000000000..646cc7c530
--- /dev/null
+++ b/research/rank-three-closed-completion/PROOF.md
@@ -0,0 +1,119 @@
+# Exact rank-three alternating completion criterion
+
+This proof and its finite corroboration were produced by Nick Petalas.
+Apache-2.0.
+
+## Statement and credited inputs
+
+Let V be a finite nondegenerate symplectic vector space over F2 with pairing
+w. Let h:U -> V be an injective linear isometry. Write d=h+I,
+K=ker d, D=d(U), and
+
+    b(d(u),d(v)) = w(u,d(v)).
+
+Assume dim D=3 and b is alternating of rank two. Its radical R has
+dimension one. Set U_R=d^-1(R), a subspace of U. All sums and inverse
+images refer to the given V. Spectators required to remain fixed belong
+to U with h(v)=v. Let L(h) be the minimum number of nonzero-axis
+transvections in a symplectic extension of h in V.
+
+**Theorem.** If U_R is contained in K+D, then L(h)=5. Otherwise L(h)=4.
+Moreover, every four-turn extension in this setting has four linearly
+independent, pairwise orthogonal axes.
+
+The new result is the closed-case lower bound and the necessary commuting
+structure. Ali Romman's [#6525](https://github.com/CrocSwap/integer-mult-bounds/pull/6525)
+already proves 4<=L(h)<=5 and constructs four turns when U_R is not
+contained in K+D. Those constructive upper bounds are used as premises;
+they are not reconstructed or audited here. Its r=3 five-turn fixture
+was already known. The new theorem treats every such contract in every
+ambient dimension, rather than just that fixture. Its r>=4 closed case
+remains open and can attain the lower endpoint.
+
+Krzysztof Wojt's #5097 supplies the general displacement-plus-nullity
+bound. Nick Petalas's #5085/#6494, Brian / JoyboyBrian's #5051 and the
+native/compiler lineage retained in #6525 supply the earlier problem
+and constructions. The following lower-bound argument is self-contained.
+Wall forms and binary quadratic forms are classical mathematics; no
+literature-priority claim is made.
+
+## 1. Full displacement and its form
+
+For any symplectic extension S of h, put W=im(S+I). Symplecticity gives
+
+    ker(S+I) = W-perp.
+
+For example, w(v,(S+I)x)=w((S^-1+I)v,x), so orthogonality to W is
+equivalent to S(v)=v. Thus the form
+
+    B((S+I)v,z) = w(v,z),     z in W,
+
+is well-defined and nonsingular. If its left radical contained (S+I)v,
+then v would be in W-perp and its displacement would vanish. Also
+
+    B(x,y)+B(y,x)=w(x,y),     B restricted to D equals b.       (1)
+
+The first identity follows by expanding w(Sv,Su)=w(v,u); the second
+follows from S|U=h. Since b is singular and D has dimension three,
+W cannot equal D. Hence dim W>=4.
+
+A product of t transvections has displacement image contained in the
+span of its t axes. Therefore L(h)>=4. If four turns extend h, their
+axes a1,...,a4 are independent and W is exactly their span.
+
+In execution order, write the intermediate update at turn i as c_i a_i.
+For input v the coefficients obey
+
+    c_i = w(v,a_i) + sum_(j<i) c_j w(a_j,a_i).
+
+The coefficient transformation is triangular with diagonal one. Since
+the axes are independent and V is nondegenerate, the four functionals
+w(-,a_i) are independent, so these coefficients range over F2^4.
+Consequently the matrix of B in the axis basis is upper triangular with
+diagonal one. In particular, the quadratic form q(x)=B(x,x) satisfies
+
+    q(a_i)=1 for every i,     q|D=0,     polar(q)=w|W.          (2)
+
+Thus the vectors with q=1 span W.
+
+## 2. A four-dimensional quadratic obstruction
+
+Let q be a quadratic form on a four-dimensional binary space W, vanishing
+on a three-dimensional subspace D. Suppose its polar form p is nonzero.
+Since D is isotropic of codimension one, p has rank two. Its radical Z
+has dimension two and lies in D. In particular q|Z=0.
+
+The form descends to W/Z, a nondegenerate two-dimensional quadratic
+space. D/Z is a nonzero singular line, so this is the split plane. In
+a suitable basis its form is xy. Over F2 it has exactly one vector
+with value one. Therefore {x:q(x)=1} is one coset of Z in W and spans
+only a three-dimensional subspace. It cannot span W.
+
+Apply this to (2). The anisotropic vectors do span W, so p=0. By (1),
+W is totally isotropic. In particular the four axes commute. This proves
+the extra assertion without assuming any special source coordinates.
+
+## 3. Closed radical lifts contradict four turns
+
+Let 0!=z in R. If U_R is contained in K+D, choose a lift u in U with
+d(u)=z and write u=k+x with k in K and x in D. The extension fixes k.
+Total isotropy gives W contained in W-perp=ker(S+I), and x is in D
+contained in W. Hence S fixes x as well. It fixes u, contradicting
+(S+I)u=d(u)=z!=0.
+
+No four-turn extension exists in the closed case. Together with the
+credited upper bound five this gives L(h)=5. In the escaping case the
+credited four-turn construction attains the lower bound from section 1.
+
+## Scope
+
+This is an unsigned binary label-word theorem with fixed prescribed
+spectators and no ambient enlargement. It does not price Gaussian rank,
+sign or absolute-phase corrections, physical routing, owner cleanup,
+precision, stock, tape, compiler closure or outer recursion. The five
+selected assumptions remain. It supplies no multiplier or new kappa.
+Independent human and formal proof-kernel acceptance are unclaimed.
+
+The verifier checks the new quadratic obstruction and all independent
+four-turn Gram topologies by exact finite arithmetic. It does not certify
+the written arbitrary-dimension proof or replay the credited upper bounds.
diff --git a/research/rank-three-closed-completion/README.md b/research/rank-three-closed-completion/README.md
new file mode 100644
index 0000000000..ab7c7414d8
--- /dev/null
+++ b/research/rank-three-closed-completion/README.md
@@ -0,0 +1,123 @@
+# Exact rank-three alternating completion criterion
+
+Scoped written proof with exact finite corroboration, produced by Nick Petalas.
+
+For a partial binary symplectic isometry h:U -> V, put d=h+I, K=ker d,
+D=d(U), and b(d(u),d(v))=w(u,d(v)). Suppose dim D=3 and b is alternating
+of rank two. Set R=rad b and U_R=d^-1(R). Then the exact unsigned
+transvection minimum in the original ambient space is
+
+    L(h) = 5 if U_R is contained in K+D, and 4 otherwise.
+
+Every four-turn extension necessarily has independent, commuting axes.
+The new [proof](PROOF.md) excludes four turns for every closed contract,
+in every ambient dimension. It settles the r=3 portion of Open next
+question 1 in Ali Romman's [#6525](https://github.com/CrocSwap/integer-mult-bounds/pull/6525).
+That source already supplies the general interval [4,5], the escaping-lift
+four-turn construction and one closed five-turn example. Those are credited
+inputs, not new constructions or audit deliverables. No predecessor
+scientific verifier or numerical receipt is replayed.
+
+The proof uses the quadratic form of a hypothetical four-turn completion.
+A totally singular hyperplane in a four-dimensional binary quadratic space
+with nonzero polar form prevents its anisotropic vectors from spanning.
+Four independent turn axes must span and each has quadratic value one.
+Thus their displacement space is totally isotropic. The completion fixes
+that entire image, which contradicts a nonzero closed radical lift.
+
+## Exact finite evidence
+
+[verify.py](verify.py) enumerates the new obstruction's finite coefficient
+model, without rerunning the known five-turn fixture:
+
+- All 1,024 four-dimensional binary quadratic forms and their 15 hyperplanes.
+  There are 240 totally singular form/hyperplane pairs. All 210 with nonzero
+  polar form have polar rank two and anisotropic span dimension three.
+- All 64 ordered independent four-axis Gram topologies, each realized by a
+  literal chronological word on an eight-dimensional symplectic space.
+  All 16,384 input vectors pass displacement and inverse checks; 65,536
+  Wall basis equalities agree with a separate triangular formula.
+- All 960 topology/hyperplane restrictions. Exactly one canonical pair has
+  alternating residual rank two. Its axes commute and all 16 radical lifts
+  escape K+D. This counts coefficient-model pairs, not all partial isometries.
+- The 180 nonalternating rank-two restrictions with closed left-radical lifts
+  show that alternation is essential. All 256 single-turn omissions damage
+  their whole endpoints. A changed Wall diagonal and zero axis reject for
+  their specific intended reasons.
+
+[RESULT.json](RESULT.json) is generated from these enumerations and binds
+six package sources by SHA256. Default replay recomputes and compares it.
+The written proof supplies the arbitrary-dimension conclusion; finite checks
+corroborate it. The credited upper bounds are mathematical premises, not
+independently certified by this verifier.
+
+## Reproduce
+
+CPython 3.12 and its standard library suffice. From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/rank-three-closed-completion/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/rank-three-closed-completion/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rank-three-closed-completion
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rank-three-closed-completion --check-source-history
+```
+
+Both direct modes print `PASS_RANK_THREE_CLOSED_COMPLETION`. Each registered
+command has a 120-second bound. The standalone verifier needs only this
+package, without Git, network or predecessor executables. After a deliberate
+source edit, `verify.py --write-report` regenerates the receipt only after
+all enumerations and controls succeed.
+
+Base e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8,
+selected #7000. The card's selected-binding orientation passed. Live overlap
+and main searches checked the rank-three, closed, alternating and radical-lift
+formulations and the general completion question. The overlap snapshot covered
+558 open PRs, 7,223 Discussion records and all 10,178 tracked top-level package
+notes at that base. Nested diffs and unpublished work remain outside that
+coverage. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542394).
+
+## Limits and implementation bounds
+
+Only the closed-case lower bound and commuting necessity are new. Exact
+attainment uses #6525's cited upper bounds. The theorem is binary and fixes
+displacement rank three. Prescribed fixed spectators belong in U. No ambient
+enlargement, signed Gaussian realization, physical costs, owner cleanup,
+precision, stock, tape, compiler closure or outer admission is supplied.
+The five selected assumptions remain. No new kappa or selected-frontier
+change is claimed. Lean, Docker and the selected cold replay are not run.
+Independent human and formal proof-kernel review are unclaimed.
+
+There is no recursion or unbounded search. The largest outer census has
+1,024 forms; words have four axes, coefficient spaces have 16 elements,
+literal spaces have 256 elements and all nested loops have those fixed
+bounds. Functions fit within 60 lines. Explicit exceptions remain active
+under optimized Python. Managed Python allocations are a documented deviation
+from fixed-allocation execution; live collections have the bounds above.
+Warning-strict normal and optimized execution and source compilation provide
+diagnostics. No static type checker is a declared dependency. Explicit
+`--write-report` is the verifier's only mutation.
+
+## Open next questions
+
+1. Classify the alternating closed case at displacement rank four and above.
+   The quadratic obstruction here no longer applies directly; #6525 already
+   gives a closed r=4 contract attaining six turns. Start with minimal Wall
+   extensions containing a totally singular subspace of codimension two,
+   retaining the prescribed radical-lift action. A complete criterion and
+   constructive attaining words are missing.
+2. Bind a qualifying partial contract to an actual signed native contact.
+   State its source, fixed spectators and phase anchor, then price every
+   turn, sign correction and physical operation. A short unsigned word alone
+   gives no recursive supplier improvement.
+
+## Credit
+
+The new lower-bound proof and verifier were produced by Nick Petalas.
+Ali Romman #6525 supplies the question, interval, escaping construction and
+known fixtures. Krzysztof Wojt #5097 supplies the general lower bound and
+zero-form completion; Nick Petalas #5085/#6494 supplies earlier residual-form
+and rank-one work; Brian / JoyboyBrian #5051 supplies signed partial-contract
+compatibility. Credit also David Ganz / Dugongue #4841, Cao Yifan / intqwq,
+Cinna Davis, zxv, Jacob Alan Sussman and the native/compiler lineage retained
+by those sources. Wall forms and binary quadratic forms are classical;
+no literature-priority claim is made. New work is Apache-2.0.
diff --git a/research/rank-three-closed-completion/RESULT.json b/research/rank-three-closed-completion/RESULT.json
new file mode 100644
index 0000000000..52d7a98c6d
--- /dev/null
+++ b/research/rank-three-closed-completion/RESULT.json
@@ -0,0 +1,46 @@
+{
+  "claim_type": "scoped written proof with exact finite corroboration",
+  "failure_controls": 2,
+  "quadratic_census": {
+    "hyperplanes_per_form": 15,
+    "nonzero_polar_pairs": 210,
+    "quadratic_forms": 1024,
+    "totally_singular_pairs": 240
+  },
+  "schema_version": 1,
+  "source_sha256": {
+    "PROOF.md": "76a9d6940954e1713daa69d51ec7f2cc5bd2832f5609cb287db553552875638b",
+    "README.md": "deedfdd99861da222b810b0d003eeb4e75fd8b6269aa8b564f951afd4fd5bbf7",
+    "SOURCES.json": "24ec60eb76794700e5551259beead67ab40e3195426b162feca7d5be349126d3",
+    "TASK.json": "c6ee382f3088b8c1b2e5d9a0b58781ecfd0ff39a9ee767577a972fc98aa525be",
+    "VERIFY.json": "84376ae6324d6688129491c0b26f779a2cb3c4c7ab3ac692fa5ef6169596be5f",
+    "verify.py": "6b8bf3627a10826a14d8c38fc74f66be1b21970a25d29a9af62bd52339a9d23a"
+  },
+  "word_census": {
+    "counts": {
+      "alternating_rank_two_contracts": 1,
+      "escaping_radical_lifts": 16,
+      "gram_topologies": 64,
+      "hyperplane_restrictions": 960,
+      "literal_input_vectors": 16384,
+      "nonalternating_closed_controls": 180,
+      "omitted_turn_controls": 256,
+      "wall_basis_equalities": 65536
+    },
+    "nonalternating_control": {
+      "axes": [
+        1,
+        18,
+        20,
+        8
+      ],
+      "gram_code": 3,
+      "hyperplane_mask": 6,
+      "restricted_rows": [
+        1,
+        0,
+        4
+      ]
+    }
+  }
+}
diff --git a/research/rank-three-closed-completion/SOURCES.json b/research/rank-three-closed-completion/SOURCES.json
new file mode 100644
index 0000000000..36b824f989
--- /dev/null
+++ b/research/rank-three-closed-completion/SOURCES.json
@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/rank-two-residual-completion/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "5a39770f196692268ba17dfcc4a01cbfe5f7fc40",
+      "sha256": "9e8b66ca71656833e47ea78635bb46f195076fef33cf26cefabac897256dd19f"
+    },
+    {
+      "path": "research/rank-two-residual-completion/README.md",
+      "usage": "provenance",
+      "git_blob": "8008576fd96f1cb925d5ebb990fa2a58a6a75628",
+      "sha256": "b9ff73eb40d38453312a1e5d1f5b0580314173f273bccb355c32019301d7c1af"
+    },
+    {
+      "path": "research/singular-rank-two-pauli/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c8ffbe676f33e14105c188959e47d8aafeaaae3e",
+      "sha256": "bc43da28cf432e370532cdeb1622ce8efb175d497fe83b632d8560fd27c20a5b"
+    }
+  ],
+  "bibliographic_predecessors": [
+    {
+      "pr": 6525,
+      "author": "aliromman",
+      "head": "9797b952ee174f845f682b1a121600416f5c7bd1",
+      "role": "General interval and escaping upper bound; open closed-case question. No predecessor executable replayed."
+    }
+  ]
+}
diff --git a/research/rank-three-closed-completion/TASK.json b/research/rank-three-closed-completion/TASK.json
new file mode 100644
index 0000000000..8d15bde397
--- /dev/null
+++ b/research/rank-three-closed-completion/TASK.json
@@ -0,0 +1,102 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact four-versus-five unsigned transvection criterion for displacement-rank-three binary partial isometries with alternating rank-two residual form.",
+  "scope_change_reason": "Take the r=3 portion of Ali Romman PR6525 Open next question 1 as a written algebraic theorem. No Lean or selected-caller formalization is claimed.",
+  "bottleneck_link": "A partial native-label completion tariff: rules out all four-turn closed completions and identifies necessary commuting axes. Physical signed costs remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified original lower bound, without extending to higher displacement rank or physical supplier construction.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; exact quadratic and independent four-turn Gram-topology census; generated source-hash-bound RESULT.json.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Classify alternating closed contracts at displacement rank four and above.",
+      "why_it_matters": "Determines the remaining one-turn completion gap left by PR6525.",
+      "first_step": "Analyze minimal Wall extensions with a totally singular codimension-two subspace and prescribed radical lifts.",
+      "blocked_by": "The four-dimensional anisotropic-span argument does not extend directly; known closed r=4 examples already attain the lower endpoint."
+    },
+    {
+      "question": "Can an actual signed native contact profit from this exact label criterion?",
+      "why_it_matters": "Unsigned turn count alone does not determine recursive paid rank.",
+      "first_step": "Fix the full source, spectators and phase anchor; price every turn and physical correction.",
+      "blocked_by": "No signed native caller or complete physical invoice is supplied."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542394"
+}
diff --git a/research/rank-three-closed-completion/VERIFY.json b/research/rank-three-closed-completion/VERIFY.json
new file mode 100644
index 0000000000..d0bfc52eb4
--- /dev/null
+++ b/research/rank-three-closed-completion/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": 120,
+      "checks": "Exact quadratic and four-turn Gram census, literal endpoints, hypothesis and corruption controls, source-hash receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Identical exact evidence and explicit failure controls under optimized Python."
+    }
+  ]
+}
diff --git a/research/rank-three-closed-completion/verify.py b/research/rank-three-closed-completion/verify.py
new file mode 100644
index 0000000000..80db47e05a
--- /dev/null
+++ b/research/rank-three-closed-completion/verify.py
@@ -0,0 +1,241 @@
+#!/usr/bin/env python3
+"""Exact finite corroboration of the new rank-three obstruction.
+
+Standard library only. No predecessor executable or receipt is consumed.
+"""
+
+import argparse
+import hashlib
+import json
+from pathlib import Path
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def parity(value):
+    return value.bit_count() & 1
+
+
+def span(basis):
+    require(len(basis) <= 8, "bounded binary basis")
+    values = [0]
+    for vector in basis:
+        values += [old ^ vector for old in values]
+    return frozenset(values)
+
+
+def basis_of(vectors):
+    require(len(vectors) <= 256, "bounded binary vector set")
+    basis = []
+    occupied = {0}
+    for vector in sorted(vectors):
+        if vector not in occupied:
+            require(len(basis) < 8, "binary dimension limit")
+            basis.append(vector)
+            occupied = set(span(basis))
+    return tuple(basis)
+
+
+def rank(vectors):
+    return len(basis_of(vectors))
+
+
+def pairing(left, right):
+    return parity((left & 15) & (right >> 4)) ^ parity((right & 15) & (left >> 4))
+
+
+def word_image(value, axes):
+    require(len(axes) <= 4 and all(0 < a < 256 for a in axes), "word bound")
+    for axis in axes:
+        if pairing(value, axis):
+            value ^= axis
+    return value
+
+
+def combine(coordinates, axes):
+    value = 0
+    for index, axis in enumerate(axes):
+        if coordinates & (1 << index):
+            value ^= axis
+    return value
+
+
+def bilinear(left, right, rows):
+    image = sum(parity(row & right) << i for i, row in enumerate(rows))
+    return parity(image & left)
+
+
+def quadratic_table(code):
+    diagonal = code & 15
+    edges = tuple((i, j) for i in range(4) for j in range(i + 1, 4))
+    table = []
+    for value in range(16):
+        result = parity(value & diagonal)
+        for bit, (i, j) in enumerate(edges):
+            result ^= ((code >> (bit + 4)) & 1) & (value >> i) & (value >> j) & 1
+        table.append(result)
+    return tuple(table)
+
+
+def quadratic_census():
+    totals = {"quadratic_forms": 1024, "hyperplanes_per_form": 15,
+              "totally_singular_pairs": 0, "nonzero_polar_pairs": 0}
+    for code in range(1024):
+        q = quadratic_table(code)
+        polar = tuple(sum((q[(1 << i) ^ (1 << j)] ^ q[1 << i] ^ q[1 << j]) << j
+                          for j in range(4)) for i in range(4))
+        for mask in range(1, 16):
+            plane = tuple(x for x in range(16) if not parity(x & mask))
+            if any(q[x] for x in plane):
+                continue
+            totals["totally_singular_pairs"] += 1
+            if rank(polar):
+                totals["nonzero_polar_pairs"] += 1
+                radical = tuple(x for x in range(16)
+                                 if all(not parity(row & x) for row in polar))
+                anisotropic = tuple(x for x in range(16) if q[x])
+                require(rank(polar) == 2, "nonzero polar rank")
+                require(set(radical) <= set(plane), "radical lies in hyperplane")
+                require(all(not q[x] for x in radical), "quadratic radical vanishes")
+                require(len(anisotropic) == 4 and rank(anisotropic) == 3,
+                        "anisotropic vectors cannot span four dimensions")
+    require(totals["nonzero_polar_pairs"] > 0, "nonvacuous quadratic control")
+    return totals
+
+
+def topology(code):
+    axes = [1 << i for i in range(4)]
+    rows = [1 << i for i in range(4)]
+    bit = 0
+    for i in range(4):
+        for j in range(i + 1, 4):
+            if code & (1 << bit):
+                axes[j] ^= 1 << (i + 4)
+                rows[i] ^= 1 << j
+            bit += 1
+    require(rank(axes) == 4, "independent chronological axes")
+    return tuple(axes), tuple(rows)
+
+
+def literal_wall(axes, rows):
+    images = tuple(word_image(v, axes) for v in range(256))
+    for value in range(256):
+        displacement = images[value] ^ value
+        coordinates = displacement & 15
+        require(combine(coordinates, axes) == displacement, "literal displacement")
+        for i, axis in enumerate(axes):
+            require(bilinear(coordinates, 1 << i, rows) == pairing(value, axis),
+                    "triangular Wall form matches literal chronological word")
+        require(word_image(images[value], tuple(reversed(axes))) == value,
+                "literal inverse")
+    for i in range(8):
+        for j in range(i + 1, 8):
+            require(pairing(images[1 << i], images[1 << j]) == pairing(1 << i, 1 << j),
+                    "whole symplectic endpoint")
+    return images
+
+
+def contract_classification(axes, rows, images, plane):
+    vectors = tuple(combine(x, axes) for x in plane)
+    radical = tuple(x for x in plane
+                     if all(not bilinear(x, y, rows) for y in plane))
+    require(len(radical) == 2, "rank-two restriction has one-dimensional radical")
+    z = combine(next(x for x in radical if x), axes)
+    kernel = tuple(v for v in range(256) if images[v] == v)
+    kernel_plus_d = {k ^ d for k in kernel for d in vectors}
+    lifts = tuple(v for v in range(256) if images[v] ^ v == z)
+    require(len(lifts) > 0, "nonzero radical has a source lift")
+    closed = all(v in kernel_plus_d for v in lifts)
+    return closed, len(lifts)
+
+
+def word_census():
+    totals = {"gram_topologies": 64, "literal_input_vectors": 0,
+              "wall_basis_equalities": 0, "hyperplane_restrictions": 0,
+              "alternating_rank_two_contracts": 0, "escaping_radical_lifts": 0,
+              "nonalternating_closed_controls": 0, "omitted_turn_controls": 0}
+    control = None
+    for code in range(64):
+        axes, rows = topology(code)
+        images = literal_wall(axes, rows)
+        totals["literal_input_vectors"] += 256
+        totals["wall_basis_equalities"] += 256 * 4
+        for omitted in range(4):
+            damaged = axes[:omitted] + axes[omitted + 1:]
+            require(any(word_image(v, damaged) != images[v] for v in range(256)),
+                    "omitting a turn must damage the whole endpoint")
+            totals["omitted_turn_controls"] += 1
+        for mask in range(1, 16):
+            totals["hyperplane_restrictions"] += 1
+            plane = tuple(x for x in range(16) if not parity(mask & x))
+            basis = basis_of(plane)
+            restricted = tuple(sum(bilinear(x, y, rows) << j for j, y in enumerate(basis))
+                               for x in basis)
+            if rank(restricted) != 2:
+                continue
+            closed, lift_count = contract_classification(axes, rows, images, plane)
+            alternating = all(not bilinear(x, x, rows) for x in plane)
+            if alternating:
+                totals["alternating_rank_two_contracts"] += 1
+                require(code == 0 and not closed, "four turns force commuting axes and escape")
+                totals["escaping_radical_lifts"] += lift_count
+            elif closed:
+                totals["nonalternating_closed_controls"] += 1
+                if control is None:
+                    control = {"gram_code": code, "hyperplane_mask": mask,
+                               "axes": list(axes), "restricted_rows": list(restricted)}
+    require(totals["alternating_rank_two_contracts"] == 1, "nonvacuous sharp four-turn case")
+    require(totals["nonalternating_closed_controls"] > 0, "alternation is necessary")
+    return {"counts": totals, "nonalternating_control": control}
+
+
+def failure_controls():
+    axes, rows = topology(0)
+    wrong_rows = (rows[0] ^ 1,) + rows[1:]
+    rejected = 0
+    try:
+        literal_wall(axes, wrong_rows)
+    except ValueError as error:
+        require(str(error) == "triangular Wall form matches literal chronological word",
+                "diagonal mutation rejects for the intended reason")
+        rejected += 1
+    try:
+        word_image(0, (0,))
+    except ValueError as error:
+        require(str(error) == "word bound", "zero axis rejects at the boundary")
+        rejected += 1
+    require(rejected == 2, "both failure controls reject")
+    return rejected
+
+
+def receipt():
+    package = Path(__file__).resolve().parent
+    source_names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json",
+                    "VERIFY.json", "verify.py")
+    hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest()
+              for name in source_names}
+    return {"schema_version": 1,
+            "claim_type": "scoped written proof with exact finite corroboration",
+            "source_sha256": hashes, "quadratic_census": quadratic_census(),
+            "word_census": word_census(), "failure_controls": failure_controls()}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--write-report", action="store_true")
+    args = parser.parse_args()
+    report = receipt()
+    path = Path(__file__).resolve().with_name("RESULT.json")
+    if args.write_report:
+        path.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n")
+    else:
+        require(json.loads(path.read_text()) == report, "receipt differs from exact replay")
+    print(json.dumps(report, sort_keys=True))
+    print("PASS_RANK_THREE_CLOSED_COMPLETION")
+
+
+if __name__ == "__main__":
+    main()