diff --git a/research/schur-boundary-residual/PROOF.md b/research/schur-boundary-residual/PROOF.md
new file mode 100644
index 0000000000..02c7657c40
--- /dev/null
+++ b/research/schur-boundary-residual/PROOF.md
@@ -0,0 +1,268 @@
+# The actual scalar boundary solve against the original Schur matrix
+
+This independently audits one implication in Jose Manuel / `jmbarrancoml`'s
+[PR3851 physical Gaussian core](../physical-gaussian-core/PROOF.md), retained
+at `7ab67b4a84d28cd562b9711aa315ca5b47822b37`. It addresses a sub-obligation
+of [PR5081's local-defect handoff](../tensor-compression-error-refinement/README.md):
+the unchanged scalar `BandedSolve` compared with the **original** old-H
+Schur matrix. It does not prove the complete Core approximation theorem.
+
+Two setup perturbations must remain distinct. `Window.prepare_schur` first
+rounds the exact Schur matrix and computes exact LU of that rounded matrix.
+`prepare_bands` then rounds the strict triangular factors and the **pivot
+reciprocals**. The online upper diagonal is consequently the inverse of a
+stored reciprocal. It is not the rounded original upper diagonal.
+
+## 1. Quantified statement and inherited premises
+
+For a complex vector use `||v||_infinity=max_i |v_i|`, where `|.|` is complex
+modulus; for a matrix use the induced row-sum norm `max_i sum_j |M_ij|`.
+The matrices in this caller are real, but right-hand sides may be complex.
+All rounding below acts separately on real and imaginary components.
+`BandedSolve` is a scalar owner: the complex statement pairs its two real
+component executions with the same factors, as in `Core.scalar`.
+
+Let `p>=101` be an integer, `P=32768p`, and `eta=2^-P`. Let `H` be the
+source's finite global real old-H matrix with positive diagonal and row gap
+
+```text
+H_ii - sum_(j!=i) |H_ij| >= 1/(8p).
+```
+
+Let `H_W` be an admitted principal window, partitioned into interior `I`
+and nonempty boundary `B`. Empty `I` is allowed. Define the exact reference
+
+```text
+S = H_BB - H_BI H_II^-1 H_IB,
+Sbar = round_P(S),       Sbar = L U.
+```
+
+The following source premises are retained, rather than inferred from a
+successful parse or finite execution:
+
+1. The page is produced from this original `H_W` and this exact `S`.
+   Its boundary order has half-bandwidth `b=2w<=2p`, and exact no-pivot
+   LU of `Sbar` has unit lower diagonal, positive upper pivots, and the
+   same half-bandwidth. The source's stored zero padding preserves it.
+2. These exact factors satisfy `||L||<=65p^2` and `||U||<2`.
+   These are the retained factor-growth caps for `LU(round_P(S))`, not
+   caps assumed for an unrelated factorization of `S`.
+3. Signed records, exact products and complete dot products implement their
+   stated arithmetic before truncation, and the invocation satisfies its
+   storage/width, ownership and extent contracts. We analyze unbounded
+   integer arithmetic first; this note does not prove full-Core headroom.
+
+The global gap itself, matching coefficient/old-H production, bandwidth,
+positive pivots and factor caps are inherited analytic/setup obligations.
+We derive the inverse estimates used below from these premises. Neither
+`||L^-1||` nor `||U^-1||` is an additional premise for this argument.
+
+For every represented complex P-grid right-hand side `r` satisfying premise3,
+let `x` be the actual two-pass boundary return in physical value units.
+Then, with `R=max(1,||r||)`,
+
+```text
+||x - S^-1 r|| < 2^17 p^5 eta R.                           (1)
+```
+
+The constant is independent of `|B|`, the number of cells and the number
+of completed rows. This recovers the explicit noncyclic allowance in the retained
+[RaD phase-cell report](../../references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md);
+it is not a new precision policy or a cost saving.
+
+## 2. The exact reference has inverse norm at most 8p
+
+Restricting a row to a principal set only removes off-diagonal absolute
+values, so both `H_W` and a nonempty `H_II` retain the same gap. For any
+complex vector `v`, choose `i` with `|v_i|=||v||`. The reverse triangle
+inequality gives
+
+```text
+|(H_W v)_i| >= (H_ii - sum_(j!=i,j in W)|H_ij|) ||v||
+             >= ||v||/(8p).
+```
+
+Thus `H_W` and `H_II` are invertible, with inverse norm at most `8p`.
+The exact block inverse identity says `(H_W^-1)_BB=S^-1`. Equivalently,
+solve `H_W z=(0,r_B)` and eliminate `z_I`; its boundary equation is
+`S z_B=r_B`. Boundary injection and restriction both have norm one, hence
+
+```text
+||S^-1|| <= ||H_W^-1|| <= 8p.                              (2)
+```
+
+For empty `I`, `S=H_W` and the conclusion is immediate. This argument
+does not replace the old-H inverse by the local q-model inverse.
+
+## 3. Both setup roundings and the effective upper diagonal
+
+Write `tau_P` for truncation toward zero to the eta grid. The actual
+`Rational.rounded` computes that operation. Each real entry moves by less
+than `eta`. A row of `S` has at most `2b+1<=4p+1<=5p` nonzero positions;
+zero entries stay zero. Therefore
+
+```text
+E0 = Sbar-S,             ||E0|| < 5p eta.                  (3)
+```
+
+In `prepare_bands`, let `Lhat` have exact unit diagonal and rounded strict
+lower entries; let `uhat_ij=tau_P(U_ij)` for `j>i`. For every pivot put
+
+```text
+q_i=1/U_ii,       qhat_i=tau_P(q_i),
+(Ueff)_ii=1/qhat_i,       (Ueff)_ij=uhat_ij for j>i.
+```
+
+Since `0<U_ii<2`, `q_i>1/2`. Also `eta<=1/4`, so `qhat_i>1/4` is positive.
+The effective diagonal satisfies
+
+```text
+|1/qhat_i-U_ii| = U_ii |q_i-qhat_i|/qhat_i < 8 eta.
+```
+
+This explicitly prices reciprocal rounding. Counting the band entries gives
+
+```text
+DL=Lhat-L,       ||DL|| < 2p eta,
+DU=Ueff-U,       ||DU|| < (2p+8)eta <= 3p eta,
+||Lhat|| <= 65p^2+2p eta <= 66p^2.                         (4)
+```
+
+For `T=Lhat Ueff`, expand the product rather than multiplying rounded
+inverse bounds:
+
+```text
+E1=T-Sbar = DL U + L DU + DL DU,
+||E1|| < (4p+195p^3)eta+6p^2 eta^2 < 200p^3 eta.           (5)
+```
+
+The final inequality uses `p>=101`, `4p<=4p^3`, and `6eta<p`; it follows
+for every stated p, not from a sampled precision table. Combining (3),(5),
+
+```text
+||T-S|| < (200p^3+5p)eta <= 205p^3 eta.                   (6)
+```
+
+Here is a separate Neumann step for each setup perturbation. For every
+positive integer p, `p<=2^p`. Consequently
+
+```text
+40p^2 eta < 2^(6-32766p) < 1/2,
+3200p^4 eta < 2^(12-32764p) < 1/2.
+```
+
+Equations (2),(3) therefore give `||Sbar^-1||<=16p`; equations (5) and
+that bound give
+
+```text
+||T^-1|| <= 32p.                                         (7)
+```
+
+Thus the source's product-inverse bound concerns the effective factor
+product actually solved online. It incorporates the initial Schur rounding,
+not just rounding of factors from an assumed exact `S`.
+
+## 4. Exact residual of the executed two-pass program
+
+The row order and rounding sites in `gaussian_boundary.py` are:
+
+```text
+y_i = tau_P(r_i - sum_(j<i) Lhat_ij y_j),
+x_i = tau_P(qhat_i (y_i - sum_(j>i) uhat_ij x_j)).
+```
+
+The first pass runs forward; the second runs backward with its stored
+future-value buffer. `subtract_row` accumulates the full dot product exactly
+on the 2P grid. The upper pass multiplies this **unrounded** residual by
+the stored reciprocal, then truncates from the 3P grid to the P grid.
+There is no intermediate upper-residual truncation. These are statements
+about the unchanged source, not a replacement evaluation order.
+
+Define residuals at these actual computed states:
+
+```text
+e_f = Lhat y-r,           e_b = Ueff x-y.
+```
+
+Each real and imaginary component of `e_f` has absolute value below `eta`, so
+`||e_f||<sqrt(2)eta<2eta`. If `epsilon_i` is the final upper truncation
+error, each of its real/imaginary components is below `eta`, and
+`(e_b)_i=epsilon_i/qhat_i`. Hence
+
+```text
+||e_b|| < 4sqrt(2)eta < 8eta.
+```
+
+In particular `e_b` is not just the final truncation error. The reciprocal
+conversion is necessary even when the stored reciprocal is exact.
+Substitution gives the exact completed residual identity
+
+```text
+rho = T x-r = e_f + Lhat e_b.                             (8)
+```
+
+By (4),
+
+```text
+||rho|| < (2+528p^2)eta <= 530p^2 eta.                    (9)
+```
+
+This is a maximum over rows. No factor proportional to the number of rows
+appears. Neither the computed solver nor its individual rounded passes are
+assumed linear, Lipschitz, or exact inverses of one another.
+
+## 5. Error against the original old-H Schur system
+
+Let `v=S^-1 r`. From (8) obtain the identity
+
+```text
+x-v = T^-1 [rho-(T-S)v].                                 (10)
+```
+
+The error has two independent sources: the completed online residual and
+both setup perturbations. Using (2),(6),(7),(9) in (10) yields
+
+```text
+||x-v|| < 32p [530p^2 eta + 205p^3 eta (8p||r||)]
+         = 16960p^3 eta + 52480p^5 eta ||r||
+         <= 69440p^5 eta max(1,||r||)
+         < 131072p^5 eta max(1,||r||).
+```
+
+This proves (1), including `r=0`; no strict inequality is inferred from a
+zero input-scaled term. The larger `max(1,||r||)` allowance is intentional.
+The right-hand side may already contain errors from Core's first interior
+pass. The theorem compares with `S^-1` on **that same actual r**. Transport
+of its earlier error is a separate completed-Core obligation.
+
+## Evidence, attribution and remaining obligations
+
+Finite evidence should check the actual rounded-factor serialization,
+forward and backward values, (8) and (10), and distinguish initial Schur
+rounding from factor rounding. A reduced page is arithmetic conformance
+evidence; it does not establish the global gap, factor caps or production
+admission. The package receipt records the particular observations and
+controls actually run. Those observations do not prove the quantified
+inequalities above, and their observed error is not a fitted bound.
+
+Credit Jose Manuel / `jmbarrancoml` for the unchanged PR3851 producer/solver
+and its claimed scalar error allowance; Chafik Boukhalfa / PR489 and the
+retained RaD (`hipotures`), Gaussian, word and manuscript lineage; and
+James Reed's [factor-perturbation-margin](../factor-perturbation-margin/README.md)
+for the already-covered scalar perturbation/growth comparisons. That note
+explicitly leaves the product-inverse cap and actual Core outside its scope.
+JoyboyBrian's PR5081 identifies the local-defect handoff, and
+[PR5059](../physical-boundary-pages/README.md) explicitly separates original
+S from `LU(round(S))`. Its inverse-block ABI is different and is not installed
+here. The #4100 uniform-transfer discussion supplies broader motivation,
+not the definition of this scalar program or a newly accepted global premise.
+
+This note retains exact primitive and stored-width correctness; original
+Gaussian coefficient, global gap, bandwidth and factor-growth proofs;
+the interior q-model/old-H comparison; both interior applications and
+coupling errors; locality, H-to-N resolvent and normalization; tensor/chirp,
+CRT recovery, all physical costs and complete supplier admission. It proves
+one conditional scalar boundary bridge, not all of #5081 OQ1 or the complete
+multiplication theorem. No selected-frontier, algorithm or precision change
+is made. Prepared by Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex
+assistance. Apache-2.0; no independent human or proof-kernel acceptance claimed.
diff --git a/research/schur-boundary-residual/README.md b/research/schur-boundary-residual/README.md
new file mode 100644
index 0000000000..6d0b3a230a
--- /dev/null
+++ b/research/schur-boundary-residual/README.md
@@ -0,0 +1,121 @@
+# Actual scalar boundary solve against the original Schur matrix
+
+This closes one conditional implication in the unchanged PR3851 Gaussian
+boundary solver: the stored reciprocal pivots and the initial Schur rounding
+both enter the error against the **original** old-H Schur system. It supplies
+the product-inverse bridge explicitly excluded by `factor-perturbation-margin`
+and a narrow part of PR5081's local Core defect handoff. No new κ is claimed.
+
+For integer `p>=101`, `P=32768p`, `eta=2^-P`, the [proof](PROOF.md) derives
+
+```text
+T = Lhat Ueff,    Ueff_ii = 1/round_P(1/U_ii),
+T x-r = e_f + Lhat e_b,
+||T^-1||_infinity <= 32p,
+||x-S^-1 r||_infinity < 2^17 p^5 eta max(1,||r||_infinity).
+```
+
+The constants do not grow with the boundary dimension. `S` is the original
+Schur matrix; exact `L U` factors `round_P(S)`. The upper pass multiplies its
+complete unrounded dot-product residual by the stored reciprocal and rounds
+once. Substituting a rounded upper diagonal or rounding that residual early
+analyzes a different program.
+
+The theorem retains the original old-H row gap, matching source/page,
+bandwidth, positive pivots, exact factor caps for `LU(round_P(S))`, primitive
+arithmetic and adequate record widths. It derives both inverse bounds rather
+than assuming the published product-inverse cap. These premises are not
+certified by a successful finite replay.
+
+## Evidence and reproduction
+
+[fixture.py](fixture.py) executes the authenticated source producer and scalar
+solver, with independent rational reconstruction and observation of computed
+states. [RESULT.json](RESULT.json) records the complete deterministic result.
+The page crosses a physical period and has eight source rows, three eliminated
+interior rows and five boundary rows. Two scalar calls execute 20 boundary truncations
+and 50 exact multiplication calls in total. Both components distinguish all
+three semantic controls, and borrowed ports and scratch are restored. The
+finite parameters `s=13,t=14,u=w=1,p=16,P=24` are reduced calibration
+parameters, outside the production theorem. [verify.py](verify.py) also isolates the missing initial
+Schur perturbation: a scalar solve has zero online residual but nonzero error
+against the original matrix. A two-row control distinguishes premature upper
+residual truncation. These controls test the claimed mathematical distinctions.
+
+Local environment: CPython 3.12.13, Linux x86_64, standard library only.
+Run from the repository root with Python 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/schur-boundary-residual --check-only
+python3.12 -B scripts/research_package.py --package research/schur-boundary-residual
+python3.12 -I -O -B research/schur-boundary-residual/verify.py
+```
+
+The direct verifier authenticates every declared live input before importing
+source code, uses a fresh bytecode cache, and authenticates the retained nested
+word/branch-free archives. The registered command has a 300-second limit.
+`--write` regenerates the complete receipt; ordinary replay compares every
+field, not only an output digest. Explicit exceptions remain enabled under
+optimized Python. A committed package export supports the same direct command
+outside Git; the generic metadata runner requires Git history.
+
+## Scope, overlap and stopping decision
+
+Base main `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority revision7.
+[TASK.json](TASK.json) preserves the original `uniform-transfer-audit` card,
+refinement, overlap coverage and [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/3664#discussioncomment-19150318).
+[SOURCES.json](SOURCES.json) binds exact live source bytes and historical
+catalogue/selected-record provenance. Full refresh covered 353 open PR bodies,
+4,564 Discussion records and all 7,091 local notes; targeted live checks
+separated this question from the expansion/chirp/compression join, which was
+reported complete conditionally in [Discussion3664](https://github.com/CrocSwap/integer-mult-bounds/discussions/3664#discussioncomment-19150284).
+This is coverage evidence, not proof of novelty or an atomic board snapshot.
+
+The boundary owner borrows factor bands and a dyadic RHS, returns a protected
+solution and restores borrowed ports and scratch. No production algorithm or
+paid cost changes. Its complete physical cost remains inherited; global
+coefficient/interval acceptance, full Core headroom, two interior applications,
+coupling errors, locality, normalization, tensor/chirp and CRT admission remain
+open here. We compared the PR5292 three-register eleven-call question and
+stopped before an unpriced large search. The decision is to narrow this round
+to an existing numerical acceptance gap, then stop at that implication.
+
+## Open next questions
+
+1. Compose the complete old-H local Core defect on its actual computed input.
+   Begin with both interior passes and the rounded coupling RHSs, then apply
+   this boundary estimate and final normalization. This matters because this
+   lemma alone does not close PR5081 OQ1. Interior approximation, coefficient
+   intervals, locality and primitive acceptance remain blockers.
+2. Independently audit the inherited global row gap and exact factor-growth
+   caps for `LU(round_P(S))`. Start at the corresponding source proof and its
+   diagonal-dominant elimination argument, retaining the initial Schur
+   perturbation. The current result is conditional on those analytic premises.
+
+## Credit
+
+Prepared by Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance
+in proof, source audit, checker, coordination and writing. Apache-2.0. This is
+an author-checked conditional argument and finite source replay, with additional
+AI review; it is not independent human or formal-kernel acceptance.
+
+Jose Manuel / `jmbarrancoml` supplied the unchanged physical Gaussian Core,
+[PR3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851), head
+`7ab67b4a84d28cd562b9711aa315ca5b47822b37`, including its finite old-H setup
+checks and claimed scalar allowance. We retain Chafik Boukhalfa's PR489
+branch-free source at `8922e3b3f0fd7772b0fb42028eb2532984c3ab42`, PR3787's
+physical word source at `9b5474f47b0ea9a3c76bb5b1b577fb36704815e0`, and their
+nested notices and full Gaussian/RaD/manuscript lineage. The displayed
+`2^17 p^5 eta` allowance already appears in the retained
+[RaD phase-cell report](../../references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md);
+our contribution is the explicit actual-caller bridge and residual evidence,
+not a new constant. Its LICENSE and NOTICE are declared export inputs. James Reed's
+[factor margin audit](../factor-perturbation-margin/README.md), commit
+`b1d6a2447f8d05d3f859dd278d333e247ee9a8e0`, already covers scalar perturbation
+and growth margins; we do not claim those as new. JoyboyBrian's
+[PR5081](https://github.com/CrocSwap/integer-mult-bounds/pull/5081), head
+`4c49fff7fdfa4ddda6ef615575b6762b3f46f9cd`, requests the local-defect audit.
+PR5059 explicitly separates original `S` from `LU(round(S))`, but uses a
+different block ABI. PR5255 concerns a graph-support resolvent bound and
+excludes Gaussian rounding. Cinna Davis's PR4100 supplies the wider uniform
+transfer context, rather than this scalar solver's definition.
diff --git a/research/schur-boundary-residual/RESULT.json b/research/schur-boundary-residual/RESULT.json
new file mode 100644
index 0000000000..875c0dec01
--- /dev/null
+++ b/research/schur-boundary-residual/RESULT.json
@@ -0,0 +1,1122 @@
+{
+  "algebra": {
+    "early_round_control": {
+      "P": 3,
+      "actual": [
+        "1/8",
+        "1/4"
+      ],
+      "mutant": [
+        "0",
+        "1/4"
+      ]
+    },
+    "neumann_envelopes": [
+      "40 p^2 eta < 2^(6-32766p) < 1/2",
+      "3200 p^4 eta < 2^(12-32764p) < 1/2"
+    ],
+    "original_S_error_constant": 69440,
+    "reported_allowance": "2^17 p^5 eta max(1,||r||_infinity)",
+    "scalar_omission_control": {
+      "P": 8,
+      "online_residual": "0",
+      "original_error": "1/769"
+    },
+    "scope": "Exact scalar controls and arithmetic of the written proof; no finite test establishes the analytic premises.",
+    "uniform_domain": "integer p >= 101, P=32768p; explicit source premises in PROOF.md"
+  },
+  "physical": {
+    "all_cleanup_checks": true,
+    "bank_sha256": [
+      "66e2c4ace0c351f5e209922814dc8785319b8b1bee82bae01e0f968393a130ab",
+      "60354c09073b2a837b8c83f10032d578b82e1c760bfcb82009ec8369ed78a15d"
+    ],
+    "banks_bound_to_page_suffix": true,
+    "compiled_page_sha256": "b1c55482a25953a866ad87f974208b0c6ecbbce89c5f449d9b341c1d5dcf0d81",
+    "components": [
+      {
+        "backward_residual": [
+          [
+            869857,
+            17592186044416
+          ],
+          [
+            -549035601731,
+            295488208426196008960
+          ],
+          [
+            -29156201412463,
+            1181954381817155944448
+          ],
+          [
+            58165,
+            1007591358464
+          ],
+          [
+            -2759767,
+            46966650175488
+          ]
+        ],
+        "borrowed_restored": true,
+        "early_rounding_output": [
+          [
+            -6349727,
+            16777216
+          ],
+          [
+            512623,
+            16777216
+          ],
+          [
+            66965,
+            131072
+          ],
+          [
+            -2213925,
+            8388608
+          ],
+          [
+            787269,
+            4194304
+          ]
+        ],
+        "early_rounding_rejected": true,
+        "effective_residual": [
+          [
+            869857,
+            17592186044416
+          ],
+          [
+            -16579996622295413451,
+            309841843638706906291240960
+          ],
+          [
+            -838247851912897921489949,
+            14784897538945224220133933711360
+          ],
+          [
+            1023237213449685190308431147,
+            9527416169741003991418345908862976
+          ],
+          [
+            -594769582759,
+            5641363960841109504
+          ]
+        ],
+        "factor_rounding_contribution": [
+          [
+            0,
+            1
+          ],
+          [
+            358124634887408949,
+            309841843638706906291240960
+          ],
+          [
+            430430036797568701096931,
+            14784897538945224220133933711360
+          ],
+          [
+            -63717566371901315751443157,
+            9527416169741003991418345908862976
+          ],
+          [
+            -169468021731773153,
+            47323190852823417914130432
+          ]
+        ],
+        "first_rounding_contribution": [
+          [
+            -1633989,
+            28534525764042752
+          ],
+          [
+            1808883547111,
+            200332214849438220288
+          ],
+          [
+            -21754481,
+            14267262882021376
+          ],
+          [
+            61672075214047368628538377056625,
+            6518770129509936191132799756516068425728
+          ],
+          [
+            -2520930330009285601628661978195,
+            409122283583321191122870252239895658496
+          ]
+        ],
+        "forward": [
+          [
+            -3,
+            8
+          ],
+          [
+            556159,
+            8388608
+          ],
+          [
+            4185147,
+            8388608
+          ],
+          [
+            -552205,
+            2097152
+          ],
+          [
+            1572723,
+            8388608
+          ]
+        ],
+        "forward_residual": [
+          [
+            0,
+            1
+          ],
+          [
+            -7,
+            134217728
+          ],
+          [
+            -17591,
+            549755813888
+          ],
+          [
+            7083409,
+            140737488355328
+          ],
+          [
+            -410481,
+            8796093022208
+          ]
+        ],
+        "max_solution_error": [
+          80768952984869630666252208384829749843709090493964731744319594531707,
+          754187490330013135406506853482649488596568144080839138468278647785571483648
+        ],
+        "multiply_calls": 25,
+        "original_residual": [
+          [
+            1412542043,
+            28534525764042752
+          ],
+          [
+            -12760442920081,
+            200332214849438220288
+          ],
+          [
+            -9620045391,
+            114138103056171008
+          ],
+          [
+            682035161311721490617363882233487,
+            6518770129509936191132799756516068425728
+          ],
+          [
+            -39147775446112440173588064005037,
+            409122283583321191122870252239895658496
+          ]
+        ],
+        "output": [
+          [
+            -6349727,
+            16777216
+          ],
+          [
+            32039,
+            1048576
+          ],
+          [
+            8571521,
+            16777216
+          ],
+          [
+            -2213925,
+            8388608
+          ],
+          [
+            787269,
+            4194304
+          ]
+        ],
+        "rhs": [
+          [
+            -3,
+            8
+          ],
+          [
+            1,
+            16
+          ],
+          [
+            1,
+            2
+          ],
+          [
+            -1,
+            4
+          ],
+          [
+            3,
+            16
+          ]
+        ],
+        "solution_error": [
+          [
+            6121901729984876104779870371169189727530064717280988137196686569489,
+            109109399484518741842354939598262929879790642600320184582379351584660258816
+          ],
+          [
+            -2654452708736768909698091616736047179079733807146947677205728807811,
+            45683675046192225988711034743939773276580037087510755459006397746567446528
+          ],
+          [
+            -471887728265211008819973978480078148713134029421565673,
+            5365003334677184856303416440705219410655107225695529694396416
+          ],
+          [
+            80768952984869630666252208384829749843709090493964731744319594531707,
+            754187490330013135406506853482649488596568144080839138468278647785571483648
+          ],
+          [
+            -755682997572135336680439541035952357675651515010261707953206428007,
+            7888883489872479987553228369423163707728656713421451673870544293284806656
+          ]
+        ],
+        "truncate_calls": 10,
+        "wrong_diagonal_residual": [
+          [
+            869857,
+            17592186044416
+          ],
+          [
+            -16480554465699,
+            295147905179352825856
+          ],
+          [
+            -1792825774013,
+            18446744073709551616
+          ],
+          [
+            533831984557615,
+            4722366482869645213696
+          ],
+          [
+            -32209829179527,
+            295147905179352825856
+          ]
+        ]
+      },
+      {
+        "backward_residual": [
+          [
+            13787541,
+            281474976710656
+          ],
+          [
+            -1501696092813,
+            29548820842619600896
+          ],
+          [
+            39747321276769,
+            1181954381817155944448
+          ],
+          [
+            -3795123,
+            141062790184960
+          ],
+          [
+            -412583,
+            35224987631616
+          ]
+        ],
+        "borrowed_restored": true,
+        "early_rounding_output": [
+          [
+            -2180249,
+            8388608
+          ],
+          [
+            1462035,
+            16777216
+          ],
+          [
+            -5273001,
+            16777216
+          ],
+          [
+            70347,
+            8388608
+          ],
+          [
+            1312235,
+            4194304
+          ]
+        ],
+        "early_rounding_rejected": true,
+        "effective_residual": [
+          [
+            13787541,
+            281474976710656
+          ],
+          [
+            -64670910426518176667,
+            991493899643862100131971072
+          ],
+          [
+            9595615111958355601127,
+            134408159444956583819399397376
+          ],
+          [
+            -13197470173310477748365621583,
+            333459565940935139699642106810204160
+          ],
+          [
+            -39971060808367,
+            592343215888316497920
+          ]
+        ],
+        "factor_rounding_contribution": [
+          [
+            0,
+            1
+          ],
+          [
+            3268458756937563237,
+            991493899643862100131971072
+          ],
+          [
+            -2506780686454090930457,
+            134408159444956583819399397376
+          ],
+          [
+            837267472344161664208012977,
+            333459565940935139699642106810204160
+          ],
+          [
+            63598696093875967133,
+            9937870079092917761967390720
+          ]
+        ],
+        "first_rounding_contribution": [
+          [
+            -74563785,
+            456552412224684032
+          ],
+          [
+            402391030707,
+            33388702474906370048
+          ],
+          [
+            -992721765,
+            228276206112342016
+          ],
+          [
+            167537854391924984825193566973455,
+            19556310388529808573398399269548205277184
+          ],
+          [
+            -2015532450771885002193018433039,
+            409122283583321191122870252239895658496
+          ]
+        ],
+        "forward": [
+          [
+            -1,
+            4
+          ],
+          [
+            1091071,
+            16777216
+          ],
+          [
+            -5260843,
+            16777216
+          ],
+          [
+            70185,
+            8388608
+          ],
+          [
+            655361,
+            2097152
+          ]
+        ],
+        "forward_residual": [
+          [
+            0,
+            1
+          ],
+          [
+            -1,
+            67108864
+          ],
+          [
+            42441,
+            1099511627776
+          ],
+          [
+            -3819873,
+            281474976710656
+          ],
+          [
+            -1962179,
+            35184372088832
+          ]
+        ],
+        "max_solution_error": [
+          789810707280372882937034761442779743972215163189402647,
+          8047505002015777284455124661057829115982660838543294541594624
+        ],
+        "multiply_calls": 25,
+        "original_residual": [
+          [
+            22437955287,
+            456552412224684032
+          ],
+          [
+            -2690259251393,
+            33388702474906370048
+          ],
+          [
+            21547195609,
+            228276206112342016
+          ],
+          [
+            -990629208348230403786947662851599,
+            19556310388529808573398399269548205277184
+          ],
+          [
+            -28210091511068257922008314401265,
+            409122283583321191122870252239895658496
+          ]
+        ],
+        "output": [
+          [
+            -2180249,
+            8388608
+          ],
+          [
+            1462035,
+            16777216
+          ],
+          [
+            -2636501,
+            8388608
+          ],
+          [
+            70347,
+            8388608
+          ],
+          [
+            1312235,
+            4194304
+          ]
+        ],
+        "rhs": [
+          [
+            -1,
+            4
+          ],
+          [
+            1,
+            16
+          ],
+          [
+            -5,
+            16
+          ],
+          [
+            0,
+            1
+          ],
+          [
+            5,
+            16
+          ]
+        ],
+        "solution_error": [
+          [
+            9681561424202075763574461665165456141770884707460934738044575882149,
+            163664099226778112763532409397394394819685963900480276873569027376990388224
+          ],
+          [
+            -193069831720569262016888906699216902868875150824015487931665613480029,
+            2192816402217226847458129667709109117275841780200516262032307091835237433344
+          ],
+          [
+            789810707280372882937034761442779743972215163189402647,
+            8047505002015777284455124661057829115982660838543294541594624
+          ],
+          [
+            -120667822576776043410220650481079552307433543648728168793985137202879,
+            2262562470990039406219520560447948465789704432242517415404835943356714450944
+          ],
+          [
+            -1633843857577769272866653250667838770878883320498725866161121983995,
+            23666650469617439962659685108269491123185970140264355021611632879854419968
+          ]
+        ],
+        "truncate_calls": 10,
+        "wrong_diagonal_residual": [
+          [
+            13787541,
+            281474976710656
+          ],
+          [
+            -339362686217407,
+            4722366482869645213696
+          ],
+          [
+            1774007897227,
+            18446744073709551616
+          ],
+          [
+            -2887065106053,
+            73786976294838206464
+          ],
+          [
+            -21736995273527,
+            295147905179352825856
+          ]
+        ]
+      }
+    ],
+    "effective_upper": [
+      [
+        [
+          1,
+          1
+        ],
+        [
+          1907127,
+          16777216
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          1048576,
+          1049785
+        ],
+        [
+          1174949,
+          16777216
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          8388608,
+          8398291
+        ],
+        [
+          725009,
+          16777216
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          16777216,
+          16815995
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          16777216,
+          16796583
+        ]
+      ]
+    ],
+    "factor_rounding_norm": [
+      56748589511775331,
+      881248565849377168424960
+    ],
+    "fixture": {
+      "P": 24,
+      "boundary": [
+        0,
+        1,
+        2,
+        3,
+        7
+      ],
+      "cells": [
+        [
+          0,
+          1,
+          2
+        ],
+        [
+          3,
+          4,
+          5,
+          6,
+          7
+        ]
+      ],
+      "interior": [
+        4,
+        5,
+        6
+      ],
+      "p": 16,
+      "s": 13,
+      "selected": [
+        10,
+        11,
+        12,
+        13,
+        14,
+        15,
+        16,
+        17
+      ],
+      "t": 14,
+      "u": 1,
+      "w": 1,
+      "width": 226,
+      "window": [
+        11,
+        8,
+        12,
+        4
+      ]
+    },
+    "observer_only": true,
+    "original_schur": [
+      [
+        [
+          1,
+          1
+        ],
+        [
+          3093360045,
+          27212644352
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          461755015,
+          45575307264
+        ],
+        [
+          1,
+          1
+        ],
+        [
+          461755015,
+          6593445888
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          223760445,
+          13606322176
+        ],
+        [
+          1,
+          1
+        ],
+        [
+          725009,
+          16777216
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          447135,
+          16777216
+        ],
+        [
+          78954524883583384457951754161,
+          79045667366873540044192219136
+        ],
+        [
+          -64840780035047264642185625,
+          2331293867651201316523361118978048
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          -3099431321837356525270633125,
+          48771176765360974207266599206912
+        ],
+        [
+          78954524883583384457951754161,
+          79045667366873540044192219136
+        ]
+      ]
+    ],
+    "production_precision_claim": false,
+    "rounded_schur": [
+      [
+        [
+          1,
+          1
+        ],
+        [
+          1907127,
+          16777216
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          169981,
+          16777216
+        ],
+        [
+          1,
+          1
+        ],
+        [
+          1174949,
+          16777216
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          137953,
+          8388608
+        ],
+        [
+          1,
+          1
+        ],
+        [
+          725009,
+          16777216
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          447135,
+          16777216
+        ],
+        [
+          16757871,
+          16777216
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          -533,
+          8388608
+        ],
+        [
+          16757871,
+          16777216
+        ]
+      ]
+    ],
+    "schur_rounding_norm": [
+      679,
+      13606322176
+    ],
+    "solution_error_identity": true,
+    "source_calls": 2,
+    "stored_lower": [
+      [
+        [
+          1,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          169981,
+          16777216
+        ],
+        [
+          1,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          1079,
+          65536
+        ],
+        [
+          1,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          447651,
+          16777216
+        ],
+        [
+          1,
+          1
+        ],
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          0,
+          1
+        ],
+        [
+          -267,
+          4194304
+        ],
+        [
+          1,
+          1
+        ]
+      ]
+    ],
+    "stored_reciprocals": [
+      [
+        1,
+        1
+      ],
+      [
+        1049785,
+        1048576
+      ],
+      [
+        8398291,
+        8388608
+      ],
+      [
+        16815995,
+        16777216
+      ],
+      [
+        16796583,
+        16777216
+      ]
+    ]
+  },
+  "source_inputs": 24,
+  "status": "PASS_SCHUR_BOUNDARY_RESIDUAL"
+}
diff --git a/research/schur-boundary-residual/SOURCES.json b/research/schur-boundary-residual/SOURCES.json
new file mode 100644
index 0000000000..64a4836f93
--- /dev/null
+++ b/research/schur-boundary-residual/SOURCES.json
@@ -0,0 +1,162 @@
+{
+  "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": "references/semantic-bulk/rad20/LICENSE",
+      "usage": "input",
+      "git_blob": "0e259d42c996742e9e3cba14c677129b2c1b6311",
+      "sha256": "a2010f343487d3f7618affe54f789f5487602331c0a8d03f49e9a7c547cf0499"
+    },
+    {
+      "path": "references/semantic-bulk/rad20/NOTICE",
+      "usage": "input",
+      "git_blob": "544634f5f3001c50330413f22dc0070e07c46738",
+      "sha256": "82fc72aff49769ae82a8ce886846d9bd0601827a09c955042d26a61177d14369"
+    },
+    {
+      "path": "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md",
+      "usage": "input",
+      "git_blob": "d72345a0aa748443c4efcddf87aa10d524664841",
+      "sha256": "3cdf492bcb719db4295658604dc202d6a2c5a008b87de43ec54f0107c64db730"
+    },
+    {
+      "path": "research/factor-perturbation-margin/README.md",
+      "usage": "input",
+      "git_blob": "3068149c467d73b7e7c57668e33fec8fd3125bfa",
+      "sha256": "5c3d392da8e396a0fa7f9b23ccd491c0de54f1d78bc95b88434f68986571503a"
+    },
+    {
+      "path": "research/physical-gaussian-core/PROOF.md",
+      "usage": "input",
+      "git_blob": "883c8d4a6f0eead888fb3532b60db41596940889",
+      "sha256": "e909026dd3f455c35ff28210a0c4ffa232ad8d7633174e481094fd09e2469d7a"
+    },
+    {
+      "path": "research/physical-gaussian-core/README.md",
+      "usage": "input",
+      "git_blob": "94caa778ca1eedcbbb3953db5cb215d3206ec0b6",
+      "sha256": "ce063e3796bdcea206959918915826ae75c1bcbd74736913e5b330aa04fb5791"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_axis.py",
+      "usage": "input",
+      "git_blob": "edc443a7281e83536a00e9f9fa950d7d854705a3",
+      "sha256": "d416918d7442c5033e43fba94ccc5ed33badc3aebe90ddd479b0b6c020de9724"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_boundary.py",
+      "usage": "input",
+      "git_blob": "840b90a239a3d76fd42dffc8cdbd7857f7173bad",
+      "sha256": "02303c11978baa4cbc707afb116b8cdb3314dbb2246fa4fe54dafc585d3e5122"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_check_boundary.py",
+      "usage": "input",
+      "git_blob": "cef86647bca8aef22ba2ed717d0559c9c02e8847",
+      "sha256": "c526df6d0f58ab645ffa24df198e528fd1b91848606f8fcfe90cfa38d44ce05a"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_check_window.py",
+      "usage": "input",
+      "git_blob": "f6a28a04a5f5966464b9a6d8e7fda1871b7062bf",
+      "sha256": "34713e5b89ff3ca28621c2ee4dae2c72468407189a37a583fad8210de2a8aaea"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_convolution.py",
+      "usage": "input",
+      "git_blob": "611c6c6d4ab04e404e17dff6d2e0b65d5383546d",
+      "sha256": "57fc34acfef9921d805c8c3bdcd0227e67c2ba6b5114c1b373446680e29e3210"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_core.py",
+      "usage": "input",
+      "git_blob": "373dbaaca689e1e5834ecf571af1de37b669587f",
+      "sha256": "4b5011528a0aedbfa6a7ff577cee2690581b38544cba301120eaf68e7491b9c7"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_exponentials.py",
+      "usage": "input",
+      "git_blob": "8f0f32d7090554b47c112142e300c88fb8e5db4d",
+      "sha256": "f7a27cacbb27c0cfa4a63054e83feba2beae91b3fa9d3c37f903620b3899e67b"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_interior.py",
+      "usage": "input",
+      "git_blob": "8c7fed2531e69967958096cbb3602dbc9be79734",
+      "sha256": "38ffb65cbb40a60ac8d9b45665e752abc34dd2bf403dbc64c89f25a34b7fc2ae"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_matrix.py",
+      "usage": "input",
+      "git_blob": "fc41183a42f5e1af5ea2294c295a0519abbcdb6c",
+      "sha256": "5bb982c6f36083b646bd5a5ab2ea4059c203fa0cc824e9f28132c0f323824bac"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_page.py",
+      "usage": "input",
+      "git_blob": "58877f3e315e53515d4dc022c48b2f379a57bede",
+      "sha256": "001f7be5c70fa7d59c4e4c8d59337eab9c4498003d6686bdb4d97a900eb0b85d"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_prepare.py",
+      "usage": "input",
+      "git_blob": "32e18686b653a09804941f5fd81b715973337aeb",
+      "sha256": "38aa123f80c68f7fcb9e60acae79543cf55f6fd37e12a548cffae11a9b50c1e5"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_rationals.py",
+      "usage": "input",
+      "git_blob": "053404d91c1bef0d4bb0f6647491847bf5879aaf",
+      "sha256": "6f9a380c8c7b4233c3bc338a6206d65cc85bee2e4f5625c2a212065f04f4b73d"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_rows.py",
+      "usage": "input",
+      "git_blob": "4b786bf2774fb317762b6148864f5192292da8e7",
+      "sha256": "821fd15a9b82f182f28055d4b83340e697906203f0728a36dc03196eca13c535"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_sources.py",
+      "usage": "input",
+      "git_blob": "ce521f91997775e189f984ba7dd68a15bf9ecd9b",
+      "sha256": "c5889a97a11a9c6c6c44deb8a2042498ddc3f55703de15269132b8f198e24b15"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_window.py",
+      "usage": "input",
+      "git_blob": "335e0e2d2ee67302a67d1c5ba7c63baecc9b02d8",
+      "sha256": "d10eb4ac559a5dc3ef4a6178ab4cac7dfdcdb5e84ef8acf372bd22c81ab64996"
+    },
+    {
+      "path": "research/physical-gaussian-core/inputs/branchfree-source.tar",
+      "usage": "input",
+      "git_blob": "48dc77f5145d649bfed6745e38ab18b11772d597",
+      "sha256": "e6cdacd59a067189a99bfe03f4448913bb8d518ed4a9b1d981a68c5c666529c7"
+    },
+    {
+      "path": "research/physical-gaussian-core/inputs/word-export.tar",
+      "usage": "input",
+      "git_blob": "885794cf3328941209034ee2d946ed76dbea8ce3",
+      "sha256": "d428e8b6aef4d348fa2e922ca64c4cfd634bbb2f0c150033273e65fcf4600b49"
+    },
+    {
+      "path": "research/tensor-compression-error-refinement/README.md",
+      "usage": "input",
+      "git_blob": "51c76581c835df9d339b1c402bf82d4ede15162f",
+      "sha256": "8aa5f16ca8826ef0de4c07b8639092a85bb59c0dc7b6b6e1daf43099fdef7aa2"
+    }
+  ]
+}
diff --git a/research/schur-boundary-residual/TASK.json b/research/schur-boundary-residual/TASK.json
new file mode 100644
index 0000000000..0c692125a6
--- /dev/null
+++ b/research/schur-boundary-residual/TASK.json
@@ -0,0 +1,104 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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": "Conditional original-Schur error of the unchanged PR3851 scalar BandedSolve, including initial Schur rounding and reciprocal-defined effective upper diagonal",
+  "scope_change_reason": "Take the narrower source-bound boundary-solve obligation within PR5081 OQ1; the broader PR4100 transfer and full Core remain open.",
+  "bottleneck_link": "The computed compression Core requires a uniform defect for its actual rounded boundary solve before downstream tensor/CRT error joins can inherit it.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at this boundary caller: no full Core/interior/locality acceptance, production execution, new arithmetic algorithm or frontier change.",
+  "outcome": "partial",
+  "evidence": "PROOF.md conditional all-size implication; fixture.py actual source-prepared old-H Schur solve with exact rational residual controls; RESULT.json finite receipt.",
+  "author": "Hiroki KUMAZAKI",
+  "ai_assistance": "Substantial OpenAI Codex assistance in source audit, proof, checker, coordination and writing; no independent human or formal-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Compose the complete old-H local Core defect at the executed input",
+      "why_it_matters": "This boundary lemma closes only one consumer inside the two-pass interior/boundary Core.",
+      "first_step": "Combine the two actual interior errors and rounded coupling RHSs with this boundary estimate, retaining source norms and the final normalization.",
+      "blocked_by": "Independent interior approximation, coefficient interval/locality and primitive premises; no production replay is supplied."
+    },
+    {
+      "question": "Independently justify the production global gap and exact rounded-Schur factor caps",
+      "why_it_matters": "The uniform solution estimate is conditional on these inherited analytic bounds.",
+      "first_step": "Audit physical-gaussian-core/PROOF.md sections on old-H dominance and diagonal-dominant elimination, including the perturbation from S to round(S).",
+      "blocked_by": "Analytic/interval premises are retained; this package verifies the downstream implication, not those premises."
+    }
+  ],
+  "coordination": {
+    "canonical": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3664#discussioncomment-19150318",
+    "overlap_coverage": {
+      "local": {
+        "head": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+        "records": 7091,
+        "head_records": 7091,
+        "complete_head_inventory": true,
+        "unsearched_head_paths": []
+      },
+      "open_prs": {
+        "fetched_at": "2026-10-23T16:47:38.713864+00:00",
+        "complete_pagination": true,
+        "records": 353
+      },
+      "discussions": {
+        "fetched_at": "2026-10-23T16:53:49.908792+00:00",
+        "complete_pagination": true,
+        "records": 4564
+      }
+    },
+    "overlap_limits": "Bodies/notes and targeted live tails, not arbitrary code diffs, unpublished work or later activity. The separate Ali Romman downstream Tensor join was reported conditionally complete in Discussion3664 comment19150284; its local Core premises remain inherited.",
+    "family_decision": "Narrow to the explicit product-inverse/initial-Schur-rounding gap; compared the PR5292 three-register eleven-call question and stopped before an unpriced large search."
+  }
+}
diff --git a/research/schur-boundary-residual/VERIFY.json b/research/schur-boundary-residual/VERIFY.json
new file mode 100644
index 0000000000..cb13dae82f
--- /dev/null
+++ b/research/schur-boundary-residual/VERIFY.json
@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "references/semantic-bulk/rad20/LICENSE",
+    "references/semantic-bulk/rad20/NOTICE",
+    "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md",
+    "research/factor-perturbation-margin/README.md",
+    "research/physical-gaussian-core/PROOF.md",
+    "research/physical-gaussian-core/README.md",
+    "research/physical-gaussian-core/gaussian_axis.py",
+    "research/physical-gaussian-core/gaussian_boundary.py",
+    "research/physical-gaussian-core/gaussian_check_boundary.py",
+    "research/physical-gaussian-core/gaussian_check_window.py",
+    "research/physical-gaussian-core/gaussian_convolution.py",
+    "research/physical-gaussian-core/gaussian_core.py",
+    "research/physical-gaussian-core/gaussian_exponentials.py",
+    "research/physical-gaussian-core/gaussian_interior.py",
+    "research/physical-gaussian-core/gaussian_matrix.py",
+    "research/physical-gaussian-core/gaussian_page.py",
+    "research/physical-gaussian-core/gaussian_prepare.py",
+    "research/physical-gaussian-core/gaussian_rationals.py",
+    "research/physical-gaussian-core/gaussian_rows.py",
+    "research/physical-gaussian-core/gaussian_sources.py",
+    "research/physical-gaussian-core/gaussian_window.py",
+    "research/physical-gaussian-core/inputs/branchfree-source.tar",
+    "research/physical-gaussian-core/inputs/word-export.tar",
+    "research/tensor-compression-error-refinement/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Authenticated actual old-H Schur page/BandedSolve, exact residual/error identity and semantic controls; conditional scalar induction margins"
+    }
+  ]
+}
diff --git a/research/schur-boundary-residual/fixture.py b/research/schur-boundary-residual/fixture.py
new file mode 100644
index 0000000000..69a50b6471
--- /dev/null
+++ b/research/schur-boundary-residual/fixture.py
@@ -0,0 +1,373 @@
+"""Finite, observer-only replay of the retained Window/BandedSolve source.
+
+The caller authenticates and opens gaussian_sources before calling run_fixture.
+Raw tape snapshots are decoded only after the protected source call returns.
+No Fraction value is supplied to setup or used to replace runtime arithmetic.
+The small p=16, P=24 fixture does not satisfy the production precision premise.
+"""
+from fractions import Fraction as Q
+from hashlib import sha256
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def tape_bytes(tape):
+    """Observer-only copy, including the physical tape behind a setup lease."""
+    from session import borrowed_tape
+    return bytes(borrowed_tape(tape).cells)
+
+
+def count(raw):
+    require(raw[0] == 2, "observed Count left marker")
+    value, end = field(raw, 1)
+    require(all(x == 4 for x in raw[end:]), "observed Count complete extent")
+    return value
+
+
+def field(raw, pos):
+    start, value = pos, 0
+    while pos < len(raw) and raw[pos] in (0, 1):
+        value += raw[pos] << (pos-start)
+        pos += 1
+    require(pos > start and pos < len(raw) and raw[pos] == 3, "canonical count record")
+    require(pos == start+1 or raw[pos-1] == 1, "canonical count high bit")
+    return value, pos+1
+
+
+def body(raw):
+    require(raw[0] == 2, "observed tape left marker")
+    end = raw.find(bytes([4]), 1)
+    end = len(raw) if end < 0 else end
+    require(all(x == 4 for x in raw[end:]), "observed erased suffix")
+    return raw[1:end]
+
+
+def matrix_snapshot(matrix):
+    return (tape_bytes(matrix.rows.tape), tape_bytes(matrix.columns.tape), tape_bytes(matrix.current))
+
+
+def matrix(snapshot):
+    rows, columns = count(snapshot[0]), count(snapshot[1])
+    raw, pos, result = snapshot[2], 1, []
+    require(raw[0] == 2, "matrix left marker")
+    for _ in range(rows):
+        row = []
+        for _ in range(columns):
+            sign = raw[pos]
+            require(sign in (0, 1), "matrix rational sign")
+            numerator, pos = field(raw, pos+1)
+            denominator, pos = field(raw, pos)
+            require(denominator > 0 and (numerator or not sign), "matrix rational form")
+            row.append(Q((-1 if sign else 1)*numerator, denominator))
+        result.append(row)
+    require(all(x == 4 for x in raw[pos:]), "matrix exact extent")
+    return result
+
+
+def fixed(raw, width):
+    payload = body(raw)
+    require(len(payload) % width == 0 and all(x in (0, 1) for x in payload),
+            "fixed signed record extent")
+    result = []
+    for start in range(0, len(payload), width):
+        bits = payload[start:start+width]
+        result.append(sum(v << i for i, v in enumerate(bits))-(bits[-1] << width))
+    return result
+
+
+def inverse(a):
+    n = len(a)
+    work = [list(row)+[Q(int(i == j)) for j in range(n)] for i, row in enumerate(a)]
+    for col in range(n):
+        pivot = next((i for i in range(col, n) if work[i][col]), None)
+        require(pivot is not None, "independent inverse nonsingularity")
+        work[col], work[pivot] = work[pivot], work[col]
+        scale = work[col][col]
+        work[col] = [x/scale for x in work[col]]
+        for i in range(n):
+            if i != col:
+                scale = work[i][col]
+                work[i] = [x-scale*y for x, y in zip(work[i], work[col])]
+    return [row[n:] for row in work]
+
+
+def mul(a, b):
+    return [[sum((x*y for x, y in zip(row, col)), Q(0))
+             for col in zip(*b)] for row in a]
+
+
+def mv(a, v):
+    return [sum((x*y for x, y in zip(row, v)), Q(0)) for row in a]
+
+
+def sub(a, b):
+    return [[x-y for x, y in zip(row, other)] for row, other in zip(a, b)]
+
+
+def vector_sub(a, b):
+    return [x-y for x, y in zip(a, b)]
+
+
+def norm(a):
+    return max((sum(map(abs, row), Q(0)) for row in a), default=Q(0))
+
+
+def encode(value):
+    if isinstance(value, Q):
+        return [value.numerator, value.denominator]
+    if isinstance(value, (tuple, list)):
+        return [encode(x) for x in value]
+    if isinstance(value, dict):
+        return {key: encode(item) for key, item in value.items()}
+    return value
+
+
+def run_fixture():
+    from cardinal_counts import Count
+    from check_support import no_decode
+    from gaussian_axis import Axis
+    import gaussian_boundary as boundary_module
+    import gaussian_window as window_module
+    from ring_words import Signed, write_signed
+    from router_metadata import owned
+    from scratch_pool import ScratchPool
+    from session import OuterScope, borrowed_tape, erase_marker, sealed_constructors
+
+    bits, p, scale, bandwidth = 24, 16, 1 << 24, 2
+    rounding = lambda x: Q(int(x*scale), scale)
+    observed = {}
+    saved_prepare, saved_close = window_module.prepare_bands, window_module.Window.close_dense
+
+    def observe_banks(*args):
+        result = saved_prepare(*args)
+        observed["banks"] = tuple(tape_bytes(tape) for tape in result)
+        return result
+
+    def observe_dense(self):
+        if self.schur is not None:
+            observed["dense"] = {name: matrix_snapshot(getattr(self, name))
+                                 for name in ("principal", "schur", "rounded_schur", "lower", "upper")}
+            observed["width"] = tape_bytes(self.width.tape)
+        return saved_close(self)
+
+    pool = ScratchPool(512)
+    scope = OuterScope(pool)
+    axis = window = None
+    window_module.prepare_bands, window_module.Window.close_dense = observe_banks, observe_dense
+    try:
+        with owned(*(Count.literal(v) for v in (13, 14, 1, 1, bits))) as parameters:
+            with sealed_constructors(), scope.installed():
+                try:
+                    with no_decode():
+                        axis = Axis(*parameters, pool)
+                    observed["old_h"] = matrix_snapshot(axis.matrix)
+                    observed["weights"] = matrix_snapshot(axis.weights)
+                    with owned(Signed(Count.literal(11)), Count.literal(8),
+                               Signed(Count.literal(12)), Count.literal(4), Count.literal(p)) as args:
+                        with no_decode():
+                            window = window_module.Window(axis, *args, pool)
+                        require(all(getattr(window, name) is None for name in
+                                    ("principal", "schur", "rounded_schur", "lower", "upper")),
+                                "source Window releases dense setup")
+                        page_body = body(tape_bytes(window.page))
+                        require(page_body.endswith(b"".join(body(bank) for bank in observed["banks"])),
+                                "reused banks are the actual compiled Window page suffix")
+                        observed["page_sha256"] = sha256(page_body).hexdigest()
+                finally:
+                    if window is not None:
+                        window.close()
+                    if axis is not None:
+                        axis.close()
+                    pool.empty()
+    finally:
+        window_module.prepare_bands, window_module.Window.close_dense = saved_prepare, saved_close
+    for tape in pool.tapes:
+        erase_marker(tape)
+    require(not pool.live and all(t.head == 1 and all(x == 4 for x in t.cells) for t in pool.tapes),
+            "complete setup scratch cleanup")
+
+    h, weights = matrix(observed["old_h"]), matrix(observed["weights"])
+    selected = list(range(Q(13*21, 28).__ceil__(), Q(13*37, 28).__ceil__()))
+    cells, previous = [], None
+    for position, j in enumerate(selected):
+        key = (j//13, weights[j % 13][2])
+        if key != previous:
+            cells.append([])
+        cells[-1].append(position)
+        previous = key
+    interior = [i for cell in cells if len(cell) > 4 for i in cell[1:-1]]
+    boundary = [i for cell in cells for i in (cell[:1]+cell[-1:] if len(cell) > 4 else cell)]
+    require(interior and boundary, "actual old-H fixture includes eliminated interior")
+    principal = [[h[i % 13][j % 13] for j in selected] for i in selected]
+    hii = [[principal[i][j] for j in interior] for i in interior]
+    hbi = [[principal[i][j] for j in interior] for i in boundary]
+    hib = [[principal[i][j] for j in boundary] for i in interior]
+    schur = sub([[principal[i][j] for j in boundary] for i in boundary], mul(mul(hbi, inverse(hii)), hib))
+    dense = {name: matrix(value) for name, value in observed["dense"].items()}
+    require(principal == dense["principal"] and schur == dense["schur"],
+            "independent old-H elimination matches actual setup")
+    rounded = [[rounding(x) for x in row] for row in schur]
+    require(rounded == dense["rounded_schur"], "observed first Schur rounding")
+    low, high = dense["lower"], dense["upper"]
+    require(mul(low, high) == rounded, "actual exact LU factors the rounded Schur matrix")
+    n, width = len(boundary), count(observed["width"])
+    low_bank, high_bank = [fixed(raw, width) for raw in observed["banks"]]
+    require(len(low_bank) == n*bandwidth and len(high_bank) == n*(bandwidth+1), "actual prepared bank extents")
+    lower = [[Q(int(i == j)) for j in range(n)] for i in range(n)]
+    upper = [[Q(0) for _ in range(n)] for _ in range(n)]
+    reciprocal = [Q(0)]*n
+    pos = 0
+    for i in range(n):
+        for j in range(i-bandwidth, i):
+            value = Q(low_bank[pos], scale)
+            pos += 1
+            require(value == (rounding(low[i][j]) if j >= 0 else 0), "actual lower coefficient")
+            if j >= 0:
+                lower[i][j] = value
+    pos = 0
+    for i in reversed(range(n)):
+        for j in range(i+1, i+bandwidth+1):
+            value = Q(high_bank[pos], scale)
+            pos += 1
+            require(value == (rounding(high[i][j]) if j < n else 0), "actual upper coefficient")
+            if j < n:
+                upper[i][j] = value
+        reciprocal[i] = Q(high_bank[pos], scale)
+        pos += 1
+        require(reciprocal[i] == rounding(1/high[i][i]) and reciprocal[i] > 0, "actual pivot reciprocal")
+        upper[i][i] = 1/reciprocal[i]
+    effective = mul(lower, upper)
+    e0, e1 = sub(rounded, schur), sub(effective, rounded)
+    require(norm(e0) > 0 and norm(e1) > 0, "two distinct nonzero setup perturbations")
+
+    def solve_model(rhs, early=False):
+        forward, result = [Q(0)]*n, [Q(0)]*n
+        for i in range(n):
+            forward[i] = rounding(rhs[i]-sum((lower[i][j]*forward[j] for j in range(i)), Q(0)))
+        for i in reversed(range(n)):
+            residual = forward[i]-sum((upper[i][j]*result[j] for j in range(i+1, n)), Q(0))
+            result[i] = rounding(reciprocal[i]*(rounding(residual) if early else residual))
+        return forward, result
+
+    # Bounded fixture selection only: all candidates use the actual saved banks.
+    candidates = [[Q(((7*i+3+5*k) % 19)-9, 16) for i in range(n)] for k in range(64)]
+    chosen = next((rhs for rhs in candidates if solve_model(rhs)[1] != solve_model(rhs, True)[1]), None)
+    require(chosen is not None, "actual bank witness distinguishes premature upper rounding")
+    right_hands = [chosen, [Q(((5*i+1) % 11)-5, 16) for i in range(n)]]
+    owner = boundary_module.BandedSolve()
+    input_pool, components = ScratchPool(256), []
+    input_scope = OuterScope(input_pool)
+    raw_trace = []
+    saved_truncate = boundary_module.truncate
+
+    def observe_truncate(value, amount):
+        before = (value.negative, tape_bytes(value.magnitude.tape), tape_bytes(amount.tape))
+        result = saved_truncate(value, amount)
+        raw_trace.append((before, result.negative, tape_bytes(result.magnitude.tape)))
+        return result
+
+    try:
+        with owned(*(Count.literal(v) for v in (n, bandwidth, width, bits))) as args:
+            with sealed_constructors(), input_scope.installed():
+                tapes = [input_pool.acquire() for _ in range(3)]
+                try:
+                    for target, raw in zip(tapes[:2], observed["banks"]):
+                        for bit in body(raw):
+                            target.append(bit)
+                        target.rewind()
+                    for rhs in right_hands:
+                        for item in rhs:
+                            integer = int(item*scale)
+                            with owned(Signed(Count.literal(abs(integer)), integer < 0)) as (value,):
+                                write_signed(value, tapes[2], args[2])
+                        tapes[2].rewind()
+                        ports = [borrowed_tape(x) for x in tapes]+[borrowed_tape(x.tape) for x in args]
+                        borrowed = [(bytes(x.cells), x.head) for x in ports]
+                        raw_trace.clear()
+                        boundary_module.truncate = observe_truncate
+                        products_before = owner.arithmetic.products
+                        try:
+                            with input_scope.suspended(), no_decode():
+                                output = owner.run(*tapes, *args)
+                        finally:
+                            boundary_module.truncate = saved_truncate
+                        require(borrowed == [(bytes(x.cells), x.head) for x in ports], "all source borrowed ports restored")
+                        result = [Q(x, scale) for x in fixed(bytes(output.cells), width)]
+                        trace = [(((-1 if before[0] else 1)*count(before[1]), count(before[2])),
+                                  (-1 if sign else 1)*count(after)) for before, sign, after in raw_trace]
+                        require(len(trace) == 2*n and [a[0][1] for a in trace] == [bits]*n+[2*bits]*n,
+                                "actual forward/backward truncation schedule")
+                        forward = [Q(item[1], scale) for item in trace[:n]]
+                        require(result == [Q(item[1], scale) for item in reversed(trace[n:])], "observed backward outputs")
+                        expected_y, expected_x = solve_model(rhs)
+                        require((forward, result) == (expected_y, expected_x), "independent rational model agrees with actual source")
+                        for i in range(n):
+                            raw = rhs[i]-sum((lower[i][j]*forward[j] for j in range(i)), Q(0))
+                            require(trace[i][0][0] == raw*scale*scale, "actual exact forward dot product")
+                            raw = reciprocal[i]*(forward[i]-sum((upper[i][j]*result[j] for j in range(i+1, n)), Q(0)))
+                            require(trace[2*n-1-i][0][0] == raw*scale**3, "actual unrounded upper residual times reciprocal")
+                        ef, eb = vector_sub(mv(lower, forward), rhs), vector_sub(mv(upper, result), forward)
+                        rho = vector_sub(mv(effective, result), rhs)
+                        split = [a+b for a, b in zip(ef, mv(lower, eb))]
+                        require(rho == split and any(ef) and any(eb), "nonzero computed-state residual identity")
+                        require(max(map(abs, ef)) < Q(1, scale)
+                                and all(abs(error*qhat) < Q(1, scale) for error, qhat in zip(eb, reciprocal)),
+                                "forward and reciprocal-scaled backward truncation bounds")
+                        original_residual = vector_sub(mv(schur, result), rhs)
+                        complete = [a-b-c for a, b, c in zip(rho, mv(e1, result), mv(e0, result))]
+                        require(original_residual == complete, "complete original-Schur residual decomposition")
+                        omitted = vector_sub(rho, mv(e1, result))
+                        require(original_residual != omitted, "omitting first Schur rounding fails")
+                        wrong_upper = [row[:] for row in upper]
+                        for i in range(n):
+                            wrong_upper[i][i] = rounding(high[i][i])
+                        wrong_diagonal = vector_sub(mv(mul(lower, wrong_upper), result), rhs)
+                        require(wrong_diagonal != rho, "rounded U diagonal is not the source effective diagonal")
+                        ideal = mv(inverse(schur), rhs)
+                        error = vector_sub(result, ideal)
+                        recovered_error = mv(inverse(effective), vector_sub(rho, mv(sub(effective, schur), ideal)))
+                        require(error == recovered_error, "exact original-Schur solution error identity")
+                        require(owner.arithmetic.products-products_before == 5*n, "source multiply calls")
+                        components.append({"rhs": rhs, "forward": forward, "output": result,
+                                           "forward_residual": ef, "backward_residual": eb,
+                                           "effective_residual": rho, "original_residual": original_residual,
+                                           "first_rounding_contribution": mv(e0, result),
+                                           "factor_rounding_contribution": mv(e1, result),
+                                           "solution_error": error,
+                                           "max_solution_error": max(map(abs, error)),
+                                           "early_rounding_output": solve_model(rhs, True)[1],
+                                           "early_rounding_rejected": solve_model(rhs, True)[1] != result,
+                                           "wrong_diagonal_residual": wrong_diagonal,
+                                           "truncate_calls": len(trace), "multiply_calls": 5*n,
+                                           "borrowed_restored": True})
+                        output.clear()
+                        erase_marker(output)
+                        owner.idle()
+                        require(owner.closed and not owner.pool.live and all(
+                            t.head == 1 and all(x == 4 for x in t.cells) for t in owner.pool.tapes),
+                            "source solver scratch blank after completed call")
+                        borrowed_tape(tapes[2]).clear()
+                finally:
+                    for tape in tapes:
+                        tape.clear()
+                    input_pool.empty()
+    finally:
+        boundary_module.truncate = saved_truncate
+    for tape in input_pool.tapes:
+        erase_marker(tape)
+    require(not input_pool.live and all(t.head == 1 and all(x == 4 for x in t.cells) for t in input_pool.tapes),
+            "input carrier cleanup")
+    return encode({"fixture": {"s": 13, "t": 14, "u": 1, "w": 1, "P": bits, "p": p,
+                               "window": [11, 8, 12, 4], "selected": selected, "cells": cells,
+                               "boundary": boundary, "interior": interior, "width": width},
+                   "original_schur": schur, "rounded_schur": rounded,
+                   "stored_lower": lower, "effective_upper": upper, "stored_reciprocals": reciprocal,
+                   "schur_rounding_norm": norm(e0), "factor_rounding_norm": norm(e1),
+                   "bank_sha256": [sha256(body(raw)).hexdigest() for raw in observed["banks"]],
+                   "compiled_page_sha256": observed["page_sha256"], "components": components,
+                   "banks_bound_to_page_suffix": True, "solution_error_identity": True,
+                   "observer_only": True, "source_calls": owner.calls, "all_cleanup_checks": True,
+                   "production_precision_claim": False})
diff --git a/research/schur-boundary-residual/verify.py b/research/schur-boundary-residual/verify.py
new file mode 100644
index 0000000000..3feca2c0aa
--- /dev/null
+++ b/research/schur-boundary-residual/verify.py
@@ -0,0 +1,115 @@
+#!/usr/bin/env python3
+"""Scoped exact boundary evidence; source authentication precedes all imports."""
+import argparse
+from fractions import Fraction as Q
+from hashlib import sha256
+import json
+from pathlib import Path
+import sys
+import tempfile
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def source_bytes():
+    manifest = json.loads((HERE / 'SOURCES.json').read_text())
+    rows = [r for r in manifest['files'] if r['usage'] == 'input']
+    for row in rows:
+        path = ROOT / row['path']
+        need(path.is_file() and not path.is_symlink(), 'regular input: ' + row['path'])
+        need(sha256(path.read_bytes()).hexdigest() == row['sha256'], 'exact input: ' + row['path'])
+    return len(rows)
+
+
+def algebra():
+    # Check the constants/base steps of the written induction, not an all-p census.
+    # p <= 2^p follows at p=1 and p+1 <= 2p. The bounds below then
+    # decrease geometrically at every integer p >= 1.
+    need(1 <= 2 and 1 + 1 <= 2 * 1, 'elementary induction base')
+    for coefficient, degree, ceiling_bits in ((40, 2, 6), (3200, 4, 12)):
+        need(coefficient < 1 << ceiling_bits, 'strict power-of-two coefficient envelope')
+        need(ceiling_bits - (32768 - degree) < -1, 'Neumann envelope below one half at p=1')
+        need(32768 - degree > 0, 'Neumann envelope decreases for every p increment')
+    eta_cap = Q(1, 1 << 16)
+    need(32768 > 16, 'uniform coarse eta cap')
+    need(195 + 4 + 6 * eta_cap < 200, 'factor product coefficient')
+    need(65 + 2 * eta_cap < 66, 'rounded lower growth')
+    need(2 + 8 * 66 == 530, 'combined residual coefficient')
+    need(200 + 5 == 205, 'both setup perturbations')
+    need(32 * 530 == 16960 and 32 * 205 * 8 == 52480, 'solution error constants')
+    need(16960 + 52480 == 69440 < 1 << 17, 'final constant')
+    need(2 * 101 + 8 <= 3 * 101, 'effective diagonal within stated p domain')
+
+    # An exact zero-online-residual example isolates the initial Schur rounding.
+    unit = 1 << 8
+    S = 1 + Q(1, 3 * unit)
+    Sbar = Q(int(S * unit), unit)
+    x = r = Q(1)
+    rho = Sbar * x - r
+    error = x - r / S
+    need(Sbar == 1 and rho == 0 and error == Q(1, 3 * unit + 1),
+         'omitting initial Schur rounding falsely predicts zero error')
+    need(error == (rho - (Sbar - S) * r / S) / Sbar, 'complete scalar error identity')
+
+    # A two-row P=3 model separates the actual one-round upper program from
+    # rounding its dot-product residual before multiplication by the reciprocal.
+    def tau(v):
+        return Q(int(v * 8), 8)
+    qhat = tau(Q(8, 3))
+    y = [Q(1, 8), Q(1, 8)]
+    last = tau(qhat * y[1])
+    residual = y[0] - Q(1, 8) * last
+    first = tau(qhat * residual)
+    wrong = tau(qhat * tau(residual))
+    need([first, last] == [Q(1, 8), Q(1, 4)] and wrong == 0,
+         'premature upper residual rounding distinguished')
+    need(1 / qhat != tau(Q(3, 8)), 'effective diagonal is not rounded U diagonal')
+    return {
+        'uniform_domain': 'integer p >= 101, P=32768p; explicit source premises in PROOF.md',
+        'neumann_envelopes': ['40 p^2 eta < 2^(6-32766p) < 1/2',
+                              '3200 p^4 eta < 2^(12-32764p) < 1/2'],
+        'original_S_error_constant': 69440,
+        'reported_allowance': '2^17 p^5 eta max(1,||r||_infinity)',
+        'scalar_omission_control': {'P': 8, 'online_residual': '0', 'original_error': str(error)},
+        'early_round_control': {'P': 3, 'actual': [str(first), str(last)], 'mutant': [str(wrong), str(last)]},
+        'scope': 'Exact scalar controls and arithmetic of the written proof; no finite test establishes the analytic premises.'
+    }
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--write', action='store_true', help='write the complete deterministic finite receipt')
+    args = parser.parse_args()
+    count = source_bytes()
+    # -B prevents writes, not reads: isolate cached bytecode before importing
+    # any authenticated predecessor module or the local fixture.
+    with tempfile.TemporaryDirectory(prefix='schur-boundary-pycache-') as cache:
+        old = sys.pycache_prefix
+        sys.pycache_prefix = cache
+        try:
+            sys.path.insert(0, str(HERE))
+            sys.path.insert(0, str(ROOT / 'research/physical-gaussian-core'))
+            from gaussian_sources import opened
+            from fixture import run_fixture
+            with opened():
+                physical = run_fixture()
+        finally:
+            sys.pycache_prefix = old
+    result = {'status': 'PASS_SCHUR_BOUNDARY_RESIDUAL', 'source_inputs': count,
+              'algebra': algebra(), 'physical': physical}
+    path = HERE / 'RESULT.json'
+    if args.write:
+        path.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n')
+    else:
+        need(result == json.loads(path.read_text()), 'complete typed finite receipt')
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()