diff --git a/research/gaussian-cross-rounding/README.md b/research/gaussian-cross-rounding/README.md
new file mode 100644
index 0000000000..7e1092eb65
--- /dev/null
+++ b/research/gaussian-cross-rounding/README.md
@@ -0,0 +1,228 @@
+# Downward rounding of the actual across-cell Gaussian coefficient
+
+**Result:** the retained two-ulp repair applies to the original across-cell
+Gaussian exponent. It constructs a stored coefficient `H` satisfying
+
+```text
+0 <= H <= n,                 0 <= n - H < 4 * 2^-P.
+```
+
+This supplies the coefficient-construction step left open by James Reed's
+[PR #4442](https://github.com/CrocSwap/integer-mult-bounds/pull/4442), pinned
+at `d079c2b058ebd3d7a9ff424113b095bf61175427`. The subtraction/clipping method
+is already in the retained phase-cell review. The contribution is its exact
+caller instantiation, error accounting and separately written controls.
+It does not establish that an existing executable page generator uses this
+construction. No new kappa or selected-frontier change is claimed.
+
+## Caller and exact exponential arguments
+
+Let `s,t,u` be positive integers with `t>s` and `u=alpha^2`. Write
+
+```text
+rho = t/s,
+q_i = floor(t*i/s + 1/2),
+b_i = t*i - s*q_i,           beta_i = b_i/s.
+```
+
+Thus `-s/2 <= b_i < s/2`, including the specified tie convention. For any
+integer offset `h`, the original coefficient in LOG-A section 1 is
+
+```text
+n_i,h = exp(-pi*u*((rho*h + beta_i)^2 - beta_(i+h)^2)).
+```
+
+Use the nonnegative integers
+
+```text
+j = u*((t*h + b_i)^2 - b_(i+h)^2),       k = s^2.
+```
+
+Then **exactly** `n_i,h = exp(-pi*j/k)`. No approximate exponent or
+within-cell gauge identity is substituted. If `h != 0`,
+
+```text
+|t*h + b_i| >= t*|h| - |b_i| > s/2 >= |b_(i+h)|,
+```
+
+so `j>0`. If `h=0`, `j=0`; the source construction stores the diagonal as
+exactly one instead of applying the repair. This proves the nonnegative
+argument condition for every retained off-diagonal coefficient, including
+cell changes and either sign of `h`.
+
+A second form useful for checking the integer arithmetic is
+
+```text
+d = q_(i+h) - q_i,
+j/k = u*d*(d + 2*b_(i+h)/s).
+```
+
+At a physical period cut, keep the unwrapped signed offset `h`:
+`q_(i+s)=q_i+t` and `b_(i+s)=b_i`. Do not replace `h` by a residue before
+forming the square gap. This treats the single retained coefficient at
+that offset, not a sum of all periodic aliases. The truncation and deletion
+of nonzero diagonal aliases remain the source construction's choices.
+For a circular band with `2W<s`, retained signed offsets identify distinct
+columns, so the entry count below applies without alias multiplicities.
+
+## Repair lemma and its exact boundary
+
+Let `eta=2^-P` and suppose the negative-real exponential routine returns a
+real P-grid number `z` with `|z-n|<2*eta`. This is the error contract invoked
+in the retained review's **Computable rounding and perturbation** section;
+see also Harvey and van der Hoeven, [negative real exponentials, Lemma 2.13](https://www.texmacs.org/joris/nlogn/nlogn.pdf).
+Take the real component if the routine represents its output as complex.
+Define
+
+```text
+H = max(0, z - 2*eta).
+```
+
+If `z>2*eta`, then `H=z-2*eta<n` and
+`n-H=n-z+2*eta<4*eta`. Otherwise `H=0` and
+`n<z+2*eta<=4*eta`. In both cases `0<=H<=n` and the stated strict error
+bound holds. The output remains on the P-grid. Underflow to zero is
+permitted for these off-diagonal entries; the separate positive-weight
+requirement inside a cell is not being weakened.
+
+A two-ulp margin is necessary among nonnegative integer-ulp safety
+margins under this black-box error
+contract: `n=3*eta/2, z=3*eta` is admissible, but subtracting only one ulp
+still exceeds `n`. The constant four is a sharp supremum for the same
+contract: `z=2*eta, n=(4-delta)*eta`, with `0<delta<1`, produces zero and
+error approaching `4*eta`. These are statements about the stated oracle
+contract, not lower bounds for a more accurate exponential implementation.
+
+The exact `j,k` above therefore discharge the missing application of the
+repair to across-cell entries. If `j>=k*P`, zero is already safe because
+`exp(-pi*j/k)<=exp(-pi*P)<2^-P`. Otherwise `j<k*P`; the exponential
+routine receives an ordinary nonnegative rational argument. In the source
+parameter regime, `log s`, `log t`, `log u`, `log W` and `P` are polynomially
+bounded in the outer parameter. Forming `j,k`, subtracting two ulps and
+clipping consequently need only polynomial per-coefficient work and no
+larger output grid. This does not count all coefficient requests or prove
+the global setup, routing or tape bound. The published fast exponential
+lemma is an inherited mathematical input, not re-proved here.
+
+For a row or column with at most `2W` retained off-diagonal entries, the
+**across-cell rounding contribution alone** has absolute sum below
+`8W*2^-P` when `W>0` (zero when `W=0`). This does not include truncation,
+within-cell weight ratios, diagonal aliases or later page-rounding errors.
+Under #4442's other hypotheses, its across-cell domination premise is now
+available for the reference constructed with this routine. Its ideal gaps,
+within-cell estimate and halo exponent/minimality calculations have not
+been independently audited by this package.
+
+## Two distinctions that matter at the caller
+
+The repair must approximate the original `n_i,h`, not the bare Toeplitz
+kernel. The inherited #4442 example has `s=4,t=5,u=1,i=1,h=1`:
+`beta_i=1/4`, `beta_(i+h)=-1/2`, and the square gap is `2`, while
+`rho*h^2=5/4`. The checker certifies that even the repaired 64-bit bare
+kernel exceeds the true coefficient. This counterexample is credited to
+#4442; its interval check is new here.
+
+The reference `H` and its online coupling pages are separate objects.
+Later nearest rounding to a coarser grid can destroy domination. For
+example, the admissible oracle values `n=3*eta/2,z=3*eta` give `H=eta`;
+nearest rounding to the `2*eta` grid, with ties upward, gives `2*eta>n`.
+Further rounding **toward zero** preserves domination, with its own added
+absolute-error budget. The source reports already charge separate coupling
+rounding; no zero-cost or exact-page identification is asserted here.
+
+## Evidence and reproduction
+
+`verify.py` uses only Python's standard library and exact integer/Fraction
+arithmetic. Its separately written numerical oracle encloses pi with
+Machin's identity and alternating arctangent sums, encloses `exp(-x)` by
+alternating Taylor sums after reducing to `[0,1/2]`, and rounds both
+endpoints outward after every squaring. Monotonicity combines the argument
+and exponential enclosures. A nearest-grid midpoint supplies `z`; the
+checker then requires `H<=lower(n)` and `upper(n)-H<4*eta`. It does not
+implement or test the published fast exponential routine.
+
+The series enclosures follow from alternating terms of decreasing size.
+After reduction, all exact exponentials and their clipped upper endpoints
+lie in `[0,1]`; squaring is monotone there. Machin's identity is
+`pi=16*atan(1/5)-4*atan(1/239)`. The chosen signs in `pi_bounds` round the
+subtraction outward. Increasing internal precision until the interval is
+shorter than `eta/8` terminates; no floating-point comparison is used.
+The coarse underflow interval `[0,eta]` uses the analytic shortcut above.
+
+[RESULT.json](RESULT.json) records 384 coefficient cases, 1,624 phase
+identities, 2,019 oracle-boundary cases and the coefficient digest. In 81
+coefficient cases the uncorrected approximation provably exceeds the exact
+coefficient, so the downward correction has an observable effect.
+Fixtures cover five rational phase models, precisions 24, 64 and 128,
+positive and clipped outputs, both offset signs, internal and physical
+period cuts, and nearest-index ties. These are boundary models, not
+complete fine-prime multiplication instances. A separate rational mesh
+checks every admissible integer oracle output at 513 exact target values.
+Ten explicit controls cover missing/insufficient subtraction, missing
+clipping, a nonstrict oracle error bound, later nearest rerounding,
+wrong-kernel substitution and four invalid input domains. All checks use
+explicit exceptions and remain active with `-O`.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/gaussian-cross-rounding --check-only
+python3.12 -B scripts/research_package.py --package research/gaussian-cross-rounding
+```
+
+The registered command runs ordinary and optimized Python. A Git-free
+export containing the declared inputs can run the direct verifier:
+
+```sh
+python3.12 -B research/gaussian-cross-rounding/verify.py
+python3.12 -O -B research/gaussian-cross-rounding/verify.py
+```
+
+These checks support the written lemma; finite cases do not prove its
+universal quantifiers. No complete selected replay, Schur solve, native
+supplier replay, Lean proof, independent human review or new kappa is
+claimed. Source binding is separate from mathematical verification.
+
+## Sources, coordination and attribution
+
+Scientific base: canonical main
+`2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision 7, selected
+`kappa=23/10000`. [SOURCES.json](SOURCES.json) binds the four live caller
+notes and the original catalogue/selected provenance. No frozen file is
+changed. #4442 is a motivating handoff; its unmerged Git objects are not
+required for replay. The canonical investigation is
+[Discussion #4444](https://github.com/CrocSwap/integer-mult-bounds/discussions/4444).
+
+The initial overlap scan fetched complete pagination for 301 open PRs,
+3,289 Discussion records and 3,787 closed PRs at 21:01-21:03 UTC on
+2026-10-21. Targeted searches covered `four-ulp`, `across-cell` and
+`downward exponential`, plus available top-level package notes. This does
+not search every diff or nested file and is not a novelty certificate.
+The card's baseline command was attempted but stopped on the initially
+omitted selected package in the sparse checkout; no baseline PASS or full
+selected replay is claimed.
+
+Credit: James Reed (#4442 and the #4438/#4439 chain) for the exact handoff
+and wrong-kernel witness; RaD/hipotures and the retained phase-cell
+producer/reviewer for the two-ulp repair and structured reference;
+Vlado Vojdanovski and PR1673's credited contributors for LOG-A/capped
+Gaussian construction; Chafik Boukhalfa (#1758/#1786) for the fine-prime
+and setup-precision lineage; Cinna Davis (#4100) for the retained all-size
+notes; Ryanson Jonathan (#4402) for the column-gap lineage; David Harvey
+and Joris van der Hoeven for the exponential contract. Mason Hale's
+certified Gaussian recovery and Dugongue's Gaussian expansion headroom
+already use directed interval/coefficients; this package does not claim
+that method as new and imports neither implementation. Douglas Colkitt,
+the retained OpenAI framework and all source-specific notices retain credit.
+
+Prepared for **mihir-s-05** with substantial **OpenAI Codex assistance** in
+mathematics, code, verification and writing. No subagents. New work is
+Apache-2.0.
+
+## Open next questions
+
+Does one actual online coupling-page generator preserve domination or
+correctly charge its separate rounding error? This matters because the
+coarse nearest-grid control fails even when the reference is downward.
+First pin that generator, its output precision and rounding mode, then
+check the control and the source coupling perturbation budget. The missing
+piece is an executed page generator and its consumer; this package stops
+at construction of the stored reference coefficient.
diff --git a/research/gaussian-cross-rounding/RESULT.json b/research/gaussian-cross-rounding/RESULT.json
new file mode 100644
index 0000000000..3376cbfaad
--- /dev/null
+++ b/research/gaussian-cross-rounding/RESULT.json
@@ -0,0 +1,14 @@
+{
+  "source_files": 4,
+  "coefficients": 384,
+  "positive": 171,
+  "clipped": 213,
+  "period_cuts": 156,
+  "cell_cuts": 228,
+  "ties": 6,
+  "unrepaired_overshoots": 81,
+  "phase_identities": 1624,
+  "oracle_boundary_cases": 2019,
+  "failure_controls": 10,
+  "record_sha256": "7c40c3a5fce673456776f8e8d27cf47c273a6858883f9e589a88d0f554828789"
+}
diff --git a/research/gaussian-cross-rounding/SOURCES.json b/research/gaussian-cross-rounding/SOURCES.json
new file mode 100644
index 0000000000..1e11052b68
--- /dev/null
+++ b/research/gaussian-cross-rounding/SOURCES.json
@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md",
+      "usage": "input",
+      "git_blob": "d72345a0aa748443c4efcddf87aa10d524664841",
+      "sha256": "3cdf492bcb719db4295658604dc202d6a2c5a008b87de43ec54f0107c64db730"
+    },
+    {
+      "path": "references/semantic-bulk/rad20/reports/review-phase-cell-inverse.md",
+      "usage": "input",
+      "git_blob": "395eab8ee1d58e84353f554dcfe9473b5913dda5",
+      "sha256": "113927dd4fb77a55a457bd5f6da8cbfc7262d0fbc4e9d708b591a1d632e6caf6"
+    },
+    {
+      "path": "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
+      "usage": "input",
+      "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73",
+      "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272"
+    },
+    {
+      "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md",
+      "usage": "input",
+      "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3",
+      "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce"
+    }
+  ]
+}
diff --git a/research/gaussian-cross-rounding/TASK.json b/research/gaussian-cross-rounding/TASK.json
new file mode 100644
index 0000000000..881cd3fca3
--- /dev/null
+++ b/research/gaussian-cross-rounding/TASK.json
@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db",
+  "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": "Instantiate the retained two-ulp downward exponential repair at the across-cell square-gap coefficient, the open question of PR4442.",
+  "scope_change_reason": "The live handoff narrows the broad precision/conditioning audit to one missing caller-bound implication; it does not reopen the within-cell or halo calculations.",
+  "bottleneck_link": "PR4442 needs 0 <= H[i,i+h] <= n[i,h] on across-cell entries to transfer its norm ceiling. This package supplies the exact oracle arguments and stored-value guarantee.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at coefficient construction and its perturbation bound; no complete solver, native, tape, halo-optimality or kappa claim.",
+  "outcome": "completed",
+  "evidence": "README.md gives the universal caller/rounding proof. verify.py independently constructs rational enclosures and checks RESULT.json, including failure controls.",
+  "author": "mihir-s-05",
+  "ai_assistance": "Substantial OpenAI Codex assistance in source inspection, mathematics, implementation, verification and writing. No subagents.",
+  "open_questions": [
+    {
+      "question": "Do the actual online coupling pages preserve the stored-reference downward inequality, or charge their separate rounding error?",
+      "why_it_matters": "Nearest rounding on a coarser grid can overshoot even a downward reference coefficient. The new guarantee concerns H, not every later page.",
+      "first_step": "Pin one actual page generator; identify its output grid and rounding mode, then test the rerounding control and include the source coupling perturbation budget.",
+      "blocked_by": "No online page generator or full Schur solver is executed by this package."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4444",
+  "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19108213",
+  "predecessor": {
+    "pr": 4442,
+    "head": "d079c2b058ebd3d7a9ff424113b095bf61175427",
+    "role": "Motivating open question only; its halo proof is not imported or certified."
+  }
+}
diff --git a/research/gaussian-cross-rounding/VERIFY.json b/research/gaussian-cross-rounding/VERIFY.json
new file mode 100644
index 0000000000..8f6d8f2a17
--- /dev/null
+++ b/research/gaussian-cross-rounding/VERIFY.json
@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md",
+    "references/semantic-bulk/rad20/reports/review-phase-cell-inverse.md",
+    "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
+    "research/unconditional-batched-crt/vendor/FINE-PRIME.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Pinned caller sources; exact phase/exponent identities, interval-certified across-cell coefficients, adversarial oracle error mesh and semantic failure controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same evidence and rejection controls with Python assertions disabled."
+    }
+  ]
+}
diff --git a/research/gaussian-cross-rounding/verify.py b/research/gaussian-cross-rounding/verify.py
new file mode 100644
index 0000000000..d34abfdb9e
--- /dev/null
+++ b/research/gaussian-cross-rounding/verify.py
@@ -0,0 +1,231 @@
+#!/usr/bin/env python3
+"""Exact controls for the across-cell coefficient lemma; not a solver replay.
+
+Prepared for mihir-s-05 with substantial OpenAI Codex assistance. Apache-2.0.
+The subtract-two-ulps repair is credited predecessor work; see README.md.
+"""
+from fractions import Fraction as F
+from functools import lru_cache
+from hashlib import sha256
+from pathlib import Path
+import json
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def floor(x):
+    return x.numerator // x.denominator
+
+
+def ceil(x):
+    return -floor(-x)
+
+
+def phase(s, t, i):
+    """Exact nearest integer, including negative indices and half-integer ties."""
+    q = (2 * t * i + s) // (2 * s)
+    return q, t * i - s * q
+
+
+def exponent_ratio(s, t, u, i, h):
+    """Return j/k for exp(-pi*j/k), with the physical unwrapped offset h."""
+    require(all(type(v) is int for v in (s, t, u, i, h)), "integer phase inputs required")
+    require(s > 0 and t > s and u > 0, "require s>0, t>s, u>0")
+    _, b = phase(s, t, i)
+    _, c = phase(s, t, i + h)
+    numerator = u * ((t * h + b) ** 2 - c ** 2)
+    require(numerator >= 0, "negative Gaussian exponent")
+    return F(numerator, s * s)
+
+
+def repair(q, eta):
+    require(eta > 0, "positive grid spacing required")
+    require((q / eta).denominator == 1, "oracle output must be on the grid")
+    return max(F(0), q - 2 * eta)
+
+
+def check_bound(stored, lo, hi, eta):
+    require(0 <= stored <= lo and hi - stored < 4 * eta, "downward/error bound")
+
+
+def rejects_bound(stored, value, eta):
+    try:
+        check_bound(stored, value, value, eta)
+    except ValueError:
+        return
+    raise ValueError("invalid output accepted by bound check")
+
+
+def atan_bounds(inv, bits):
+    """Consecutive alternating sums enclose atan(1/inv)."""
+    total, power, sign, k = F(0), F(1, inv), 1, 0
+    target = F(1, 2 ** bits)
+    while True:
+        term = power / (2 * k + 1)
+        previous = total
+        total += sign * term
+        if term < target:
+            return min(total, previous), max(total, previous)
+        power /= inv * inv
+        sign = -sign
+        k += 1
+
+
+@lru_cache(None)
+def pi_bounds(bits):
+    """Machin identity, with outward dyadic endpoints."""
+    a, b = atan_bounds(5, bits + 8)
+    c, d = atan_bounds(239, bits + 8)
+    scale = 2 ** bits
+    return F(floor((16 * a - 4 * d) * scale), scale), F(ceil((16 * b - 4 * c) * scale), scale)
+
+
+def exp_minus_bounds(x, bits):
+    """Alternating Taylor on [0,1/2], then outward-rounded squaring."""
+    require(x >= 0, "nonnegative argument required")
+    y, squarings = x, 0
+    while y > F(1, 2):
+        y /= 2
+        squarings += 1
+    scale = 2 ** bits
+    target = F(1, scale)
+    total, term, k = F(1), F(1), 0
+    while True:
+        k += 1
+        previous = total
+        term *= y / k
+        total += (-1 if k % 2 else 1) * term
+        if term < target:
+            lo = F(floor(min(previous, total) * scale), scale)
+            hi = F(ceil(max(previous, total) * scale), scale)
+            break
+    for _ in range(squarings):
+        lo = F(floor(lo * lo * scale), scale)
+        hi = min(F(1), F(ceil(hi * hi * scale), scale))
+    return lo, hi
+
+
+@lru_cache(None)
+def gaussian_bounds(ratio, precision):
+    """Separate rational enclosure oracle, not an implementation of HvH 2.13."""
+    require(type(precision) is int and precision >= 2 and ratio >= 0, "invalid enclosure domain")
+    eta = F(1, 2 ** precision)
+    if ratio >= precision:
+        # pi > 1 and e > 2 imply exp(-pi*ratio) < 2^-precision.
+        return F(0), eta
+    bits = precision + 32
+    while True:
+        pl, ph = pi_bounds(bits)
+        lo, _ = exp_minus_bounds(ph * ratio, bits)
+        _, hi = exp_minus_bounds(pl * ratio, bits)
+        require(0 <= lo <= hi <= 1, "invalid exponential enclosure")
+        if hi - lo < eta / 8:
+            return lo, hi
+        bits *= 2
+
+
+def source_check():
+    sources = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))
+    count = 0
+    for entry in sources["files"]:
+        if entry["usage"] == "input":
+            raw = (ROOT / entry["path"]).read_bytes()
+            require(sha256(raw).hexdigest() == entry["sha256"], "source hash mismatch: " + entry["path"])
+            count += 1
+    return count
+
+
+def verify():
+    pins = source_check()
+    # Exact boundary models, not complete fine-prime multiplier instances.
+    families = ((4, 5, 1, 1), (7, 8, 1, 2), (31, 32, 4, 3), (31, 34, 1, 3), (127, 128, 9, 4))
+    records = []
+    counts = dict(coefficients=0, positive=0, clipped=0, period_cuts=0, cell_cuts=0, ties=0,
+                  unrepaired_overshoots=0, phase_identities=0, oracle_boundary_cases=0)
+    for s, t, u, width in families:
+        for i in range(s):
+            qi, bi = phase(s, t, i)
+            for h in range(-width, width + 1):
+                qj, bj = phase(s, t, i + h)
+                ratio = exponent_ratio(s, t, u, i, h)
+                # Independent form uses the nearest-index jump.
+                jump = qj - qi
+                require(ratio == u * jump * (jump + F(2 * bj, s)), "phase identity")
+                require(-s <= 2 * bi < s and -s <= 2 * bj < s, "nearest-index range")
+                require((ratio == 0) == (h == 0), "strict exponent sign")
+                counts["phase_identities"] += 1
+                if h == 0:
+                    continue  # Store the matrix diagonal as exactly one.
+                period_cut = i // s != (i + h) // s
+                cell_cut = qi - i != qj - (i + h)
+                if not (period_cut or cell_cut):
+                    continue
+                for precision in (24, 64, 128):
+                    eta = F(1, 2 ** precision)
+                    lo, hi = gaussian_bounds(ratio, precision)
+                    q = floor((lo + hi) / (2 * eta) + F(1, 2)) * eta
+                    require(max(abs(q - lo), abs(q - hi)) < 2 * eta, "oracle error contract")
+                    stored = repair(q, eta)
+                    check_bound(stored, lo, hi, eta)
+                    counts["coefficients"] += 1
+                    counts["positive" if stored else "clipped"] += 1
+                    counts["period_cuts"] += int(period_cut)
+                    counts["cell_cuts"] += int(cell_cut)
+                    counts["ties"] += int(2 * bi == -s or 2 * bj == -s)
+                    counts["unrepaired_overshoots"] += int(q > hi)
+                    records.append([s, t, u, i, h, precision, str(ratio), str(stored)])
+    # Exhaust permitted oracle numerators on a rational test mesh, including
+    # negative outputs and both sides of the clipping point.
+    eta = F(1, 32)
+    for n16 in range(513):
+        value = n16 * eta / 16
+        for m in range(floor(value / eta) - 3, ceil(value / eta) + 4):
+            q = m * eta
+            if abs(q - value) < 2 * eta:
+                out = repair(q, eta)
+                check_bound(out, value, value, eta)
+                counts["oracle_boundary_cases"] += 1
+    # Rational counterexamples to weakening each stated requirement.
+    rejects_bound(3 * eta, F(3, 2) * eta, eta)  # no subtraction
+    rejects_bound(3 * eta - eta, F(3, 2) * eta, eta)  # only one ulp
+    rejects_bound(-2 * eta, eta / 4, eta)  # no clipping
+    rejects_bound(repair(2 * eta, eta), 4 * eta, eta)  # nonstrict oracle error
+    coarse = 2 * eta
+    rerounded = floor(repair(3 * eta, eta) / coarse + F(1, 2)) * coarse
+    rejects_bound(rerounded, F(3, 2) * eta, eta)  # later nearest-grid rounding
+    wrong_ratio = F(5, 4)  # #4442's bare-kernel substitution.
+    right_ratio = exponent_ratio(4, 5, 1, 1, 1)
+    require(right_ratio == 2, "cross-cell square-gap witness")
+    wl, wh = gaussian_bounds(wrong_ratio, 64)
+    _, right_upper = gaussian_bounds(right_ratio, 64)
+    unit = F(1, 2 ** 64)
+    wrong_stored = repair(floor((wl + wh) / (2 * unit) + F(1, 2)) * unit, unit)
+    require(wrong_stored > right_upper, "wrong kernel must violate the upper bound")
+    for args in ((0, 1, 1, 0, 1), (4, 4, 1, 1, 1), (4, 5, 0, 1, 1), (4, 5, 1, 1, F(1, 2))):
+        try:
+            exponent_ratio(*args)
+        except ValueError:
+            pass
+        else:
+            raise ValueError("invalid domain accepted")
+    require(all(counts[k] > 0 for k in counts), "missing positive/boundary coverage")
+    return {"source_files": pins, **counts, "failure_controls": 10,
+            "record_sha256": sha256(json.dumps(records, separators=(",", ":")).encode("ascii")).hexdigest()}
+
+
+if __name__ == "__main__":
+    result = verify()
+    if sys.argv[1:] == ["--emit"]:
+        print(json.dumps(result, indent=2))
+    else:
+        require(not sys.argv[1:], "usage: verify.py [--emit]")
+        expected = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8"))
+        require(result == expected, "receipt mismatch")
+        print("PASS_GAUSSIAN_CROSS_ROUNDING " + json.dumps(result, sort_keys=True))