Prove the unique optimal Gaussian chirp origin (no new κ)

research/gaussian-origin-optimum/PROOF.md

@@ -0,0 +1,126 @@
+# The unique optimal origin in the quadratic chirp family
+
+This proof and its finite corroboration were produced by Nick Petalas.
+
+## Model and statement
+
+Let n >= 2, 1 <= W <= n-1 be integers, let a, theta > 0 and beta be real,
+and put rho = 1+theta. Vertices are 0,...,n-1. For every real c define
+the matrix N(c) to have diagonal 1, zero outside bandwidth W, and entries
+
+```text
+N(c)[i,j] = exp(-a rho h^2 - 2a beta h
+                  + a theta ((i-c)^2-(j-c)^2)),  h=j-i,
+0 < |h| <= W.
+```
+
+This is exactly the Gaussian chirp formula in Cinna Davis's PR #4100
+gauge-free note, with t_i=i-c. We treat it as a specified mathematical
+family. We do not assert that changing c is a free operation at its caller.
+The individual fixed-origin results of James Reed's #4304/#4305 are
+predecessors, not assumptions needed for the following optimization proof.
+
+Write R_i(c) for the sum of off-diagonal entries in row i and
+R(c)=max_i R_i(c)=||N(c)-I||_infinity. Then its unique minimum over all
+real c occurs at
+
+```text
+c* = (n-1)/2 + beta/theta.                                      (1)
+```
+
+This optimizes only c. It is not a claim about all positive diagonal
+scalings, nor does optimality imply R(c*)<1 in every parameter regime.
+
+## Reflection and strict convexity
+
+Expand the squares and put m=(n-1)/2 and u=c-c*. The exponent becomes
+
+```text
+-a ((1+2theta) h^2 + 2theta(i-m-u)h).                           (2)
+```
+
+Under i -> n-1-i, j -> n-1-j, u -> -u, both h and i-m-u change
+sign. The bandwidth and endpoint truncation are preserved. Thus
+
+```text
+R_i(c*+u) = R_(n-1-i)(c*-u),    R(c*+u)=R(c*-u).                (3)
+```
+
+Each R_i is a finite sum of positive exponentials of affine functions
+of c. Its second derivative is
+
+```text
+R_i''(c) = sum_(0<|j-i|<=W) (2a theta(j-i))^2 N(c)[i,j] > 0.    (4)
+```
+
+Every vertex has at least one neighbor, so the inequality is strict.
+The finite maximum R is also strictly convex. Indeed, at an interior
+convex combination choose a maximizing row. Its strict convexity bounds
+its value strictly below the same convex combination of its endpoint
+values, which are at most the corresponding endpoint maxima.
+
+For u != 0, strict midpoint convexity and (3) give
+R(c*) < (R(c*+u)+R(c*-u))/2 = R(c*+u). This proves existence and
+uniqueness directly, even though R need not be differentiable.
+No bounded numerical search supplies the universal quantifiers.
+
+## A usable sufficient contraction bound
+
+Suppose delta=1-(n-3)theta > 0. At c*, for k=|h| >= 1 the positive
+coefficient q in the exponent -a q obeys
+
+```text
+q = (1+2theta)h^2 + 2theta(i-m)h
+  >= (1+2theta)k^2 - theta(n-1)k
+   = delta k^2 + theta(n-1)k(k-1)
+  >= delta k^2.                                               (5)
+```
+
+The first inequality uses |i-m|<=m, including truncated boundary rows.
+There are at most two entries for each k, hence
+
+```text
+R(c*) <= 2 sum_(k=1)^W exp(-a delta k^2)
+       <= 2W exp(-a delta).                                   (6)
+```
+
+Delta>0 is sufficient for this bound, not necessary for the optimizer
+or for contraction. The checker includes a regime with R(c*)>1.
+
+## The ten-vertex prime-scale section
+
+Use the parameters of James Reed's #4305: n=10, W=2,
+theta=1/1444, beta=-1/2, a=9pi. Formula (1) gives c*=-1435/2,
+and delta=1437/1444. Machin's identity and alternating arctangent
+bounds give
+
+```text
+pi > 16(1/5-1/375)-4/239 > 157/50,
+9pi * 1437/1444 > 28.                                        (7)
+```
+
+All terms of the exponential Taylor series are positive, and the exact
+rational sum sum_(k=0)^12 7^k/k! is greater than 1024. Therefore
+exp(7)>2^10 and exp(28)>2^40. Applying (6) proves
+
+```text
+||N(-1435/2)-I||_infinity < 4 exp(-28) < 2^-38.                (8)
+```
+
+The cited fixed-origin section at c=0 has the predecessor's bound 97/100.
+Equation (8) is a new bound on a changed member of the same family,
+not a re-computation of that predecessor. Uniqueness also proves the
+actual norm strictly decreases when c moves from 0 to c*.
+
+The scaling has a material cost. For D(c)[i,i]=exp(a theta(i-c)^2),
+the ratio of its largest to smallest diagonal at c* is
+
+```text
+D(c*)[9,9]/D(c*)[0,0] = exp(81pi).                            (9)
+```
+
+Indeed, theta((9+1435/2)^2-(1435/2)^2)=9. Changing c is diagonal
+similarity: N(c)=D(c) K D(c)^-1 for the same truncated Toeplitz K.
+Thus the improvement of this infinity norm does not change eigenvalues.
+We make no claim that its conversion, storage or precision costs fit a
+physical supplier. No selected assumption is discharged by (8).

research/gaussian-origin-optimum/README.md

@@ -0,0 +1,127 @@
+# The unique optimal origin for a finite Gaussian chirp
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+
+For every finite banded Gaussian chirp in the family below, the unique
+real origin minimizing the largest off-diagonal row sum is
+`c*=(n-1)/2+beta/theta`. At the ten-vertex, width-2, p=19 section of
+James Reed's [PR #4305](https://github.com/CrocSwap/integer-mult-bounds/pull/4305),
+the changed origin `-1435/2` gives `||N-I||_infinity < 2^-38`.
+The cited origin-zero section has the predecessor's bound `97/100`.
+The actual norm strictly decreases by uniqueness of the minimizer.
+
+Claim type: a scoped written analytic proof with exact finite corroboration.
+No kappa, supplier admission or selected framework assumption changes.
+The favorable norm requires a chirp diagonal range of `exp(81*pi)` in
+the example, which has no paid implementation here.
+
+## Model and new step
+
+For integers `n>=2`, `1<=W<=n-1`, real `a,theta>0`, `beta` and origin `c`,
+use diagonal 1 and, for `h=j-i`,
+
+```text
+N(c)[i,j] = exp(-a(1+theta)h^2 - 2a beta h
+                + a theta((i-c)^2-(j-c)^2)),  0<|h|<=W.
+```
+
+All other entries are zero. This is Cinna Davis's PR #4100 Gaussian
+chirp formula, the same family as James Reed's #4304/#4305 sections.
+Their fixed-origin results are cited, not independently replayed.
+
+[PROOF.md](PROOF.md) expands the exponent, reflects the finite path and
+proves strict convexity of each row sum and their maximum. These facts
+give the unique optimizer over every real origin. If
+`delta=1-(n-3)theta>0`, it also proves
+`||N(c*)-I||_infinity <= 2W exp(-a delta)`.
+At `n=10,W=2,theta=1/1444,beta=-1/2,a=9*pi`, exact elementary
+bounds give `a delta>28` and `exp(28)>2^40`.
+
+Only the origin varies. This is not optimization over all positive
+diagonal scalings. The matrices are diagonally similar and have the same
+eigenvalues. Optimality does not imply contraction in every parameter regime.
+
+## Evidence and reproduction
+
+From the repository root, with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-origin-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/gaussian-origin-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-origin-optimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-origin-optimum --check-source-history
+```
+
+Another installed CPython 3.12 can replace the local interpreter path.
+The direct verifier also runs in a Git-free export and prints
+`PASS_GAUSSIAN_ORIGIN_OPTIMUM`. `--emit` prints only its generated JSON
+receipt, including hashes of all six package files. It writes no files.
+There is no handwritten receipt or expected-output file.
+
+The fixtures take `a=96 log(2)`, so every entry is an exact rational
+power of two. They compare the literal squared-distance formula with
+the expanded formula, check reflected rows and strict row midpoint
+inequalities, and check strict improvement at two offsets from c*.
+There are 216 parameter fixtures, 4,140 exponent fixtures, 2,790
+reflected-row equalities and 3,222 strict inequalities.
+The prime-scale certificate checks all 34 in-band entries using rational
+exponent inequalities, Machin's arctangent bound and a positive Taylor sum.
+Finite fixtures corroborate the written proof's universal quantifiers.
+
+Fifteen controls cover invalid dimensions, bandwidths and theta values,
+nonintegral and oversized fixture exponents, the wrong beta sign,
+the wrong path midpoint, an omitted theta term, a valid noncontracting
+regime and the degenerate theta-zero boundary. Explicit exceptions keep
+checks active in optimized Python.
+
+## Sources and limits
+
+The scientific base is canonical main
+`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8.
+[SOURCES.json](SOURCES.json) pins the original catalogue, selected record,
+James Reed's retained PR #4305 README and Cinna Davis's gauge-free formula
+as bibliographic provenance. No predecessor executable or numerical
+receipt is consumed. The selected metadata baseline passed for orientation;
+it is not a scientific replay.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220028)
+states the changed origin-optimization scope. Entry searches included live
+open PRs, recent account PRs, active Discussions and handoffs, targeted
+merged searches and all-main README terms. They rejected the already-solved
+origin-zero question before this claim. Sparse cached local-note coverage
+is incomplete, and search absence is not proof of novelty.
+
+No physical conversion, precision/tape invoice, source ownership, native
+supplier, recursive Schur schedule, stock, compiler or analytic recovery
+theorem is established. The five selected assumptions remain. Lean,
+Docker, selected cold replay, independent human review and formal
+proof-kernel review are unrun. No construction expansion is proposed.
+
+Build the Lever supplies a standalone exact verifier. Prove It Works
+requires full row sums of its rational fixtures. Power of Ten bounds
+fixtures by ten vertices, bandwidth three, rational exponents of magnitude
+at most 4096, and six files of at most 128 KiB. Functions stay below
+60 physical lines. Warning-strict normal and optimized Python provide
+recurring diagnostics. Managed allocation is a bounded rule-3 deviation
+because Python integers and Fractions allocate dynamically. There is no
+recursion, subprocess, network access or dynamic code generation.
+The rejection helper's ten callbacks are fixed local controls, a bounded
+rule-9 deviation; no external callback is accepted.
+
+## Open next questions
+
+What origin is best under an explicit logarithmic range budget on the
+chirp diagonal? This matters because the unconstrained example needs
+range `exp(81*pi)`. First intersect the origins with a specified range
+allowance and minimize the convex row-norm objective there. A real caller
+must supply the scaling and precision budget. The structured question is
+in [TASK.json](TASK.json) and is not reserved here.
+
+## Credit
+
+The new origin-optimization proof and verifier were produced by Nick Petalas.
+James Reed / jwr404 supplied the origin question and fixed-origin sections
+in #4304/#4305. Cinna Davis supplied the PR #4100 Gaussian and gauge-free
+formulas. Their attribution and frozen files remain intact. Convexity,
+path reflection, Machin's identity and Taylor bounds are classical methods.
+Independent human and formal proof-kernel review are unclaimed.

research/gaussian-origin-optimum/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/gaussian-prime-origin/README.md",
+      "usage": "provenance",
+      "git_blob": "ffd1945a6cd39d7509acfb1c7c543babdbfc29d6",
+      "sha256": "aea95b73b3a4a048549c138ecee0a92fe549c10a568997931658a343522acc5d"
+    },
+    {
+      "path": "research/unconditional-batched-crt/vendor/GAUGEFREE-INTERIORS.md",
+      "usage": "provenance",
+      "git_blob": "20585e44fa4e49b13b5d8495bbf6ed254459a362",
+      "sha256": "d1423ac0ea0003521797209f4396e6981a66994bbee4f8b48026e5b95f8c5116"
+    }
+  ]
+}

research/gaussian-origin-optimum/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the unique real origin minimizing the infinity norm of N(c)-I for every finite banded Gaussian chirp in the specified quadratic family; certify a strict improvement on the ten-vertex p=19 section.",
+  "scope_change_reason": "This is a new conditioning optimization lemma motivated by James Reed PR4305, rather than an audit or discharge of a selected framework assumption.",
+  "bottleneck_link": "The origin controls the row-gap hypothesis of Gaussian Neumann inversion. Optimizing it can improve conditioning, but the diagonal conversion range and full precision/tape invoice remain separate costs.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved strict origin improvement and its bounded exact corroboration. Do not extend to physical admission, other gauges or recursive Schur optimization.",
+  "outcome": "partial",
+  "evidence": "PROOF.md gives the all-parameter unique-minimizer theorem and the analytic norm bound below 2^-38. verify.py corroborates exact exponent identities, rational exponential fixtures and the constant certificate.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the best row-norm bound after imposing an explicit logarithmic range budget on the chirp diagonal?",
+      "why_it_matters": "The unconstrained optimum in the ten-vertex example has diagonal range exp(81*pi); conditioning alone does not pay for conversion or precision.",
+      "first_step": "Intersect the allowed origins with a fixed bound on max_i log D_i(c)-min_i log D_i(c), then minimize the convex row-norm objective on that feasible set.",
+      "blocked_by": "A physical caller must supply its actual scaling and precision allowance."
+    }
+  ]
+}