diff --git a/research/gaussian-concentration-threshold/PROOF.md b/research/gaussian-concentration-threshold/PROOF.md
new file mode 100644
index 0000000000..2efc909c8b
--- /dev/null
+++ b/research/gaussian-concentration-threshold/PROOF.md
@@ -0,0 +1,164 @@
+# The sharp concentration threshold for nearest-grid Gaussian dominance
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## Model and statement
+
+Let \(s,t\) be integers with \(s<t<2s\), \(\rho=t/s=1+\theta\),
+and use the physical Gaussian source's half-up convention
+
+\[
+q_j=\lfloor\rho j+1/2\rfloor,\qquad \beta_j=\rho j-q_j\in[-1/2,1/2).
+\]
+
+For real \(a>0\), define the original-coordinate coefficient at displacement
+\(h\ne0\) by
+
+\[
+k_{i,h}(a)=\exp\{-a[(\rho h+\beta_i)^2-\beta_{i+h}^2]\}.
+\]
+
+The cyclic matrix \(N_{s,t,w}(a)\), for integer \(1\le w<s/2\), has diagonal
+one and coefficient \(k_{i,h}\) at column \(i+h\pmod s\) for
+\(0<|h|\le w\); all other entries vanish. Since \(\beta_{j+s}=\beta_j\),
+this agrees with the source's signed cyclic displacement, including physical
+period seams. It is an ideal matrix, before numerical coefficient errors.
+The production concentration is \(a=\pi u\); here \(a\) is allowed to vary.
+
+Write \(R_i(a)=\sum_{0<|h|\le w}k_{i,h}(a)\). For every \(a\ge1\),
+
+\[
+\boxed{R_i(a)\le e^{-2a\theta}+2e^{-2a}
+                   +\frac{2e^{-6a}}{1-e^{-6a}}.}                 \tag{1}
+\]
+
+For even \(s\ge6\), \(t=s+1\), and \(2\le w<s/2\), the half-tie row
+\(i=s/2\) also satisfies
+
+\[
+\boxed{R_{s/2}(a)\ge e^{-2a/s}+e^{-a(2+4/s)}+e^{-a(2+8/s)}.}  \tag{2}
+\]
+
+For this family there is a unique threshold \(A_{s,w}>0\) such that every
+row is strictly diagonally dominant exactly when \(a>A_{s,w}\). Uniformly
+over every allowed \(w\ge2\), as even \(s\to\infty\),
+
+\[
+\boxed{A_{s,w}=\tfrac12(\log s-\log\log s+\log2)+o(1).}        \tag{3}
+\]
+
+All logarithms are natural. In particular the leading concentration
+coefficient \(1/2\), the subtractive log-log term, and the additive
+\(\log2/2\) are necessary for a uniform continuous-concentration guarantee.
+For integer \(u\), the least admitted value is
+\(\lfloor A_{s,w}/\pi\rfloor+1\); its corresponding expansion has
+\(O(1)\), rather than \(o(1)\), rounding uncertainty.
+
+## Upper bound
+
+The retained LOG-A-PHASE-SCHUR-AUDIT, section 1, already proves
+
+\[
+k_{i,-1}+k_{i,1}\le e^{-2a\theta}+e^{-2a(1+\theta)}.           \tag{4}
+\]
+
+We use that result as a premise. The new estimate concerns the farther
+tail. Since \(\beta_{i+h}^2\le1/4\), for each positive \(h\ge2\),
+
+\[
+k_{i,h}+k_{i,-h}\le
+e^{-a((\rho h+\beta_i)^2-1/4)}+
+e^{-a((\rho h-\beta_i)^2-1/4)}.
+\]
+
+The right side is an even convex function of \(\beta_i\) on
+\([-1/2,1/2]\). Indeed each summand's second derivative has the sign of
+\(2a(\rho h\pm\beta_i)^2-1\), which is positive for \(a\ge1,h\ge2\).
+Its maximum is therefore at an endpoint. Since \(\rho>1\), this gives
+
+\[
+k_{i,h}+k_{i,-h}\le e^{-ah(h-1)}+e^{-ah(h+1)}.
+\]
+
+Summing the positive convergent series and shifting the first index yields
+
+\[
+\sum_{|h|\ge2}k_{i,h}\le e^{-2a}
+           +2\sum_{r\ge2}e^{-ar(r+1)}
+\le e^{-2a}+\frac{2e^{-6a}}{1-e^{-6a}}.                        \tag{5}
+\]
+
+For the last inequality, successive exponents \(r(r+1)\) differ by at least
+six for \(r\ge2\). Combine (4), (5), and
+\(e^{-2a(1+\theta)}\le e^{-2a}\). A finite band only removes positive terms,
+so (1) follows without an infinite-period identification or a tail-admission
+assumption. The earlier \(5e^{-2a}\) tail coefficient is sufficient but
+does not locate the additive transition constant.
+
+## Lower bound
+
+For \(t=s+1\), even \(s\), and \(i=s/2\), the actual nearest convention gives
+
+\[
+\beta_i=-1/2,\quad
+\beta_{i+1}=-1/2+1/s,\quad
+\beta_{i-1}=1/2-1/s,\quad
+\beta_{i+2}=-1/2+2/s.
+\]
+
+Substitution into the coefficient definition gives exponents
+\(2/s\), \(2+4/s\), and \(2+8/s\) at displacements \(+1,-1,+2\).
+All three are retained for every \(w\ge2\). Dropping the other nonnegative
+entries proves (2). The second farther entry matters: retaining only one
+\(e^{-2a}\) contribution predicts an incorrect additive threshold.
+
+## Threshold and its uniform asymptotics
+
+Every off-diagonal exponent is positive because
+\(|\rho h+\beta_i|\ge\rho|h|-1/2>1/2\ge|\beta_{i+h}|\).
+Thus \(\max_i R_i(a)\) is continuous and strictly decreasing. At zero it is
+\(2w>1\), and it tends to zero at infinity. This proves existence and
+uniqueness of \(A_{s,w}\), including the strict endpoint convention.
+
+Set \(L=\log s\) and, for any fixed real \(b\),
+
+\[
+a_s(b)=\tfrac12(L-\log L+b),\qquad e^{-2a_s(b)}=s^{-1}Le^{-b}.
+\]
+
+As \(s\to\infty\), \(a_s(b)\to\infty\), \(a_s(b)/s\to0\), and
+
+\[
+\frac{1-e^{-2a_s(b)/s}}{s^{-1}L}\longrightarrow1.
+\]
+
+In (1) the other leading contribution, divided by \(s^{-1}L\), is
+\(2e^{-b}\); the remaining geometric tail divided by that scale tends
+to zero. In (2), the two farther terms have sum
+
+\[
+s^{-1}Le^{-b}(e^{-4a_s(b)/s}+e^{-8a_s(b)/s}),
+\]
+
+whose normalized limit is also \(2e^{-b}\). Consequently (1) proves
+dominance eventually whenever \(b>\log2\), and (2) proves failure
+eventually whenever \(b<\log2\). Neither estimate depends on \(w\).
+Sandwiching the threshold between these two concentrations, with \(b\)
+arbitrarily close to \(\log2\), proves (3) uniformly in \(w\).
+No sign at the exact choice \(b=\log2\) is asserted.
+
+## Scope and predecessor credit
+
+The matrix convention comes from Jose Manuel's PR3851 physical Gaussian
+core. The nearest-neighbor estimate (4) comes from Vlado Vojdanovski's
+retained phase-cell audit in the PR1673 lineage and its RaD/hipotures
+predecessors. The new result is the matching concentration threshold,
+using (5) and the three-entry obstruction. No predecessor computation is
+replayed as a contribution.
+
+This theorem varies concentration outside the unchanged production guard.
+It does not prove a changed production caller, coefficient-error bound,
+inverse implementation, complete signed invoice, or new multiplication
+theorem or kappa. The selected frontier and all five assumptions remain.
+The universal result is this written proof; the accompanying exact finite
+checks corroborate its new formulas and detect missing-tail admissions.
diff --git a/research/gaussian-concentration-threshold/README.md b/research/gaussian-concentration-threshold/README.md
new file mode 100644
index 0000000000..c4455545eb
--- /dev/null
+++ b/research/gaussian-concentration-threshold/README.md
@@ -0,0 +1,111 @@
+# A sharp Gaussian concentration threshold
+
+Scoped proof with exact finite controls. This contribution was produced by
+Nick Petalas. Apache-2.0. No new kappa is claimed.
+
+For the nearest-grid Gaussian matrix with expansion ratio \(1+1/s\), even
+\(s\), and any retained bandwidth \(2\le w<s/2\), let \(A_{s,w}\) be the
+continuous concentration at which the largest off-diagonal row sum equals
+one. [PROOF.md](PROOF.md) establishes
+
+\[
+A_{s,w}=\frac{\log s-\log\log s+\log2}{2}+o(1),
+\]
+
+uniformly in the bandwidth. Every row is strictly dominant exactly above
+that threshold. The result determines both the log-log correction and the
+additive constant. Integer concentration \(u\), with \(a=\pi u\), has the
+corresponding bounded rounding uncertainty.
+
+The new proof sharpens the farther-tail estimate to obtain
+
+\[
+R_i(a)\le e^{-2a\theta}+2e^{-2a}
+                    +\frac{2e^{-6a}}{1-e^{-6a}},\qquad a\ge1.
+\]
+
+Three literal entries at the half-tie row give the matching obstruction.
+At \(a=k\log2\) and \(s=2^{20}\), the exact controls certify failure for
+\(k=8\) and dominance for \(k=9\). A separate \(s=2^{19},k=8\) control
+shows that deleting one of the two leading tail contributions falsely
+certifies dominance. These finite examples are supporting certificates;
+the asymptotic statement follows from the written proof.
+
+## Reproduction and evidence
+
+From the repository root, using CPython 3.12 and only its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-concentration-threshold
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-concentration-threshold --check-source-history --check-modes
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/gaussian-concentration-threshold/verify.py
+```
+
+Use another CPython 3.12 executable on other machines. The registered commands
+run both normal and optimized modes. Each prints
+`PASS_GAUSSIAN_CONCENTRATION_THRESHOLD` and a generated report bound to the
+package and live-source SHA256 hashes. No receipt is handwritten.
+
+The finite checks enumerate 522 geometry equalities, 336 complete band rows
+and their 4,368 retained off-diagonal entries. They also classify all 231
+declared dyadic concentration/period pairs through \(s=2^{24}\), with 136
+certified dominant and 95 certified nondominant cases, none unresolved.
+Four malformed arithmetic-domain cases are rejected. All interval endpoints
+are integers on a 192-bit dyadic grid, using outward integer multiplication,
+integer square roots and bounded exponentiation. No floating point,
+transcendental implementation or predecessor verifier is used.
+
+The retained sources have exact main-commit, Git-blob and SHA256 pins in
+[SOURCES.json](SOURCES.json). Their mathematical conventions are inputs;
+their prior scientific results are cited rather than re-audited. The source
+checker authenticates both live files before the new finite calculations.
+
+## Scope and relation to existing work
+
+The [original question](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241969)
+changes concentration outside the unchanged production guard. It asks for
+a matching obstruction and sufficient condition at that changed guard.
+
+Jose Manuel's [PR3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851)
+supplies the physical matrix convention. The retained PR1673 phase-cell
+audit by Vlado Vojdanovski, with its RaD/hipotures predecessors, supplies
+the nearest-neighbor majorant. Its farther-tail estimate has coefficient
+five; the new estimate and half-tie obstruction determine the threshold.
+Gaussian convexity and geometric-series arguments are standard.
+
+[PR6099](https://github.com/CrocSwap/integer-mult-bounds/pull/6099) concerns
+coefficient perturbation and leaves production row dominance open.
+[PR6126](https://github.com/CrocSwap/integer-mult-bounds/pull/6126) improves
+the inverse bound under unchanged production guards. Neither is a theorem
+dependency here. The present result varies the guard and supplies a matching
+failure family, rather than computing that production inverse bound.
+
+No complete physical caller at reduced concentration is supplied. The theorem
+does not bound numerical coefficient errors, infinite periodization error,
+LU growth, physical preparation, tensor assembly or the full recursive bill.
+No selected cold replay, proof kernel or independent human review ran.
+The selected frontier and all five inherited assumptions remain unchanged.
+There is no sign claim at the exact critical asymptotic offset.
+
+## Open next questions
+
+1. Can a reduced-concentration physical caller pay its coefficient errors and
+   retain a sufficient inverse allowance? This could reduce normalization
+   charges. Start with the explicit sufficient bound above at one complete
+   production parameter tuple; physical geometry and the full error/cost
+   invoice remain blockers.
+2. What is the first vanishing correction to the continuous threshold? Start
+   with the same three half-tie entries and a sharper uniform remainder.
+   Identifying an exact maximizing row is the remaining obstacle. This is
+   separate from the proved additive \(\log2/2\) constant.
+
+## Verifier bounds
+
+The verifier has fixed finite fixture sets, at most 24 root or exponent-bit
+iterations per arithmetic call, and at most 256 indices in a geometry loop.
+Its matrix fixtures have at most 32 rows. It uses no recursion or indirect
+code execution. Python allocates managed integers and dictionaries during
+execution, a documented deviation from static allocation; their sizes are
+bounded by these fixtures and the fixed grid. Runtime contracts remain
+enabled under optimization. The universal mathematical claim rests on the
+proof, not on expanding those finite bounds.
diff --git a/research/gaussian-concentration-threshold/SOURCES.json b/research/gaussian-concentration-threshold/SOURCES.json
new file mode 100644
index 0000000000..fba299d5ef
--- /dev/null
+++ b/research/gaussian-concentration-threshold/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/capped-phase-fusion/evidence/gaussian_fast_ultra/LOG-A-PHASE-SCHUR-AUDIT.md",
+      "usage": "input",
+      "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73",
+      "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_axis.py",
+      "usage": "input",
+      "git_blob": "edc443a7281e83536a00e9f9fa950d7d854705a3",
+      "sha256": "d416918d7442c5033e43fba94ccc5ed33badc3aebe90ddd479b0b6c020de9724"
+    }
+  ]
+}
diff --git a/research/gaussian-concentration-threshold/TASK.json b/research/gaussian-concentration-threshold/TASK.json
new file mode 100644
index 0000000000..771179181c
--- /dev/null
+++ b/research/gaussian-concentration-threshold/TASK.json
@@ -0,0 +1,112 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the sharp continuous-concentration threshold for strict row dominance of the nearest-grid cyclic Gaussian family, uniformly in every retained bandwidth at least two.",
+  "scope_change_reason": "The formal-interface card is used for a written analytic interface theorem rather than proof-assistant formalization. This original changed-concentration question targets the cost of Gaussian normalization and a matching obstruction, not a predecessor audit or the separately reserved production-rowgap question.",
+  "bottleneck_link": "Concentration drives normalization and conditioning allowances in the retained physical Gaussian interface. A sharp necessary/sufficient threshold identifies a possible reduction and the obstruction that any such change must respect; no complete caller price or kappa improvement is asserted.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved new threshold with exact finite controls; leave reduced-concentration physical integration and lower-order refinements open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the uniform asymptotic threshold. verify.py checks 522 geometry equalities, 336 full band rows with 4368 retained entries, 231 concentration/period pairs, opposite dominance outcomes and a false-admission control.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a reduced-concentration physical caller pay coefficient errors while retaining a sufficient inverse allowance?",
+      "why_it_matters": "It could reduce normalization charges at the actual analytic interface.",
+      "first_step": "Apply the explicit row majorant to one complete production tuple and keep the numerical perturbation debit explicit.",
+      "blocked_by": "Physical geometry, coefficient error and complete caller cost obligations are not established at the changed guard."
+    },
+    {
+      "question": "What is the first vanishing correction to the continuous threshold?",
+      "why_it_matters": "It would quantify finite-parameter headroom beyond the proved additive constant.",
+      "first_step": "Expand the three half-tie entries and sharpen the uniform farther-tail remainder.",
+      "blocked_by": "An exact maximizing-row characterization is not established."
+    }
+  ],
+  "claim_type": "scoped proof with exact finite corroboration",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241969",
+  "environment": {
+    "python": "CPython 3.12.15",
+    "dependencies": "standard library only"
+  },
+  "principles": {
+    "build-the-lever": "Keep the exact finite corroboration as a standalone rerunnable script.",
+    "prove-it-works": "Run the registered checks, committed-source preflight and Git-free replay on the actual package.",
+    "power-of-ten": "Fixed finite loops, explicit runtime contracts and bounded fixed-grid arithmetic; managed Python allocation is documented."
+  }
+}
diff --git a/research/gaussian-concentration-threshold/VERIFY.json b/research/gaussian-concentration-threshold/VERIFY.json
new file mode 100644
index 0000000000..17d19a76b7
--- /dev/null
+++ b/research/gaussian-concentration-threshold/VERIFY.json
@@ -0,0 +1,31 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/capped-phase-fusion/evidence/gaussian_fast_ultra/LOG-A-PHASE-SCHUR-AUDIT.md",
+    "research/physical-gaussian-core/gaussian_axis.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact upper/lower concentration certificates, full finite band rows, half-up tie geometry and rejected arithmetic domains."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same complete scope with every runtime contract retained under optimization."
+    }
+  ]
+}
diff --git a/research/gaussian-concentration-threshold/verify.py b/research/gaussian-concentration-threshold/verify.py
new file mode 100644
index 0000000000..c878cd06a7
--- /dev/null
+++ b/research/gaussian-concentration-threshold/verify.py
@@ -0,0 +1,233 @@
+"""Exact finite controls for the Gaussian concentration threshold.
+
+Produced by Nick Petalas. Apache-2.0.
+The all-size theorem is in PROOF.md; no transcendental oracle is used here.
+"""
+
+from fractions import Fraction
+from hashlib import sha256
+from math import isqrt
+from pathlib import Path
+import json
+
+
+BITS = 192
+UNIT = 1 << BITS
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def times(left, right):
+    """Outward multiplication of nonnegative UNIT-grid intervals."""
+    require(0 <= left[0] <= left[1] <= UNIT, "left interval domain")
+    require(0 <= right[0] <= right[1] <= UNIT, "right interval domain")
+    return (left[0] * right[0] // UNIT,
+            (left[1] * right[1] + UNIT - 1) // UNIT)
+
+
+def root(interval):
+    require(0 <= interval[0] <= interval[1] <= UNIT, "root interval domain")
+    lower = isqrt(interval[0] * UNIT)
+    upper = isqrt(interval[1] * UNIT)
+    upper += upper * upper != interval[1] * UNIT
+    return lower, upper
+
+
+def power(interval, exponent):
+    require(isinstance(exponent, int) and 0 <= exponent < 1 << 24,
+            "bounded nonnegative interval power")
+    result = (UNIT, UNIT)
+    base = interval
+    for _ in range(exponent.bit_length()):
+        if exponent & 1:
+            result = times(result, base)
+        exponent >>= 1
+        base = times(base, base)
+    require(exponent == 0, "power consumes every exponent bit")
+    return result
+
+
+def decay(k, exponent):
+    """Enclose exp(-a*exponent), a=k*log(2), for dyadic exponent."""
+    require(isinstance(k, int) and 1 <= k <= 16, "dyadic decay parameter")
+    require(isinstance(exponent, Fraction) and exponent >= 0,
+            "nonnegative exact decay exponent")
+    exponent *= k
+    whole, remainder = divmod(exponent.numerator, exponent.denominator)
+    denominator = exponent.denominator
+    require(denominator <= 1 << 24 and denominator & (denominator - 1) == 0,
+            "bounded power-of-two exponent denominator")
+    if whole >= BITS:
+        return (1, 1) if whole == BITS and remainder == 0 else (0, 1)
+    base = (UNIT // 2, UNIT // 2)
+    for _ in range(denominator.bit_length() - 1):
+        base = root(base)
+    low, high = power(base, remainder)
+    shift = 1 << whole
+    return low // shift, (high + shift - 1) // shift
+
+
+def offset(s, index):
+    rho = Fraction(s + 1, s)
+    nearest = (2 * (s + 1) * index + s) // (2 * s)
+    beta = rho * index - nearest
+    require(-Fraction(1, 2) <= beta < Fraction(1, 2), "half-up offset range")
+    return beta
+
+
+def exponent(s, index, displacement):
+    rho = Fraction(s + 1, s)
+    result = ((rho * displacement + offset(s, index)) ** 2
+              - offset(s, index + displacement) ** 2)
+    require(displacement == 0 or result > 0, "strict off-diagonal decay")
+    return result
+
+
+def upper(k, s, tail_count=2):
+    """Universal majorant in the proof, with rational tail terms."""
+    require(tail_count in (1, 2), "explicit tail coefficient control")
+    z = decay(k, Fraction(2, s))
+    q = Fraction(1, 1 << k)
+    tail = tail_count * q ** 2 + 2 * q ** 6 / (1 - q ** 6)
+    return Fraction(z[0], UNIT) + tail, Fraction(z[1], UNIT) + tail
+
+
+def lower(k, s):
+    """Three actual entries in the half-tie row, including h=+2."""
+    theta = Fraction(1, s)
+    terms = [decay(k, value) for value in
+             (2 * theta, 2 + 4 * theta, 2 + 8 * theta)]
+    return (Fraction(sum(value[0] for value in terms), UNIT),
+            Fraction(sum(value[1] for value in terms), UNIT))
+
+
+def check_sources():
+    manifest = json.loads((PACKAGE / "SOURCES.json").read_text())
+    pins = {}
+    require(len(manifest["files"]) == 4, "bounded source inventory")
+    for row in manifest["files"]:
+        if row["usage"] == "input":
+            digest = sha256((ROOT / row["path"]).read_bytes()).hexdigest()
+            require(digest == row["sha256"], "source hash: " + row["path"])
+            pins[row["path"]] = digest
+    require(len(pins) == 2, "both mathematical source conventions are pinned")
+    return pins
+
+
+def check_arithmetic():
+    require(root((UNIT // 4, UNIT // 4)) == (UNIT // 2, UNIT // 2),
+            "exact square root positive fixture")
+    value = root((UNIT // 2, UNIT // 2))
+    require(value[0] ** 2 <= UNIT ** 2 // 2 <= value[1] ** 2,
+            "irrational square root enclosure")
+    require(power((UNIT // 2, UNIT // 2), 3) == (UNIT // 8, UNIT // 8),
+            "exact interval cube")
+    require(decay(2, Fraction(3, 2)) == (UNIT // 8, UNIT // 8),
+            "fractional decay with integral product")
+    require(decay(1, Fraction(BITS + 1)) == (0, 1), "bounded underflow enclosure")
+    rejected = 0
+    for k, value in ((0, Fraction(1)), (17, Fraction(1)),
+                     (1, Fraction(-1)), (1, Fraction(1, 3))):
+        try:
+            decay(k, value)
+        except ValueError:
+            rejected += 1
+    require(rejected == 4, "all invalid arithmetic domains rejected")
+    return rejected
+
+
+def check_geometry():
+    checked = 0
+    for s in (8, 16, 32, 64, 128, 256):
+        i = s // 2
+        require(offset(s, i) == -Fraction(1, 2), "literal half-up tie")
+        theta = Fraction(1, s)
+        for h, expected in ((1, 2 * theta), (-1, 2 + 4 * theta),
+                            (2, 2 + 8 * theta)):
+            require(exponent(s, i, h) == expected, "three-entry lower identity")
+            checked += 1
+        for j in range(s):
+            require(offset(s, j + s) == offset(s, j), "physical period offsets")
+            checked += 1
+    return checked
+
+
+def check_complete_rows():
+    rows = entries = 0
+    for s in (8, 16, 32):
+        for k in (2, 3, 4):
+            bound = upper(k, s)[1]
+            for w in (2, s // 2 - 1):
+                tie_low = None
+                for i in range(s):
+                    low = high = 0
+                    for h in range(-w, w + 1):
+                        if h:
+                            left, right = decay(k, exponent(s, i, h))
+                            low += left
+                            high += right
+                            entries += 1
+                    require(Fraction(high, UNIT) <= bound, "complete row below majorant")
+                    if i == s // 2:
+                        tie_low = Fraction(low, UNIT)
+                    rows += 1
+                require(tie_low is not None and tie_low >= lower(k, s)[0],
+                        "actual half-tie row contains lower witness")
+    return rows, entries
+
+
+def check_transition_controls():
+    admitted = excluded = unresolved = 0
+    for log_s in range(4, 25):
+        s = 1 << log_s
+        for k in range(2, 13):
+            lo, hi = lower(k, s)
+            left, right = upper(k, s)
+            require(lo <= hi and left <= right and lo <= right,
+                    "consistent independent upper/lower enclosures")
+            if right < 1:
+                admitted += 1
+            elif lo > 1:
+                excluded += 1
+            else:
+                unresolved += 1
+    s, k = 1 << 19, 8
+    bad = lower(k, s)[0]
+    wrong = upper(k, s, tail_count=1)[1]
+    require(wrong < 1 < bad, "omitting one leading tail gives a false admission")
+    require(upper(9, 1 << 20)[1] < 1 < lower(8, 1 << 20)[0],
+            "same-period positive and negative concentration controls")
+    require(admitted + excluded + unresolved == 231, "complete bounded scan")
+    return {"admitted": admitted, "excluded": excluded, "unresolved": unresolved,
+            "omitted_tail_false_admission": {"s": s, "k": k},
+            "same_period_bracket": {"s": 1 << 20, "bad_k": 8, "good_k": 9}}
+
+
+def main():
+    sources = check_sources()
+    rejected = check_arithmetic()
+    geometry = check_geometry()
+    rows, entries = check_complete_rows()
+    require((geometry, rows, entries) == (522, 336, 4368),
+            "complete registered geometry and row coverage")
+    transitions = check_transition_controls()
+    files = sorted(PACKAGE.glob("*"))
+    require(len(files) == 6 and all(path.is_file() for path in files),
+            "six regular package artifacts")
+    result = {"status": "PASS_GAUSSIAN_CONCENTRATION_THRESHOLD",
+              "arithmetic_rejections": rejected, "geometry_equalities": geometry,
+              "complete_rows": rows, "complete_entries": entries,
+              "transition_controls": transitions, "source_sha256": sources,
+              "package_sha256": {path.name: sha256(path.read_bytes()).hexdigest()
+                                 for path in files},
+              "scope": "Exact finite controls; the uniform asymptotic claim is a written proof."}
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()