diff --git a/research/rank-one-residual-completion/PROOF.md b/research/rank-one-residual-completion/PROOF.md
new file mode 100644
index 0000000000..3f469834de
--- /dev/null
+++ b/research/rank-one-residual-completion/PROOF.md
@@ -0,0 +1,104 @@
+# Rank-one residual forms at every displacement rank
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof. The new cases have displacement rank
+at least three. Krzysztof Wojt's [PR5097](https://github.com/CrocSwap/integer-mult-bounds/pull/5097)
+provides the lower bound, zero-form construction and rank-two predecessor.
+Nick Petalas's PR5085 provides the residual-form and low-length framework.
+The present step is the dimension-independent rank-one pivot below.
+
+Let V be a finite-dimensional nondegenerate symplectic space over F2, with
+pairing omega. Let h:U -> V be an injective linear map preserving omega on U.
+Set d=h+I, D=d(U), r=dim D, and define
+
+    b(d(u), d(v)) = omega(u, d(v)).
+
+This is well defined. If k is fixed by h, preservation of its pairing with
+u implies omega(k,d(u))=0. Expanding the isometry identity also gives
+
+    b(x,y) + b(y,x) = omega(x,y), for x,y in D.             (1)
+
+Suppose b has rank exactly one. Then the least length ell(h) of a product
+of nonzero-axis symplectic transvections extending h is
+
+    ell(h) = 2r - 1.                                    (2)
+
+Every axis lies in V. No ancillary dimension is adjoined. The extension is
+free outside U. Required fixed spectators must therefore be included in U.
+
+## Lower bound, credited predecessor argument
+
+For any full symplectic extension S, put W=im(S+I). Its residual form B,
+defined by B((S+I)v,w)=omega(v,w), is nonsingular and restricts to b on D.
+Indeed W-perp=ker(S+I); this proves both well-definedness and nonsingularity.
+The left radical of b injects into (W/D)* through B. Thus
+
+    dim W >= r + nullity(b) = 2r-1.
+
+Rank subadditivity applied to a transvection word gives length at least
+rank(S+I)=dim W. This is PR5097's displacement-plus-nullity lower bound,
+restated to make the present proof self-contained.
+
+## One pivot leaves a zero form
+
+A nonzero rank-one bilinear form factors as b(x,y)=lambda(x) mu(y), for
+nonzero binary functionals lambda and mu. There is an a with
+lambda(a)=mu(a)=1. If the functionals coincide, choose any vector on which
+they are one. If they differ, they are independent and the two equations
+are solvable. Therefore b(a,a)=1, and
+
+    b(x,y) = b(x,a) b(a,y).                             (3)
+
+Let T_a(v)=v+omega(v,a)a and h'=T_a h. Equations (1) give
+
+    d'(u) = d(u) + b(a,d(u))a.
+
+The map P:x -> x+b(a,x)a on D has kernel <a> and image
+L=ker b(a,-). Hence dim d'(U)=r-1.
+
+For x,y in L, choose u,v with d(u)=x and d(v)=y. Since P fixes L,
+d'(u)=x and d'(v)=y. The residual form of h' is consequently
+
+    b'(x,y)=omega(u,y)=b(x,y)=0,
+
+where the final equality uses (3) and b(a,y)=0. Thus the new residual form
+is identically zero on all r-1 displacement dimensions. This argument
+uses rank one, without a restriction to a two-dimensional D.
+
+PR5097 proves that a zero residual form of displacement rank s has an
+attaining 2s-turn completion in the original V. Apply it with s=r-1 and
+undo T_a. This yields at most 1+2(r-1)=2r-1 turns. The lower bound proves
+equality. When r=1, h' is already the identity on U.
+
+## Explicit completion of the zero-form remainder
+
+For completeness, the constructor uses the predecessor's general at-most-2s
+reduction. At a current partial isometry let K be its fixed subspace. Pick
+u outside K and set p=h(u)+u. If omega(u,p)=1, the one turn T_p corrects u
+and fixes K. Otherwise solve
+
+    omega(K,a)=0, omega(u,a)=1, omega(p,a)=0.
+
+The equations are consistent because u is not in K+<p>. Otherwise either
+u is fixed, or h(u) is a member k of K with h(k)=k, contrary to injectivity.
+Nondegeneracy represents this consistent functional by a in V.
+The two nonzero orthogonal axes a and a+p give an involution correcting u
+and fixing K. The new displacement rank decreases by at least one.
+After at most s reductions the map is fixed on U. Reversing the correction
+word gives its extension. On a zero-form input the lower bound 2s forces
+this at-most-2s construction to attain exactly 2s.
+
+## Interface and limits
+
+The new theorem optimizes unsigned binary symplectic transvection count.
+Under PR5085/PR5051's compatible signed-Pauli contract and free arbitrary
+Pauli-correction tariff, the same minimum applies to the projective signed
+lift. That is a cited interface implication, not a new phase implementation.
+Absolute target phase needs an amplitude anchor. Every monomial pass and
+native Gaussian service still needs pricing by an actual physical caller.
+
+No improvement to native paid rank, recursive children, a complete supplier
+invoice or kappa follows from (2) alone. Arbitrary higher-rank residual forms
+remain open here. Finite checks corroborate the written proof; they do not
+constitute independent human review or formal proof-kernel verification.
diff --git a/research/rank-one-residual-completion/README.md b/research/rank-one-residual-completion/README.md
new file mode 100644
index 0000000000..7fec03abce
--- /dev/null
+++ b/research/rank-one-residual-completion/README.md
@@ -0,0 +1,130 @@
+# Exact all-rank completion for a rank-one residual form
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with exact finite corroboration. For an
+injective binary symplectic partial map h:U -> V, let D=(h+I)U, r=dim D,
+and let b((h+I)u,(h+I)v)=omega(u,(h+I)v). If rank b=1, then
+
+    minimum transvection length = 2r-1.
+
+The new cases have r at least three. Krzysztof Wojt's
+[PR5097](https://github.com/CrocSwap/integer-mult-bounds/pull/5097) proves
+the lower bound r+nullity(b), the zero-form optimum 2r, and the rank-two
+rank-one case. Its Open next question 1 asks about higher-rank nonzero forms.
+This contribution supplies the attaining word for the rank-one slice at
+every r. At r=3 it closes the interval [5,6] at five. It does not classify
+other residual ranks or improve kappa.
+
+[PROOF.md](PROOF.md) shows that one anisotropic pivot leaves a zero residual
+form on r-1 displacement dimensions. The predecessor's two-turn reduction
+then finishes the word. [completion.py](completion.py) implements that
+construction locally. It validates independence, injectivity and preservation
+of pairings, and rejects residual forms whose rank differs from one.
+
+All axes lie in the original V. The action outside U is free. Required fixed
+spectators must be prescribed in U, and the implementation preserves them.
+Under the cited signed-Pauli contract, compatible sign corrections are free
+in this formal tariff. Absolute phase and physical costs are separate.
+
+## Exact evidence and reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rank-one-residual-completion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rank-one-residual-completion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rank-one-residual-completion
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rank-one-residual-completion --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. The standalone marker
+is `PASS_RANK_ONE_RESIDUAL_COMPLETION`; the launcher must also print
+`PASS_REGISTERED_RESEARCH_PACKAGE`. Receipts are generated on stdout and bind
+every regular package file by SHA256. No receipt is hand-written or stored in
+the checkout. The standalone commands are read-only and require no Git or
+external source inputs.
+
+The finite checks cover exactly:
+
+- Every nonzero rank-one binary form in dimensions 3, 4 and 5, represented
+  uniquely as p q-transpose for nonzero p,q. There are 1,235 forms. Each has
+  a literal symplectic realization and two prescribed fixed spectators.
+- All 242 of those forms with zero diagonal, where a sum of basis vectors
+  rather than a basis vector must supply the anisotropic pivot.
+- 52 larger or conjugated fixtures, through displacement rank 12, including
+  a rank-three contract in the original six-dimensional ambient space.
+- Independent dense-coordinate evaluation of every emitted full matrix,
+  every prescribed image, all symplectic pairings and full displacement rank
+  exactly 2r-1. The checker uses dense row elimination rather than the
+  constructor's packed binary elimination.
+- 182 rejecting one-turn omissions, plus malformed/out-of-scope contracts
+  and an inconsistent pairing system. The generated receipt gives the
+  control count.
+
+These are finite corroborations of the written dimension-uniform proof.
+They do not enumerate all partial maps in the tested dimensions. No
+predecessor scientific executable, receipt, census or compiler is replayed.
+
+## Scope and provenance
+
+Base: canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority
+revision 8, selected PR6030. [TASK.json](TASK.json) records the explicit change
+from the formal-interface-lemma card to this written interface side result.
+[SOURCES.json](SOURCES.json) pins the problem statements as provenance only.
+The selected source-binding orientation command passed. The advance
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363481)
+and scoped overlap checks precede the construction.
+
+The turn count is an abstract tariff. It is not native Gaussian rank, paid
+recursive rank, a favorable supplier invoice, physical tape cost or a new
+multiplication theorem. A compatible signed lift with charged monomial
+passes, phase anchor, actual caller, dirty-owner restoration, precision,
+stock and compiler/outer admission remains to be supplied. The selected
+frontier and five retained assumptions are unchanged. Selected cold replay,
+Lean and Docker were not run. Independent human and formal proof-kernel
+review are unclaimed. CI results belong in the PR body.
+
+## Implementation bounds
+
+The public `complete` entry point accepts at most 16 qubits, hence at most
+32 basis vectors and 32-bit ambient vectors. Every elimination loop is bounded
+by these dimensions. A correction has at most 2r-1 turns and each step
+strictly decreases displacement rank. Helpers operate on validated internal
+data. The mathematical theorem has no dimension cap.
+
+Power of Ten rule 3 has a managed-runtime deviation in `completion.py` and
+`verify.py`. Python allocates integers and collections during execution.
+The API cap above bounds the live algebraic data; the verifier has fixed
+finite census bounds and does not accumulate per-case matrices. Verification
+checks the accepted cap and rejects a dimension above it. A fixed-capacity
+native implementation would be needed before a steady-allocation claim.
+Rule 10 uses warning-strict normal/optimized replay and source compilation;
+availability of additional static diagnostics is recorded in the PR body.
+No function exceeds 60 physical lines. There is no recursion, dynamic code
+generation, network access or subprocess execution in either scientific file.
+The verifier loads the named local completion module through the standard
+import loader; that is its sole dynamic dispatch boundary.
+
+## Open next questions
+
+- Determine an attaining formula for residual rank two at displacement rank
+  at least three. First examine the residual form after an anisotropic pivot;
+  a nonzero alternating remainder is an unresolved obstruction here.
+- Price one actual signed native contact satisfying this partial contract.
+  Include fixed spectators and an absolute phase anchor, then charge every
+  turn, Pauli correction, monomial pass and owner/restoration operation.
+  A shorter formal word alone gives no recursive saving.
+
+## Credit
+
+Krzysztof Wojt / krzysztofwojt / PR5097 supplies the explicit higher-rank
+question, displacement-plus-nullity lower bound, zero-form construction and
+rank-two pivot proof. Nick Petalas / PR5085 supplies the residual form and
+low-length cutoff. Brian / JoyboyBrian / PR5051 supplies signed compatibility;
+David Ganz / Dugongue / PR4841 supplies native compiler context. Cao Yifan /
+intqwq, Cinna Davis, zxv, Jacob Alan Sussman and the retained native/compiler
+lineage retain their predecessor credit. Symplectic transvections, residual
+forms and binary elimination are classical. No literature-priority claim is
+made. The new step is the all-rank rank-one attainment proof and its local
+constructor; predecessor files and credit lines are unchanged.
diff --git a/research/rank-one-residual-completion/SOURCES.json b/research/rank-one-residual-completion/SOURCES.json
new file mode 100644
index 0000000000..fdb163ca2c
--- /dev/null
+++ b/research/rank-one-residual-completion/SOURCES.json
@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/singular-rank-two-pauli/README.md",
+      "usage": "provenance",
+      "git_blob": "340e9004be1cbc28917adac5db6dfa8950c00dc5",
+      "sha256": "2be2b460c1ce24261e3f887cb583163e86233217a6ccaa61c9a6a8b8d1ec7cb0"
+    },
+    {
+      "path": "research/singular-rank-two-pauli/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c8ffbe676f33e14105c188959e47d8aafeaaae3e",
+      "sha256": "bc43da28cf432e370532cdeb1622ce8efb175d497fe83b632d8560fd27c20a5b"
+    },
+    {
+      "path": "research/partial-pauli-two-transvection/README.md",
+      "usage": "provenance",
+      "git_blob": "fa6116dfce698f9e51ed910d974c9707028ca3e6",
+      "sha256": "06b3084c46bea30e06519385258a355c4b6d9b622281e1fda9a5b794b233a2c5"
+    },
+    {
+      "path": "research/signed-pauli-partial-extension/README.md",
+      "usage": "provenance",
+      "git_blob": "b7f3c12b91656ce3ee1c1753a2799fd1861345a9",
+      "sha256": "8bde3fc092ef164f974d63350df97b95bcab3d490d71bc3d9100baaaf9693666"
+    }
+  ],
+  "credit": "PR5097 poses the higher-rank question and supplies the lower bound and zero-form construction; PR5085 and PR5051 supply residual and signed-contract context. No predecessor scientific replay is a deliverable."
+}
diff --git a/research/rank-one-residual-completion/TASK.json b/research/rank-one-residual-completion/TASK.json
new file mode 100644
index 0000000000..ae914dc30d
--- /dev/null
+++ b/research/rank-one-residual-completion/TASK.json
@@ -0,0 +1,107 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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 minimum 2r-1 for every binary symplectic partial map with displacement rank r and residual-form rank one; new cases r>=3.",
+  "scope_change_reason": "A written algebraic interface side result answering the rank-one slice of PR5097 Open next question 1, rather than a proof-assistant discharge of a selected assumption.",
+  "bottleneck_link": "Short partial native-contact completions can reduce a future physical word, but turn count alone does not establish a favorable full signed invoice.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified all-rank rank-one extension; do not extend to other residual ranks or a native caller.",
+  "outcome": "completed",
+  "evidence": "Written proof; 1235 rank-one forms at r=3,4,5; 52 larger/conjugated fixtures through r=12; literal full matrix and fixed-spectator checks; 182 rejecting omissions; generated hash-bound stdout receipts.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Determine exact attainment for residual rank two at displacement rank at least three.",
+      "why_it_matters": "This is a further slice of PR5097 higher-rank completion, outside the proved rank-one case.",
+      "first_step": "Analyze the residual form after an anisotropic diagonal pivot and isolate a nonzero alternating remainder.",
+      "blocked_by": "No general attainment or normal-form argument is supplied here."
+    },
+    {
+      "question": "Can an actual signed native contact use this shorter word at a favorable complete cost?",
+      "why_it_matters": "Formal turn count is separate from paid native and recursive rank.",
+      "first_step": "Specify an actual partial signed contract, fixed spectators and phase anchor, then charge the complete emitted word.",
+      "blocked_by": "No physical caller, native invoice, owner/restoration or precision contract is supplied."
+    }
+  ],
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363481",
+  "upstream_checkpoint": {
+    "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "priority_revision": 8,
+    "checked_at": "2026-11-03T00:47:29Z"
+  }
+}
diff --git a/research/rank-one-residual-completion/VERIFY.json b/research/rank-one-residual-completion/VERIFY.json
new file mode 100644
index 0000000000..05472d812e
--- /dev/null
+++ b/research/rank-one-residual-completion/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "New all-rank rank-one completion: exhaustive forms r=3,4,5; literal matrices, fixed spectators, larger conjugates and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "New all-rank rank-one completion: exhaustive forms r=3,4,5; literal matrices, fixed spectators, larger conjugates and rejection controls."
+    }
+  ]
+}
diff --git a/research/rank-one-residual-completion/completion.py b/research/rank-one-residual-completion/completion.py
new file mode 100644
index 0000000000..9ea8891f50
--- /dev/null
+++ b/research/rank-one-residual-completion/completion.py
@@ -0,0 +1,166 @@
+"""Exact rank-one-residual completion in the original binary symplectic space.
+
+Produced by Nick Petalas. Apache-2.0.
+The reduction and lower bound build on Krzysztof Wojt, PR5097.
+Vectors store e coordinates below f coordinates. No signed/phase API is implied.
+"""
+
+MAX_QUBITS = 16
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def pairing(x: int, y: int, n: int) -> int:
+    mask = (1 << n) - 1
+    return (((x & mask) & (y >> n)).bit_count()
+            ^ ((y & mask) & (x >> n)).bit_count()) & 1
+
+
+def turn(x: int, axis: int, n: int) -> int:
+    return x ^ (axis if pairing(x, axis, n) else 0)
+
+
+def apply_word(x: int, word: tuple[int, ...], n: int) -> int:
+    for axis in word:
+        x = turn(x, axis, n)
+    return x
+
+
+def linear_combination(rows: tuple[int, ...], coefficients: int) -> int:
+    result = 0
+    for i, row in enumerate(rows):
+        if (coefficients >> i) & 1:
+            result ^= row
+    return result
+
+
+def elimination(rows: tuple[int, ...]) -> tuple[tuple[int, ...], tuple[int, ...]]:
+    """Return independent input indices and a basis of coefficient relations."""
+    pivots: dict[int, tuple[int, int]] = {}
+    selected = []
+    relations = []
+    for i, original in enumerate(rows):
+        row, coefficients = original, 1 << i
+        for pivot in sorted(pivots, reverse=True):
+            if (row >> pivot) & 1:
+                other, relation = pivots[pivot]
+                row ^= other
+                coefficients ^= relation
+        if row:
+            pivots[row.bit_length() - 1] = (row, coefficients)
+            selected.append(i)
+        else:
+            relations.append(coefficients)
+    return tuple(selected), tuple(relations)
+
+
+def validate(n: int, source: tuple[int, ...], image: tuple[int, ...]) -> None:
+    require(type(n) is int and 1 <= n <= MAX_QUBITS, "unsupported dimension")
+    require(type(source) is tuple and type(image) is tuple, "use immutable tuples")
+    require(len(source) == len(image) <= 2 * n, "source/image lengths")
+    limit = 1 << (2 * n)
+    require(all(type(v) is int and 0 <= v < limit for v in source + image),
+            "binary vector outside ambient space")
+    require(len(elimination(source)[0]) == len(source), "dependent source basis")
+    require(len(elimination(image)[0]) == len(image), "noninjective image")
+    for i, x in enumerate(source):
+        for j, y in enumerate(source):
+            require(pairing(x, y, n) == pairing(image[i], image[j], n),
+                    "partial map does not preserve pairings")
+
+
+def residual(n: int, source: tuple[int, ...], image: tuple[int, ...]
+             ) -> tuple[tuple[int, ...], tuple[int, ...], tuple[int, ...]]:
+    displacement = tuple(x ^ y for x, y in zip(source, image))
+    indices, _ = elimination(displacement)
+    basis = tuple(displacement[i] for i in indices)
+    lifts = tuple(source[i] for i in indices)
+    rows = tuple(sum(pairing(u, d, n) << j for j, d in enumerate(basis))
+                 for u in lifts)
+    return basis, lifts, rows
+
+
+def solve_pairings(n: int, constraints: tuple[tuple[int, int], ...]) -> int:
+    pivots: dict[int, tuple[int, int]] = {}
+    mask = (1 << n) - 1
+    for vector, value in constraints:
+        row = ((vector & mask) << n) | (vector >> n)
+        for pivot in sorted(pivots, reverse=True):
+            if (row >> pivot) & 1:
+                other, rhs = pivots[pivot]
+                row ^= other
+                value ^= rhs
+        if row:
+            pivots[row.bit_length() - 1] = (row, value)
+        else:
+            require(value == 0, "inconsistent pairing equations")
+    result = 0
+    for pivot in sorted(pivots):
+        row, rhs = pivots[pivot]
+        if rhs ^ ((row & result).bit_count() & 1):
+            result |= 1 << pivot
+    require(all(pairing(vector, result, n) == value
+                for vector, value in constraints), "pairing solution failed")
+    return result
+
+
+def upper_correction(n: int, source: tuple[int, ...], image: tuple[int, ...]
+                     ) -> tuple[int, ...]:
+    """PR5097's at-most-two-per-displacement reduction, implemented locally."""
+    correction = []
+    initial_rank = len(residual(n, source, image)[0])
+    for _ in range(initial_rank):
+        displacement = tuple(x ^ y for x, y in zip(source, image))
+        indices, relations = elimination(displacement)
+        if not indices:
+            break
+        i = indices[0]
+        u, p = source[i], displacement[i]
+        if pairing(u, p, n):
+            axes = (p,)
+        else:
+            fixed = tuple(linear_combination(source, relation) for relation in relations)
+            constraints = tuple((k, 0) for k in fixed) + ((u, 1), (p, 0))
+            a = solve_pairings(n, constraints)
+            axes = (a, a ^ p)
+        require(all(axes), "zero correction axis")
+        image = tuple(apply_word(y, axes, n) for y in image)
+        require(len(residual(n, source, image)[0]) < len(indices),
+                "correction did not decrease displacement rank")
+        correction.extend(axes)
+    require(image == source, "upper correction did not finish")
+    return tuple(correction)
+
+
+def complete(n: int, source: tuple[int, ...], image: tuple[int, ...]
+             ) -> tuple[int, ...]:
+    """Attain the exact 2r-1 minimum, rejecting other residual-form ranks."""
+    validate(n, source, image)
+    basis, _, rows = residual(n, source, image)
+    r = len(basis)
+    require(len(elimination(rows)[0]) == 1, "residual form must have rank one")
+    candidates = tuple(1 << i for i in range(r)) + tuple(
+        (1 << i) | (1 << j) for i in range(r) for j in range(i))
+    axis = None
+    for coefficients in candidates:
+        value = 0
+        for i, row in enumerate(rows):
+            if (coefficients >> i) & 1:
+                value ^= (row & coefficients).bit_count() & 1
+        if value:
+            axis = linear_combination(basis, coefficients)
+            break
+    require(axis is not None and axis != 0, "missing anisotropic pivot")
+    reduced = tuple(turn(y, axis, n) for y in image)
+    reduced_basis, _, reduced_rows = residual(n, source, reduced)
+    require(len(reduced_basis) == r - 1 and not any(reduced_rows),
+            "rank-one pivot did not leave a zero form")
+    correction = (axis,) + upper_correction(n, source, reduced)
+    word = tuple(reversed(correction))
+    require(len(word) == 2 * r - 1, "word length does not attain the lower bound")
+    require(tuple(apply_word(x, word, n) for x in source) == image,
+            "completion does not realize the partial contract")
+    return word
diff --git a/research/rank-one-residual-completion/verify.py b/research/rank-one-residual-completion/verify.py
new file mode 100644
index 0000000000..7da679bbd8
--- /dev/null
+++ b/research/rank-one-residual-completion/verify.py
@@ -0,0 +1,231 @@
+"""Finite corroboration of the new r>=3 rank-one-residual theorem.
+
+Produced by Nick Petalas. Apache-2.0. Standard library only.
+No predecessor executable or scientific receipt is imported or replayed.
+"""
+
+import hashlib
+import importlib.util
+import json
+from pathlib import Path
+
+
+PACKAGE = Path(__file__).resolve().parent
+SPEC = importlib.util.spec_from_file_location("rank_one_completion", PACKAGE / "completion.py")
+if SPEC is None or SPEC.loader is None:
+    raise RuntimeError("cannot load local completion module")
+C = importlib.util.module_from_spec(SPEC)
+SPEC.loader.exec_module(C)
+
+
+def check(condition: bool, message: str) -> None:
+    if not condition:
+        raise RuntimeError(message)
+
+
+def coordinates(x: int, dimension: int) -> list[int]:
+    return [(x >> j) & 1 for j in range(dimension)]
+
+
+def dense_pair(x: list[int], y: list[int], n: int) -> int:
+    return sum(x[j] * y[n + j] + x[n + j] * y[j] for j in range(n)) % 2
+
+
+def dense_word(n: int, word: tuple[int, ...]) -> list[list[int]]:
+    columns = [coordinates(1 << j, 2 * n) for j in range(2 * n)]
+    for axis in word:
+        a = coordinates(axis, 2 * n)
+        for column in columns:
+            if dense_pair(column, a, n):
+                for j in range(2 * n):
+                    column[j] ^= a[j]
+    return columns
+
+
+def dense_apply(columns: list[list[int]], x: int) -> int:
+    dimension = len(columns)
+    bits = coordinates(x, dimension)
+    return sum((sum(bits[i] * columns[i][j] for i in range(dimension)) % 2) << j
+               for j in range(dimension))
+
+
+def dense_rank(matrix: list[list[int]]) -> int:
+    rows = [row[:] for row in matrix]
+    if not rows:
+        return 0
+    height, width, pivot_row = len(rows), len(rows[0]), 0
+    for j in range(width):
+        found = next((i for i in range(pivot_row, height) if rows[i][j]), None)
+        if found is None:
+            continue
+        rows[pivot_row], rows[found] = rows[found], rows[pivot_row]
+        for i in range(pivot_row + 1, height):
+            if rows[i][j]:
+                rows[i] = [a ^ b for a, b in zip(rows[i], rows[pivot_row])]
+        pivot_row += 1
+        if pivot_row == height:
+            break
+    return pivot_row
+
+
+def fixture(rows: tuple[int, ...]) -> tuple[int, tuple[int, ...], tuple[int, ...]]:
+    """Realize any r-square residual matrix, with two prescribed spectators."""
+    r = len(rows)
+    n = 2 * r + 1
+    source = tuple(1 << i for i in range(r))
+    displacement = []
+    for j in range(r):
+        first_f = sum(((rows[i] >> j) & 1) << (n + i) for i in range(r))
+        second_f = sum(((rows[i] >> j) & 1) << (n + r + i) for i in range(r))
+        displacement.append((1 << (r + j)) ^ first_f ^ second_f)
+    image = tuple(x ^ d for x, d in zip(source, displacement))
+    fixed = (1 << (2 * r), 1 << (n + 2 * r))
+    return n, source + fixed, image + fixed
+
+
+def compact_fixture(r: int, spectators: bool = True
+                    ) -> tuple[int, tuple[int, ...], tuple[int, ...]]:
+    """Use x^(r-1)+x+1 to avoid eigenvalues zero and one on the e block."""
+    k = r - 1
+    n = r + int(spectators)
+    source = tuple(1 << i for i in range(k)) + (1 << (n + k),)
+    columns = tuple(1 << (i + 1) for i in range(k - 1)) + (3,)
+    image = tuple((1 << i) ^ columns[i] for i in range(k))
+    image += ((1 << (n + k)) ^ (1 << k),)
+    if spectators:
+        fixed = (1 << r, 1 << (n + r))
+        source, image = source + fixed, image + fixed
+    return n, source, image
+
+
+def check_case(n: int, source: tuple[int, ...], image: tuple[int, ...], r: int
+               ) -> tuple[int, ...]:
+    word = C.complete(n, source, image)
+    check(len(word) == 2 * r - 1, "wrong exact length")
+    check(all(0 < a < 1 << (2 * n) for a in word), "axis left original space")
+    columns = dense_word(n, word)
+    check(tuple(dense_apply(columns, x) for x in source) == image,
+          "literal dense word failed prescribed map or fixed spectators")
+    for i, x in enumerate(columns):
+        for j, y in enumerate(columns):
+            expected = int((i < n and j == i + n) or (j < n and i == j + n))
+            check(dense_pair(x, y, n) == expected, "full word is not symplectic")
+    delta = [[value ^ int(i == j) for j, value in enumerate(column)]
+             for i, column in enumerate(columns)]
+    check(dense_rank(delta) == 2 * r - 1, "full displacement does not attain bound")
+    check(dense_rank([coordinates(x ^ y, 2 * n) for x, y in zip(source, image)]) == r,
+          "fixture has wrong displacement rank")
+    return word
+
+
+def exhaustive_forms() -> tuple[int, int, int]:
+    cases = 0
+    off_diagonal = 0
+    omissions = 0
+    for r in range(3, 6):
+        for p in range(1, 1 << r):
+            for q in range(1, 1 << r):
+                rows = tuple(q if (p >> i) & 1 else 0 for i in range(r))
+                n, source, image = fixture(rows)
+                word = check_case(n, source, image, r)
+                cases += 1
+                if not p & q:
+                    off_diagonal += 1
+                if p == 1 and q in (1, 2):
+                    for j in range(len(word)):
+                        shorter = word[:j] + word[j + 1:]
+                        columns = dense_word(n, shorter)
+                        check(tuple(dense_apply(columns, x) for x in source) != image,
+                              "a one-turn omission still realizes the contract")
+                        omissions += 1
+    return cases, off_diagonal, omissions
+
+
+def larger_cases() -> tuple[int, int]:
+    cases = 0
+    omissions = 0
+    for r in range(3, 13):
+        n, source, image = compact_fixture(r)
+        for seed in range(5):
+            limit = (1 << (2 * n)) - 1
+            axes = tuple(((seed + 1) * (j + 3) * 7919) % limit + 1
+                         for j in range(8)) if seed else ()
+            change = dense_word(n, axes)
+            moved_source = tuple(dense_apply(change, x) for x in source)
+            moved_image = tuple(dense_apply(change, y) for y in image)
+            word = check_case(n, moved_source, moved_image, r)
+            cases += 1
+            if seed == 1:
+                for j in range(len(word)):
+                    columns = dense_word(n, word[:j] + word[j + 1:])
+                    check(tuple(dense_apply(columns, x) for x in moved_source) != moved_image,
+                          "a conjugated one-turn omission still realizes the contract")
+                    omissions += 1
+    # A rank-three example already fits the six-dimensional original space.
+    n, source, image = compact_fixture(3, spectators=False)
+    check_case(n, source, image, 3)
+    # Exercise the public dimension cap while keeping displacement rank three.
+    n, source, image = compact_fixture(3)
+    cap = C.MAX_QUBITS
+    mask = (1 << n) - 1
+    cap_source = tuple((x & mask) | ((x >> n) << cap) for x in source)
+    cap_image = tuple((x & mask) | ((x >> n) << cap) for x in image)
+    check_case(cap, cap_source, cap_image, 3)
+    return cases + 2, omissions
+
+
+def rejecting_controls() -> int:
+    n, source, image = compact_fixture(3)
+    invalid = [
+        (0, source, image),
+        (C.MAX_QUBITS + 1, source, image),
+        (True, source, image),
+        (n, list(source), image),
+        (n, source, image[:-1]),
+        (n, (True,) + source[1:], image),
+        (n, ((1 << (2 * n)),) + source[1:], image),
+        (n, source + (source[0],), image + (image[0],)),
+        (n, source, (0,) + image[1:]),
+        (n, source, (image[0] ^ (1 << (n + 1)),) + image[1:]),
+        (n, source, source),
+        fixture((1, 2, 0)),
+        fixture((2, 1, 0)),
+    ]
+    for args in invalid:
+        try:
+            C.complete(*args)
+        except ValueError:
+            continue
+        raise RuntimeError("malformed or out-of-scope contract was accepted")
+    try:
+        C.solve_pairings(1, ((1, 0), (1, 1)))
+    except ValueError:
+        return len(invalid) + 1
+    raise RuntimeError("inconsistent pairing system was accepted")
+
+
+def main() -> None:
+    forms, off_diagonal, form_omissions = exhaustive_forms()
+    larger, large_omissions = larger_cases()
+    rejected = rejecting_controls()
+    check(forms == sum(((1 << r) - 1) ** 2 for r in range(3, 6)),
+          "rank-one form census incomplete")
+    files = sorted(path for path in PACKAGE.iterdir() if path.is_file())
+    receipt = {
+        "status": "PASS_RANK_ONE_RESIDUAL_COMPLETION",
+        "claim_type": "scoped algebraic proof with finite corroboration",
+        "new_displacement_ranks": "3 through 12 in finite checks; all r in written proof",
+        "exhaustive_rank_one_forms_r3_r4_r5": forms,
+        "zero_diagonal_forms_requiring_sum_pivot": off_diagonal,
+        "larger_and_conjugated_contracts": larger,
+        "rejected_one_turn_omissions": form_omissions + large_omissions,
+        "rejecting_controls": rejected,
+        "source_sha256": {path.name: hashlib.sha256(path.read_bytes()).hexdigest()
+                          for path in files},
+        "no_new_kappa": True,
+    }
+    print(json.dumps(receipt, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()