diff --git a/research/production-gaussian-rowgap/PROOF.md b/research/production-gaussian-rowgap/PROOF.md new file mode 100644 index 0000000000..507afff930 --- /dev/null +++ b/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. diff --git a/research/production-gaussian-rowgap/README.md b/research/production-gaussian-rowgap/README.md new file mode 100644 index 0000000000..42ee30d964 --- /dev/null +++ b/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. diff --git a/research/production-gaussian-rowgap/SOURCES.json b/research/production-gaussian-rowgap/SOURCES.json new file mode 100644 index 0000000000..e39dd9b95a --- /dev/null +++ b/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" + } + ] +} diff --git a/research/production-gaussian-rowgap/TASK.json b/research/production-gaussian-rowgap/TASK.json new file mode 100644 index 0000000000..60e268cd08 --- /dev/null +++ b/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" +} diff --git a/research/production-gaussian-rowgap/VERIFY.json b/research/production-gaussian-rowgap/VERIFY.json new file mode 100644 index 0000000000..d3663ce03b --- /dev/null +++ b/research/production-gaussian-rowgap/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "research/physical-gaussian-core/PROOF.md", + "research/physical-gaussian-core/gaussian_axis.py", + "research/physical-gaussian-core/gaussian_check_production.py", + "research/physical-gaussian-core/gaussian_prepare.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New exact rational gap inequalities; finite tie/seam geometry; rounding exponent; rejected domains; removed-similarity counterexample." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same complete scoped check with Python assertions disabled." + } + ] +} diff --git a/research/production-gaussian-rowgap/verify.py b/research/production-gaussian-rowgap/verify.py new file mode 100644 index 0000000000..970ed0b569 --- /dev/null +++ b/research/production-gaussian-rowgap/verify.py @@ -0,0 +1,147 @@ +"""Exact corroboration of the new production Gaussian gap inequalities. + +Produced by Nick Petalas. Apache-2.0. +The universal result is the written proof; no predecessor replay is run. + +Rule 3 deviation: Fraction and JSON require managed allocation. The fixed +fixtures stream one row at a time; live source payloads are capped at 200000 +bytes and arithmetic fixture inputs at p=65536. The registered checks exercise +these bounds. Any future configurable fixture inventory must validate its +capacity before iteration. No persistent resource or mutable shared state is used. +""" +from fractions import Fraction +import hashlib +import json +from math import isqrt +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +MAX_SOURCE_BYTES = 200_000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate_sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + inputs = [row for row in manifest["files"] if row["usage"] == "input"] + require(len(inputs) == 5, "five declared live source pins") + for row in inputs: + source = ROOT / row["path"] + require(source.stat().st_size <= MAX_SOURCE_BYTES, "source size bound") + payload = source.read_bytes() + require(hashlib.sha256(payload).hexdigest() == row["sha256"], + "source hash mismatch: " + row["path"]) + return len(inputs) + + +def rational_gap(p, u): + require(type(p) is int and type(u) is int, "integer production parameters") + require(101 <= p <= 65_536 and 1 <= u <= p, "finite fixture domain") + require(u >= (8 * p - 1).bit_length(), "concentration guard") + v = u * u + tail = Fraction(5, (8 * p) ** 6) + lower = Fraction(3 * v, 2 * p + 3 * v) - tail + ideal = Fraction(v, p + v) + difference = Fraction(p * v, (2 * p + 3 * v) * (p + v)) + require(lower - ideal == difference - tail, "new gap identity") + require(difference >= Fraction(1, 10 * p ** 3), "uniform reserve") + require(tail < Fraction(1, 10 * p ** 3), "tail fits reserve") + require(lower > ideal, "new ideal gap") + return ideal / 2 + + +def algebra_cases(): + count = 0 + digest = hashlib.sha256() + for p in range(101, 513): + for u in range((8 * p - 1).bit_length(), p + 1): + value = rational_gap(p, u) + digest.update(f"{p},{u},{value}\n".encode()) + count += 1 + for p in range(513, 4097): + minimum = (8 * p - 1).bit_length() + for u in sorted({minimum, minimum + 1, max(minimum, isqrt(p)), p // 2, p}): + value = rational_gap(p, u) + digest.update(f"{p},{u},{value}\n".encode()) + count += 1 + return {"cases": count, "sha256": digest.hexdigest()} + + +def nearest(s, t, i): + q = (2 * t * i + s) // (2 * s) + return q, Fraction(t * i, s) - q + + +def geometry_cases(): + count = ties = wrapped = 0 + for s in (8, 16, 33, 64, 127): + for t in sorted({s + 1, s + 2, s + 5}): + rho = Fraction(t, s) + for i in range(s): + qi, bi = nearest(s, t, i) + ties += int(bi == Fraction(-1, 2)) + for h in (-3, -1, 1, 3): + j = (i + h) % s + _, bj = nearest(s, t, j) + lifted_q, lifted_beta = nearest(s, t, i + h) + require(lifted_beta == bj, "physical-period beta identity") + exponent = (rho * h + bi) ** 2 - bj ** 2 + d = lifted_q - qi + require(exponent == d * (d + 2 * bj), "original coordinates") + require(exponent > 0, "positive off-diagonal exponent") + wrapped += int(i + h != j) + count += 1 + require(ties > 0 and wrapped > 0, "ties and physical cuts exercised") + return {"pairs": count, "tie_rows": ties, "wrapped_pairs": wrapped} + + +def proof_constants(): + require(32768 - 16 == 32752 > 7, "production rounding exponent") + require(50 < 8 ** 6, "strict uniform tail reserve") + require(7 - 2 >= 5, "linear exponent comparison for p >= 1") + # p <= 2^p and p+1 <= 2^p have base p=1 and inductive ratio <=2. + for p in range(1, 1025): + require(32 * p * (p + 1) <= 2 ** (7 * p), "rounded error budget") + example = rational_gap(16384, 32) + require(1 / example == 34, "published metadata specialization") + return {"induction_fixtures": 1024, "example_inverse_bound": str(1 / example), + "predecessor_inverse_bound": 8 * 16384} + + +def rejection_controls(): + rejected = 0 + for p, u in ((100, 32), (101, 1), (101, 102), (101, 0), (101, 1.5)): + try: + rational_gap(p, u) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid parameter accepted") + # Removing u*d<=p permits theta this small, at a nearest-index tie. + p, u, s, t = 16384, 32, 10 ** 10, 10 ** 10 + 1 + _, beta = nearest(s, t, s // 2) + _, next_beta = nearest(s, t, s // 2 + 1) + exponent = (Fraction(t, s) + beta) ** 2 - next_beta ** 2 + require(beta == Fraction(-1, 2) and exponent == Fraction(2, s), + "small-theta counterexample geometry") + # gap <= 1-exp(-pi*u*exponent) < 4*u*exponent < claimed gap. + require(4 * u * exponent < rational_gap(p, u), "similarity is essential") + return {"rejected_domains": rejected, "removed_similarity_counterexamples": 1} + + +def main(): + result = {"status": "PASS_PRODUCTION_GAUSSIAN_ROWGAP", + "claim_type": "scoped written proof with finite corroboration", + "live_sources": authenticate_sources(), + "algebra": algebra_cases(), "geometry": geometry_cases(), + "constants": proof_constants(), "controls": rejection_controls()} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()