Prove sharp theta order for broad Gaussian edge inverses (no κ)

research/gaussian-phase-cell-lower/PROOF.md

@@ -0,0 +1,134 @@
+# A matching lower order at a broad Gaussian cell edge
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Theorem and domain
+
+Let alpha > 0, theta > 0, rho = 1+theta, b0 = pi/alpha^2,
+gamma = b0/rho, and c = 1/(2rho). For integers 0 <= k,i < N define
+
+```text
+K[k,i] = alpha^-1 exp(-b0 (i-k/rho-c)^2).
+```
+
+Assume theta(N-1) <= 1, so beta_k = theta k - 1/2 lies in the
+closed phase interval [-1/2,1/2]. For every positive integer m with
+2m <= N,
+
+```text
+||K^-1||_2 >= alpha m exp(-gamma theta (2m-1)^2).             (1)
+```
+
+In particular, if 0 < theta <= 1/16 and
+N >= 2 floor(1/(2 sqrt(theta))), then
+
+```text
+||K^-1||_2 >= (alpha/4) exp(-pi/alpha^2) theta^(-1/2).       (2)
+```
+
+Thus the theta^(-1/2) upper order proved by JoyboyBrian in #5103 is
+sharp for fixed alpha on these boundary sections. This is an order theorem,
+not Ryanson Jonathan's #4435 proposed sharp leading coefficient. It is not
+a lower bound for every section contained anywhere inside a phase cell.
+
+## Cited finite inverse and the new positive rectangle
+
+Put q = exp(-gamma), P_0=1 and
+P_s=product_(r=1)^s(1-q^(2r)). The finite Gaussian Toeplitz matrix
+G[i,j]=q^((i-j)^2) has the q-LDU factorization retained in Jose Manuel's
+#4193 and reproduced in #5103. In the convention
+[k choose i]_(q^2)=P_k/(P_i P_(k-i)), its inverse is
+
+```text
+G^-1[i,j] = (-1)^(i+j) sum_(k=max(i,j))^(N-1)
+    q^(2k-i-j) [k choose i]_(q^2) [k choose j]_(q^2) / P_k.  (3)
+```
+
+Every summand after the checkerboard sign is positive. For i <= j, the
+k=j summand alone is q^(j-i)/(P_i P_(j-i)), which is at least q^(j-i).
+Symmetry gives, for every i,j,
+
+```text
+(-1)^(i+j) G^-1[i,j] >= q^|i-j|.                          (4)
+```
+
+The factorization and inverse sum are cited predecessor mathematics. The
+new step keeps this positive lower term under the broad cell's gauges,
+then tests a whole rectangle rather than a single entry.
+
+The exact diagonal factorization K=Dr G Dc is
+
+```text
+Dc[i] = exp(-b0 (theta/rho i^2 - 2c i)),
+Dr[j] = alpha^-1 exp(b0 (theta/rho^2 j^2 - 2c/rho j - c^2)).
+```
+
+These are positive real diagonals. Hence K is invertible, and
+K^-1=Dc^-1 G^-1 Dr^-1 has the same checkerboard signs. Multiplying (4)
+by the positive inverse gauges gives, when i <= j,
+
+```text
+(-1)^(i+j) K^-1[i,j]
+ >= alpha exp(b0 beta_j^2/rho^2 - gamma theta (j^2-i^2)).   (5)
+```
+
+To verify the exponent, before substituting c it is
+
+```text
+b0 (theta/rho i^2 - 2c i - theta/rho^2 j^2
+    + 2c/rho j + c^2) - gamma(j-i).
+```
+
+Set c=1/(2rho), beta_j=theta j-1/2, and expand. This gives the exponent
+in (5) exactly. On 0 <= i < m and m <= j < 2m, its first term is
+nonnegative and j^2-i^2 <= (2m-1)^2. Every entry of this m by m
+rectangle, after checkerboard signs, is therefore at least
+
+```text
+B = alpha exp(-gamma theta (2m-1)^2).
+```
+
+Choose x_j=(-1)^j/sqrt(m) on m <= j < 2m and zero elsewhere.
+Its Euclidean norm is one. For each of the first m output rows, (5)
+shows |(K^-1 x)_i| >= sqrt(m) B, with no cancellation. Summing their
+squared magnitudes gives ||K^-1 x||_2 >= m B. This proves (1).
+
+## Matching order and scope
+
+For (2), set m=floor(1/(2 sqrt(theta))). Since theta <= 1/16,
+1/(2 sqrt(theta)) >= 2, and floor(x) >= x/2 gives
+m >= 1/(4 sqrt(theta)). Also theta(2m-1)^2 <= 1 and
+gamma <= pi/alpha^2. Substitution into (1) proves (2).
+
+For example, N=floor(1/theta) meets the size and phase assumptions
+for all 0 < theta <= 1/16. This includes N=400 at theta=1/400.
+At alpha=3, m=10, the new bound is
+30 exp(-361 pi/(3600 rho)), rho=401/400, and in particular exceeds
+109/5. A rational certificate uses pi<22/7 and
+exp(-t) >= 1-t+t^2/2-t^3/6 for 0<t<1, with
+t=(22/63)(361/400), which overestimates the positive exponent.
+
+For completeness, #5103 supplies
+
+```text
+||K^-1||_2 <= alpha exp(b0/(4rho^2)) P_(N-1)^(-3)
+             (1+sqrt(pi/(gamma theta))).
+```
+
+Its cited product estimate is P_(N-1)^(-3) <= exp(pi^2/(4gamma)).
+For theta <= 1/16, gamma >= gamma0=16pi/(17alpha^2), giving a
+finite fixed-alpha upper constant times theta^(-1/2). Combining that
+cited upper result with (2) proves Theta_alpha(theta^(-1/2)) on the
+stated family. No upper proof or numerical table of a predecessor is
+claimed as new or replayed as a deliverable.
+
+The lower proof also works with arbitrary b0>0 independent of the positive
+normalization alpha. The exact rational fixtures use this larger algebraic
+family; specializing b0=pi/alpha^2 gives the source kernel. Finite tests
+corroborate the inverse-sum, sign, gauge and rectangle steps. The written
+argument carries the universal real-parameter claims.
+
+The sharp leading constant, a matching growing-alpha law, rounded inverse
+execution, coefficient preparation, circuit prefixes, physical storage/tape,
+native admission, outer transfer and integer recovery remain open. This
+does not change the selected frontier or prove a multiplication theorem.

research/gaussian-phase-cell-lower/README.md

@@ -0,0 +1,121 @@
+# Broad Gaussian edge conditioning has sharp theta order
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped analytic proof with exact finite corroboration. No new kappa.
+
+For the broad Gaussian matrix
+
+```text
+K[k,i] = alpha^-1 exp(-pi/alpha^2 (i-k/rho-c)^2),
+rho=1+theta, c=1/(2rho), 0<=k,i<N, theta(N-1)<=1,
+```
+
+the new result is
+
+```text
+||K^-1||_2 >= alpha m exp(-pi theta (2m-1)^2/(alpha^2 rho))
+for every integer m>=1 with 2m<=N.
+```
+
+Consequently, for 0<theta<=1/16 and
+N>=2 floor(1/(2 sqrt(theta))),
+
+```text
+||K^-1||_2 >= (alpha/4) exp(-pi/alpha^2) theta^(-1/2).
+```
+
+Together with the cited upper theorem of JoyboyBrian's
+[PR5103](https://github.com/CrocSwap/integer-mult-bounds/pull/5103), this proves
+the sharp order Theta_alpha(theta^(-1/2)) for these boundary sections at
+fixed alpha. This answers its open matching-lower-estimate question. The
+sharp leading coefficient in Ryanson Jonathan's
+[PR4435](https://github.com/CrocSwap/integer-mult-bounds/pull/4435) remains open.
+
+[PROOF.md](PROOF.md) gives the universal argument. A checkerboard sign change
+makes every inverse entry positive. One positive term of the cited finite
+q-LDU inverse survives the exact diagonal gauges. An m by m rectangle at
+the cell edge then gives an explicit alternating unit test vector and the
+norm lower bound. No floating inverse, SVD or asymptotic boundary condition
+is used in this proof.
+
+## Evidence and reproduction
+
+The verifier independently eliminates 36 rational Gaussian matrices of sizes
+two through five, checks 416 inverse entries and 50 rectangle/test-vector
+estimates. These fixtures use the larger algebraic family with independent
+positive Gaussian exponent and normalization. They do not purport to sample
+the transcendental source kernel exactly. Another 520 exact rational
+exponent checks include the source fixture theta=1/400. There are 1,009
+floor-inequality checks and nine boundary/sign/overstatement controls.
+
+At the actual alpha=3, theta=1/400, N=400 fixture, m=10 gives a new
+certified lower estimate exceeding 109/5. The rational polynomial
+certificate is 8753084362189/400075200000 > 109/5. This is a lower bound
+on the inverse norm, not its exact value or the sharp asymptotic constant.
+The source fixture is used for this new estimate only; no predecessor
+operator replay or numerical table is repeated as a contribution.
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-phase-cell-lower/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-phase-cell-lower/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-phase-cell-lower
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-phase-cell-lower --check-source-history
+```
+
+Any CPython 3.12 installation can replace the displayed interpreter path.
+The direct checks report PASS_GAUSSIAN_PHASE_CELL_LOWER; the registered
+runner reports PASS_REGISTERED_RESEARCH_PACKAGE. Default execution writes
+nothing. Optional --receipt NEW_EXTERNAL_PATH exclusively creates a generated
+JSON receipt binding all six package files by SHA256. No receipt is handwritten.
+
+## Sources and limits
+
+The scientific base is canonical main
+a5df48c55ea806d7952b65acc9c76d878ff09b13, priority revision 7.
+[SOURCES.json](SOURCES.json) pins predecessor texts as provenance. No
+predecessor code is imported and no external scientific input is read at replay.
+The originating uniform-transfer-audit card is changed to this original
+conditioning side result. The purpose is to settle the necessity of the edge
+conditioning loss before refining its sharp constant or pricing a caller.
+
+Credit JoyboyBrian #5103 for the rigorous upper theorem and the open lower
+question; Ryanson Jonathan #4408/#4435 for the scaling observation and formal
+leading-coefficient prediction; Jose Manuel/jmbarrancoml #4193 for the finite
+Toeplitz inverse estimate; Vlado Vojdanovski and the retained #1673 Gaussian
+and q-LDU lineage; and Cinna Davis's later Gaussian caller. Classical finite
+q-binomial identities retain their earlier mathematical credit. Their results,
+credit lines and frozen evidence are unchanged. The positive lower rectangle
+and the resulting matching-order theorem are the new contribution.
+
+This theorem fixes beta_0=-1/2 and requires a section containing a sufficiently
+long boundary window. It gives no theta-dependent lower bound for arbitrary
+tiny sections or sections separated from both edges. The alpha-dependent
+constant is deliberately coarse. The universal claim rests on the written
+proof, with finite exact checks as corroboration. Independent human and
+formal proof-kernel review are unclaimed.
+
+Coefficient preparation, rounded inverse application, all circuit-prefix
+norms, physical source access, restoration, storage/tape, native implementation,
+compiler and outer integer recovery remain unpriced. No Lean, Docker, selected
+operator replay or complete multiplication theorem is claimed.
+
+Live open PRs, recent account PRs, handoffs, active discussions, distinctive
+main-tree and merged searches were checked before claiming and submission.
+The initial cache covers 305 open PRs and 4,166 Discussion records. Sparse
+local-note coverage is incomplete; no exhaustive novelty claim follows.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144272)
+records the scope.
+
+## Open next questions
+
+- Recover #4435's sharp leading coefficient, with a uniform boundary remainder
+  and a growing-alpha regime. Start by retaining more positive inverse terms
+  and optimizing boundary test vectors; a comparably sharp upper estimate is
+  still needed. The present lower constant does not establish that coefficient.
+- Bind a complete rounded Gaussian caller before changing numerical guards.
+  Start with one pinned caller and retain its coefficient, prefix, restoration,
+  movement and storage costs. Endpoint conditioning alone supplies no physical
+  invoice. Structured questions are in [TASK.json](TASK.json).

research/gaussian-phase-cell-lower/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "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/broad-phase-cell-inverse-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "7f9ff994918c5c75e9006a8ceeed76a9cbbc2df8",
+      "sha256": "9fccbb6d58c5239c5f1072a2793df030657dd743b64ea44f637fba622c2f9a7f"
+    },
+    {
+      "path": "research/broad-phase-cell-inverse-bound/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "efc7842083ea33a69525f2baf17febae17bd8b6d",
+      "sha256": "3107aa37b026fef8b21f8ba859acfc7968eb94fed28a3169f5e559fbbd70e52d"
+    },
+    {
+      "path": "research/forward-turning-point/README.md",
+      "usage": "provenance",
+      "git_blob": "3f487ef4f53021863060ca5b1a7560de22a287b5",
+      "sha256": "cae911dd36e8911333312a7640aa0ea513e76b2f4c4b8ef1eb1524302cd5a2d6"
+    },
+    {
+      "path": "research/forward-fine-theta-conditioning/README.md",
+      "usage": "provenance",
+      "git_blob": "8e2831a88a7edc504daeba91261546437a2a5375",
+      "sha256": "8aafb8704479eefe1772b7f0d68284bac02ac916473f1a72c258be598c18e964"
+    },
+    {
+      "path": "research/forward-fine-theta-conditioning/verify.py",
+      "usage": "provenance",
+      "git_blob": "48fdf11e4bb4da2928c439d03f05574f7b2c88a7",
+      "sha256": "0484ba72b20a805ae2a0e9bde0527f6d048389c6453642d5337064d2da23e547"
+    },
+    {
+      "path": "research/capped-phase-fusion/FORWARD-SMALL-A-AUDIT.md",
+      "usage": "provenance",
+      "git_blob": "0f7f80b3f74d469c2f72f3b9f338d32568b4eae3",
+      "sha256": "e37aaa30b15671a1dff00676b14572213efaaac99df202dbba5e09f57af487c0"
+    }
+  ]
+}

research/gaussian-phase-cell-lower/TASK.json

@@ -0,0 +1,86 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "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_status": "changed",
+  "actual_scope": "Prove a matching theta^(-1/2) lower order for broad Gaussian phase-cell inverses at beta_0=-1/2, using a positive checkerboard rectangle.",
+  "scope_change_reason": "This answers the matching-lower-estimate question in PR5103 as an original precision-interface side result. It proves necessity of the cell-edge loss rather than auditing a predecessor's upper estimate.",
+  "bottleneck_link": "The Gaussian conditioning exponent affects precision budgets. A lower estimate distinguishes an unavoidable edge loss from slack in an upper proof; it does not price physical execution.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved matching-order lower estimate. Leave the sharp constant and complete physical caller open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md supplies the universal argument. verify.py independently eliminates bounded rational Gaussian matrices, checks the new entry/rectangle inequalities and certifies the original alpha=3, theta=1/400 lower estimate.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the sharp leading constant at the broad phase-cell boundary?",
+      "why_it_matters": "The order theorem does not prove the formal coefficient predicted in PR4435, especially as alpha grows.",
+      "first_step": "Retain more positive terms of the finite inverse and optimize boundary test vectors, then prove an equally sharp upper estimate.",
+      "blocked_by": "Uniform boundary remainder and control of the growing-alpha regime."
+    },
+    {
+      "question": "Can a complete rounded Gaussian caller consume the matching-order estimates?",
+      "why_it_matters": "Endpoint conditioning alone gives no coefficient preparation, rounding, storage or tape implementation.",
+      "first_step": "Pin one actual caller and account for its complete prefix and preparation costs.",
+      "blocked_by": "A concrete physical caller and its full invoice."
+    }
+  ],
+  "claim_type": "Scoped analytic proof with exact finite corroboration",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144272",
+  "environment": {
+    "python": "Python 3.12.15",
+    "dependencies": "Python standard library only"
+  }
+}