From f1401fd8618394634c4f2a2171a668ba5f6915c2 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 09:07:25 +0000 Subject: [PATCH] feat(research): prove sharp half-shift inverse lower envelope --- .../gaussian-half-shift-envelope/PROOF.md | 149 ++++++++++++ .../gaussian-half-shift-envelope/README.md | 125 ++++++++++ .../gaussian-half-shift-envelope/SOURCES.json | 42 ++++ .../gaussian-half-shift-envelope/TASK.json | 97 ++++++++ .../gaussian-half-shift-envelope/VERIFY.json | 34 +++ .../gaussian-half-shift-envelope/verify.py | 222 ++++++++++++++++++ 6 files changed, 669 insertions(+) create mode 100644 research/gaussian-half-shift-envelope/PROOF.md create mode 100644 research/gaussian-half-shift-envelope/README.md create mode 100644 research/gaussian-half-shift-envelope/SOURCES.json create mode 100644 research/gaussian-half-shift-envelope/TASK.json create mode 100644 research/gaussian-half-shift-envelope/VERIFY.json create mode 100644 research/gaussian-half-shift-envelope/verify.py diff --git a/research/gaussian-half-shift-envelope/PROOF.md b/research/gaussian-half-shift-envelope/PROOF.md new file mode 100644 index 0000000000..91c607502d --- /dev/null +++ b/research/gaussian-half-shift-envelope/PROOF.md @@ -0,0 +1,149 @@ +# The sharp scale-uniform half-shift lower envelope + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Fix an integer N >= 1. For 0 < q < 1 and epsilon in {-1,1}, define the +normalized, untruncated Gaussian section on indices 0,...,N-1 by + +```text +T_N^epsilon(q)[i,j] = q^((j-i)^2-epsilon(j-i)). +c_N = 1 / (2 sin(pi/(4N+2))). +``` + +Then + +```text +||T_N^epsilon(q)^(-1)||_2 >= c_N, +inf_(0= 2 the first inequality is strict at every admissible q. Its +infimum is approached as q tends to zero. For N = 1 the norm is always 1. +This is an exact infimum at each finite size, uniform over Gaussian scale. +It is not the norm at a specified positive q or a fixed-q asymptotic formula. + +In particular c_N/N tends to 2/pi. At any fixed q, the cited upper bound +N/P_(N-1)^3 and P_infinity > 0 show that the half-shift inverse grows in +Theta(N). The new result is the sharp q-uniform envelope, rather than a +claim that every linear-growth consequence is new. Nick Petalas's #5150 +already supplies related lower estimates for varying-phase Gaussian cells. + +## Cited input and conventions + +Jose Manuel / jmbarrancoml's #4193, Section 3a of +`research/shifted-gaussian-conditioning/PROOF.md`, retains Vlado +Vojdanovski's finite Gaussian q-LDU factors. We cite those exact identities +as premises. No predecessor scientific verifier is rerun here. + +Put Q=q^2, P_0=1, P_r=product_(h=1)^r(1-Q^h) and +[k choose i]_Q=P_k/(P_i P_(k-i)). For G[i,j]=q^((i-j)^2), the factors imply + +```text +G^(-1)[i,j] = (-1)^(i+j) sum_(k=max(i,j))^(N-1) + q^(2k-i-j) [k choose i]_Q [k choose j]_Q / P_k. +``` + +Every unsigned summand is positive. The half-shift convention is +T_N^+(q)=D G D^(-1), D[i,i]=q^i. Therefore, for the orthogonal sign matrix +J[i,i]=(-1)^i, B=J T_N^+(q)^(-1) J has entries + +```text +B[i,j] = sum_(k=max(i,j))^(N-1) + Q^(k-j) [k choose i]_Q [k choose j]_Q / P_k. (1) +``` + +Equation (1) is only the cited inverse identity under the stated diagonal +conjugation. The new step below uses its whole positive upper triangle. + +## Triangular domination + +Let U_N[i,j]=1 when i<=j, and zero otherwise. For i<=j, retain the k=j +term in (1). It is + +```text +[j choose i]_Q / P_j = 1/(P_i P_(j-i)) >= 1. +``` + +For i>j every term is positive. Thus B>=U_N entrywise. If real matrices +0<=A<=B entrywise, then ||A||_2<=||B||_2. Indeed, for any complex vector x, +|Ax|<=A|x|<=B|x| coordinatewise. Taking Euclidean norms and a supremum +proves the assertion. Orthogonality of J gives + +```text +||T_N^+(q)^(-1)||_2 = ||B||_2 >= ||U_N||_2. (2) +``` + +For N>=2, B[N-1,N-1]=1/P_(N-1)>1. A maximizing right singular vector of +U_N can be chosen strictly positive: U_N^T U_N has strictly positive +entries, so the elementary Perron theorem applies. Both U_N x and Bx +are positive and the last coordinate of Bx is strictly larger. Hence (2) +is strict. The negative endpoint is the transpose and has the same norm. + +## The classical triangular singular value + +Let S have ones on the first superdiagonal and zeros elsewhere. +U_N^(-1)=I-S. The symmetric matrix + +```text +(I-S)(I-S)^T +``` + +has diagonal (2,...,2,1) and neighboring entries -1. Its interior +eigenvector recurrence has solution v_i=sin((i+1)theta) and eigenvalue +lambda=2-2cos(theta). The first boundary is v_(-1)=0. The last boundary +is v_N=v_(N-1), so + +```text +theta_k = (2k-1)pi/(2N+1), k=1,...,N. +``` + +These give N distinct eigenvalues and hence the complete spectrum. The +least is 4 sin^2(pi/(4N+2)), proving ||U_N||_2=c_N. The same argument +includes N=1. An exact corroborating identity for the characteristic +polynomial p_N is + +```text +p_N(2-z-z^(-1)) = sum_(j=-N)^N (-1)^j z^j. (3) +``` + +Multiplication by z^N(z+1) gives (-1)^N(z^(2N+1)+1). The root z=-1 +is canceled and the remaining paired roots yield the angles above. +These triangular singular values are classical; no priority is claimed +for that elementary matrix calculation. + +## Sharpness over scales + +Keep N fixed and let q decrease to zero. The integer exponent h(h-1) +is zero exactly at h=0,1 and positive at every other integer. Thus + +```text +T_N^+(q) -> I+S, +(I+S)^(-1) = J U_N J. +``` + +The limiting matrix is invertible. Finite-dimensional inversion and the +Euclidean operator norm are continuous there. Consequently the norms +tend to c_N. Combined with the lower bound, this proves the exact infimum. +Transposition proves the other endpoint. Finally sin(x)/x tends to 1, +giving c_N/N -> 2/pi. No exchange of a q-limit and an N-limit is used. + +## Evidence and limits + +The new verifier constructs literal rational endpoint kernels and inverts +them with Gauss-Jordan elimination, checking both inverse products. It +checks the new triangular domination directly, positivity, strictness and +size-one equality. It does not reconstruct or audit the predecessor's +q-LDU factors. Exact Laurent coefficients check the entire spectral +identity (3) at every tested size, without floating point trigonometry. +Separate small-q fixtures measure the full rational Frobenius difference +from U_N. All finite counts come from the generated receipt. + +The universal quantifiers, strictness and limiting statement rely on this +written proof and its cited q-LDU premise. Finite tests do not establish +them by extrapolation. Independent human and formal proof-kernel review +are unclaimed. No actual raw normalization, production diagonal gauge, +rounding rule, native algorithm, compiler/stock/tape bill or supplier is +provided. Interior shifts are outside the lower bound. The fixed-q sharp +coefficient and growing-parameter estimates remain open. diff --git a/research/gaussian-half-shift-envelope/README.md b/research/gaussian-half-shift-envelope/README.md new file mode 100644 index 0000000000..3b78aa37be --- /dev/null +++ b/research/gaussian-half-shift-envelope/README.md @@ -0,0 +1,125 @@ +# Sharp Gaussian half-shift inverse lower envelope + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. No new kappa. + +For every integer N>=1, define the normalized Gaussian section + +```text +T_N^epsilon(q)[i,j] = q^((j-i)^2-epsilon(j-i)), +0=2 every admissible q gives a strictly larger norm, and q tending +to zero approaches the infimum. At N=1 the norm is exactly one. The +envelope divided by N tends to 2/pi. This gives a sharp universal lower +allowance at each size. It does not give the actual norm at a fixed q. + +[PROOF.md](PROOF.md) uses the q-LDU identities cited from Jose Manuel / +jmbarrancoml's [#4193](https://github.com/CrocSwap/integer-mult-bounds/pull/4193). +The new step compares the entire positive checkerboard inverse with the +upper triangular all-ones matrix, whose classical singular value is +explicit. The small-q limit proves sharpness. This takes the finite-cap +sharpness question of #4193; it does not audit its factors or scientific +verifier. Earlier related lower estimates in Nick Petalas's #5150 and +the upper-bound improvement in #6459 retain their credit. No claim that +all linear-growth consequences are new is made. + +## Reproduce + +From the repository root with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-half-shift-envelope/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-half-shift-envelope/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-half-shift-envelope +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-half-shift-envelope --check-source-history +``` + +Another CPython 3.12 path may be substituted. The direct checker prints +`PASS_GAUSSIAN_HALF_SHIFT_ENVELOPE` in a generated JSON receipt bound to +all six package files by SHA256. It writes nothing. Expected wrapper +statuses are `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_RESEARCH_COMMIT_BYTES`. No receipt is handwritten or committed. + +The exact check enumerates 80 rational endpoint matrices at five scales +and sizes one through eight. Gauss-Jordan inversion checks both inverse +products, then all 2,040 entries against the new triangular comparison. +All 70 nontrivial-size cases have a strict diagonal witness. It also +checks 32 complete Laurent-polynomial spectral identities, eight pairs +of triangular inverse identities, 28 small-scale matrices and 21 strict +decreases in their squared Frobenius errors. Ten invalid inputs reject. +Five semantic controls distinguish the triangular comparator, checkerboard +signs, endpoint transpose, inverse corruption and the interior-shift domain. +Every check remains active with Python optimization enabled. + +## Scope and credit + +The universal quantifiers and infimum rely on the written proof and its +cited q-LDU premise. Finite checks are corroboration. No predecessor code +or external mathematical runtime input is imported. [SOURCES.json](SOURCES.json) +pins exact predecessor statements as historical provenance at canonical +main e54523517d0f03e58352e647c403a5af3e525a57. Frozen sources are unchanged. + +Credit Jose Manuel / jmbarrancoml #4193 for the explicit question and +finite-cap framework; Vlado Vojdanovski #1673 for the retained Gaussian +q-LDU identities; Jeremy Kothe and the #1758 contributors for the shifted +Gaussian lineage; Cinna Davis for the later broad caller; and Nick +Petalas #5150/#6459 for related lower and upper results. Triangular +singular values, positivity, Perron's theorem and continuity of inversion +are classical. The contribution here is their sharp scale-uniform +half-shift consequence. No general literature-priority claim is made. + +This changes the `uniform-transfer-audit` card to an analytic side result, +as recorded in [TASK.json](TASK.json). The card's selected-binding first +control passed. The live selected #7000 result and kappa 0.00363005817 +remain unchanged. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538492) +records the target and overlap checks. Those checks cannot exclude +unpublished work or every historical diff. + +No interior-shift lower envelope, fixed-q sharp coefficient, production +normalization/gauges, rounded inverse, physical execution, native/compiler/ +stock/tape invoice, supplier admission or complete multiplication theorem +is supplied. No selected framework assumption is discharged. Lean, Docker, +predecessor scientific suites and the selected full cold replay are unrun. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Determine the sharp leading coefficient at a fixed positive q as N + grows. First bound the positive inverse's difference from a constant + multiple of the triangular matrix. Boundary and near-diagonal terms + are the missing estimate. +- Determine the finite-size crossover for shifts approaching a half. + First retain the geometrically decaying triangle under diagonal + conjugation. A sharp two-parameter estimate and justified limit regime + remain open. Interior shifts can have a bounded inverse norm as N grows. + +Structured relevance, first steps and blockers are in TASK.json. + +## Verifier constraints + +The verifier has no recursion, dynamic code, subprocess, network, solver +or third-party dependency. Matrices are at most 8 by 16 including +augmentation; polynomial degrees are at most 32 and Laurent supports +have at most 65 entries. Input fractions have at most 20 bits per part; +the fixed fixture list bounds all exact arithmetic. Each function has +fewer than 60 physical lines. Explicit exceptions preserve invariants +under optimization. Package hash reads cover six files of at most 256 KiB. + +Power of Ten rule 3 deviation: CPython allocates managed integers, +fractions and containers during these finite checks. Only one matrix +case is live at a time, with the fixed dimensions and fraction inputs +above. This is a bounded certificate checker, not a fixed-allocation +numerical runtime. A runtime integration would require a separate +storage design. Warning-strict normal/optimized runs and source +compilation supply the available diagnostics; separate type/lint +analysis and repository-wide analyzer changes are unrun. diff --git a/research/gaussian-half-shift-envelope/SOURCES.json b/research/gaussian-half-shift-envelope/SOURCES.json new file mode 100644 index 0000000000..0cf28f52b0 --- /dev/null +++ b/research/gaussian-half-shift-envelope/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/shifted-gaussian-conditioning/README.md", + "usage": "provenance", + "git_blob": "90beab7d54ff5145653c262824238bcd5e59e871", + "sha256": "20a0b0429979eca448898b1789d42b56d36db4a2f9a1394c963619f2690da860" + }, + { + "path": "research/shifted-gaussian-conditioning/PROOF.md", + "usage": "provenance", + "git_blob": "b0110758f3c72e1a9eebff3b621476ee776e9ad5", + "sha256": "362a71f8eb6e41e6a1551b4e787eee52586ae42232d1a2e55305e89a049cc51b" + }, + { + "path": "research/gaussian-phase-cell-lower/README.md", + "usage": "provenance", + "git_blob": "53e21a09266219869102226c5dcfa4617945bb39", + "sha256": "16e8027f7bdf9f07948f575fefb0f0ea2ca8e52d1946ef17a27ea012a2bc50cf" + }, + { + "path": "research/gaussian-finite-cap-frobenius/README.md", + "usage": "provenance", + "git_blob": "a7940580d62b50a311d7bb4b621d028cdcbbdda0", + "sha256": "8897c838ebd9abb8643aa05edc2af39406330cfe20da025ae33d210d27dce819" + } + ] +} diff --git a/research/gaussian-half-shift-envelope/TASK.json b/research/gaussian-half-shift-envelope/TASK.json new file mode 100644 index 0000000000..62cf67f996 --- /dev/null +++ b/research/gaussian-half-shift-envelope/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Determine the exact scale-uniform infimum of the inverse Euclidean norm of every finite normalized Gaussian section at either half-shift endpoint.", + "scope_change_reason": "An original analytic side result takes the finite-cap sharpness question of Jose Manuel / PR4193. No selected assumption is audited or discharged.", + "bottleneck_link": "The lower envelope shows that no scale-uniform constant or sublinear size allowance can replace the linear half-shift inverse budget. Production normalization, gauges and complete costs remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved and exactly corroborated envelope; leave fixed-q constants, interior crossover and physical integration open.", + "outcome": "completed", + "evidence": "Written proof and exact finite corroboration: 80 literal endpoint inverses, 2040 entries, 70 strict cases, 32 complete Laurent identities, eight triangular inverse pairs, 28 small-scale matrices, 21 error comparisons, ten rejected inputs and five semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the sharp leading coefficient at a fixed positive q as N grows?", + "why_it_matters": "The exact infimum over q does not determine the norm at a fixed Gaussian scale.", + "first_step": "Study the positive inverse in the bulk upper triangle and bound its difference from a constant multiple of U_N in operator norm.", + "blocked_by": "A uniform bound on boundary and near-diagonal contributions, with q fixed." + }, + { + "question": "What finite-size lower envelope holds for shifts approaching but not equal to one half?", + "why_it_matters": "Interior shifts can have a size-independent inverse allowance, unlike the endpoints.", + "first_step": "Retain the decaying geometric triangle under the exact diagonal conjugation and identify its largest singular value.", + "blocked_by": "A sharp two-parameter bound and a justified limit regime; no interior claim is made here." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538492", + "source": "PR #4193", + "source_author": "jmbarrancoml", + "priority_revision": 8, + "selected_pr": 7000, + "overlap_coverage": "100 current PR metadata records; 200 own PR records; last 30 handoff comments and active Discussions; full cached 477 open PRs and 7125 Discussion records; main README formula/object searches and merged searches. A separate full PR-body source search found zero own PRs created since 2026-11-04 referring to #4193. Sparse notes, arbitrary diffs and unpublished work remain coverage limits." + } +} diff --git a/research/gaussian-half-shift-envelope/VERIFY.json b/research/gaussian-half-shift-envelope/VERIFY.json new file mode 100644 index 0000000000..67d303f73b --- /dev/null +++ b/research/gaussian-half-shift-envelope/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": "Literal endpoint inverses and new triangular domination; complete spectral polynomial identities; sharp-limit fixtures and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete exact checks under optimized Python." + } + ] +} diff --git a/research/gaussian-half-shift-envelope/verify.py b/research/gaussian-half-shift-envelope/verify.py new file mode 100644 index 0000000000..a139406464 --- /dev/null +++ b/research/gaussian-half-shift-envelope/verify.py @@ -0,0 +1,222 @@ +"""Exact finite corroboration for the half-shift lower envelope. + +Produced by Nick Petalas. Apache-2.0. +No predecessor executable is imported. The universal theorem is in PROOF.md. +""" + +from fractions import Fraction as F +from hashlib import sha256 +import json +from pathlib import Path +import platform + + +MAX_N = 8 +MAX_SPECTRAL_N = 32 +PACKAGE_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py" +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def kernel(n, q, endpoint): + require(type(n) is int and 1 <= n <= MAX_N, "finite size domain") + require(type(q) is F and 0 < q < 1, "Gaussian scale domain") + require(q.numerator.bit_length() <= 20, "numerator capacity") + require(q.denominator.bit_length() <= 20, "denominator capacity") + require(type(endpoint) is int and endpoint in (-1, 0, 1), "shift domain") + return [[q ** ((j - i) ** 2 - endpoint * (j - i)) + for j in range(n)] for i in range(n)] + + +def multiply(a, b): + n = len(a) + return [[sum((a[i][k] * b[k][j] for k in range(n)), F(0)) + for j in range(n)] for i in range(n)] + + +def inverse(a): + n = len(a) + aug = [list(row) + unit for row, unit in zip(a, identity(n))] + for j in range(n): + pivot = next((i for i in range(j, n) if aug[i][j]), None) + require(pivot is not None, "singular matrix") + aug[j], aug[pivot] = aug[pivot], aug[j] + scale = aug[j][j] + aug[j] = [x / scale for x in aug[j]] + for i in range(n): + if i != j: + scale = aug[i][j] + aug[i] = [x - scale * y for x, y in zip(aug[i], aug[j])] + result = [row[n:] for row in aug] + require(multiply(a, result) == identity(n), "right inverse") + require(multiply(result, a) == identity(n), "left inverse") + return result + + +def checkerboard(a): + n = len(a) + return [[(-1) ** (i + j) * a[i][j] for j in range(n)] for i in range(n)] + + +def dominates_triangle(b, endpoint): + n = len(b) + for i in range(n): + for j in range(n): + triangle = i <= j if endpoint == 1 else j <= i + require(b[i][j] >= int(triangle), "triangular domination") + + +def check_gaussians(): + cases = entries = strict = 0 + largest_bits = 0 + for q in (F(1, 8), F(1, 3), F(1, 2), F(2, 3), F(7, 8)): + for n in range(1, MAX_N + 1): + for endpoint in (-1, 1): + a = kernel(n, q, endpoint) + inv = inverse(a) + b = checkerboard(inv) + dominates_triangle(b, endpoint) + require(all(x > 0 for row in b for x in row), "positive inverse") + if n > 1: + require(b[-1][-1] > 1, "strict norm comparison witness") + strict += 1 + else: + require(b == [[F(1)]], "size-one equality") + cases += 1 + entries += n * n + for row in inv: + for x in row: + bits = max(abs(x.numerator).bit_length(), x.denominator.bit_length()) + largest_bits = max(largest_bits, bits) + require(bits <= 8192, "arithmetic capacity") + return {"matrices": cases, "entries": entries, "strict_cases": strict, + "largest_inverse_rational_bits": largest_bits} + + +def poly_step(poly, diagonal, previous): + out = [0] * (len(poly) + 1) + for i, value in enumerate(poly): + out[i] -= diagonal * value + out[i + 1] += value + for i, value in enumerate(previous): + out[i] -= value + return out + + +def spectral_polynomial(n): + previous, current = [0], [1] + for size in range(1, n + 1): + diagonal = 1 if size == n else 2 + previous, current = current, poly_step(current, diagonal, previous) + return current + + +def laurent_substitution(coefficients): + out = {} + for coefficient in reversed(coefficients): + following = {} + for exponent, value in out.items(): + for delta, scale in ((-1, -1), (0, 2), (1, -1)): + key = exponent + delta + following[key] = following.get(key, 0) + scale * value + following[0] = following.get(0, 0) + coefficient + out = {key: value for key, value in following.items() if value} + return out + + +def check_spectral_identity(): + for n in range(1, MAX_SPECTRAL_N + 1): + poly = spectral_polynomial(n) + actual = laurent_substitution(poly) + expected = {j: (-1 if j % 2 else 1) for j in range(-n, n + 1)} + require(actual == expected, "complete characteristic identity") + if n <= MAX_N: + u = [[F(i <= j) for j in range(n)] for i in range(n)] + difference = [[F(i == j) - F(j == i + 1) + for j in range(n)] for i in range(n)] + require(multiply(u, difference) == identity(n), "triangular inverse") + require(multiply(difference, u) == identity(n), "reverse triangular inverse") + return {"complete_laurent_identities": MAX_SPECTRAL_N, + "triangular_inverse_pairs": MAX_N} + + +def check_limit(): + cases = 0 + for n in range(2, MAX_N + 1): + previous = None + for bits in (2, 4, 8, 16): + b = checkerboard(inverse(kernel(n, F(1, 2 ** bits), 1))) + error = sum((b[i][j] - int(i <= j)) ** 2 + for i in range(n) for j in range(n)) + require(error > 0, "limit is not finite-scale equality") + if previous is not None: + require(error < previous, "finite approach-to-limit fixture") + previous = error + cases += 1 + require(previous < F(1, 10 ** 12), "small-scale limit fixture") + return {"limit_matrices": cases, "decreasing_error_comparisons": 3 * (MAX_N - 1)} + + +def expect_rejection(n, q, endpoint): + try: + kernel(n, q, endpoint) + except ValueError: + return + raise ValueError("invalid input accepted") + + +def check_controls(): + invalid = ((0, F(1, 2), 1), (9, F(1, 2), 1), (True, F(1, 2), 1), + (2, F(0), 1), (2, F(1), 1), (2, F(-1), 1), + (2, 0.5, 1), (2, F(1, 2), 2), (2, F(1, 2), True), + (2, F(1, 2 ** 21), 1)) + for n, q, endpoint in invalid: + expect_rejection(n, q, endpoint) + a = kernel(3, F(1, 8), 1) + inv = inverse(a) + b = checkerboard(inv) + require(b[1][0] < 1, "all-ones comparator must fail") + require(inv[0][1] < 0, "checkerboard sign is essential") + require(checkerboard(inverse(kernel(3, F(1, 8), -1)))[0][1] < 1, + "transpose changes triangle") + inv[0][0] += 1 + require(multiply(a, inv) != identity(3), "altered inverse control") + interior = inverse(kernel(2, F(1, 4), 0)) + row_bound = max(sum(abs(x) for x in row) for row in interior) + require(row_bound == F(4, 3) < F(3, 2), "interior norm upper bound") + require(F(13, 5) > F(3, 2) ** 2, "triangle trial vector exceeds interior") + return {"invalid_inputs_rejected": len(invalid), "semantic_controls": 5} + + +def package_hashes(): + root = Path(__file__).resolve().parent + result = {} + for name in PACKAGE_FILES: + path = root / name + require(path.stat().st_size <= 262144, "package hash read capacity") + result[name] = sha256(path.read_bytes()).hexdigest() + return result + + +def main(): + receipt = {"status": "PASS_GAUSSIAN_HALF_SHIFT_ENVELOPE", + "claim_type": "scoped written proof with exact finite corroboration", + "python": platform.python_version(), + "gaussians": check_gaussians(), + "spectral_identity": check_spectral_identity(), + "limit": check_limit(), "controls": check_controls(), + "source_sha256": package_hashes()} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()