Prove the sharp half-shift Gaussian inverse lower envelope (no κ)

research/gaussian-half-shift-envelope/PROOF.md

@@ -0,0 +1,149 @@
+# The sharp scale-uniform half-shift lower envelope
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Fix an integer N >= 1. For 0 < q < 1 and epsilon in {-1,1}, define the
+normalized, untruncated Gaussian section on indices 0,...,N-1 by
+
+```text
+T_N^epsilon(q)[i,j] = q^((j-i)^2-epsilon(j-i)).
+c_N = 1 / (2 sin(pi/(4N+2))).
+```
+
+Then
+
+```text
+||T_N^epsilon(q)^(-1)||_2 >= c_N,
+inf_(0<q<1) ||T_N^epsilon(q)^(-1)||_2 = c_N.
+```
+
+For N >= 2 the first inequality is strict at every admissible q. Its
+infimum is approached as q tends to zero. For N = 1 the norm is always 1.
+This is an exact infimum at each finite size, uniform over Gaussian scale.
+It is not the norm at a specified positive q or a fixed-q asymptotic formula.
+
+In particular c_N/N tends to 2/pi. At any fixed q, the cited upper bound
+N/P_(N-1)^3 and P_infinity > 0 show that the half-shift inverse grows in
+Theta(N). The new result is the sharp q-uniform envelope, rather than a
+claim that every linear-growth consequence is new. Nick Petalas's #5150
+already supplies related lower estimates for varying-phase Gaussian cells.
+
+## Cited input and conventions
+
+Jose Manuel / jmbarrancoml's #4193, Section 3a of
+`research/shifted-gaussian-conditioning/PROOF.md`, retains Vlado
+Vojdanovski's finite Gaussian q-LDU factors. We cite those exact identities
+as premises. No predecessor scientific verifier is rerun here.
+
+Put Q=q^2, P_0=1, P_r=product_(h=1)^r(1-Q^h) and
+[k choose i]_Q=P_k/(P_i P_(k-i)). For G[i,j]=q^((i-j)^2), the factors imply
+
+```text
+G^(-1)[i,j] = (-1)^(i+j) sum_(k=max(i,j))^(N-1)
+    q^(2k-i-j) [k choose i]_Q [k choose j]_Q / P_k.
+```
+
+Every unsigned summand is positive. The half-shift convention is
+T_N^+(q)=D G D^(-1), D[i,i]=q^i. Therefore, for the orthogonal sign matrix
+J[i,i]=(-1)^i, B=J T_N^+(q)^(-1) J has entries
+
+```text
+B[i,j] = sum_(k=max(i,j))^(N-1)
+    Q^(k-j) [k choose i]_Q [k choose j]_Q / P_k.          (1)
+```
+
+Equation (1) is only the cited inverse identity under the stated diagonal
+conjugation. The new step below uses its whole positive upper triangle.
+
+## Triangular domination
+
+Let U_N[i,j]=1 when i<=j, and zero otherwise. For i<=j, retain the k=j
+term in (1). It is
+
+```text
+[j choose i]_Q / P_j = 1/(P_i P_(j-i)) >= 1.
+```
+
+For i>j every term is positive. Thus B>=U_N entrywise. If real matrices
+0<=A<=B entrywise, then ||A||_2<=||B||_2. Indeed, for any complex vector x,
+|Ax|<=A|x|<=B|x| coordinatewise. Taking Euclidean norms and a supremum
+proves the assertion. Orthogonality of J gives
+
+```text
+||T_N^+(q)^(-1)||_2 = ||B||_2 >= ||U_N||_2.              (2)
+```
+
+For N>=2, B[N-1,N-1]=1/P_(N-1)>1. A maximizing right singular vector of
+U_N can be chosen strictly positive: U_N^T U_N has strictly positive
+entries, so the elementary Perron theorem applies. Both U_N x and Bx
+are positive and the last coordinate of Bx is strictly larger. Hence (2)
+is strict. The negative endpoint is the transpose and has the same norm.
+
+## The classical triangular singular value
+
+Let S have ones on the first superdiagonal and zeros elsewhere.
+U_N^(-1)=I-S. The symmetric matrix
+
+```text
+(I-S)(I-S)^T
+```
+
+has diagonal (2,...,2,1) and neighboring entries -1. Its interior
+eigenvector recurrence has solution v_i=sin((i+1)theta) and eigenvalue
+lambda=2-2cos(theta). The first boundary is v_(-1)=0. The last boundary
+is v_N=v_(N-1), so
+
+```text
+theta_k = (2k-1)pi/(2N+1),  k=1,...,N.
+```
+
+These give N distinct eigenvalues and hence the complete spectrum. The
+least is 4 sin^2(pi/(4N+2)), proving ||U_N||_2=c_N. The same argument
+includes N=1. An exact corroborating identity for the characteristic
+polynomial p_N is
+
+```text
+p_N(2-z-z^(-1)) = sum_(j=-N)^N (-1)^j z^j.             (3)
+```
+
+Multiplication by z^N(z+1) gives (-1)^N(z^(2N+1)+1). The root z=-1
+is canceled and the remaining paired roots yield the angles above.
+These triangular singular values are classical; no priority is claimed
+for that elementary matrix calculation.
+
+## Sharpness over scales
+
+Keep N fixed and let q decrease to zero. The integer exponent h(h-1)
+is zero exactly at h=0,1 and positive at every other integer. Thus
+
+```text
+T_N^+(q) -> I+S,
+(I+S)^(-1) = J U_N J.
+```
+
+The limiting matrix is invertible. Finite-dimensional inversion and the
+Euclidean operator norm are continuous there. Consequently the norms
+tend to c_N. Combined with the lower bound, this proves the exact infimum.
+Transposition proves the other endpoint. Finally sin(x)/x tends to 1,
+giving c_N/N -> 2/pi. No exchange of a q-limit and an N-limit is used.
+
+## Evidence and limits
+
+The new verifier constructs literal rational endpoint kernels and inverts
+them with Gauss-Jordan elimination, checking both inverse products. It
+checks the new triangular domination directly, positivity, strictness and
+size-one equality. It does not reconstruct or audit the predecessor's
+q-LDU factors. Exact Laurent coefficients check the entire spectral
+identity (3) at every tested size, without floating point trigonometry.
+Separate small-q fixtures measure the full rational Frobenius difference
+from U_N. All finite counts come from the generated receipt.
+
+The universal quantifiers, strictness and limiting statement rely on this
+written proof and its cited q-LDU premise. Finite tests do not establish
+them by extrapolation. Independent human and formal proof-kernel review
+are unclaimed. No actual raw normalization, production diagonal gauge,
+rounding rule, native algorithm, compiler/stock/tape bill or supplier is
+provided. Interior shifts are outside the lower bound. The fixed-q sharp
+coefficient and growing-parameter estimates remain open.

research/gaussian-half-shift-envelope/README.md

@@ -0,0 +1,125 @@
+# Sharp Gaussian half-shift inverse lower envelope
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with exact finite corroboration. No new kappa.
+
+For every integer N>=1, define the normalized Gaussian section
+
+```text
+T_N^epsilon(q)[i,j] = q^((j-i)^2-epsilon(j-i)),
+0<q<1, epsilon in {-1,1}, 0<=i,j<N.
+```
+
+Its exact scale-uniform inverse-norm infimum is
+
+```text
+inf_(0<q<1) ||T_N^epsilon(q)^(-1)||_2
+    = 1/(2 sin(pi/(4N+2))).
+```
+
+For N>=2 every admissible q gives a strictly larger norm, and q tending
+to zero approaches the infimum. At N=1 the norm is exactly one. The
+envelope divided by N tends to 2/pi. This gives a sharp universal lower
+allowance at each size. It does not give the actual norm at a fixed q.
+
+[PROOF.md](PROOF.md) uses the q-LDU identities cited from Jose Manuel /
+jmbarrancoml's [#4193](https://github.com/CrocSwap/integer-mult-bounds/pull/4193).
+The new step compares the entire positive checkerboard inverse with the
+upper triangular all-ones matrix, whose classical singular value is
+explicit. The small-q limit proves sharpness. This takes the finite-cap
+sharpness question of #4193; it does not audit its factors or scientific
+verifier. Earlier related lower estimates in Nick Petalas's #5150 and
+the upper-bound improvement in #6459 retain their credit. No claim that
+all linear-growth consequences are new is made.
+
+## Reproduce
+
+From the repository root with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-half-shift-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-half-shift-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-half-shift-envelope
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-half-shift-envelope --check-source-history
+```
+
+Another CPython 3.12 path may be substituted. The direct checker prints
+`PASS_GAUSSIAN_HALF_SHIFT_ENVELOPE` in a generated JSON receipt bound to
+all six package files by SHA256. It writes nothing. Expected wrapper
+statuses are `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_RESEARCH_COMMIT_BYTES`. No receipt is handwritten or committed.
+
+The exact check enumerates 80 rational endpoint matrices at five scales
+and sizes one through eight. Gauss-Jordan inversion checks both inverse
+products, then all 2,040 entries against the new triangular comparison.
+All 70 nontrivial-size cases have a strict diagonal witness. It also
+checks 32 complete Laurent-polynomial spectral identities, eight pairs
+of triangular inverse identities, 28 small-scale matrices and 21 strict
+decreases in their squared Frobenius errors. Ten invalid inputs reject.
+Five semantic controls distinguish the triangular comparator, checkerboard
+signs, endpoint transpose, inverse corruption and the interior-shift domain.
+Every check remains active with Python optimization enabled.
+
+## Scope and credit
+
+The universal quantifiers and infimum rely on the written proof and its
+cited q-LDU premise. Finite checks are corroboration. No predecessor code
+or external mathematical runtime input is imported. [SOURCES.json](SOURCES.json)
+pins exact predecessor statements as historical provenance at canonical
+main e54523517d0f03e58352e647c403a5af3e525a57. Frozen sources are unchanged.
+
+Credit Jose Manuel / jmbarrancoml #4193 for the explicit question and
+finite-cap framework; Vlado Vojdanovski #1673 for the retained Gaussian
+q-LDU identities; Jeremy Kothe and the #1758 contributors for the shifted
+Gaussian lineage; Cinna Davis for the later broad caller; and Nick
+Petalas #5150/#6459 for related lower and upper results. Triangular
+singular values, positivity, Perron's theorem and continuity of inversion
+are classical. The contribution here is their sharp scale-uniform
+half-shift consequence. No general literature-priority claim is made.
+
+This changes the `uniform-transfer-audit` card to an analytic side result,
+as recorded in [TASK.json](TASK.json). The card's selected-binding first
+control passed. The live selected #7000 result and kappa 0.00363005817
+remain unchanged. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538492)
+records the target and overlap checks. Those checks cannot exclude
+unpublished work or every historical diff.
+
+No interior-shift lower envelope, fixed-q sharp coefficient, production
+normalization/gauges, rounded inverse, physical execution, native/compiler/
+stock/tape invoice, supplier admission or complete multiplication theorem
+is supplied. No selected framework assumption is discharged. Lean, Docker,
+predecessor scientific suites and the selected full cold replay are unrun.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Determine the sharp leading coefficient at a fixed positive q as N
+  grows. First bound the positive inverse's difference from a constant
+  multiple of the triangular matrix. Boundary and near-diagonal terms
+  are the missing estimate.
+- Determine the finite-size crossover for shifts approaching a half.
+  First retain the geometrically decaying triangle under diagonal
+  conjugation. A sharp two-parameter estimate and justified limit regime
+  remain open. Interior shifts can have a bounded inverse norm as N grows.
+
+Structured relevance, first steps and blockers are in TASK.json.
+
+## Verifier constraints
+
+The verifier has no recursion, dynamic code, subprocess, network, solver
+or third-party dependency. Matrices are at most 8 by 16 including
+augmentation; polynomial degrees are at most 32 and Laurent supports
+have at most 65 entries. Input fractions have at most 20 bits per part;
+the fixed fixture list bounds all exact arithmetic. Each function has
+fewer than 60 physical lines. Explicit exceptions preserve invariants
+under optimization. Package hash reads cover six files of at most 256 KiB.
+
+Power of Ten rule 3 deviation: CPython allocates managed integers,
+fractions and containers during these finite checks. Only one matrix
+case is live at a time, with the fixed dimensions and fraction inputs
+above. This is a bounded certificate checker, not a fixed-allocation
+numerical runtime. A runtime integration would require a separate
+storage design. Warning-strict normal/optimized runs and source
+compilation supply the available diagnostics; separate type/lint
+analysis and repository-wide analyzer changes are unrun.

research/gaussian-half-shift-envelope/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/shifted-gaussian-conditioning/README.md",
+      "usage": "provenance",
+      "git_blob": "90beab7d54ff5145653c262824238bcd5e59e871",
+      "sha256": "20a0b0429979eca448898b1789d42b56d36db4a2f9a1394c963619f2690da860"
+    },
+    {
+      "path": "research/shifted-gaussian-conditioning/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "b0110758f3c72e1a9eebff3b621476ee776e9ad5",
+      "sha256": "362a71f8eb6e41e6a1551b4e787eee52586ae42232d1a2e55305e89a049cc51b"
+    },
+    {
+      "path": "research/gaussian-phase-cell-lower/README.md",
+      "usage": "provenance",
+      "git_blob": "53e21a09266219869102226c5dcfa4617945bb39",
+      "sha256": "16e8027f7bdf9f07948f575fefb0f0ea2ca8e52d1946ef17a27ea012a2bc50cf"
+    },
+    {
+      "path": "research/gaussian-finite-cap-frobenius/README.md",
+      "usage": "provenance",
+      "git_blob": "a7940580d62b50a311d7bb4b621d028cdcbbdda0",
+      "sha256": "8897c838ebd9abb8643aa05edc2af39406330cfe20da025ae33d210d27dce819"
+    }
+  ]
+}