diff --git a/research/sharp-gaussian-schur-range/PROOF.md b/research/sharp-gaussian-schur-range/PROOF.md
new file mode 100644
index 0000000000..3daa4261e7
--- /dev/null
+++ b/research/sharp-gaussian-schur-range/PROOF.md
@@ -0,0 +1,166 @@
+# The sharp uniform Gaussian minor range
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement and predecessor boundary
+
+Let b>=1 and n>=1 be integers, and let t>0 be real. On indices 0,...,n-1 put
+
+```text
+G[i,j] = t^((i-j)^2) if |i-j|<=b, and 0 otherwise.
+```
+
+The largest parameter interval on which the following criterion holds for
+every n and b is exactly **0<t<=1/2**. For any equally long increasing row
+and column lists R and C,
+
+```text
+det G[R,C] > 0  iff  |R_l-C_l|<=b for every l;
+det G[R,C] = 0  otherwise.
+```
+
+The empty minor is one. Consequently all principal pivots are positive.
+For any eliminated set E and surviving i<j, the Schur entry is nonzero
+exactly when the chain from i to j through E intersect (i,j) has every
+successive gap at most b. Its sign is (-1)^|E intersect (i,j)|. Diagonal
+Schur entries are positive. Independent positive row and column gauges
+preserve these conclusions.
+
+PR5207 proves these implications from a positive bidiagonal factorization
+of the finite Gaussian polynomial and establishes the sufficient range
+0<t<=1/3. That theorem and its classical path argument are cited premises,
+not audit targets. The new steps are a sharper alternating-sign estimate,
+the exceptional repeated-root endpoint, and an obstruction at every t>1/2.
+They answer its Open next question 2. A short account of the inherited
+factorization implication below makes the dependency explicit.
+
+## 1. The alternating tail
+
+For L>=0 define A_L(t)=sum_(r=1)^L (-1)^r t^(r^2). For 0<t<1,
+
+```text
+A_0=0,  A_1=-t,  A_L>-t for every L>=2.
+```
+
+Indeed, after the first term, pair the terms of indices 2,3, then 4,5,
+and so on. Each pair t^((2k)^2)-t^((2k+1)^2) is strictly positive.
+An unpaired last even term is also strictly positive. This works for
+each finite tail and does not replace it by an absolute-value bound.
+
+Define the degree-2b polynomial
+
+```text
+P_b(z) = sum_(h=-b)^b t^(h^2) z^(h+b).
+```
+
+At z_j=-t^(-2j), for -b<=j<=b, division by its jth summand gives
+
+```text
+P_b(z_j) / [(-1)^(j+b) t^(-j^2-2jb)]
+    = 1 + A_(b+j)(t) + A_(b-j)(t).
+```
+
+If one tail is empty, this is at least 1-t>0. If both are nonempty,
+it is at least 1-2t. Thus it is strictly positive for t<1/2.
+At t=1/2 and b>=2, the two lengths sum to 2b>=4, so at least one is
+at least two. Its strict tail inequality again gives strict positivity.
+
+The 2b+1 negative evaluation points are distinct, and the displayed
+signs alternate. The intermediate value theorem supplies a root in
+each consecutive interval. The degree is 2b, so all roots are negative
+and simple in these cases. Write them as -lambda_r with lambda_r>0.
+
+The only omitted case is b=1, t=1/2. Here
+
+```text
+P_1(z) = (z+1)^2/2.
+```
+
+Its repeated root is still negative. Repeated roots do not remove the
+strict minor criterion: its path weights remain strictly positive.
+For every 0<t<=1/2 and every b>=1 we have therefore proved
+
+```text
+P_b(z) = t^(b^2) product_(r=1)^(2b) (z+lambda_r),  lambda_r>0.
+```
+
+## 2. The factorization implication
+
+As in PR5207, let T[i,j]=1 if i=j+1. The formal Laurent expression
+for the doubly infinite band kernel is
+
+```text
+G = t^(b^2) T^(-b) product_r (lambda_r I+T).
+```
+
+This is a finite path identity with 2b steps, so there is no convergence
+issue. A path from column c to row r+b stays put or advances by one at
+each step. Its weight is positive, including when some lambdas coincide.
+The classical determinant path cancellation leaves precisely the
+nonintersecting, order-preserving path families. Such a family requires
+|R_l-C_l|<=b. When those inequalities hold, positions
+
+```text
+x_l(s) = max(C_l, R_l+b-(2b-s)),  0<=s<=2b,
+```
+
+give a family explicitly: each increment is zero or one, and positions
+strictly increase with l at every time. The minor is then strictly
+positive. If an inequality fails, there is no surviving family and
+the minor is zero. This proves that the new factorization satisfies
+exactly the premise used by PR5207; simplicity of roots is unnecessary.
+
+For the Schur conclusion, the block determinant formula expresses S[i,j]
+as the minor with row list (E,i) and column list (E,j), divided by the
+positive principal minor on E. Sorting the appended lists gives sign
+(-1)^|E intersect (i,j)|. The ordered-minor criterion becomes the stated
+chain-gap criterion. For i=j it is a principal numerator. Positive
+diagonal gauges multiply the Schur entry by the corresponding positive
+row and column factors.
+
+## 3. Every larger t fails
+
+Set b=1 and let D_n be the full n-by-n principal determinant. Expansion
+along the last row of this tridiagonal matrix gives
+
+```text
+D_0=1, D_1=1, D_n=D_(n-1)-t^2 D_(n-2).
+```
+
+At t=1/2 this recurrence gives D_n=(n+1)/2^n>0, consistent with
+the included repeated-root endpoint.
+
+For any t>1/2 put theta=arccos(1/(2t)). Then 0<theta<pi/2.
+The same initial values and sine addition identity prove
+
+```text
+D_n = t^n sin((n+1)theta)/sin(theta).
+```
+
+Choose n=floor(pi/theta). Then
+
+```text
+pi < (n+1)theta <= pi+theta < 3pi/2,
+```
+
+so D_n<0. Its row and column lists agree, hence every matched distance
+is zero. The asserted strict positivity criterion therefore fails.
+An earlier determinant may vanish; that also contradicts positivity
+of every principal pivot and does not affect this negative witness.
+This excludes every t>1/2, not merely a finite sample above the endpoint.
+
+## Scope
+
+This is a scoped algebraic proof, with exact finite corroboration in
+verify.py. It proves the maximal uniform parameter interval, not a
+maximal interval at a fixed bandwidth or matrix size. Classical
+alternating sums, polynomial separation, determinant paths and the
+tridiagonal recurrence retain their usual credit. No literature-priority
+claim is made for those methods or for general total-positivity theory.
+
+No concrete retained Gaussian caller has been shown to meet the real,
+linear-path and positive-gauge hypotheses. Periodic or complex kernels,
+conditioning, rounding, tape execution, routing, native implementation,
+stock, compiler admission and exact recovery remain separate obligations.
+No new kappa, selected-frontier change or complete multiplication theorem
+is claimed. Independent human and formal proof-kernel review are unclaimed.
diff --git a/research/sharp-gaussian-schur-range/README.md b/research/sharp-gaussian-schur-range/README.md
new file mode 100644
index 0000000000..afaaa05f9c
--- /dev/null
+++ b/research/sharp-gaussian-schur-range/README.md
@@ -0,0 +1,127 @@
+# Sharp Gaussian Schur-fill range: 0<t<=1/2
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with exact finite corroboration. No new kappa.
+
+For every finite line and every integer bandwidth b>=1, define
+
+```text
+G[i,j] = t^((i-j)^2) if |i-j|<=b, and 0 otherwise.
+```
+
+The exact positive parameter range with the following strict ordered-minor
+criterion, uniformly over all sizes and bandwidths, is **0<t<=1/2**:
+
+```text
+det G[R,C] > 0 iff |R_l-C_l|<=b for every matched position l;
+det G[R,C] = 0 otherwise.
+```
+
+Here R and C are equally long increasing lists. Every principal pivot is
+positive. For surviving i<j after eliminating E, a Schur entry is nonzero
+exactly when the chain through E intersect (i,j) has every successive gap
+at most b. Its sign is (-1)^|E intersect (i,j)|. Schur diagonal entries
+are positive, and independent positive row and column scalings preserve
+these statements.
+
+[PR5207](https://github.com/CrocSwap/integer-mult-bounds/pull/5207) proves
+the sufficient range 0<t<=1/3 and explicitly leaves the largest uniform
+range open. The new result settles that question. It replaces the earlier
+absolute-value estimate by a finite alternating-tail bound and handles
+the repeated root at b=1,t=1/2. For every t>1/2 a width-one principal
+determinant is negative at an explicitly specified finite order.
+[PROOF.md](PROOF.md) gives the universal proof. The predecessor's path
+factorization implication is cited and explained; its census is not replayed.
+
+## Exact evidence
+
+The standalone verifier tests only parameters in the new range,
+t=2/5,9/20,1/2. It uses the standard library and exact integers/fractions.
+
+- 503 strictly signed polynomial evaluations through b=12, the one
+  exceptional zero at b=1,t=1/2, and 75 alternating-tail checks.
+- All 8,307 nonempty ordered minors of six-vertex kernels at b=1,2,3:
+  6,525 positive and 1,782 zero.
+- All 2,223 nonempty-survivor Schur layouts through n=7 at b=1,2,3.
+  Literal rational pivot updates and integer determinant ratios agree on
+  all 25,335 entries: 16,503 positive, 4,632 negative and 4,200 zero.
+- Six rational parameters above 1/2 have first negative principal orders
+  5,4,15,22,49,157, respectively for t=3/5,2/3,51/100,101/200,501/1000,
+  5001/10000. Rational and denominator-cleared integer recurrences agree.
+  The endpoint identity D_n=(n+1)/2^n is checked through n=512.
+- Eight invalid inputs and three altered matrices reject. Two exact Schur
+  fixtures detect fill beyond the original band and negative fill parity.
+
+These finite computations corroborate the written proof. They do not
+establish its universal quantifiers by extrapolation. Checks use explicit
+exceptions and remain active under optimized Python.
+
+## Reproduce
+
+From the repository root, with CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sharp-gaussian-schur-range/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sharp-gaussian-schur-range/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sharp-gaussian-schur-range
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sharp-gaussian-schur-range --check-source-history
+```
+
+Substitute another CPython 3.12 interpreter elsewhere. Expected statuses
+are `PASS_SHARP_GAUSSIAN_SCHUR_RANGE`, `PASS_REGISTERED_RESEARCH_PACKAGE`
+and `PASS_RESEARCH_COMMIT_BYTES`. Each registered command has a 120-second
+limit. The replay writes nothing. Its generated JSON includes the result,
+enumerated counts, exact negative determinants, interpreter version and
+SHA256 hashes of all six package files. `--receipt /absolute/new/path.json`
+also writes that generated receipt to an unoccupied path outside the package.
+No receipt is handwritten or committed.
+
+All [source pins](SOURCES.json) are historical provenance at base main
+7c49fe32c55de02c2c873655c804b16e4c3fef0a. No predecessor executable or
+external scientific input is imported. [TASK.json](TASK.json) records the
+changed card scope, open questions and bounded overlap coverage. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360761)
+precedes the proof and replay.
+
+## Limitations
+
+The sharpness assertion is uniform over bandwidths. A fixed b>=2 can
+have a wider range; this package does not determine it. No concrete
+retained caller is shown to satisfy the real linear-path hypotheses.
+Periodic kernels, complex or nonpositive phases, conditioning, rounding,
+native realization, ownership, routing, stock, tape costs, compiler
+admission and exact recovery remain unproved here. The five selected
+framework assumptions remain. No supplier admission, selected-frontier
+change or complete multiplication theorem is claimed.
+
+Independent human and formal proof-kernel review are unclaimed. Lean,
+Docker, predecessor scientific replays and the selected full cold replay
+were not run. The verifier has no recursion, dynamic code generation or
+third-party dependency. Matrix dimensions are bounded by seven, polynomial
+bandwidths by twelve and recurrence orders by 512. Exact Python arithmetic
+uses managed allocation; its integer sizes are bounded by these fixed
+domains. Package-hash reads are limited to the six declared source files.
+
+## Open next questions
+
+1. Can one concrete retained Gaussian caller use the sharp criterion after
+   positive gauges? First pin its actual linear kernel, derive t and its
+   truncation, and retain all conditioning and paid caller obligations.
+   The missing caller and any additional phases are the blockers.
+2. For a fixed b>=2, what is the largest parameter interval with the same
+   ordered-minor criterion? First study the finite Gaussian polynomial's
+   roots, then prove an all-size factorization or give a failing minor.
+   A finite positive table cannot establish the interval.
+
+## Credit
+
+Nick Petalas / PR5207 supplies the question, the earlier sufficient range
+and the path-factorization implication. Ryanson Jonathan / PR4407 supplies
+the actual-real-entry question and generic support formula; unpaidmoon /
+PR4373 supplies the separated carve; James Reed supplies the earlier
+bandwidth and Gaussian fixtures; Cinna Davis / PR4100 supplies the retained
+Gaussian caller motivation and lineage. Those results are cited premises
+and their files and credit are unchanged. Alternating sums, negative-root
+factorization, path cancellation and tridiagonal recurrences are classical.
+No literature-priority claim is made for these general methods.
diff --git a/research/sharp-gaussian-schur-range/SOURCES.json b/research/sharp-gaussian-schur-range/SOURCES.json
new file mode 100644
index 0000000000..df24a28752
--- /dev/null
+++ b/research/sharp-gaussian-schur-range/SOURCES.json
@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/carve-schur-bandwidth-census/README.md",
+      "usage": "provenance",
+      "git_blob": "525387652dfb847f05b76d3e98aea653ee35749e",
+      "sha256": "e95963d7bcae7c052ddb16d086f6405b8aaee628930528d6799cc965d85b8dc9"
+    },
+    {
+      "path": "research/gaussian-carve-schur-bandwidth/README.md",
+      "usage": "provenance",
+      "git_blob": "cebb6a30cc0859822dd256dee78f54ca97fa238d",
+      "sha256": "31b2930d6c140c526ff2fe0a68216b1ff17d22df9ef4a3c518079037e86b232a"
+    },
+    {
+      "path": "research/gaussian-schur-fill-sign/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "f69ad9341bcb9719deb972c457067b0880f1ec82",
+      "sha256": "73dc1d79ab4f076de87f4700ef8b155ff7dde1698fdf34ecb7700534b453f8ae"
+    },
+    {
+      "path": "research/gaussian-schur-fill-sign/README.md",
+      "usage": "provenance",
+      "git_blob": "ea04de57acc8af0515438bdd7dce4119a6e13229",
+      "sha256": "37fad85af990fb2360d1fae2cc8b59ac099e057a58336f12c8b66e517f2f831e"
+    }
+  ]
+}
diff --git a/research/sharp-gaussian-schur-range/TASK.json b/research/sharp-gaussian-schur-range/TASK.json
new file mode 100644
index 0000000000..2c9807abaf
--- /dev/null
+++ b/research/sharp-gaussian-schur-range/TASK.json
@@ -0,0 +1,110 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "Determine the exact bandwidth-uniform positive parameter range for the strict ordered-minor and Schur-fill sign criterion of the linearly truncated real Gaussian kernel. The sharp range is 0<t<=1/2, extending PR5207's sufficient 0<t<=1/3 range and excluding every larger t.",
+  "scope_change_reason": "Take the explicit unresolved endpoint question in PR5207, Open next question 2. The formal-interface card is changed to a written algebraic interface theorem rather than an audit or a proof-assistant formalization. The predecessor criterion is cited; only the new parameter range and sharp obstruction are claimed.",
+  "bottleneck_link": "A Gaussian inverse/Schur interface side result: determine when all structural real fill is present and every principal pivot is positive. This enlarges the proven parameter range but does not bind a retained caller or move the selected supplier budget.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved endpoint improvement, its universal sharpness obstruction and bounded exact corroboration. No larger-band threshold search or caller integration.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the all-size argument. The standalone verifier checks the new range t=2/5,9/20,1/2: 503 strict polynomial evaluations and one exceptional zero; 75 finite alternating tails; 8307 ordered minors; 2223 Schur layouts and 25335 entries by rational updates and integer determinant ratios; six above-half obstructions; 511 endpoint recurrence steps; eight invalid inputs, three altered-matrix rejections and two Schur scope fixtures.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one concrete retained Gaussian caller use the sharp 0<t<=1/2 criterion after its positive gauges?",
+      "why_it_matters": "The uniform algebraic threshold alone does not admit a physical Gaussian boundary solve.",
+      "first_step": "Pin one actual linear kernel and derive its real parameter, truncation and gauge factors, then retain the complete conditioning and paid caller obligations.",
+      "blocked_by": "An authenticated concrete caller and any complex, periodic or nonpositive phase factors."
+    },
+    {
+      "question": "For a fixed bandwidth b>=2, what is the exact largest parameter interval with the ordered-minor criterion?",
+      "why_it_matters": "The sharp uniform obstruction uses b=1 and does not settle the larger fixed-bandwidth range.",
+      "first_step": "Study the corresponding finite Gaussian polynomial and supply an all-size root-factorization proof or explicit failing minors.",
+      "blocked_by": "A fixed-bandwidth all-size argument; finite positive tables alone do not establish it."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360761",
+    "upstream_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "priority_revision": 8,
+    "source_pr": 5207,
+    "source_created_at": "2026-10-23T12:33:26Z",
+    "overlap_checked_at": "2026-11-02T21:15:00Z",
+    "coverage": "Live open PRs and last 30 handoff comments, active discussions, recent same-account work, merged Gaussian/ordered-minor/root searches and main-tree README searches. Cached formal-interface scan reported 351 open PRs and 6251 Discussion records with complete remote pagination; sparse local note coverage was incomplete. No arbitrary historical diffs or unpublished-work coverage is claimed."
+  }
+}
diff --git a/research/sharp-gaussian-schur-range/VERIFY.json b/research/sharp-gaussian-schur-range/VERIFY.json
new file mode 100644
index 0000000000..5646dade02
--- /dev/null
+++ b/research/sharp-gaussian-schur-range/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact new-range polynomial signs, ordered minors, Schur signs and determinant ratios, repeated-root endpoint, above-half negative determinants and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact new-range polynomial signs, ordered minors, Schur signs and determinant ratios, repeated-root endpoint, above-half negative determinants and rejection controls under optimized Python."
+    }
+  ]
+}
diff --git a/research/sharp-gaussian-schur-range/verify.py b/research/sharp-gaussian-schur-range/verify.py
new file mode 100644
index 0000000000..24c98f5742
--- /dev/null
+++ b/research/sharp-gaussian-schur-range/verify.py
@@ -0,0 +1,276 @@
+#!/usr/bin/env python3
+"""Exact corroboration of the sharp Gaussian minor range. Apache-2.0."""
+
+import argparse
+from fractions import Fraction
+import hashlib
+from itertools import combinations
+import json
+from pathlib import Path
+import platform
+
+
+MAX_BAND = 12
+MAX_SIZE = 7
+NEGATIVE_LIMIT = 512
+PARAMETERS = (Fraction(2, 5), Fraction(9, 20), Fraction(1, 2))
+FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+
+
+def require(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def kernel(size, band, parameter):
+    if type(size) is not int or not 1 <= size <= MAX_SIZE:
+        raise ValueError("size outside finite replay domain")
+    if type(band) is not int or not 1 <= band <= MAX_BAND:
+        raise ValueError("band outside finite replay domain")
+    if not isinstance(parameter, Fraction) or not 0 < parameter < 1:
+        raise ValueError("parameter outside finite replay domain")
+    return [[parameter ** ((i - j) ** 2) if abs(i - j) <= band else Fraction(0)
+             for j in range(size)] for i in range(size)]
+
+
+def integer_kernel(size, band, parameter):
+    """Scale every entry by denominator**band**2 before Bareiss elimination."""
+    matrix = kernel(size, band, parameter)
+    scale = parameter.denominator ** (band * band)
+    integer = []
+    for row in matrix:
+        converted = [entry * scale for entry in row]
+        require(all(entry.denominator == 1 for entry in converted), "integer scaling")
+        integer.append([entry.numerator for entry in converted])
+    return integer, scale
+
+
+def determinant(matrix):
+    """Integer Bareiss determinant, including row swaps and singular minors."""
+    size = len(matrix)
+    require(size <= MAX_SIZE and all(len(row) == size for row in matrix), "minor shape")
+    if size == 0:
+        return 1
+    work = [row[:] for row in matrix]
+    previous, sign = 1, 1
+    for column in range(size - 1):
+        pivot_row = next((i for i in range(column, size) if work[i][column]), None)
+        if pivot_row is None:
+            return 0
+        if pivot_row != column:
+            work[column], work[pivot_row] = work[pivot_row], work[column]
+            sign = -sign
+        pivot = work[column][column]
+        for i in range(column + 1, size):
+            for j in range(column + 1, size):
+                value = work[i][j] * pivot - work[i][column] * work[column][j]
+                quotient, remainder = divmod(value, previous)
+                require(remainder == 0, "Bareiss exact division")
+                work[i][j] = quotient
+            work[i][column] = 0
+        previous = pivot
+    return sign * work[-1][-1]
+
+
+def submatrix(matrix, rows, columns):
+    return [[matrix[i][j] for j in columns] for i in rows]
+
+
+def check_minor(matrix, rows, columns, band):
+    value = determinant(submatrix(matrix, rows, columns))
+    permitted = all(abs(i - j) <= band for i, j in zip(rows, columns, strict=True))
+    require(value > 0 if permitted else value == 0, "ordered minor criterion")
+    return "positive" if permitted else "zero"
+
+
+def polynomial_checks():
+    positive, double_root, paired_tails = 0, 0, 0
+    for parameter in PARAMETERS:
+        for length in range(2 * MAX_BAND + 1):
+            tail = sum(((-1) ** r * parameter ** (r * r)
+                        for r in range(1, length + 1)), Fraction(0))
+            require(tail >= -parameter, "alternating tail lower bound")
+            if length >= 2:
+                require(tail > -parameter, "strict paired tail")
+            paired_tails += 1
+        for band in range(1, MAX_BAND + 1):
+            for j in range(-band, band + 1):
+                z = -(parameter ** (-2 * j))
+                value = sum((parameter ** (h * h) * z ** (h + band)
+                             for h in range(-band, band + 1)), Fraction(0))
+                normalized = value / ((-1) ** (j + band)
+                                         * parameter ** (-j * j - 2 * j * band))
+                if parameter == Fraction(1, 2) and band == 1 and j == 0:
+                    require(normalized == 0, "exceptional endpoint evaluation")
+                    double_root += 1
+                else:
+                    require(normalized > 0, "strict polynomial sign")
+                    positive += 1
+    coefficients = [Fraction(1, 2) ** (h * h) for h in (-1, 0, 1)]
+    require(coefficients == [Fraction(v, 2) for v in (1, 2, 1)], "endpoint factorization")
+    return {"positive_evaluations": positive, "double_root_evaluations": double_root,
+            "alternating_tails": paired_tails}
+
+
+def minor_checks():
+    counts = {"positive": 0, "zero": 0}
+    for parameter in PARAMETERS:
+        for band in range(1, 4):
+            matrix, _ = integer_kernel(6, band, parameter)
+            for order in range(1, 7):
+                subsets = tuple(combinations(range(6), order))
+                for rows in subsets:
+                    for columns in subsets:
+                        counts[check_minor(matrix, rows, columns, band)] += 1
+    return counts
+
+
+def schur(matrix, eliminated):
+    """Literal successive rational pivot updates; no determinant formula."""
+    work = [row[:] for row in matrix]
+    active = list(range(len(work)))
+    for pivot in eliminated:
+        diagonal = work[pivot][pivot]
+        require(diagonal > 0, "positive chronological pivot")
+        remaining = [i for i in active if i != pivot]
+        for i in remaining:
+            for j in remaining:
+                work[i][j] -= work[i][pivot] * work[pivot][j] / diagonal
+        active = remaining
+    return work, active
+
+
+def expected_entry(i, j, eliminated, band):
+    if i == j:
+        return 1
+    lower, upper = sorted((i, j))
+    inside = [e for e in eliminated if lower < e < upper]
+    chain = [lower, *inside, upper]
+    if any(y - x > band for x, y in zip(chain, chain[1:])):
+        return 0
+    return (-1) ** len(inside)
+
+
+def schur_checks():
+    counts = {"layouts": 0, "positive": 0, "negative": 0, "zero": 0,
+              "determinant_ratios": 0}
+    for parameter in PARAMETERS:
+        for band in range(1, 4):
+            for size in range(1, MAX_SIZE + 1):
+                matrix = kernel(size, band, parameter)
+                integers, scale = integer_kernel(size, band, parameter)
+                for mask in range((1 << size) - 1):
+                    eliminated = [i for i in range(size) if mask & (1 << i)]
+                    result, survivors = schur(matrix, eliminated)
+                    denominator = determinant(submatrix(integers, eliminated, eliminated))
+                    require(denominator > 0, "positive full principal pivot")
+                    counts["layouts"] += 1
+                    for i in survivors:
+                        for j in survivors:
+                            value = result[i][j]
+                            actual = (value > 0) - (value < 0)
+                            require(actual == expected_entry(i, j, eliminated, band), "Schur sign")
+                            rows, columns = [*eliminated, i], [*eliminated, j]
+                            numerator = determinant(submatrix(integers, rows, columns))
+                            require(value == Fraction(numerator, denominator * scale), "Schur ratio")
+                            counts["determinant_ratios"] += 1
+                            counts[{1: "positive", -1: "negative", 0: "zero"}[actual]] += 1
+    return counts
+
+
+def first_failed_principal(parameter):
+    require(Fraction(1, 2) < parameter < 1, "counterexample parameter")
+    previous, current = Fraction(1), Fraction(1)
+    for size in range(2, NEGATIVE_LIMIT + 1):
+        previous, current = current, current - parameter * parameter * previous
+        if current <= 0:
+            require(previous > 0, "first failed pivot has positive predecessor")
+            return size, current
+    raise AssertionError("finite counterexample search limit exhausted")
+
+
+def obstruction_checks():
+    witnesses = []
+    for text in ("3/5", "2/3", "51/100", "101/200", "501/1000", "5001/10000"):
+        parameter = Fraction(text)
+        size, value = first_failed_principal(parameter)
+        require(value < 0, "strict negative witness")
+        # An independent integer recurrence clears the rational denominator.
+        numerator, denominator = parameter.numerator, parameter.denominator
+        previous, current = 1, denominator
+        for order in range(2, size + 1):
+            previous, current = current, denominator * current - numerator * numerator * previous
+            if order < size:
+                require(current > 0, "integer positive prefix")
+        require(Fraction(current, denominator ** size) == value, "independent recurrence")
+        witnesses.append({"t": text, "first_negative_order": size,
+                          "determinant_numerator": str(value.numerator),
+                          "determinant_denominator": str(value.denominator)})
+    previous, current = Fraction(1), Fraction(1)
+    for size in range(2, NEGATIVE_LIMIT + 1):
+        previous, current = current, current - previous / 4
+        require(current == Fraction(size + 1, 2 ** size), "endpoint principal determinant")
+    return {"above_half": witnesses, "endpoint_recurrence_orders": NEGATIVE_LIMIT - 1}
+
+
+def controls():
+    rejected = 0
+    for size, band, parameter in ((0, 1, Fraction(1, 2)), (True, 1, Fraction(1, 2)),
+                                  (8, 1, Fraction(1, 2)), (3, 0, Fraction(1, 2)),
+                                  (3, 13, Fraction(1, 2)), (3, 1, Fraction(0)),
+                                  (3, 1, Fraction(1)), (3, 1, 0.5)):
+        try:
+            kernel(size, band, parameter)
+        except ValueError:
+            rejected += 1
+        else:
+            raise AssertionError("invalid input accepted")
+    mutants = []
+    matrix, _ = integer_kernel(3, 1, Fraction(1, 2))
+    bad_sign = [row[:] for row in matrix]
+    bad_sign[0][0] = -1
+    mutants.append((bad_sign, (0,), (0,)))
+    bad_support = [row[:] for row in matrix]
+    bad_support[0][2] = 1
+    mutants.append((bad_support, (0,), (2,)))
+    missing_edge = [row[:] for row in matrix]
+    missing_edge[0][1] = 0
+    mutants.append((missing_edge, (0,), (1,)))
+    for matrix, rows, columns in mutants:
+        try:
+            check_minor(matrix, rows, columns, 1)
+        except AssertionError as error:
+            require(str(error) == "ordered minor criterion", "wrong mutant failure")
+        else:
+            raise AssertionError("semantic mutant accepted")
+    result, _ = schur(kernel(4, 1, Fraction(1, 2)), [1, 2])
+    require(result[0][3] == Fraction(1, 6), "fill beyond original band")
+    result, _ = schur(kernel(3, 1, Fraction(1, 2)), [1])
+    require(result[0][2] == -Fraction(1, 4), "eliminated-index parity")
+    return {"input_rejections": rejected, "minor_mutants_rejected": len(mutants),
+            "Schur_scope_fixtures": 2}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--receipt", type=Path, help="write a new generated receipt outside the package")
+    arguments = parser.parse_args()
+    root = Path(__file__).resolve().parent
+    result = {"status": "PASS_SHARP_GAUSSIAN_SCHUR_RANGE", "claim_type": "scoped proof",
+              "sharp_endpoint": "1/2", "python": platform.python_version(),
+              "polynomial": polynomial_checks(), "ordered_minors": minor_checks(),
+              "Schur": schur_checks(), "obstructions": obstruction_checks(), "controls": controls()}
+    result["sha256"] = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() for name in FILES}
+    payload = json.dumps(result, indent=2, sort_keys=True) + "\n"
+    if arguments.receipt is not None:
+        output = arguments.receipt
+        if not output.is_absolute() or output.resolve().is_relative_to(root):
+            parser.error("receipt must be an absolute path outside the package")
+        with output.open("x", encoding="utf-8") as stream:
+            written = stream.write(payload)
+        require(written == len(payload), "complete receipt write")
+    print(payload, end="")
+
+
+if __name__ == "__main__":
+    main()