diff --git a/research/matching-layer-rounding/README.md b/research/matching-layer-rounding/README.md
new file mode 100644
index 0000000000..99f648abd6
--- /dev/null
+++ b/research/matching-layer-rounding/README.md
@@ -0,0 +1,232 @@
+# Serial rounded matching layers preserve the data grid and coordinate width
+
+Prepared by `apoursh` with substantial OpenAI Codex
+assistance. Apache-2.0. This is a scoped written proof and source-execution
+audit; independent human or proof-assistant acceptance is not claimed.
+
+## Contribution and exact interface
+
+[PR4976](https://github.com/CrocSwap/integer-mult-bounds/pull/4976) proves the
+sharp sqrt(2) interpolation bound for exact operators inside matching layers.
+Its extra-data-bit implication explicitly retains the predecessor's
+rounding-event count. This package checks that premise against the actual
+rounded executor, [exact.py](../rational-unitary-fft/exact.py), and distinguishes
+Euclidean amplitude from the size of each stored coordinate.
+
+For this executor, reordering the disjoint gates within a layer preserves its
+rounded endpoint exactly. There is still one error **vector per original
+layer**, with the original number of scalar rounding operations. Every stored
+state between output writes is a coordinate splice of the adjacent rounded
+endpoints. Consequently the existing terminal error budget, fractional grid F,
+and signed component width I remain sufficient. No extra fractional or integer
+bit is forced solely by serializing these gates or inspecting their output
+writes. A Euclidean bound at the new cuts may still require sqrt(2).
+
+This supplies an explicit source-bound explanation of a valid but implicit
+step in PR4205's layerwise analysis. It neither disputes PR4976's conservative
+extra-bit implication nor reclaims its interpolation theorem. Complete-layer
+conditioning and the local arithmetic model remain explicit premises.
+
+## Execution contract and theorem
+
+Fix a positive integer N of complex coordinates, an integer F >= 1, and
+u = 2^(-F). Inputs are on
+the componentwise u-grid. Each layer is a finite matching of valid square
+one- or two-coordinate linear gates with stored Gaussian-rational coefficients;
+gate supports are disjoint. Each gate snapshots its input, evaluates its entire
+output exactly, then rounds each real and imaginary output component once to
+the nearest u-grid point, with halfway cases toward +infinity. Untouched
+coordinates are unchanged. Products and partial sums are not rounded.
+
+Let L_j be the exact stored-coefficient layer operator and y_j its rounded
+endpoint. If the layer touches m_j coordinates, then:
+
+1. Any permutation of whole gates has the same rounded endpoint and the same
+   m_j complex-output rounding operations (2m_j real roundings).
+2. The realized residual e_j = y_j - L_j y_(j-1) is supported on those
+   coordinates. Each real/imaginary residual is at most u/2 in magnitude, so
+
+   ```
+   ||e_j||_2^2 <= (m_j/2) u^2,     ||e_j||_2 <= N u.
+   ```
+
+3. At any cut after completed output writes, let E project onto the written
+   coordinates. The actual stored state is
+
+   ```
+   y_(j,E) = (I-E) y_(j-1) + E y_j
+           = [(I-E) + E L_j] y_(j-1) + E e_j.
+   ```
+
+   This includes a cut between the two output writes of one gate. It does
+   not require E to commute with L_j or the cut map to be invertible.
+4. Every stored component is an endpoint component on the original grid.
+   If both endpoint Euclidean norms are at most A, each stored real/imaginary
+   component is at most A, while the Euclidean norm is at most sqrt(2) A.
+
+The same splice identity holds for the exact trajectory x_j and for the
+error y_j-x_j. Errors may depend on the data; no independence or unbiasedness
+assumption is used.
+
+### Proof and binding to the retained executor
+
+In `exact.apply`, a valid layer enforces disjoint supports. The executor copies
+all inputs of a gate into `before`, computes the complete list `outputs`, and
+only then enters the rounding/write loop. Earlier gates cannot have changed
+this gate's inputs. Each gate therefore sees the same local input as simultaneous
+evaluation from the layer's initial state. Its rounded outputs do not depend
+on the order of the other gates.
+
+Each output is rounded once. `round_q` computes `floor(value/u + 1/2)*u`, so
+each real residual is at most u/2, including signed ties. An untouched
+coordinate has zero residual. Summing the squares of the 2m_j real residuals
+proves the stated bound; sqrt(m_j/2) <= N for N >= 1 gives the source's
+conservative N u allowance.
+
+At a write cut, each coordinate has either its initial value or its unique
+final rounded output. All outputs of a gate were computed before any were
+stored. This proves the splice even within that gate's output-write loop,
+and proves the component/grid bounds. Adding squared norms on complementary
+coordinate sets gives the Euclidean bound. Subtracting the analogous exact
+state identity gives the error splice.
+
+For D layers the rounded trajectory is exactly
+
+```
+y_j = L_j y_(j-1) + e_j,    j = 1,...,D.
+```
+
+At a cut within layer j, there are j-1 completed residuals and the projected
+current residual E e_j: at most D residual vectors, not D+1 or the number of
+gates. This groups the actual scalar roundings; it neither replaces them by
+one scalar rounding nor evaluates errors on the unrounded trajectory.
+
+## Consequence for the Full precision contract
+
+Retain [FULL-PROOF.md](../rational-unitary-fft/FULL-PROOF.md), equations
+(14)-(18), as conditional inputs. Let K = K_phys bound exact stored prefixes,
+suffixes and their inverses at **complete physical-layer boundaries**;
+D <= D_*; ||y_0||_2 <= R; and ||T_hat-T||_2 <= e for the completed stored
+operator and intended target. Bounds only at completed atomic calls are
+insufficient for this application.
+
+Expanding the realized residual recurrence, terminal suffixes cost at most K
+and complete-boundary segments at most K^2. Hence
+
+```
+||y_D - T y_0||_2 <= e R + D_* K N 2^(-F),
+||y_j||_2 <= A := K R + D_* K^2 N 2^(-F).
+```
+
+These are the original terminal-error and completed-layer amplitude allowances.
+The original F remains sufficient because neither the rounded endpoint nor the
+number of grouped layer residuals changes.
+
+The write-cut splice retains the **component** envelope A. Thus the source's
+signed word allocation
+
+```
+I = max(1, ceil(log2(max(1,A)))) + 2
+```
+
+remains sufficient with the same F. Feeding the larger Euclidean envelope
+sqrt(2)A into this component-width formula is unnecessary. A consumer needing
+a vector-norm radius at a new cut must still use its appropriate larger radius.
+
+Apply the same argument to the separately executed stored-inverse program
+under its own input grid/radius, complete-layer bounds, and stored-to-intended
+inverse approximation allowance. The forward endpoint defect alone does not
+supply the inverse defect bound. Rounded forward execution is not claimed to
+be exactly reversible.
+
+### Component width does not imply partial invertibility
+
+A swap gate sends (0,1) to (1,0). After its first output is stored, the state
+is (1,1): Euclidean norm sqrt(2), but every component remains at most one.
+The corresponding first-write linear map has identical rows and is singular.
+Thus a zero-loss Euclidean assertion or an inverse operator claim would fail
+at arbitrary output-write cuts.
+
+Exact gate-product/sum temporaries, coefficient preparation, tape movement,
+the predecessor's all-size conditioning proof and supplier admission remain
+outside this audit. The source uses unbounded exact rational local arithmetic;
+a bounded-word implementation still needs its separate temporary/local-arithmetic
+contract. No selected exponent changes.
+
+## Independent finite evidence
+
+`verify.py` authenticates its declared source closure and compares the actual
+rounded executor with an independent simultaneous-layer oracle and independent
+rational tie rounding. Fixtures target complex nonunitary gates, signed ties,
+idle wires, gate permutations, actual FFT/shear gates, and residuals evaluated
+on the rounded trajectory. Controls distinguish the snapshot, event-count,
+disjoint-support and component-width premises. The written proof is quantified;
+finite checks corroborate source binding and selected failure modes.
+
+The bounded suite covers 10 fixtures, 145 gate-permutation orders, 607 rounded
+gate-prefix checks, 83 observed coordinate writes and seven controls. Two
+complex inputs exercise the actual retained n=2 Builder shear (12 layers,
+20 gates, 32 coordinate writes per input), with nonzero realized residuals.
+
+To inspect write cuts, the checker adds a single snapshot callback immediately
+after the source assignment `state[i] = value`. Removing that callback restores
+the exact original function AST; the output records both AST hashes. Observed
+and unmodified execution must agree on the final vector and every source
+tracking statistic. The callback only records immutable snapshots; the checker
+then compares all writes with an independently evaluated synchronous oracle.
+The source's arithmetic and checks are unchanged.
+
+Registered normal and optimized checks passed locally on CPython 3.12.14;
+their computed JSON results agree byte for byte. With CPython 3.12 and the
+standard library:
+
+```
+python3.12 -I -W error -B research/matching-layer-rounding/verify.py
+python3.12 -I -O -W error -B research/matching-layer-rounding/verify.py
+python3.12 -B scripts/research_package.py --package research/matching-layer-rounding
+```
+
+After committing:
+
+```
+python3.12 -B scripts/check_research_commit.py --package research/matching-layer-rounding --check-source-history
+```
+
+Registered replay, committed export and Git-free direct replay are separate
+checks; none establishes the retained all-size premises or human acceptance.
+
+## Scope, overlap and credit
+
+Base `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7.
+The original local interpolation draft was preserved separately after fresh
+overlap revealed PR4976. This contribution narrows to rounded execution and
+component width. PR4976's operator theorem and its existing independent review,
+PR4977's Full allocator substitution, PR5018's Gaussian allocation and PR4829's
+sharp exact dirty-shear envelope are credited existing work.
+
+The October 23 entry search covered all 6,918 upstream local note records plus
+the new draft and targeted live PR searches for rounded/disjoint gates,
+serialization, event counts and `exact.py`. Remote discussion pagination and
+unpublished work were not exhausted; the terminal helper had no remote cache.
+No exhaustive novelty claim follows. TASK.json records scope/freshness.
+The related canonical investigation is
+[Discussion #4202](https://github.com/CrocSwap/integer-mult-bounds/discussions/4202).
+
+Credit Jose Manuel (`jmbarrancoml`) for the exact rounded kernel, rational FFT
+compiler and Full precision contracts; Vlado Vojdanovski for the schedule;
+Chafik Boukhalfa for certified phases; Brian (`JoyboyBrian`) for PR4755/4976's
+cut contracts and PR4977/5018's allocator follow-ups; James Reed for the existing
+independent PR4976 review; Nick Petalas for the exact dirty-shear refinement;
+and Cinna Davis and the retained lineage for the all-size caller. Disjoint-map
+commutation and coordinate splicing are elementary; the contribution is their
+explicit runtime/precision implication and independent execution controls.
+Source notices remain unchanged.
+
+## Open next questions
+
+Can a concrete bounded-word implementation of one actual two-coordinate gate
+deliver this final-output rounding contract within the predecessor's temporary
+budget? Start with its multiply/add/round order, including signed ties and
+intermediate product widths. This matters for transferring stored-state bounds
+to physical execution; local arithmetic and temporary-storage specifications
+remain separate premises.
diff --git a/research/matching-layer-rounding/SOURCES.json b/research/matching-layer-rounding/SOURCES.json
new file mode 100644
index 0000000000..8558854742
--- /dev/null
+++ b/research/matching-layer-rounding/SOURCES.json
@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "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/capped-phase-fusion/evidence/inplace_algebra_ultra/check_circuits.py",
+      "usage": "input",
+      "git_blob": "f80c141c8116b163c2bb5a028c28212077c8d5a9",
+      "sha256": "06d1861bfe8af543908e26557ffda7e451ff176bceb9bacfaf0f04f234b336d5"
+    },
+    {
+      "path": "research/cubic-cyclic-inverse/vendor/interval_kernel.py",
+      "usage": "input",
+      "git_blob": "1182175a55cb871481de0f56ea9ae56e474705fe",
+      "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe"
+    },
+    {
+      "path": "research/matching-sublayer-norm/README.md",
+      "usage": "input",
+      "git_blob": "eb7b8be250b6f23ae30e7e611e651a8fe300ac3e",
+      "sha256": "ba6754f00779874ec981563101114cf18c03026c18338f37a813abd3fae59d21"
+    },
+    {
+      "path": "research/rational-unitary-fft/FULL-PROOF.md",
+      "usage": "input",
+      "git_blob": "e650f46863115f810e27b403f916dd7f79b37786",
+      "sha256": "acf8c596d91b5efd35a286735d6867ff8afce64354a13f680c2fae3dab824410"
+    },
+    {
+      "path": "research/rational-unitary-fft/SOURCES.json",
+      "usage": "input",
+      "git_blob": "7ee22e983f54dfb73e74d20ed1910a64d2abb6cd",
+      "sha256": "7324e22bcb202b5cc03b5f7ea713f6f0c7cd80ee60d320fb03b1e2f7b13b8c91"
+    },
+    {
+      "path": "research/rational-unitary-fft/engine.py",
+      "usage": "input",
+      "git_blob": "e9f2f2b08dc2bc4c646e47dca92059351ca89384",
+      "sha256": "9e36aee0835e6b1b62997433581f88b5a434ccab8ae43e5c25d1deaaf1ebf653"
+    },
+    {
+      "path": "research/rational-unitary-fft/exact.py",
+      "usage": "input",
+      "git_blob": "aae41e6acfb2e5a4fafdd85727891eb746b57b42",
+      "sha256": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479"
+    }
+  ]
+}
diff --git a/research/matching-layer-rounding/TASK.json b/research/matching-layer-rounding/TASK.json
new file mode 100644
index 0000000000..f9e4331e36
--- /dev/null
+++ b/research/matching-layer-rounding/TASK.json
@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Bind exact.apply rounded matching-layer execution to one residual per original layer; prove serial gate/output-write cuts preserve the fractional grid and per-component signed width.",
+  "scope_change_reason": "Fresh overlap found merged PR4976 and an independent review covering our prior local interpolation draft. Narrow to its rounding-event premise and distinguish Euclidean cut amplification from stored-coordinate widths.",
+  "bottleneck_link": "Preserves the Full terminal error and signed data-word allocation under serial disjoint-gate execution, conditional on original complete-layer stability and local arithmetic.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the source-execution proof, bounded independent rounded-trajectory checks, and publication preflight. No full compiler/supplier/native/Lean replay.",
+  "outcome": "completed",
+  "evidence": "README.md gives the quantified runtime/precision proof. verify.py authenticates seven inputs and independently checks synchronous/serial execution, every observed output write, residual counts, widths and seven discriminating controls. Registered normal/optimized replay is declared in VERIFY.json.",
+  "author": "apoursh, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance, including separate mathematical, overlap and verifier work. No independent human or proof-assistant acceptance.",
+  "open_questions": [
+    {
+      "question": "Can a bounded-word implementation of an actual two-coordinate gate realize this final-output rounding contract within its temporary budget?",
+      "why_it_matters": "Stored-state width does not certify arithmetic products, sums or physical execution.",
+      "first_step": "Specify one multiply/add/round sequence and certify signed ties and intermediate widths.",
+      "blocked_by": "A concrete local arithmetic and temporary-storage contract is required."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+    "priority_revision": 7,
+    "checked_at": "2026-10-23T11:13:56Z",
+    "decision": "Continue with rounded-execution audit; exact interpolation already covered by PR4976. Selected record and retained runtime inputs unchanged."
+  },
+  "overlap": {
+    "related_prs": [
+      4976,
+      4977,
+      5018,
+      4829,
+      4755,
+      4205
+    ],
+    "prior_review": "https://github.com/CrocSwap/integer-mult-bounds/pull/4976#issuecomment-6358034668",
+    "local_head_records": 6918,
+    "local_complete": true,
+    "remote_scope": "Targeted live PR search/read; no complete discussion pagination or unpublished-work coverage."
+  },
+  "publication_checkpoint": {
+    "upstream_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+    "checked_at": "2026-10-23T13:16:00.207211+00:00",
+    "guidance_and_declared_inputs_changed": false,
+    "overlap": "Final targeted live PR searches reviewed, including adjacent PR5153 coefficient-rounding guards (a distinct question). No duplicate of this rounded-output execution/component-width result found in inspected results; remote pagination/unpublished work not exhausted.",
+    "runner_update": "Canonical main changes Git blob-reader process cleanup only; scientific input bytes and contribution rules are unchanged."
+  }
+}
diff --git a/research/matching-layer-rounding/VERIFY.json b/research/matching-layer-rounding/VERIFY.json
new file mode 100644
index 0000000000..7707a5b87f
--- /dev/null
+++ b/research/matching-layer-rounding/VERIFY.json
@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/capped-phase-fusion/evidence/inplace_algebra_ultra/check_circuits.py",
+    "research/cubic-cyclic-inverse/vendor/interval_kernel.py",
+    "research/matching-sublayer-norm/README.md",
+    "research/rational-unitary-fft/FULL-PROOF.md",
+    "research/rational-unitary-fft/SOURCES.json",
+    "research/rational-unitary-fft/engine.py",
+    "research/rational-unitary-fft/exact.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent synchronous/rounding oracle versus source executor; layer residuals, gate-order equivalence, write-cut width and discriminating controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same source-bound exact checks with assertions disabled."
+    }
+  ]
+}
diff --git a/research/matching-layer-rounding/verify.py b/research/matching-layer-rounding/verify.py
new file mode 100644
index 0000000000..974085a2a0
--- /dev/null
+++ b/research/matching-layer-rounding/verify.py
@@ -0,0 +1,370 @@
+#!/usr/bin/env python3
+"""Exact source-bound tests for grouped rounding in a matching layer.
+
+The independent oracle uses integer divmod, frozen gate inputs, and vector
+identities. Only the retained Gaussian-rational scalar representation is reused.
+Source write observations add one AST call and leave its arithmetic unchanged.
+Substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import ast
+import copy
+from fractions import Fraction as Q
+from hashlib import sha256
+import itertools
+import json
+from pathlib import Path
+import sys
+from types import FunctionType
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+EXACT = "research/rational-unitary-fft/exact.py"
+ENGINE = "research/rational-unitary-fft/engine.py"
+ORACLE = "research/cubic-cyclic-inverse/vendor/interval_kernel.py"
+CIRCUIT = "research/capped-phase-fusion/evidence/inplace_algebra_ultra/check_circuits.py"
+SOURCE_MANIFEST = "research/rational-unitary-fft/SOURCES.json"
+HOOK = "_matching_layer_rounding_observe_write"
+C = None
+
+
+def need(ok, reason):
+    if not ok:
+        raise ValueError(reason)
+
+
+def rounded_q(value, bits):
+    """Nearest grid point, ties toward +infinity; no source rounding helper."""
+    numerator = value.numerator * (1 << bits)
+    quotient, remainder = divmod(numerator, value.denominator)
+    return Q(quotient + int(2 * remainder >= value.denominator), 1 << bits)
+
+
+def rounded_z(value, bits):
+    return C(rounded_q(value.re, bits), rounded_q(value.im, bits))
+
+
+def norm2(values):
+    return sum((v.re * v.re + v.im * v.im for v in values), Q())
+
+
+def plus(a, b):
+    need(len(a) == len(b), "vector addition dimensions")
+    return [x + y for x, y in zip(a, b)]
+
+
+def minus(a, b):
+    need(len(a) == len(b), "vector subtraction dimensions")
+    return [x - y for x, y in zip(a, b)]
+
+
+def support(layer, n):
+    used = set()
+    for ids, gate in layer:
+        need(len(ids) in (1, 2) and len(gate) == len(ids)
+             and all(len(row) == len(ids) for row in gate), "complete scalar/two-wire gate")
+        need(len(set(ids)) == len(ids) and all(type(i) is int and 0 <= i < n for i in ids),
+             "valid coordinate support")
+        need(not used.intersection(ids), "matching layer: disjoint supports")
+        used.update(ids)
+    return used
+
+
+def linear(layer, state):
+    """Independent simultaneous linear layer: every gate reads frozen state."""
+    support(layer, len(state))
+    result = list(state)
+    for ids, gate in layer:
+        for wire, row in zip(ids, gate):
+            result[wire] = sum((coefficient * state[j] for coefficient, j in zip(row, ids)), C())
+    return result
+
+
+def synchronous(layer, state, bits):
+    used = support(layer, len(state))
+    exact = linear(layer, state)
+    return [rounded_z(x, bits) if i in used else x for i, x in enumerate(exact)]
+
+
+def residual_check(residual, used, bits):
+    half = Q(1, 1 << (bits + 1))
+    need(all(i in used or x == 0 for i, x in enumerate(residual)), "residual support")
+    need(all(abs(x.re) <= half and abs(x.im) <= half for x in residual),
+         "one output rounding: component residual bound")
+    need(norm2(residual) <= len(used) * 2 * half * half, "aggregate layer residual bound")
+
+
+def reject(operation, label):
+    try:
+        operation()
+    except ValueError:
+        return label
+    raise ValueError("control unexpectedly passed: " + label)
+
+
+def instrument(exact_module, raw_source):
+    """Add an observation immediately after the source's sole coordinate write.
+
+    The callback only snapshots tuples; checks run after apply returns. Rebinding
+    the generated code to the original module globals preserves the source C
+    class's TRACK accounting. The original apply function is never replaced.
+    """
+    source_tree = ast.parse(raw_source)
+    functions = [x for x in source_tree.body if isinstance(x, ast.FunctionDef) and x.name == "apply"]
+    need(len(functions) == 1, "one retained apply function")
+    original = functions[0]
+    need(not any(isinstance(node, ast.Name) and node.id == HOOK for node in ast.walk(original)),
+         "fresh observation name")
+    wanted = ast.dump(ast.parse("state[i] = value").body[0], include_attributes=False)
+
+    class Observe(ast.NodeTransformer):
+        count = 0
+
+        def visit_Assign(self, node):
+            if ast.dump(node, include_attributes=False) != wanted:
+                return self.generic_visit(node)
+            self.count += 1
+            hook = ast.parse(HOOK + "(tuple(state), i, tuple(ids))").body[0]
+            return [node, ast.copy_location(hook, node)]
+
+    class Strip(ast.NodeTransformer):
+        count = 0
+
+        def visit_Expr(self, node):
+            if (isinstance(node.value, ast.Call) and isinstance(node.value.func, ast.Name)
+                    and node.value.func.id == HOOK):
+                self.count += 1
+                return None
+            return self.generic_visit(node)
+
+    observer = Observe()
+    observed = ast.fix_missing_locations(observer.visit(copy.deepcopy(original)))
+    stripper = Strip()
+    stripped = stripper.visit(copy.deepcopy(observed))
+    original_dump = ast.dump(original, include_attributes=False)
+    need(observer.count == stripper.count == 1, "exactly one write observation inserted/removed")
+    need(ast.dump(stripped, include_attributes=False) == original_dump,
+         "observation-stripped AST equals original apply AST")
+    scratch = {}
+    exec(compile(ast.Module(body=[observed], type_ignores=[]), "<observed pinned apply>", "exec"), scratch)
+    function = FunctionType(scratch["apply"].__code__, exact_module.__dict__,
+                            "observed_apply", exact_module.apply.__defaults__)
+    evidence = {"inserted_observation_calls": observer.count,
+                "original_apply_ast_sha256": sha256(original_dump.encode()).hexdigest(),
+                "stripped_apply_ast_sha256": sha256(ast.dump(stripped, include_attributes=False).encode()).hexdigest(),
+                "observed_apply_ast_sha256": sha256(ast.dump(observed, include_attributes=False).encode()).hexdigest()}
+    return function, evidence
+
+
+def trace_writes(exact_module, observed, plan, initial, bits, boundaries, original_result):
+    events = []
+    need(HOOK not in exact_module.__dict__, "no stale observation hook")
+    exact_module.__dict__[HOOK] = lambda state, wire, ids: events.append((state, wire, ids))
+    try:
+        observed_result = observed(plan, initial, bits)
+    finally:
+        del exact_module.__dict__[HOOK]
+    need(observed_result == original_result, "observed and unmodified source results/statistics agree")
+    event_index = 0
+    for layer, (before, after) in zip(plan, boundaries):
+        written = set()
+        exact_after = linear(layer, before)
+        layer_residual = minus(after, exact_after)
+        for ids, _ in layer:
+            for wire in ids:
+                need(event_index < len(events), "source write observation present")
+                actual, recorded_wire, recorded_ids = events[event_index]
+                need(recorded_wire == wire and recorded_ids == tuple(ids), "source coordinate write order")
+                written.add(wire)
+                splice = tuple(after[i] if i in written else before[i] for i in range(len(before)))
+                need(actual == splice, "every source coordinate write splices layer endpoints")
+                cut_linear = [exact_after[i] if i in written else before[i] for i in range(len(before))]
+                cut_residual = minus(actual, cut_linear)
+                need(cut_residual == [z if i in written else C() for i, z in enumerate(layer_residual)],
+                     "coordinate-write residual is projected original layer residual")
+                residual_check(cut_residual, written, bits)
+                need(all(abs(value.re) <= max(abs(before[i].re), abs(after[i].re))
+                         and abs(value.im) <= max(abs(before[i].im), abs(after[i].im))
+                         for i, value in enumerate(actual)), "coordinate magnitude never exceeds endpoint maximum")
+                for i, value in enumerate(actual):
+                    for part, start, end in zip((value.re, value.im), (before[i].re, before[i].im),
+                                                (after[i].re, after[i].im)):
+                        grid, first, last = (x * (1 << bits) for x in (part, start, end))
+                        need(grid.denominator == first.denominator == last.denominator == 1,
+                             "coordinate writes preserve original data grid")
+                        need(abs(grid.numerator).bit_length()
+                             <= max(abs(first.numerator).bit_length(), abs(last.numerator).bit_length()),
+                             "grid numerator width never exceeds endpoint width")
+                need(norm2(actual) <= norm2(before) + norm2(after), "write-cut Euclidean splice envelope")
+                event_index += 1
+    need(event_index == len(events), "every observed source write checked")
+    return events
+
+
+def check_plan(label, plan, initial, bits, exact_module, observed):
+    n = len(initial)
+    need(all((part * (1 << bits)).denominator == 1 for z in initial for part in (z.re, z.im)),
+         "input on declared data grid")
+    current, exact_path, accumulated = list(initial), list(initial), [C() for _ in initial]
+    boundaries = []
+    permutation_count = prefix_count = nonzero_residuals = signed_ties = 0
+    max_residual_component = Q()
+    for layer in plan:
+        used = support(layer, n)
+        before = list(current)
+        exact_next = linear(layer, before)
+        after = synchronous(layer, before, bits)
+        residual = minus(after, exact_next)
+        residual_check(residual, used, bits)
+        nonzero_residuals += int(any(x != 0 for x in residual))
+        max_residual_component = max(max_residual_component,
+                                     *(abs(part) for z in residual for part in (z.re, z.im)))
+        signed_ties += sum((part * (1 << bits)).denominator == 2
+                           for i in used for part in (exact_next[i].re, exact_next[i].im))
+        for permutation in itertools.permutations(layer):
+            permutation_count += 1
+            serial_plan = [[gate] for gate in permutation]
+            serial, stats = exact_module.apply(serial_plan, before, bits)
+            need(serial == after, "all gate permutations preserve rounded layer endpoint")
+            need(stats["rounded_outputs"] == len(used), "one source rounding per touched output")
+            for k in range(len(permutation) + 1):
+                chosen = list(permutation[:k])
+                chosen_support = support(chosen, n)
+                actual, prefix_stats = exact_module.apply(serial_plan[:k], before, bits)
+                expected = synchronous(chosen, before, bits)
+                selected_residual = [z if i in chosen_support else C() for i, z in enumerate(residual)]
+                need(actual == expected == plus(linear(chosen, before), selected_residual),
+                     "rounded prefix equals exact partial layer plus projected realized residual")
+                need(prefix_stats["rounded_outputs"] == len(chosen_support), "prefix rounding count")
+                residual_check(minus(actual, linear(chosen, before)), chosen_support, bits)
+                prefix_count += 1
+        exact_path = linear(layer, exact_path)
+        accumulated = plus(linear(layer, accumulated), residual)
+        need(minus(after, exact_path) == accumulated, "layer-grouped realized error recurrence")
+        current = after
+        boundaries.append((before, after))
+    original_result = exact_module.apply(plan, initial, bits)
+    need(original_result[0] == current, "independent synchronous oracle equals complete unmodified apply")
+    writes = trace_writes(exact_module, observed, plan, initial, bits, boundaries, original_result)
+    need(original_result[1]["rounded_outputs"] == len(writes), "full source output-rounding count")
+    return {"label": label, "dimension": n, "bits": bits, "layers": len(plan),
+            "gates": sum(len(layer) for layer in plan), "permutation_orders": permutation_count,
+            "rounded_gate_prefixes": prefix_count, "source_coordinate_writes": len(writes),
+            "nonzero_layer_residuals": nonzero_residuals, "halfway_components": signed_ties,
+            "max_component_residual_in_grid_units": str(max_residual_component * (1 << bits))}
+
+
+def controls(exact_module, observed):
+    bits, u = 3, Q(1, 8)
+    controls_out = []
+    state = [C(1), C(2)]
+    gate = [[C(1), C(1)], [C(1), C(-1)]]
+    correct = synchronous([((0, 1), gate)], state, bits)
+    overwritten = list(state)
+    for i, row in enumerate(gate):
+        overwritten[i] = rounded_z(sum((a * z for a, z in zip(row, overwritten)), C()), bits)
+    need(correct == [C(3), C(-1)] and overwritten == [C(3), C(1)], "sequential-overwrite witness")
+    controls_out.append(reject(lambda: need(overwritten == correct, "mutant differs"), "sequential-overwrite-inside-two-wire-gate"))
+    halfgate = [[C(Q(1, 2)), C(Q(1, 2))], [C(Q(1, 2)), C(Q(-1, 2))]]
+    pair = [C(u), C(u)]
+    termwise = [sum((rounded_z(a * z, bits) for a, z in zip(row, pair)), C()) for row in halfgate]
+    linear_pair = linear([((0, 1), halfgate)], pair)
+    need(synchronous([((0, 1), halfgate)], pair, bits) == [C(u), C()], "whole-output rounding witness")
+    need(termwise[0] == C(2 * u), "extra product-rounding event witness")
+    controls_out.append(reject(lambda: residual_check(minus(termwise, linear_pair), {0, 1}, bits), "rounding-each-product-exceeds-layer-budget"))
+    a, b = ((0,), [[C(Q(1, 2))]]), ((0,), [[C(Q(3, 2))]])
+    controls_out.append(reject(lambda: support([a, b], 1), "overlapping-support-oracle-rejects"))
+    controls_out.append(reject(lambda: exact_module.apply([[a, b]], [C(u)], bits), "overlapping-support-source-rejects"))
+    ab, _ = exact_module.apply([[a], [b]], [C(u)], bits)
+    ba, _ = exact_module.apply([[b], [a]], [C(u)], bits)
+    need(ab == [C(2 * u)] and ba == [C(u)], "overlap can destroy rounded commutation")
+    controls_out.append("overlap-order-dependence-witness")
+    controls_out.append(reject(lambda: residual_check([C(), C(u / 4)], {0}, bits), "residual-leakage-on-idle-wire"))
+    # Residuals are functions of actual rounded inputs, never fixed on the exact path.
+    first = synchronous([a], [C(u)], bits)
+    actual_second = synchronous([a], first, bits)
+    actual_r1 = minus(first, linear([a], [C(u)]))
+    actual_r2 = minus(actual_second, linear([a], first))
+    exact_first = linear([a], [C(u)])
+    stale_r2 = minus(synchronous([a], exact_first, bits), linear([a], exact_first))
+    need(actual_r1 == actual_r2 == [C(u / 2)] and stale_r2 == [C(-u / 4)], "data-dependent residual witness")
+    stale_prediction = plus(plus(linear([a], exact_first), linear([a], actual_r1)), stale_r2)
+    controls_out.append(reject(lambda: need(stale_prediction == actual_second, "stale residual invalid"), "residual-computed-on-exact-instead-of-rounded-input"))
+    swap = [[((0, 1), [[C(), C(1)], [C(1), C()]])]]
+    snapshots = []
+    for initial in ([C(), C(1)], [C(1), C(1)]):
+        final_result = exact_module.apply(swap, initial, bits)
+        events = trace_writes(exact_module, observed, swap, initial, bits,
+                              [(initial, synchronous(swap[0], initial, bits))], final_result)
+        snapshots.append(events[0][0])
+    need(snapshots[0] == snapshots[1] == (C(1), C(1)), "noninjective proper write-cut witness")
+    need(norm2(snapshots[0]) == 2 and norm2([C(), C(1)]) == 1, "Euclidean amplification at a source write")
+    return controls_out, {"input": [["0", "0"], ["1", "0"]],
+                          "first_write_state": [["1", "0"], ["1", "0"]],
+                          "input_squared_norm": "1", "first_write_squared_norm": "2",
+                          "component_magnitude_bound": "1", "noninjective": True,
+                          "extra_observed_source_writes": 4}
+
+
+def main():
+    global C
+    manifest = json.loads((HERE / "SOURCES.json").read_text())
+    raw = {}
+    for row in manifest["files"]:
+        if row["usage"] == "input":
+            contents = (ROOT / row["path"]).read_bytes()
+            need(sha256(contents).hexdigest() == row["sha256"], "authenticated source: " + row["path"])
+            raw[row["path"]] = contents
+    need({EXACT, ENGINE, ORACLE, CIRCUIT, SOURCE_MANIFEST}.issubset(raw), "complete runtime source closure")
+    child_sources = {row["path"]: row["sha256"] for row in json.loads(raw[SOURCE_MANIFEST])["files"]}
+    need(all(child_sources[path] == sha256(raw[path]).hexdigest() for path in (ORACLE, CIRCUIT)),
+         "retained Builder input authentication")
+    sys.path.insert(0, str(ROOT / "research/rational-unitary-fft"))
+    import exact
+    from engine import Builder, Phases
+    C = exact.C
+    observed, observation_evidence = instrument(exact, raw[EXACT])
+    cases = []
+    bits, u = 3, Q(1, 8)
+    for numerator, expected in zip((-5, -3, -1, 1, 3, 5), (-2, -1, 0, 1, 2, 3)):
+        value = Q(numerator, 2) * u
+        need(rounded_q(value, bits) == expected * u, "signed half-grid tie convention")
+        plan = [[((0,), [[C(value, -value)]])]]
+        cases.append(check_plan("signed-complex-half-tie-" + str(numerator), plan, [C(1)], bits, exact, observed))
+    plan = [
+        [((0, 2), [[C(Q(1, 2)), C(Q(1, 2))], [C(Q(1, 2)), C(Q(-1, 2))]]),
+         ((3,), [[C(Q(1, 3), Q(1, 5))]])],
+        [((0, 1), [[C(1), C(0, Q(1, 2))], [C(Q(-1, 3)), C(1)]]),
+         ((2,), [[C(Q(2, 3))]]), ((3,), [[C(Q(3, 2), Q(-1, 4))]])],
+        [],
+    ]
+    initial = [C(u, u), C(-2 * u, u), C(u, -u), C(3 * u, 2 * u), C(-u)]
+    cases.append(check_plan("mixed-scalar-two-wire-complex-with-idle-and-empty-layer", plan, initial, bits, exact, observed))
+    half = ((0,), [[C(Q(1, 2))]])
+    cases.append(check_plan("data-dependent-two-layer-half-rounding", [[half], [half]], [C(u)], bits, exact, observed))
+    builder = Builder(Phases(10, raw[ORACLE]), 10, raw[CIRCUIT])
+    toeplitz = exact.Mat([[C(Q(1, 2)), C(Q(1, 4), Q(1, 8))],
+                         [C(Q(-1, 8), Q(1, 16)), C(Q(1, 2))]])
+    actual_plan = builder.plan(toeplitz)
+    actual_inputs = [[C(3 * u, u), C(-2 * u, 3 * u), C(5 * u, -2 * u), C(-u, -4 * u)],
+                     [C(u), C(), C(-2 * u, u), C(3 * u, -u)]]
+    for i, initial in enumerate(actual_inputs):
+        cases.append(check_plan("actual-Builder-Toeplitz-shear-n2-input" + str(i), actual_plan, initial,
+                                bits, exact, observed))
+    negative_controls, write_witness = controls(exact, observed)
+    need(any(case["nonzero_layer_residuals"] >= 2 for case in cases), "multiple realized nonzero residuals exercised")
+    result = {"status": "PASS_MATCHING_LAYER_ROUNDING", "schema_version": 1,
+              "arithmetic": "exact Gaussian rationals; independent integer-divmod rounding",
+              "sources_authenticated": len(raw), "cases": cases,
+              "total_permutation_orders": sum(c["permutation_orders"] for c in cases),
+              "total_rounded_gate_prefixes": sum(c["rounded_gate_prefixes"] for c in cases),
+              "total_source_coordinate_writes": sum(c["source_coordinate_writes"] for c in cases) + 4,
+              "observation": observation_evidence, "controls": negative_controls,
+              "write_cut_singular_witness": write_witness,
+              "Builder_source_ast_sha256": builder.original_ast,
+              "Builder_adapted_ast_sha256": builder.adapted_ast,
+              "scope": "Finite source-bound evidence for layer-grouped residuals and coordinate-write splices; no physical-tape execution, all-size proof-kernel acceptance, or inverse contract inside a gate."}
+    print(json.dumps(result, sort_keys=True, indent=2))
+
+
+if __name__ == "__main__":
+    main()