Prove production Gaussian inverse bound 2 + 2p/u² (no new κ)

research/production-gaussian-rowgap/PROOF.md

@@ -0,0 +1,124 @@
+# A production Gaussian inverse bound that retains the concentration factor
+
+Produced by Nick Petalas. Apache-2.0.
+
+This is a scoped written mathematical proof. Its universal statements do not
+follow from the finite corroboration and have no independent human or formal
+proof-kernel review claimed here.
+
+## Statement and cited premises
+
+Use the unchanged parameters and original-coordinate rounded matrix H of Jose
+Manuel's [PR #3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851).
+The production guards include positive integers p,u,d with
+
+    p >= 101,  u >= ceil(log2(8p)),  u*d <= p,
+    1/(4d) < theta = t/s - 1 < 1/(2d-1),  1 < t/s < 2,
+    P = 32768p,  2w < s.
+
+Let N_w be the ideal retained-band matrix defined in JoyboyBrian's
+[PR #6099](https://github.com/CrocSwap/integer-mult-bounds/pull/6099),
+PROOF.md at `38ce77a4925c18eb66f94634b1b11a1242af8a87`. Its diagonal is
+one, its retained entry at signed offset h is
+
+    exp(-pi*u*((rho*h+beta_i)^2-beta_j^2)),
+    rho=t/s, q_i=floor(rho*i+1/2), beta_i=rho*i-q_i,
+
+and other off-diagonal entries vanish. The retained signed offsets obey
+|h|<=w and j congruent to i+h modulo s. The beta sequence is periodic,
+including ties where beta=-1/2. The physical cut remains a cell boundary.
+
+We cite two mathematical premises, without re-verifying them:
+
+1. The bilateral row majorant of PR1673,
+   `research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md` section 1,
+   with a=pi*u>=1, bounds the sum of every nonzero-offset coefficient by
+
+       S = exp(-2*pi*u*theta) + 5 exp(-2*pi*u).
+
+   It includes nonzero periodic diagonal aliases. The off-sum of N_w is a
+   subset of that nonnegative bilateral sum. Deleting aliases, discarding
+   tails and restricting to a principal window cannot increase it.
+
+2. PR6099's retained-band theorem, conditional on its cited scalar enclosure
+   theorem in PR6085, gives
+
+       ||H-N_w||_infinity < E = p*2^(16p+4)*2^(-32768p).
+
+   This theorem concerns the actual within-cell rational ratios and across-cell
+   coefficients. We use it as an input, not as an audit target. No Git objects
+   or executable code from either pending PR are imported by our verifier.
+
+Then, for H and every nonempty principal restriction H_J,
+
+    gap(N_w) > u^2/(p+u^2),
+    gap(H_J) > u^2/(2(p+u^2)),
+    ||H_J^-1||_infinity < 2 + 2p/u^2.
+
+Here gap means the minimum diagonal absolute value minus off-diagonal absolute
+row sum. In particular the source's strict row-dominance test succeeds under
+these cited premises. No production page is materialized by this argument.
+
+## The new parameter step
+
+Put v=u^2. Since d>=1 and u*d<=p, we have 1<=u<=p and 1<=v<=p^2.
+Crucially, the guards imply
+
+    u*theta > u/(4d) >= u^2/(4p).
+
+Use pi>3, e>2, and 2^u>=8p. The two terms of the cited majorant satisfy
+
+    exp(-2*pi*u*theta) < exp(-3v/(2p)) <= 2p/(2p+3v),
+    5 exp(-2*pi*u) < 5*2^(-6u) <= 5/(8p)^6 = T.
+
+The first non-strict inequality is exp(x)>=1+x. Therefore
+
+    gap(N_w) >= 1-S > 3v/(2p+3v) - T.
+
+The exact algebraic reserve above our proposed gap is
+
+    3v/(2p+3v) - v/(p+v) = p*v/((2p+3v)(p+v)).
+
+Since v<=p^2 and v>=1, this is at least
+
+    1/[p(3p+2)(p+1)] >= 1/(10p^3).
+
+Meanwhile T<1/(10p^3): clearing positive denominators reduces this to
+50<8^6*p^3, valid for every p>=1. Thus the ideal gap is strictly greater
+than v/(p+v). This retains the squared concentration factor that the
+historical 1/(8p) estimate discards.
+
+## Paying rounding and bounding the inverse
+
+Write E=16p*2^(-32752p). For integers p>=1, induction gives both p<=2^p
+and p+1<=2^p. Consequently
+
+    32p(p+1) <= 2^(2p+5) <= 2^(7p) < 2^(32752p),
+
+so E<1/[2(p+1)]<=v/[2(p+v)]. Subtract this row perturbation from the
+ideal gap. H and every principal restriction have gap strictly greater
+than v/[2(p+v)]. Their diagonals are exactly one, by the unchanged
+Axis.matrix_entry convention. Hence ||I-H_J||_infinity<1-v/[2(p+v)].
+The convergent Neumann series proves the asserted inverse bound.
+
+The published production metadata example has p=16384 and u=32. The new
+inverse bound is exactly 34, versus the old bound 8p=131072. These are
+analytic upper bounds; neither is a measurement of the actual inverse norm.
+
+## Boundaries and necessity of a hypothesis
+
+The result is conditional on the two cited estimates and their retained scalar
+arithmetic contract. It settles the row-gap part of PR6099's open question
+with a stronger bound. Its infinite-periodized comparison and tail estimate
+remain open in that question. Column or spectral norms, LU growth, physical
+setup and tape costs, full production pages, tensor/CRT assembly, the selected
+framework assumptions and a new kappa are not established here.
+
+The similarity guard cannot simply be removed. Set p=16384, u=32,
+s=10^10, t=s+1 and i=s/2. Then beta_i=-1/2 and the +1 coefficient has
+exponent 2*pi*u/s. A retained band containing that coefficient has gap at
+most 1-exp(-2*pi*u/s)<8u/s<1/34. Thus the new row-gap lower bound is false
+in this relaxed parameter family. This does not refute the inverse upper
+bound separately. The family satisfies the concentration inequality but
+cannot satisfy both u*d<=p and theta>1/(4d). This counterexample is local
+to that removed-hypothesis model, not a claim about admitted production plans.

research/production-gaussian-rowgap/README.md

@@ -0,0 +1,78 @@
+# Stronger conditioning for the physical Gaussian production matrix
+
+This scoped mathematical proof gives the unchanged original-coordinate rounded
+Gaussian matrix H, and every nonempty principal restriction, the bounds
+
+    row gap > u^2/(2(p+u^2)),
+    ||H^-1||_infinity < 2 + 2p/u^2.
+
+The production guards imply u*theta>u^2/(4p). Retaining this squared
+concentration factor improves the historical inverse estimate 8p. On the
+source's p=16384, u=32 metadata example, the new upper bound is 34 instead
+of 131072. These are analytic bounds, not measured inverse norms or runtime.
+No new kappa is claimed, and the selected frontier is unchanged.
+
+[PROOF.md](PROOF.md) proves the implication from the existing bilateral
+row majorant of PR1673 and the retained-band perturbation theorem in
+[PR6099](https://github.com/CrocSwap/integer-mult-bounds/pull/6099), at
+38ce77a4925c18eb66f94634b1b11a1242af8a87. The latter is conditional on
+PR6085's scalar enclosure theorem. Those results are cited premises; their
+re-verification is not this contribution. The new theorem answers the
+row-gap part of PR6099's Open next questions with a stronger bound.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/production-gaussian-rowgap
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/production-gaussian-rowgap --check-source-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/production-gaussian-rowgap/verify.py
+```
+
+The registered normal and optimized checks each enumerate 139850 exact rational
+parameter fixtures and 2976 nearest-index geometry pairs, including 12 tie rows
+and 120 wrapped pairs. They also check 1024 rounding-budget induction fixtures,
+five invalid parameter cases and one exact counterexample after removing the
+similarity guard. The parameter fixtures test a relaxation of the production
+domain, not 139850 complete production plans. The counterexample refutes the
+row-gap estimate in that relaxation, not the inverse estimate separately.
+
+The universal claim rests on the written proof, not these finite checks.
+The verifier authenticates five main-branch source files, imports no predecessor
+engine and uses no pending PR Git objects. A Git-free source export containing
+those declared inputs can run the direct command with any Python 3.12 binary.
+[SOURCES.json](SOURCES.json) records exact source identities; [TASK.json](TASK.json)
+records the card, changed scope and mathematical dependencies.
+
+## Limitations
+
+The result is conditional on the cited kernel and coefficient estimates. No
+independent human or formal proof-kernel review is claimed. Full production
+coefficient pages, infinite-periodized ideal comparison, column and spectral
+norms, LU growth, physical setup and tape costs, tensor/CRT composition and
+the complete multiplication theorem remain outside this result. No selected
+cold replay, Lean or Docker run is needed or performed for this scoped theorem.
+
+## Open next questions
+
+Can the retained u^2 factor reduce a complete caller's precision or locality
+budget? Start with one explicit inverse-error term and preserve its separate
+column, Schur and tape obligations. This package does not reprice that caller.
+
+Can the retained-band matrix be compared to the intended infinite-periodized
+ideal with its stated tail bound? Specify that full ideal and its omitted
+offsets across the physical seam. Deletion monotonicity suffices here; that
+identification and the tail estimate remain separate work from PR6099.
+
+## Credit
+
+This contribution was produced by Nick Petalas. New work is Apache-2.0.
+Jose Manuel / jmbarrancoml supplied the physical producer, production guards
+and old-H matrix in PR3851. JoyboyBrian supplied the retained-band theorem and
+open question in PR6099, building on the scalar theorem in PR6085. The
+bilateral row majorant is inherited from the PR1673 capped phase-cell work
+and its RaD/hipotures Gaussian sources. The logarithmic-width and rounding
+lineage, Chafik Boukhalfa's Gaussian caller work and all source-specific
+predecessor credit remain theirs. The new contribution is the stronger
+production-parameter gap and inverse implication.

research/production-gaussian-rowgap/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
+      "usage": "input",
+      "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73",
+      "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272"
+    },
+    {
+      "path": "research/physical-gaussian-core/PROOF.md",
+      "usage": "input",
+      "git_blob": "883c8d4a6f0eead888fb3532b60db41596940889",
+      "sha256": "e909026dd3f455c35ff28210a0c4ffa232ad8d7633174e481094fd09e2469d7a"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_axis.py",
+      "usage": "input",
+      "git_blob": "edc443a7281e83536a00e9f9fa950d7d854705a3",
+      "sha256": "d416918d7442c5033e43fba94ccc5ed33badc3aebe90ddd479b0b6c020de9724"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_prepare.py",
+      "usage": "input",
+      "git_blob": "32e18686b653a09804941f5fd81b715973337aeb",
+      "sha256": "38aa123f80c68f7fcb9e60acae79543cf55f6fd37e12a548cffae11a9b50c1e5"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_check_production.py",
+      "usage": "input",
+      "git_blob": "64c5e9f65c1dd621ee8bbacc9446b9f6dc741680",
+      "sha256": "08a0b2f4c3dc602ff3d8b98a37351a1910610c0bf1ea18fe7ff5378c373d1024"
+    }
+  ]
+}

research/production-gaussian-rowgap/TASK.json

@@ -0,0 +1,112 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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 unchanged physical Gaussian production matrix has row gap > u^2/(2(p+u^2)) and inverse infinity norm < 2+2p/u^2, conditional on cited predecessor estimates.",
+  "scope_change_reason": "The card asks for a source-relative uniform implication. This contribution adds a stronger quantitative Gaussian conditioning theorem to PR6099 rather than auditing its predecessor estimates.",
+  "bottleneck_link": "A scoped analytic-recovery input for the physical Gaussian producer. This improves its inverse bound but does not supply a new paid profile, supplier admission or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved conditioning improvement. Do not extend to a production page, infinite-tail theorem or multiplier.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the universal implication. verify.py checks the new exact rational inequalities, finite nearest-index geometry, parameter controls and a removed-similarity counterexample.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the retained u^2 factor improve the complete Gaussian caller precision and locality budget?",
+      "why_it_matters": "The actual inverse norm bound is smaller than the historical 8p estimate; a caller must account for all other error sources before reducing guards.",
+      "first_step": "Substitute 2+2p/u^2 into one explicit caller error term while retaining its column, Schur and tape obligations.",
+      "blocked_by": "No complete caller error ledger is repriced in this package."
+    },
+    {
+      "question": "Can the retained-band ideal be compared to the intended infinite-periodized ideal with its stated tail bound?",
+      "why_it_matters": "This is the separate remaining part of PR6099's open question.",
+      "first_step": "Specify the full periodized matrix and prove its omitted-offset tail across the physical seam.",
+      "blocked_by": "This result uses deletion monotonicity and does not establish the intended infinite-ideal identification."
+    }
+  ],
+  "question_source": {
+    "pr": 6099,
+    "author": "JoyboyBrian",
+    "head": "38ce77a4925c18eb66f94634b1b11a1242af8a87",
+    "question": "Uniform ideal rowgap and production Axis admission in Open next questions."
+  },
+  "mathematical_dependencies": [
+    {
+      "pr": 1673,
+      "claim": "Bilateral nonzero-offset row majorant exp(-2a*theta)+5exp(-2a), a>=1."
+    },
+    {
+      "pr": 6099,
+      "head": "38ce77a4925c18eb66f94634b1b11a1242af8a87",
+      "claim": "Retained-band perturbation less than p*2^(16p+4)*2^(-32768p), conditional on PR6085."
+    }
+  ],
+  "freshness": {
+    "upstream_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+    "priority_revision": 8,
+    "checked_at": "2026-10-28T12:58:42.084818+00:00"
+  },
+  "claim_type": "scoped written proof with finite corroboration"
+}