diff --git a/research/symplectic-deficiency-two-spectral/README.md b/research/symplectic-deficiency-two-spectral/README.md
new file mode 100644
index 0000000000..0de39befd9
--- /dev/null
+++ b/research/symplectic-deficiency-two-spectral/README.md
@@ -0,0 +1,266 @@
+# An exact spectral criterion for deficiency-two symplectic spread completion
+
+This contribution was produced by Nick Petalas. Independent human and formal
+proof-kernel review are unclaimed.
+
+## Result and scope
+
+**Claim type: scoped written mathematical proof, with exact finite controls.**
+Let q >= 3 be a prime power, n >= 1, and let S consist of q^n - 1 pairwise
+trivially intersecting Lagrangians in a nondegenerate alternating 2n-dimensional
+F_q-space. A full symplectic spread has q^n + 1 members, so S has deficiency two.
+
+Form the graph Gamma on the uncovered projective points. Join two distinct
+points exactly when their symplectic pairing is nonzero. Let A be its ordinary
+0/1 adjacency matrix and put
+
+$$
+N=\frac{2(q^n-1)}{q-1},\qquad k=q^{n-1},\qquad Q=kI_N+A.
+$$
+
+Then S extends to a full symplectic spread **if and only if det(Q) = 0 over the rationals**.
+Here Q is the integer signless Laplacian, regardless of the characteristic of
+F_q. More precisely:
+
+- If det(Q) = 0, Gamma is connected and bipartite, Q has nullity one, and every
+  nonzero rational kernel vector is a nonzero constant times a vector with
+  entries +1 and -1. The two sign classes are exactly the projective points of
+  the two missing Lagrangians. The unordered completion pair is unique.
+- If det(Q) != 0, Q is positive definite over R and S has no completion.
+
+Thus no search over candidate missing Lagrangians is required after the hole
+graph is constructed. This is an exact algebraic decision and recovery
+criterion, not an assertion that every deficiency-two partial spread completes.
+The explicit F3 negative fixture below has no completion.
+
+The new step is the combination of the deficiency-two hole degree with a sharp
+component-size lemma. David Ganz's [atlas, PR #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849)
+proves deficiency-one completion at B098 and explicitly leaves the stronger
+deficiency-two proposal unresolved. Its result is cited, not rechecked here.
+The signless-Laplacian kernel identity and elementary symplectic dimension
+facts are classical. This package supplies the completion criterion and its
+proof; it makes no claim of global literature priority.
+
+This is an algebraic side result. It changes the `formal-interface-lemma` card
+from a selected-supplier proof obligation to a precise completion interface in
+the atlas. It is not a new supplier, COPY invoice, kappa improvement, selected
+frontier change, or complete multiplication theorem.
+
+## Proof
+
+### 1. The hole graph has N vertices and degree k
+
+Write omega for the alternating form. Each L in S contains
+(q^n - 1)/(q - 1) projective points. Distinct members of S have disjoint point
+sets. Subtract their total from the (q^(2n) - 1)/(q - 1) ambient points to obtain
+
+$$
+|V(\Gamma)|=
+\frac{q^{2n}-1-(q^n-1)^2}{q-1}
+=\frac{2(q^n-1)}{q-1}=N.
+$$
+
+Fix a hole represented by h. For each old L, h does not belong to L = L-perp.
+The functional omega(h,-) on L is therefore nonzero. Exactly q^n - q^(n-1)
+nonzero vectors of L pair nontrivially with h, or q^(n-1) projective points.
+There are q^(2n-1) projective points in the ambient space that pair nontrivially
+with h. Consequently the number of nonorthogonal holes is
+
+$$
+q^{2n-1}-(q^n-1)q^{n-1}=q^{n-1}=k.
+$$
+
+Alternation gives no loops. Thus Gamma is a simple k-regular graph. Moreover
+
+$$
+3k-N=\frac{(q-3)q^{n-1}+2}{q-1}>0
+$$
+
+for q >= 3. In particular N <= 3k.
+
+### 2. A singular signless Laplacian forces one bipartite component
+
+For any simple k-regular graph and real vector z,
+
+$$
+z^T(kI+A)z=\sum_{\{u,v\}\in E}(z_u+z_v)^2.
+$$
+
+Hence Q is positive semidefinite and z lies in its kernel exactly when
+z_u = -z_v on every edge. A connected component supports a nonzero such vector
+exactly when it is bipartite. On a bipartite connected component the vector is
+constant on each part, with opposite constants. An odd cycle forces the
+constant to be zero. This proves the usual signless-kernel characterization
+without assuming that the whole graph is connected.
+
+Now let a simple k-regular graph with k > 0 have at most 3k vertices. A
+bipartite component has at least k vertices in each part, hence at least 2k
+vertices. Any further component has at least k + 1 vertices, since every
+vertex has k distinct neighbors. Both components would require at least
+3k + 1 vertices. Therefore a bipartite component, if present, is the whole
+graph. It is connected, and its signless kernel is one-dimensional.
+
+The size gate is sharp for general regular graphs. The disjoint union C4 and
+K3 has k = 2 and N = 3k + 1. Its signless Laplacian is singular, although the
+whole graph is not bipartite. This is an abstract graph example, not a claim
+that this graph occurs as a symplectic hole graph.
+
+Applying this lemma to Step 1, singularity of Q forces Gamma to be connected
+and bipartite. Its rational kernel is nonzero because Q has integer entries.
+Each nonzero kernel vector has equal nonzero magnitudes and opposite signs
+on the two parts.
+
+### 3. The two parts are precisely two missing Lagrangians
+
+Let X,Y be the two parts. Since Gamma is regular with positive degree,
+counting edges from each side gives k|X| = k|Y|. Thus
+
+$$
+|X|=|Y|=\frac{q^n-1}{q-1}.
+$$
+
+Representatives of points in X pair to zero, since there are no edges within X.
+Their span is isotropic, and so has dimension at most n. But a subspace of
+dimension at most n - 1 contains at most (q^(n-1) - 1)/(q - 1) projective points,
+fewer than |X|. Its span therefore has dimension n, and X is its entire
+projective point set. The same argument applies to Y.
+
+Call these spans L_X and L_Y. They meet each other trivially because X and Y
+are disjoint full point sets. They meet every old member of S trivially
+because all their points are holes. Adding them fills every hole and gives
+a full symplectic spread.
+
+Conversely, a completion partitions the holes into the two missing
+Lagrangians. There are no nonorthogonality edges within either point set,
+so Gamma is bipartite and Q is singular. Step 2 then shows that Gamma is
+connected. Its bipartition is unique up to swapping the parts, which proves
+uniqueness of the unordered completion pair. If Q is nonsingular, its
+positive semidefiniteness makes it positive definite. This proves every
+assertion of the result.
+
+## Relation to the nonzero-vector formulation
+
+The advance claim used uncovered nonzero vectors as graph vertices. The
+projective graph here compresses each scalar class of q - 1 vectors. Within
+one class the nonorthogonality adjacency rows are identical. Subtracting the
+two signless-kernel equations shows that a kernel vector is constant on every
+class, since its degree is (q - 1)k > 0 over Q. On class-constant vectors the
+uncompressed signless Laplacian acts as (q - 1)Q. The kernels therefore
+correspond exactly, so this compression preserves the claimed decision and
+recovery criterion.
+
+## Exact finite evidence
+
+The standalone verifier enumerates projective points and every Lagrangian in
+each named four-dimensional model, constructs the hole graph from the literal
+old subspaces, computes exact rational kernels and integer determinants, and
+independently enumerates possible completion pairs. It recovers both missing
+subspaces from the kernel signs in each positive case.
+
+For q = 3 and q = 5, take the standard form
+omega((x,y),(x',y')) = x dot y' - y dot x', with two-coordinate x,y.
+Choose the least nonsquare d. The q^2 - 1 old subspaces are the graphs of
+
+$$
+M(a,b)=\begin{pmatrix}a&b\\ b&da\end{pmatrix},\qquad (a,b)\ne(0,0).
+$$
+
+Their matrices are symmetric, and each nonzero difference has determinant
+d a^2 - b^2 != 0. The two missing subspaces are the graphs of zero and the
+vertical plane.
+
+For the negative F3 fixture, use the form
+omega((x,y),(x',y')) = det(x,x') - det(y,y'). Take graphs of the eight matrices
++/-I, +/-J, +/-K, +/-JK, where
+
+$$
+J=\begin{pmatrix}0&1\\2&0\end{pmatrix},\qquad
+K=\begin{pmatrix}1&1\\1&2\end{pmatrix}.
+$$
+
+These are the elementary quaternion subgroup matrices in SL2(F3). No novelty
+is claimed for the group or this fixture. Every matrix has determinant one;
+the verifier directly checks isotropy and disjointness of the eight graphs.
+
+| Fixture | Enumerated Lagrangians | Hole points | Degree | Rank Q | det Q | Completion pairs |
+|---|---:|---:|---:|---:|---:|---:|
+| F3 field puncture | 40 | 8 | 3 | 7 | 0 | 1 |
+| F3 quaternion graphs | 40 | 8 | 3 | 8 | 2304 | 0 |
+| F5 field puncture | 156 | 12 | 5 | 11 | 0 | 1 |
+
+The verifier also checks rejection of a duplicated old line in every fixture
+and the C4 disjoint K3 size-bound control. The finite controls corroborate the
+new criterion; the universal theorem rests on the written argument above.
+
+## Reproduction
+
+From the repository root, use CPython 3.12. No third-party packages or network
+are needed for the verifier.
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/symplectic-deficiency-two-spectral/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/symplectic-deficiency-two-spectral
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/symplectic-deficiency-two-spectral --check-source-history
+```
+
+The direct check prints `PASS_SYMPLECTIC_DEFICIENCY_TWO_SPECTRAL` and the table
+values above. `--receipt /absolute/path/outside-checkout/receipt.json` optionally
+writes a generated receipt binding the output to every package file's SHA256
+and the interpreter version. No receipt is handwritten or retained here.
+`SOURCES.json` pins the atlas text, original card and selected-record provenance.
+The atlas is a provenance reference; the mathematical checker does not import
+or rerun its validator or predecessor proof.
+
+Local validation used CPython 3.12.15. The direct verifier, registered replay
+and committed-byte/source-history preflight are the required local checks;
+hosted CI status is recorded in the PR body.
+
+## Limits and implementation bounds
+
+The theorem covers every prime power q >= 3 and every n >= 1. The executable
+controls use only q = 3,5 and n = 2; they are not an exhaustive finite proof of
+the all-dimension statement. There is no proof-assistant build or independent
+human proof review. General projective partial spreads without isotropy,
+higher deficiencies and the binary case in higher dimension are outside scope.
+
+The matrix is indexed by N hole points, so this is a polynomial algorithm in
+the explicit point inventory, not a polynomial algorithm in log(q) and n.
+It uses rational linear algebra even when the geometry is over a finite field.
+Taking the determinant modulo the geometry's characteristic is not the test.
+
+The verifier has no recursion, subprocesses, dynamic code evaluation or imported
+project code. Every loop ranges over explicit finite inputs: at most 5^4
+vectors, 156 projective points, 156 Lagrangians and a 12-by-12 geometric matrix.
+The exact-linear-algebra helper enforces a 16-by-16 ceiling. Python and Fraction
+allocate dynamically; this is the bounded managed-runtime deviation from the
+Power of Ten fixed-memory rule. Assertions enforce isotropy, disjointness,
+degree, kernel equations, recovery and exhaustive-completion agreement. The
+registered invocation enables warnings as errors and keeps assertions enabled.
+
+## Open next questions
+
+1. Does the singular-Q criterion hold for binary symplectic deficiency-two
+   partial spreads when n >= 3? The component-size proof no longer suffices.
+   Start by classifying whether a binary hole graph can have both a bipartite
+   component and another component. This matters because such a graph would
+   be a false positive for the proposed extension. No such example or
+   impossibility proof is supplied here.
+2. For deficiency t >= 3, can additional exact algebraic constraints recover
+   the t missing Lagrangians without solving unrestricted graph coloring?
+   The first step is to derive the corresponding hole degree and test a
+   concrete t = 3 fixture. The present two-part kernel argument does not
+   provide a criterion in that setting.
+
+## Sources and overlap
+
+The exact atlas source at base ff3cc58e370d0f678e529246f8c73e8094e18fcf is pinned
+in `SOURCES.json`; PR #2849's retained head is
+00576c07434c1196f49823dac83d57211ef731f1. Credit David Ganz for the atlas and
+its deficiency-one theorem and deficiency-two question. The elementary graph
+kernel identity is classical and is proved explicitly here.
+
+Live open PRs, recent account submissions and claims, active Discussions,
+targeted merged-PR searches and main-tree README searches were checked before
+claiming this question. The broad cached card scan reported complete remote
+pagination but incomplete sparse local-note coverage. Those checks do not
+establish global mathematical novelty or exclude unpublished work.
diff --git a/research/symplectic-deficiency-two-spectral/SOURCES.json b/research/symplectic-deficiency-two-spectral/SOURCES.json
new file mode 100644
index 0000000000..8e4302e892
--- /dev/null
+++ b/research/symplectic-deficiency-two-spectral/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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/pure-math-atlas-400/volumes/02-geometry.md",
+      "usage": "provenance",
+      "git_blob": "baef1e69c08c7cbd4dfd020862870fa5161afc86",
+      "sha256": "39fc97bdfa29337b79d1308e35df41e867ce2102d44755fd407aa09ff8352b39"
+    }
+  ]
+}
diff --git a/research/symplectic-deficiency-two-spectral/TASK.json b/research/symplectic-deficiency-two-spectral/TASK.json
new file mode 100644
index 0000000000..cc7288dcbe
--- /dev/null
+++ b/research/symplectic-deficiency-two-spectral/TASK.json
@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "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 rational signless-Laplacian criterion and unique recovery for deficiency-two symplectic partial spreads over every F_q with q >= 3, in every even dimension.",
+  "scope_change_reason": "The original selected-interface card is changed to the explicit deficiency-two completion question left by David Ganz atlas B098. This is an algebraic side result, not a formalization or supplier-admission claim.",
+  "bottleneck_link": "A precise finite-geometric completion interface may support later stabilizer-basis constructions; no costed multiplication supplier or kappa consequence is established.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved original implication with a standalone exact verifier, or a bounded dead end.",
+  "outcome": "completed",
+  "evidence": "README written all-dimension proof; verify.py exact F3/F5 positive controls, F3 negative control, complete local Lagrangian inventories, duplicated-line rejection and a sharp abstract size-bound control.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does singularity of the hole-graph signless Laplacian still characterize binary deficiency-two completion in dimensions at least six?",
+      "why_it_matters": "The degree component-size argument does not cover this range.",
+      "first_step": "Determine whether a binary hole graph can have a bipartite component and a second component.",
+      "blocked_by": "No geometric exclusion or example of such a disconnected hole graph is supplied."
+    },
+    {
+      "question": "Can exact algebraic constraints recover missing Lagrangians for deficiency at least three?",
+      "why_it_matters": "The present kernel detects only two color classes.",
+      "first_step": "Derive the hole degree and inspect a concrete deficiency-three fixture.",
+      "blocked_by": "No replacement for the two-color kernel identity is established."
+    }
+  ]
+}
diff --git a/research/symplectic-deficiency-two-spectral/VERIFY.json b/research/symplectic-deficiency-two-spectral/VERIFY.json
new file mode 100644
index 0000000000..4bc086206d
--- /dev/null
+++ b/research/symplectic-deficiency-two-spectral/VERIFY.json
@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact projective hole graphs, rational kernel recovery, exhaustive local Lagrangian completions, a noncompletion determinant and size-gate/repeated-line controls."
+    }
+  ]
+}
diff --git a/research/symplectic-deficiency-two-spectral/verify.py b/research/symplectic-deficiency-two-spectral/verify.py
new file mode 100644
index 0000000000..02009bb7a8
--- /dev/null
+++ b/research/symplectic-deficiency-two-spectral/verify.py
@@ -0,0 +1,213 @@
+#!/usr/bin/env python3
+"""Exact finite controls for the written deficiency-two completion theorem."""
+from __future__ import annotations
+
+import argparse
+import hashlib
+import itertools
+import json
+import platform
+from fractions import Fraction
+from pathlib import Path
+
+Vector = tuple[int, ...]
+Line = frozenset[Vector]
+
+
+def point(vector: Vector, prime: int) -> Vector:
+    first = next(entry for entry in vector if entry)
+    inverse = pow(first, -1, prime)
+    return tuple(entry * inverse % prime for entry in vector)
+
+
+def pairing(left: Vector, right: Vector, prime: int, split: bool) -> int:
+    if split:
+        value = left[0] * right[1] - left[1] * right[0]
+        value -= left[2] * right[3] - left[3] * right[2]
+    else:
+        value = sum(left[i] * right[i + 2] - left[i + 2] * right[i]
+                    for i in range(2))
+    return value % prime
+
+
+def projective_points(prime: int) -> list[Vector]:
+    assert prime in (3, 5)
+    vectors = itertools.product(range(prime), repeat=4)
+    return sorted({point(v, prime) for v in vectors if any(v)})
+
+
+def line_span(left: Vector, right: Vector, prime: int) -> Line:
+    vectors = (tuple((a * x + b * y) % prime for x, y in zip(left, right))
+               for a, b in itertools.product(range(prime), repeat=2))
+    return frozenset(point(v, prime) for v in vectors if any(v))
+
+
+def lagrangians(points: list[Vector], prime: int, split: bool) -> set[Line]:
+    lines = {line_span(u, v, prime) for u, v in itertools.combinations(points, 2)
+             if pairing(u, v, prime, split) == 0}
+    assert all(len(line) == prime + 1 for line in lines)
+    return lines
+
+
+def graph_line(matrix: tuple[int, ...], prime: int) -> Line:
+    a, b, c, d = matrix
+    return frozenset(point((x, y, (a * x + b * y) % prime,
+                           (c * x + d * y) % prime), prime)
+                     for x, y in itertools.product(range(prime), repeat=2)
+                     if x or y)
+
+
+def field_puncture(prime: int) -> list[Line]:
+    squares = {x * x % prime for x in range(1, prime)}
+    nonsquare = next(x for x in range(1, prime) if x not in squares)
+    return [graph_line((a, b, b, nonsquare * a % prime), prime)
+            for a, b in itertools.product(range(prime), repeat=2) if a or b]
+
+
+def matrix_product(left: tuple[int, ...], right: tuple[int, ...]) -> tuple[int, ...]:
+    return tuple(sum(left[2 * i + t] * right[2 * t + j] for t in range(2)) % 3
+                 for i, j in itertools.product(range(2), repeat=2))
+
+
+def quaternion_partial() -> list[Line]:
+    identity, first, second = (1, 0, 0, 1), (0, 1, 2, 0), (1, 1, 1, 2)
+    matrices = [tuple(sign * x % 3 for x in matrix)
+                for matrix in (identity, first, second, matrix_product(first, second))
+                for sign in (1, -1)]
+    assert len(set(matrices)) == 8
+    return [graph_line(matrix, 3) for matrix in matrices]
+
+
+def hole_graph(points: list[Vector], lines: list[Line], prime: int,
+               split: bool) -> tuple[list[Vector], list[list[int]]]:
+    if len(lines) != prime * prime - 1 or len(set(lines)) != len(lines):
+        raise ValueError("wrong partial-spread size or repeated line")
+    covered: set[Vector] = set()
+    for line in lines:
+        if len(line) != prime + 1 or not line.issubset(points):
+            raise ValueError("invalid projective line")
+        if any(pairing(u, v, prime, split) for u, v in itertools.combinations(line, 2)):
+            raise ValueError("nonisotropic line")
+        if covered.intersection(line):
+            raise ValueError("intersecting old lines")
+        covered.update(line)
+    holes = sorted(set(points) - covered)
+    adjacency = [[int(pairing(u, v, prime, split) != 0) for v in holes] for u in holes]
+    assert len(holes) == 2 * (prime + 1)
+    assert all(sum(row) == prime for row in adjacency)
+    return holes, adjacency
+
+
+def exact_kernel(matrix: list[list[int]]) -> tuple[int, int, list[list[Fraction]]]:
+    size = len(matrix)
+    assert 1 <= size <= 16 and all(len(row) == size for row in matrix)
+    rows = [[Fraction(x) for x in row] for row in matrix]
+    pivots: list[int] = []
+    determinant = Fraction(1)
+    for column in range(size):
+        rank = len(pivots)
+        pivot = next((i for i in range(rank, size) if rows[i][column]), None)
+        if pivot is None:
+            continue
+        if pivot != rank:
+            rows[pivot], rows[rank] = rows[rank], rows[pivot]
+            determinant = -determinant
+        divisor = rows[rank][column]
+        determinant *= divisor
+        rows[rank] = [x / divisor for x in rows[rank]]
+        for i in range(size):
+            if i != rank and rows[i][column]:
+                coefficient = rows[i][column]
+                rows[i] = [x - coefficient * y for x, y in zip(rows[i], rows[rank])]
+        pivots.append(column)
+    basis = []
+    for free in sorted(set(range(size)) - set(pivots)):
+        vector = [Fraction(int(i == free)) for i in range(size)]
+        for row, pivot in enumerate(pivots):
+            vector[pivot] = -rows[row][free]
+        assert all(sum(x * y for x, y in zip(row, vector)) == 0 for row in matrix)
+        basis.append(vector)
+    assert determinant.denominator == 1
+    return len(pivots), int(determinant) if len(pivots) == size else 0, basis
+
+
+def signless(adjacency: list[list[int]]) -> list[list[int]]:
+    size = len(adjacency)
+    assert all(adjacency[i][i] == 0 for i in range(size))
+    assert all(adjacency[i][j] == adjacency[j][i]
+               for i, j in itertools.product(range(size), repeat=2))
+    return [[entry + (sum(row) if i == j else 0) for j, entry in enumerate(row)]
+            for i, row in enumerate(adjacency)]
+
+
+def fixture(prime: int, split: bool, lines: list[Line], completable: bool) -> dict:
+    points = projective_points(prime)
+    inventory = lagrangians(points, prime, split)
+    assert len(inventory) == (prime + 1) * (prime * prime + 1)
+    assert set(lines).issubset(inventory)
+    holes, adjacency = hole_graph(points, lines, prime, split)
+    rank, determinant, basis = exact_kernel(signless(adjacency))
+    candidates = {line for line in inventory if line.issubset(holes)}
+    extensions = [pair for pair in itertools.combinations(candidates, 2)
+                  if pair[0].isdisjoint(pair[1])]
+    assert len(extensions) == int(completable)
+    assert (determinant == 0) == completable
+    assert len(basis) == int(completable)
+    if completable:
+        normalized = [x / basis[0][0] for x in basis[0]]
+        assert set(normalized) == {Fraction(-1), Fraction(1)}
+        recovered = {frozenset(h for h, x in zip(holes, normalized) if x == sign)
+                     for sign in (-1, 1)}
+        assert recovered == set(extensions[0])
+    else:
+        assert determinant > 0 and not candidates
+    try:
+        hole_graph(points, lines[:-1] + [lines[0]], prime, split)
+    except ValueError as error:
+        assert "repeated" in str(error)
+    else:
+        raise AssertionError("duplicate-line mutation was accepted")
+    return {"q": prime, "form": "split" if split else "standard",
+            "old_lines": len(lines), "holes": len(holes), "degree": prime,
+            "enumerated_lagrangians": len(inventory), "completion_pairs": len(extensions),
+            "signless_rank": rank, "signless_determinant": determinant}
+
+
+def component_bound_control() -> dict:
+    # C4 disjoint union K3 is regular with N=3k+1. Its Q is singular,
+    # although the full graph is not bipartite. The strict size gate matters.
+    edges = {(0, 1), (1, 2), (2, 3), (0, 3), (4, 5), (4, 6), (5, 6)}
+    adjacency = [[int((min(i, j), max(i, j)) in edges) for j in range(7)]
+                 for i in range(7)]
+    assert all(sum(row) == 2 for row in adjacency)
+    rank, determinant, basis = exact_kernel(signless(adjacency))
+    assert rank == 6 and determinant == 0 and len(basis) == 1
+    assert basis[0][4:] == [0, 0, 0]
+    return {"vertices": 7, "degree": 2, "rank": rank,
+            "scope": "abstract graph control, not a symplectic-spread example"}
+
+
+def main() -> None:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--receipt", type=Path)
+    args = parser.parse_args()
+    result = {"status": "PASS_SYMPLECTIC_DEFICIENCY_TWO_SPECTRAL",
+              "fixtures": [fixture(3, False, field_puncture(3), True),
+                           fixture(3, True, quaternion_partial(), False),
+                           fixture(5, False, field_puncture(5), True)],
+              "component_bound_control": component_bound_control(),
+              "scope": "finite exact controls; the all-dimension theorem is a written proof"}
+    if args.receipt is not None:
+        package = Path(__file__).resolve().parent
+        destination = args.receipt.resolve()
+        if destination.is_relative_to(package.parents[1]):
+            raise ValueError("receipt must be outside the checkout")
+        receipt = {"result": result, "python": platform.python_version(),
+                   "sha256": {path.name: hashlib.sha256(path.read_bytes()).hexdigest()
+                              for path in sorted(package.iterdir()) if path.is_file()}}
+        destination.write_text(json.dumps(receipt, indent=2) + "\n", encoding="utf-8")
+    print(json.dumps(result, indent=2))
+
+
+if __name__ == "__main__":
+    main()