Prove exact real Gaussian Schur fill signs for t <= 1/3 (no new κ)

research/gaussian-schur-fill-sign/PROOF.md

@@ -0,0 +1,157 @@
+# Noncancellation and signs of truncated Gaussian Schur fill
+
+This contribution was produced by Nick Petalas.
+
+## Statement
+
+Let n>=1 and b>=1 be integers, and let 0<t<=1/3 be real. On the
+linearly ordered indices 0,...,n-1 define
+
+    G[i,j] = t^((i-j)^2) if |i-j|<=b, and 0 otherwise.
+
+For any eliminated set E, every principal pivot G[E,E] has positive
+determinant, with the empty determinant defined as one. Thus the Schur
+complement S on V={0,...,n-1}\E exists.
+
+Its diagonal entries are positive. For i<j in V, form the ordered chain
+consisting of i, all elements of E strictly between i and j, and j.
+
+* S[i,j] is nonzero exactly when every successive chain gap is at most b.
+* In that case sign S[i,j] = (-1)^|E intersect (i,j)|.
+
+The same statements hold after independent positive row and column
+scalings of G. In particular positive diagonal similarities, including
+positive exponential chirps and linear shift gauges, preserve this support
+and these signs.
+
+This is a scoped written mathematical proof. It gives an actual real-entry
+attainment statement for the generic fill support discussed by Ryanson
+Jonathan in PR4407. It neither rechecks his finite-field census nor assumes
+its numerical results. It does not assert that a particular Gaussian caller
+has t<=1/3, or treat periodic distances, rounding or complex phases.
+
+## 1. A polynomial with distinct negative roots
+
+Define the degree-2b polynomial
+
+    P(z) = sum_(h=-b)^b t^(h^2) z^(h+b).
+
+For j=-b,...,b evaluate at z_j=-t^(-2j). Dividing by the jth term gives
+
+    P(z_j) / [(-1)^(j+b) t^(-j^2-2jb)]
+      = 1 + sum_(h != j) (-1)^(h-j) t^((h-j)^2).
+
+The absolute value of the sum on the right is at most
+
+    2 sum_(r>=1) t^(r^2)
+      <= 2 sum_(r>=1) t^(2r-1)
+       = 2t/(1-t^2) <= 3/4 < 1.
+
+Consequently P(z_j) has sign (-1)^(j+b). The 2b+1 evaluation points
+are distinct, ordered negative reals, and their signs alternate. Each of
+the 2b disjoint consecutive intervals contains a root by continuity.
+Since the degree is 2b, these roots are all the roots and are simple.
+Write them as -lambda_1,...,-lambda_(2b), with every lambda_r>0. Then
+
+    P(z) = t^(b^2) product_(r=1)^(2b) (z+lambda_r).
+
+This elementary sufficient range is all that is needed. No optimal
+root-realness threshold is claimed.
+
+## 2. Exactly which ordered minors are positive
+
+Consider the same kernel on all integer indices. Let T be the shift with
+T[i,j]=1 when i=j+1. Its formal Laurent polynomial representation is
+
+    G = t^(b^2) T^(-b) product_r (lambda_r I + T).
+
+Every entry involves only 2b steps, so this identity requires no convergence
+or infinite matrix multiplication. A path starts at column c, takes 2b
+steps, each staying put with weight lambda_r or increasing by one with
+weight one, and finishes at row r+b. All weights are positive.
+
+For increasing row and column lists R=(r_1,...,r_d) and C=(c_1,...,c_d),
+expand det G[R,C] as a signed sum of path families. Families with an
+intersection cancel in pairs: choose their first intersection by a fixed
+ordering and exchange the two path tails. This preserves their weight,
+reverses the endpoint permutation and is an involution. A family without
+intersections preserves the order of its starts and ends, so it contributes
+with positive sign. Therefore the minor is nonnegative.
+
+Such a family can exist only if
+
+    -b <= r_l-c_l <= b for every l.                 (1)
+
+Conversely suppose (1) holds. At time s=0,...,2b give path l position
+
+    x_l(s) = max(c_l, r_l+b-(2b-s)).
+
+It starts at c_l and ends at r_l+b. Every increment is zero or one.
+For each fixed s the positions strictly increase with l, since both
+arguments of the maximum strictly increase. These paths never intersect.
+Their positive weight proves the exact minor criterion
+
+    det G[R,C] > 0 iff |r_l-c_l|<=b for every l;
+    otherwise det G[R,C] = 0.                     (2)
+
+The cancellation argument and bidiagonal path factorization are classical
+techniques; no claim of their invention is made here. The proof above is
+included so that the specific strictness and support conclusions do not
+rely on a quoted total-positivity theorem.
+
+Taking R=C in (2) proves positivity of every principal determinant,
+including all eliminated pivots.
+
+## 3. Schur entries and their signs
+
+List E in increasing order, and append i to its row list and j to its
+column list. The block determinant formula gives
+
+    S[i,j] = det G[(E,i),(E,j)] / det G[E,E].
+
+Sorting both appended lists changes the numerator sign by
+
+    (-1)^(#{e in E:e>i} + #{e in E:e>j}).
+
+For i<j this is (-1)^|E intersect (i,j)|. The denominator is positive.
+The sorted row and column lists agree outside [i,j]. Within it they are
+respectively
+
+    (i,e_1,...,e_k) and (e_1,...,e_k,j),
+
+where e_1<...<e_k are precisely the eliminated indices between the endpoints.
+Criterion (2) is exactly that each successive gap in this chain be at most
+b. This proves both the zero criterion and the sign formula. For i=j the
+numerator is a principal determinant, so S[i,i]>0.
+
+The chain condition is equivalent to structural fill in the bandwidth-b
+path graph. If it holds, the chain itself is a path with eliminated internal
+vertices. If a gap is larger than b, no such path can cross the cut between
+these consecutive available vertices, even using eliminated vertices outside
+the endpoint interval. Thus every structurally possible fill is present,
+without any generic-entry qualification, in this restricted real Gaussian
+family. This supplies the missing actual-entry conclusion; the structural
+bandwidth formulas of PR4373/4407 remain predecessor results.
+
+## 4. Positive gauges
+
+For H=D_left G D_right with positive diagonal factors, direct substitution
+into the Schur formula gives
+
+    Schur_E(H) = D_left[V,V] S D_right[V,V].
+
+Every multiplier on an entry is positive. This proves the stated gauge
+corollary without bounding any gauge's condition number or physical cost.
+
+## Scope and first example
+
+For n=12, b=3, t=1/3 and E={4,5,6,7}, the entry between 1 and 10 is
+exactly 1/9170703360, at survivor-order distance five. The four intervening
+eliminated vertices give positive sign. This is a new Gaussian fixture,
+not a replay of James Reed's equal-weight path.
+
+Only the restricted real kernel and its positive scalings have been proved.
+The unrestricted t range, a concrete caller's admissibility, periodic
+kernels, finite-precision stability, physical routines and supplier admission
+remain outside this theorem. No new kappa or selected-frontier change.
+Independent human and formal proof-kernel review are unclaimed.

research/gaussian-schur-fill-sign/README.md

@@ -0,0 +1,111 @@
+# Exact signs and noncancellation of real Gaussian Schur fill
+
+This contribution was produced by Nick Petalas.
+
+For every bandwidth b>=1 and every finite linear path, truncate the real
+Gaussian kernel t^((i-j)^2) to |i-j|<=b. If 0<t<=1/3, every principal
+elimination pivot is invertible. The Schur entry between survivors i<j is
+nonzero exactly when the chain through the eliminated indices between i
+and j has no gap larger than b. Its sign is (-1)^k, where k is the number
+of those eliminated indices. Diagonal Schur entries are positive. Positive
+row and column scalings preserve all these conclusions.
+
+Claim type: scoped written mathematical proof with exact finite
+corroboration. [PROOF.md](PROOF.md) proves the all-size statement using an
+elementary negative-root factorization and ordered minors. Classical
+factorization and nonintersecting-path arguments are not claimed as new
+techniques. No independent human or formal proof-kernel review is claimed.
+
+This answers the explicit actual-real-entry gap in Ryanson Jonathan's
+[PR4407](https://github.com/CrocSwap/integer-mult-bounds/pull/4407) for the
+stated parameter range. That predecessor's generic support formula and
+finite-field census are cited, not replayed. The new result removes the
+possible-cancellation qualification for this restricted Gaussian family.
+It also determines every surviving sign.
+
+The first fixture has n=12, b=3, t=1/3 and eliminated set {4,5,6,7}.
+Its entry between 1 and 10 is exactly 1/9170703360, at survivor-order
+distance five. This is an actual Gaussian fixture, distinct from the
+inherited equal-weight paths.
+
+## Evidence and reproduction
+
+Use CPython 3.12 and its standard library from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-schur-fill-sign/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-schur-fill-sign/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-schur-fill-sign
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-schur-fill-sign --check-source-history
+```
+
+Substitute another CPython 3.12 interpreter elsewhere. Expected markers are
+`PASS_GAUSSIAN_SCHUR_FILL_SIGN`, `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_RESEARCH_COMMIT_BYTES`.
+
+The verifier checks 336 polynomial evaluation signs through bandwidth 12.
+For t=1/3 and 1/4 and b=1,2,3 it checks every nonempty ordered minor of
+the six-vertex kernel: 5,538 minors, of which 4,350 are positive and 1,188
+are zero. It explicitly constructs 4,350 nonintersecting path families.
+It then checks all 3,012 nonempty-survivor Schur layouts through n=8,
+including empty eliminated sets, and all 44,538 surviving entries:
+27,106 positive, 8,496 negative and 8,936 zero. Integer Bareiss determinants
+and independently implemented rational Gauss-Jordan complements agree with
+the claimed criteria. There is no finite-field or floating-point test.
+
+The first fixture and an exact positive-gauge identity pass. Six unsupported
+input fixtures are rejected; three mathematical scope controls retain the
+need for truncation, eliminated-vertex parity and a restricted t range.
+Checks remain active under optimized Python. Each run emits a generated
+receipt containing the six package-file hashes and interpreter version,
+and writes nothing. Bounded verification corroborates the universal proof;
+it does not replace it.
+
+## Scope and provenance
+
+The parameter range is a sufficient range, with no optimality claim. A
+concrete Gaussian caller has not been shown to meet it. Periodic kernels,
+complex phases, finite-precision stability, condition numbers, physical
+routing/hosting/stock/tape costs, supplier admission and the complete
+multiplication theorem are unrun or unproved here. No new kappa or
+selected-frontier change. No Lean, Docker, predecessor census or selected
+full cold replay was run.
+
+The `formal-interface-lemma` card is changed to this written real algebraic
+interface theorem. The current selected-baseline metadata orientation
+passes; it is not a mathematical premise. Canonical base is
+`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority revision 7.
+[SOURCES.json](SOURCES.json) pins predecessor and orientation documents as
+historical provenance, with no live scientific input or imported code.
+[TASK.json](TASK.json) records the scope change and structured questions.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145574)
+records the live overlap coverage and its limits. Main-tree README and
+merged-PR searches supplement the sparse local cache; none covers unpublished
+work or every historical diff.
+
+The verifier uses dynamically allocated exact Python integers, fractions and
+bounded lists, with no fixed-allocation claim. It has no recursion, solver,
+subprocess or mutable shared state. Dimensions are at most 12; the principal
+exhaustive sweep stops at eight. Every function is shorter than 60 physical
+lines. Both registered runs treat warnings as errors.
+
+## Open next questions
+
+1. Does one concrete retained caller have this real kernel after positive
+   gauges and satisfy t<=1/3? Pin the literal kernel and derive its parameter
+   and truncation convention. Complex or nonpositive phases and the actual
+   caller binding remain blockers. Do not infer admissibility from this
+   support theorem.
+2. What is the largest bandwidth-uniform t range preserving the strict
+   ordered-minor criterion? Start with the generating polynomial's roots.
+   A uniform proof or precise obstruction is needed; a finite table alone
+   cannot establish it.
+
+## Credit
+
+Credit Ryanson Jonathan/PR4407 for the real-entry question and generic
+carve formula; unpaidmoon/PR4373 for the separated carve theorem;
+James Reed/PR4285/4298/4299 for earlier bandwidth fixtures; and Cinna
+Davis/PR4100 for the Gaussian caller and retained predecessor lineage.
+The new repository result is the restricted real-Gaussian noncancellation
+and sign theorem. New work is Apache-2.0. No literature-priority claim.

research/gaussian-schur-fill-sign/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "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"
+    }
+  ]
+}