From 587475d5cbb4b10c564913d06a0fa4858ce3375f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 00:04:48 +0000 Subject: [PATCH] feat(research): sharpen finite-cap Gaussian inverse bounds --- .../gaussian-finite-cap-frobenius/PROOF.md | 107 +++++++++ .../gaussian-finite-cap-frobenius/README.md | 122 ++++++++++ .../SOURCES.json | 30 +++ .../gaussian-finite-cap-frobenius/TASK.json | 108 +++++++++ .../gaussian-finite-cap-frobenius/VERIFY.json | 34 +++ .../gaussian-finite-cap-frobenius/verify.py | 211 ++++++++++++++++++ 6 files changed, 612 insertions(+) create mode 100644 research/gaussian-finite-cap-frobenius/PROOF.md create mode 100644 research/gaussian-finite-cap-frobenius/README.md create mode 100644 research/gaussian-finite-cap-frobenius/SOURCES.json create mode 100644 research/gaussian-finite-cap-frobenius/TASK.json create mode 100644 research/gaussian-finite-cap-frobenius/VERIFY.json create mode 100644 research/gaussian-finite-cap-frobenius/verify.py diff --git a/research/gaussian-finite-cap-frobenius/PROOF.md b/research/gaussian-finite-cap-frobenius/PROOF.md new file mode 100644 index 0000000000..f132c28fdb --- /dev/null +++ b/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=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=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. diff --git a/research/gaussian-finite-cap-frobenius/README.md b/research/gaussian-finite-cap-frobenius/README.md new file mode 100644 index 0000000000..a7940580d6 --- /dev/null +++ b/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. diff --git a/research/gaussian-finite-cap-frobenius/SOURCES.json b/research/gaussian-finite-cap-frobenius/SOURCES.json new file mode 100644 index 0000000000..e267d3d087 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/gaussian-finite-cap-frobenius/TASK.json b/research/gaussian-finite-cap-frobenius/TASK.json new file mode 100644 index 0000000000..2ccb937c38 --- /dev/null +++ b/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 + } + } +} diff --git a/research/gaussian-finite-cap-frobenius/VERIFY.json b/research/gaussian-finite-cap-frobenius/VERIFY.json new file mode 100644 index 0000000000..175e922e29 --- /dev/null +++ b/research/gaussian-finite-cap-frobenius/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact geometric identities, strict improvements, finite rational inverse bounds and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete exact checks with optimization enabled." + } + ] +} diff --git a/research/gaussian-finite-cap-frobenius/verify.py b/research/gaussian-finite-cap-frobenius/verify.py new file mode 100644 index 0000000000..603c7917a7 --- /dev/null +++ b/research/gaussian-finite-cap-frobenius/verify.py @@ -0,0 +1,211 @@ +"""Exact corroboration of the smaller finite-cap Gaussian norm bound. + +This contribution was produced by Nick Petalas. Apache-2.0. +The universal theorem is the written argument in PROOF.md. +""" +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +import sys + + +HERE = Path(__file__).resolve().parent +MAX_SIZE = 128 +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def validate(size, q): + need(type(size) is int and 1 <= size <= MAX_SIZE, "size must be an integer in 1..128") + need(type(q) is Q and 0 < q < 1, "q must be a Fraction strictly between zero and one") + need(max(q.numerator.bit_length(), q.denominator.bit_length()) <= 20, "q encoding exceeds limit") + + +def majorant_squared(size, q): + validate(size, q) + x = q ** 4 + geometric = ((size - 1) * x - size * x * x + x ** (size + 1)) / (1 - x) ** 2 + return Q(size * (size + 1), 2) + geometric + + +def pivot_product(size, q): + validate(size, q) + value = Q(1) + for r in range(1, size): + value *= 1 - q ** (2 * r) + need(value > 0, "positive finite pivot product") + return value + + +def direct_majorant(size, q): + """Sum an entrywise matrix, independently of the closed geometric sum.""" + validate(size, q) + return sum((Q(1) if i <= j else q ** (4 * (i - j)) + for i in range(size) for j in range(size)), Q(0)) + + +def shifted_matrix(root, size, shift_index): + need(type(root) is Q and 0 < root < 1, "rational kernel root") + need(type(size) is int and 1 <= size <= 6, "matrix size in 1..6") + need(type(shift_index) is int and -4 <= shift_index <= 4, "shift index in -4..4") + # q=root^4, s=shift_index/8. Every exponent is an integer. + return [[root ** (4 * (j - i) ** 2 - shift_index * (j - i)) + for j in range(size)] for i in range(size)] + + +def inverse(matrix): + size = len(matrix) + need(1 <= size <= 6 and all(len(row) == size for row in matrix), "bounded square matrix") + rows = [list(row) + [Q(i == j) for j in range(size)] for i, row in enumerate(matrix)] + for column in range(size): + candidates = [i for i in range(column, size) if rows[i][column]] + need(bool(candidates), "singular matrix") + pivot = candidates[0] + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = rows[column][column] + rows[column] = [value / scale for value in rows[column]] + for i in range(size): + if i != column: + scale = rows[i][column] + rows[i] = [a - scale * b for a, b in zip(rows[i], rows[column])] + need(all(rows[i][j] == (i == j) for i in range(size) for j in range(size)), "elimination identity") + return [row[size:] for row in rows] + + +def check_inverse(matrix, candidate): + size = len(matrix) + for left, right in ((matrix, candidate), (candidate, matrix)): + for i in range(size): + for j in range(size): + need(sum((left[i][k] * right[k][j] for k in range(size)), Q(0)) == (i == j), + "literal left/right inverse") + + +def geometric_checks(): + cases = strict = 0 + for q in (Q(1, 16), Q(1, 4), Q(1, 2), Q(3, 4), Q(7, 8), Q(15, 16), Q(31, 32)): + for size in range(1, MAX_SIZE + 1): + value = majorant_squared(size, q) + # A separate one-dimensional weighted sum checks the closed formula. + direct = Q(size * (size + 1), 2) + sum( + ((size - d) * q ** (4 * d) for d in range(1, size)), Q(0)) + need(value == direct, "closed geometric sum") + need(value <= size * size, "old norm ceiling") + if size > 1: + need(value < size * size, "strict improvement at every nontrivial size") + strict += 1 + x = q ** 4 + tail_majorant = Q(size * (size + 1), 2) + size * x / (1 - x) + need(value < tail_majorant, "linear remainder and bound-ratio limit") + cases += 1 + return cases, strict + + +def finite_matrix_checks(): + matrices = entries = shifted_sums = 0 + for root in (Q(1, 2), Q(2, 3), Q(3, 4), Q(7, 8)): + q = root ** 4 + for size in (1, 2, 3, 4, 6): + ceiling = majorant_squared(size, q) + need(ceiling == direct_majorant(size, q), "entrywise majorant reconstruction") + bound = ceiling / pivot_product(size, q) ** 6 + for shift_index in range(-4, 5): + decay = Q(size) + for d in range(1, size): + decay += (size - d) * (root ** ((8 + 2 * shift_index) * d) + + root ** ((8 - 2 * shift_index) * d)) + need(decay <= ceiling, "closed-half-shift envelope") + if size > 1 and abs(shift_index) < 4: + need(decay < ceiling, "interior-shift strict envelope") + shifted_sums += 1 + matrix = shifted_matrix(root, size, shift_index) + candidate = inverse(matrix) + check_inverse(matrix, candidate) + norm_squared = sum((value * value for row in candidate for value in row), Q(0)) + need(norm_squared <= bound, "new norm bound on a literal inverse") + matrices += 1 + entries += size * size + return matrices, entries, shifted_sums + + +def reject_size(size): + try: + majorant_squared(size, Q(1, 2)) + except ValueError: + return + raise ValueError("invalid size accepted") + + +def reject_q(q): + try: + majorant_squared(2, q) + except ValueError: + return + raise ValueError("invalid q accepted") + + +def controls(): + bad_sizes = (0, -1, 129, True, Q(2), 2.0) + bad_qs = (Q(0), Q(1), Q(-1), Q(2), 0.5, 1, True, Q(1, 1 << 21)) + for size in bad_sizes: + reject_size(size) + for q in bad_qs: + reject_q(q) + need(majorant_squared(1, Q(1, 2)) == 1, "size-one equality retained") + need(majorant_squared(2, Q(1, 2)) == Q(49, 16), "lower-triangle term cannot be omitted") + need(majorant_squared(2, Q(1, 2)) != 3, "upper triangle alone is insufficient") + need(majorant_squared(3, Q(1, 2)) != 3, "diagonal alone is insufficient") + matrix = shifted_matrix(Q(1, 2), 2, 4) + wrong = inverse(matrix) + wrong[0][1] = -wrong[0][1] + try: + check_inverse(matrix, wrong) + except ValueError: + pass + else: + raise ValueError("wrong inverse sign accepted") + try: + inverse([[Q(1), Q(1)], [Q(1), Q(1)]]) + except ValueError: + pass + else: + raise ValueError("singular inverse accepted") + need(Q(49, 16) / pivot_product(2, Q(1, 2)) ** 6 == Q(112, 27) ** 2, + "exact improved example") + need(Q(2) / pivot_product(2, Q(1, 2)) ** 3 == Q(128, 27), "credited old example") + need(Q(112, 128) == Q(7, 8), "exact one-eighth reduction") + groups = ("size-one equality", "distance term", "missing lower triangle", "missing off-diagonal", + "wrong inverse sign", "singular inverse", "new example", "old example", "reduction ratio") + return {"rejected_inputs": len(bad_sizes) + len(bad_qs), "semantic_groups": list(groups)} + + +def file_hashes(): + result = {} + for name in FILES: + path = HERE / name + need(path.is_file() and path.stat().st_size <= 262144, "bounded package file") + with path.open("rb") as stream: + raw = stream.read(262145) + need(len(raw) <= 262144, "bounded package read") + result[name] = sha256(raw).hexdigest() + return result + + +def main(): + cases, strict = geometric_checks() + matrices, entries, shifted_sums = finite_matrix_checks() + result = {"status": "PASS_GAUSSIAN_FINITE_CAP_FROBENIUS", "claim_type": "scoped proof with finite corroboration", + "geometric_cases": cases, "strict_improvements": strict, "literal_inverses": matrices, + "inverse_entries": entries, "shift_envelopes": shifted_sums, "controls": controls(), + "example": {"q": "1/2", "size": 2, "old_bound": "128/27", "new_bound": "112/27"}, + "python": sys.version.split()[0], "sha256": file_hashes()} + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()