Sharpen a uniform finite-cap Gaussian inverse bound (no κ)

research/gaussian-finite-cap-frobenius/PROOF.md

@@ -0,0 +1,107 @@
+# A smaller finite-cap inverse bound
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and credited premise
+
+Let N be a positive integer, gamma>0, q=exp(-gamma), and |s|<=1/2.
+Use the normalized real Gaussian section
+
+    T_N(s)[i,j] = q^((j-i)^2-2s(j-i)),  0<=i,j<N,
+    P_(N-1) = product_(r=1)^(N-1) (1-q^(2r)).
+
+The empty product is one. Jose Manuel / PR4193, Section 3a of
+`research/shifted-gaussian-conditioning/PROOF.md`, proves invertibility and
+
+    |T_N(s)^(-1)[i,j]| <= q^(|i-j|+2s(i-j)) / P_(N-1)^3.       (1)
+
+It then bounds the spectral norm by N/P_(N-1)^3. That entry theorem and
+its finite q-LDU derivation are cited premises. This contribution neither
+audits them nor claims their factorization as new. The norm below is the
+Euclidean induced norm. The Frobenius norm is the square root of the sum
+of squared entries.
+
+## The new bound
+
+Put x=q^4 and define
+
+    D_N(x) = N(N+1)/2 + sum_(d=1)^(N-1) (N-d)x^d
+           = N(N+1)/2 + ((N-1)x-Nx^2+x^(N+1))/(1-x)^2.        (2)
+
+For every N>=1, gamma>0 and |s|<=1/2,
+
+    ||T_N(s)^(-1)||_2 <= sqrt(D_N(q^4)) / P_(N-1)^3.           (3)
+
+For every N>=2 this is strictly smaller than N/P_(N-1)^3.
+There is equality between the two displayed bounds at N=1. We do not
+claim equality between the inverse norm and the new bound.
+
+To prove (3), square (1) and sum all N^2 entries. The diagonal contributes
+N. For distance d>=1, each orientation occurs N-d times. Therefore
+
+    P_(N-1)^6 ||T_N(s)^(-1)||_F^2
+      <= N + sum_(d=1)^(N-1) (N-d)
+               [q^(2d+4sd)+q^(2d-4sd)].                    (4)
+
+The function t -> q^(2d+2dt)+q^(2d-2dt) is even and convex on [-1,1].
+Indeed its second derivative is (2d log q)^2 times itself, which is
+positive. Convexity bounds it by its equal endpoint values. Taking t=2s
+thus bounds the bracket in (4) by 1+q^(4d). Summing gives D_N(q^4).
+The elementary inequality ||A||_2<=||A||_F proves (3). This argument also
+covers either half-shift endpoint without a positive infinite-symbol gap.
+For N>=2 the bracket is strictly smaller at every interior shift.
+
+For the closed form in (2), multiplying
+A=sum_(d=1)^(N-1)(N-d)x^d by 1-x gives
+
+    (1-x)A = (N-1)x - sum_(d=2)^N x^d.
+
+Multiplying again by 1-x gives (N-1)x-Nx^2+x^(N+1).
+This identity includes N=1.
+
+Since 0<x<1, for N>=2,
+
+    D_N(x) < N(N+1)/2 + sum_(d=1)^(N-1)(N-d) = N^2.          (5)
+
+At least the distance-one term is strictly smaller, so this proves the
+strict improvement for every nontrivial size, rather than only samples.
+
+## Size dependence and an exact example
+
+For fixed q in (0,1),
+
+    N(N+1)/2 <= D_N(q^4)
+             < N(N+1)/2 + N q^4/(1-q^4).
+
+After division by N^2 both ends tend to 1/2. Consequently the ratio of
+the new upper bound to the credited old upper bound tends to 1/sqrt(2).
+This is a limit of two upper bounds, not an asymptotic formula for the
+actual inverse norm. The statement keeps q fixed. It does not justify a
+uniform growing-gamma or vanishing-gamma caller substitution.
+
+For N=2 and q=1/2, x=1/16, P_1=3/4 and D_2=49/16. Thus the old bound is
+128/27 and the new bound is 112/27, exactly one eighth smaller. These are
+analytic upper bounds, not measured inverse norms or runtime numbers.
+
+## Scope and remaining obligations
+
+The universal quantifiers follow from this written proof and premise (1).
+The finite exact checks corroborate the new norm inequality by independent
+rational inversion. They do not certify a complete multiplication theorem
+or provide independent human or proof-kernel acceptance.
+
+The result sharpens the same finite-cap constant-shift contract. It does
+not establish an optimal constant, a better asymptotic exponent, a physical
+inverse algorithm, intermediate rounding stability, coefficient generation,
+diagonal-gauge bounds, native implementation, restoration, physical stock,
+tape costs or supplier admission. The source caller must keep those costs.
+JoyboyBrian / PR5103 and PR5183 address a different varying-phase full-cell
+kernel and its boundary-layer limit. No claim about that limit is changed.
+
+Frobenius domination, convexity and finite geometric sums are classical.
+Credit Jose Manuel / jmbarrancoml PR4193 for the entry estimate and explicit
+finite-cap sharpness question; Vlado Vojdanovski / PR1673 for the retained
+q-LDU framework; Jeremy Kothe and PR1758 contributors for the shifted-kernel
+lineage; and Cinna Davis for the later broad Gaussian caller. Their frozen
+sources and credit remain unchanged. The new result is the explicit
+all-size improvement (2)-(5), including its exact bound-ratio consequence.

research/gaussian-finite-cap-frobenius/README.md

@@ -0,0 +1,122 @@
+# A smaller finite-cap Gaussian inverse bound
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped written proof with exact finite corroboration. No new kappa.**
+For every N>=2, gamma>0 and |s|<=1/2, the normalized Gaussian section
+
+    T_N(s)[i,j] = q^((j-i)^2-2s(j-i)),  q=exp(-gamma),
+
+has the improved bound
+
+    ||T_N(s)^(-1)||_2 <= sqrt(D_N(q^4)) / P_(N-1)^3 < N/P_(N-1)^3,
+    P_(N-1) = product_(r=1)^(N-1) (1-q^(2r)),
+    D_N(x) = N(N+1)/2 + ((N-1)x-Nx^2+x^(N+1))/(1-x)^2.
+
+The old bound and inverse-entry estimate are credited to Jose Manuel /
+[PR4193](https://github.com/CrocSwap/integer-mult-bounds/pull/4193).
+This answers its first Open next question in part. The new step sums the
+squares of the complete entry-decay estimate before applying the Frobenius
+norm. [PROOF.md](PROOF.md) proves the all-size corollary, endpoint envelope,
+closed form and strictness. There is equality between the two bounds at N=1.
+
+At N=2 and q=1/2 the old bound is 128/27 and the new bound is 112/27,
+exactly one eighth smaller. For fixed q, their ratio tends to 1/sqrt(2) as
+N grows. This is a limit of upper bounds. No asymptotic formula or optimal
+constant for the actual inverse norm is claimed.
+
+## Reproduce
+
+From the worktree root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-finite-cap-frobenius/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-finite-cap-frobenius/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-finite-cap-frobenius
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-finite-cap-frobenius --check-source-history --check-modes
+```
+
+Another CPython 3.12 path may be substituted. The direct verifier prints
+`PASS_GAUSSIAN_FINITE_CAP_FROBENIUS` in a generated JSON receipt bound to all
+six package-file hashes. It writes nothing and runs without Git, network or
+predecessor executables. No handwritten receipt is supplied.
+
+The finite checks compare the closed form to independent weighted and
+entrywise sums, test the closed-half-shift envelope, and construct literal
+rational inverses by Gauss-Jordan elimination. Every inverse is checked on
+both sides before its full squared Frobenius norm is compared with the new
+bound. Invalid parameters, an omitted lower triangle, a wrong inverse sign,
+a singular matrix and the size-one equality are explicit controls. All
+checks remain active under optimization. The written proof supplies the
+universal quantifiers; finite checks are corroboration. The local complete
+replay passes 896 geometric cases, 889 strict improvements, 180 literal
+inverses with 2,376 entries and 180 shift-envelope cases. Fourteen invalid
+inputs reject and nine named semantic control groups pass.
+
+## Scope, sources and credit
+
+This is an analytic side result under the cited PR4193 entry theorem. It is
+not an audit of that result. No predecessor scientific suite is imported or
+replayed. The complete source proof and README are pinned as historical
+provenance in [SOURCES.json](SOURCES.json). Frozen sources are unchanged.
+
+The original `uniform-transfer-audit` card is marked changed in
+[TASK.json](TASK.json). Entry orientation used the current selected-binding
+positive control. No selected framework assumption is discharged. Scientific
+base is canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority
+revision 8, selected PR6030. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362912)
+records this target. Live claims, local reservations, recent account work,
+main formula/object searches and merged/open PR bodies were checked. Sparse
+notes, arbitrary historical diffs and unpublished work remain coverage limits.
+
+Credit Jose Manuel / jmbarrancoml PR4193 for the explicit question, entry
+bound and finite-cap framework; Vlado Vojdanovski / PR1673 for the retained
+q-LDU identities; Jeremy Kothe and the PR1758 contributors for the shifted
+Gaussian lineage; and Cinna Davis for the later broad Gaussian caller.
+Frobenius domination, convexity and finite geometric sums are classical.
+The explicit improved bound and its proof are the additional contribution.
+
+JoyboyBrian / PR5103 and PR5183 prove varying-phase full-cell bounds and a
+boundary-layer operator limit. They do not supply the constant-shift finite
+Frobenius improvement here. Recent Schur-fill results study eliminated
+boundary matrices rather than this input inverse-norm estimate. No common
+numerical norm or contradictory value is inferred.
+
+Optimal inverse constants, a growing-parameter caller substitution,
+coefficient preparation, rounded-prefix errors, diagonal gauges, native
+operators, physical movement/stock, restoration, compiler and complete
+supplier costs remain separate. No selected cold replay, native suite, Lean
+or Docker build is run. Independent human and formal proof-kernel review
+are unclaimed. The selected frontier is unchanged.
+
+## Open next questions
+
+- Find a matching finite-size lower bound or the sharp fixed-q half-shift
+  inverse-norm asymptotic. Start with a trial vector for the positive
+  checkerboard inverse and retain every boundary row. Sharpness remains
+  the missing step.
+- Bind one actual rounded constant-shift caller to the new allowance.
+  Substitute it into that caller's perturbation inequality, retaining its
+  diagonal gauges and complete coefficient, precision and physical costs.
+  Those caller obligations are not supplied here.
+
+Structured first steps and blockers are in TASK.json. The first verified
+improvement is shipped without pursuing these follow-ons.
+
+## Verifier constraints
+
+The executable accepts no command-line workload. Numeric helper sizes are
+capped at 128, rational encodings at 20 bits and literal inverse matrices at
+6 by 6. Loops are bounded by those caps, four kernel roots, five sizes and
+nine shifts. Functions have fewer than 60 physical lines. State is local
+apart from immutable constants; file handles are scoped; errors propagate.
+There is no recursion, indirect dispatch, subprocess or dynamic evaluation.
+
+Power of Ten rule 3 deviation: CPython dynamically allocates managed integers,
+Fractions and containers in this finite command. Matrices are at most 6 by 12
+including augmentation, only one inverse case is live, and file reads are
+capped at 256 KiB per each of six files. Exact arithmetic sizes are bounded
+by the fixed rational grids and loop caps. Revisit fixed storage before
+embedding this in a runtime with allocation constraints. Normal/optimized
+warning-strict runs and source compilation are the available diagnostics;
+no repository-wide analyzer configuration is changed.

research/gaussian-finite-cap-frobenius/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/shifted-gaussian-conditioning/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "b0110758f3c72e1a9eebff3b621476ee776e9ad5",
+      "sha256": "362a71f8eb6e41e6a1551b4e787eee52586ae42232d1a2e55305e89a049cc51b"
+    },
+    {
+      "path": "research/shifted-gaussian-conditioning/README.md",
+      "usage": "provenance",
+      "git_blob": "90beab7d54ff5145653c262824238bcd5e59e871",
+      "sha256": "20a0b0429979eca448898b1789d42b56d36db4a2f9a1394c963619f2690da860"
+    }
+  ]
+}

research/gaussian-finite-cap-frobenius/TASK.json

@@ -0,0 +1,108 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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 a strictly smaller finite-cap spectral-norm upper bound for every nontrivial normalized constant-shift Gaussian section, retaining the full inverse-entry decay in its Frobenius sum.",
+  "scope_change_reason": "This is an original analytic corollary answering PR4193's first open question in part. It is a side result, not an audit or discharge of a selected framework assumption.",
+  "bottleneck_link": "Sharper Gaussian inverse allowances can reduce a caller precision constant, but actual rounded-caller integration and complete costs remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified strict bound improvement; do not extend to optimal constants, growing-parameter asymptotics or physical caller integration.",
+  "outcome": "completed",
+  "evidence": "Written universal proof; exact replay passes 896 geometric cases, 889 strict improvements, 180 literal inverses and 2376 entries, 180 shift envelopes, 14 rejected inputs and nine enumerated semantic control groups. Warning-strict normal/optimized outputs agree. Registered replay passes.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the sharp finite-size norm or its fixed-q half-shift asymptotic constant be identified?",
+      "why_it_matters": "The Frobenius bound improves the predecessor constant but need not be optimal.",
+      "first_step": "Use the positive checkerboard inverse and a size-dependent trial vector, keeping all boundary rows.",
+      "blocked_by": "A matching lower bound; no sharpness claim is supplied here."
+    },
+    {
+      "question": "Can a named rounded caller consume the new bound while preserving its complete error and resource ledger?",
+      "why_it_matters": "A smaller matrix bound alone does not improve a supplier or multiplication exponent.",
+      "first_step": "Pin one constant-shift finite-cap caller and substitute (3) into its exact perturbation inequality.",
+      "blocked_by": "Actual diagonal gauges, coefficient preparation, rounding, tape and full physical costs."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362912",
+    "source": "PR #4193",
+    "source_author": "jmbarrancoml",
+    "base_checked_utc": "2026-11-02T23:56:52Z",
+    "priority_revision": 8,
+    "selected_pr": 6030,
+    "coverage_limits": "Sparse historical notes, arbitrary diffs and unpublished work are not exhaustively covered.",
+    "overlap_coverage": {
+      "open_prs": 406,
+      "open_prs_complete_pagination": true,
+      "open_prs_fetched_at": "2026-11-02T23:59:48.533082+00:00",
+      "discussion_records": 6358,
+      "discussions_complete_pagination": true,
+      "discussions_fetched_at": "2026-11-03T00:01:44.093980+00:00",
+      "working_local_records": 127,
+      "head_inventory_complete": false
+    }
+  }
+}