Prove the sharp t=1/2 boundary for Gaussian Schur fill (no κ)

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.

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.

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"
+    }
+  ]
+}