diff --git a/research/gaussian-chirp-domain-audit/CLAIM.md b/research/gaussian-chirp-domain-audit/CLAIM.md new file mode 100644 index 0000000000..89aa4621e1 --- /dev/null +++ b/research/gaussian-chirp-domain-audit/CLAIM.md @@ -0,0 +1,44 @@ +# Sprint claim: Gaussian chirp domain and block budgets + +- Track: adversarial mathematical audit; OS-random assignment seed **64** + (`secrets.randbelow(100)`, drawn 2026-10-13 03:37 UTC). +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Claimed at: 2026-10-13 03:43 UTC. Expected finish: 04:17 UTC. +- Exact object: the hypotheses, integer windows and precision budgets of + `lem:chirped-gaussian`, as inserted by `scripts/make_fast_gaussian_patch.py`; + compare the domain caveat in PR #371 at + `988ef67986c313445936fc7103908b6163b9d47e`. +- Method: follow generated source rather than the unmodified upstream header; + derive rational uniform bounds and use a separate standard-library checker + for bounded integer cases and deliberately invalid controls. +- Deliverable: one source-pinned audit note, reproducible exact checker and + receipt. No new kappa or full analytic/tape theorem claim. +- Time allocation: 40 minutes from 03:37 UTC; orientation ends before 03:45, + verification and handoff begin no later than 04:07. + +## Selection and overlap + +Three narrow candidates were considered, ordered as follows: + +0. Recheck the missing exact infeasibility evidence behind PR #620's P111 + decoder floor. The review already identifies absent proof logs and + nonportable scripts; a portable solver audit would need more setup. +1. Audit the Gaussian chirp domain and block budgets left conditional in + PR #371. This is an older unreviewed contribution with a small exact seam. +2. Audit the normalized zero/power-of-two boundary in PR #573's eight-tape + handoff. The sources have substantial scoped Lean checks already. + +Seed `64 % 3 = 1` chooses candidate 1. It also determines the finite residue +sampling order; the claim is useful because it checks a different obligation, +not because it uses a different random seed. + +At selection, GitHub returned 491 open PRs. The central ledger marks #371 +unreviewed. Its final-grid counterexample and correction are predecessor work, +not claimed here. PRs #479, #481 and #489 address different Gaussian mechanisms. +The repository had no pinned issues and its sole open issue was #650 +(Discussions), so this claim is recorded locally. Pinned issues and #371's +head/comments were refreshed immediately before recording the claim. + +## Result update + +Pending verification and handoff. diff --git a/research/gaussian-chirp-domain-audit/INDEPENDENT-REVIEW.md b/research/gaussian-chirp-domain-audit/INDEPENDENT-REVIEW.md new file mode 100644 index 0000000000..d4dc9751b8 --- /dev/null +++ b/research/gaussian-chirp-domain-audit/INDEPENDENT-REVIEW.md @@ -0,0 +1,144 @@ +# Independent source and arithmetic review + +Reviewed on base `66849e1475c930fd7732b1a0067ffee7e1e95f60`, assignment +seed 64. This review covers the generated Gaussian chirp domain, integer +window containment and the two displayed working-precision budgets. It does +not certify the analytic or tape-complexity theorem and claims no new kappa. + +## Source composition resolves the apparent domain mismatch + +The unmodified header in +[`upstream/build/sections/07-resampling.tex`, lines 53–59](../../upstream/build/sections/07-resampling.tex#L53-L59) +has the older condition `theta > p/alpha^4`. Reading that header together +with the new chirp note would indeed leave the latter's upper bound on theta +unexplained. They are not the composed manuscript. + +[`scripts/make_fast_gaussian_patch.py`, lines 23–33](../../scripts/make_fast_gaussian_patch.py#L23-L33) +replaces that condition by `alpha^-2 <= theta <= 1/4`, while retaining integer +`p > 100`, integer `2 <= alpha < sqrt(p)`, coprime integer `2 <= s < t < 2^p`, +and `sigma = t/s = 1+theta`. The chirp note is inserted by the same function +at line 160; dispatch occurs at lines 300–312. Calling `patched_files()` on +the exact base produced these conditions at generated +`build/sections/07-resampling.tex:59–65`, and the chirp lemma refers back to +them at generated lines 392–400. Thus `sigma <= 5/4 < 2` is available. + +The generated assembly also supplies this domain: source +[`scripts/make_fast_gaussian_patch.py`, lines 232–263](../../scripts/make_fast_gaussian_patch.py#L232-L263), +generated `build/sections/08-assembly.tex:105–115,160–174`, gives +`alpha=floor(sqrt(b/(8d)))`, `eta=1/(4d)`, +`eta < theta_i < 1/(2d-1) <= 1/4` for `d>=3`, and +`alpha^2 theta_i > b/(64d^2) >= 1` eventually. This verifies the particular +domain transfer; it does not independently prove the prime-existence or +asymptotic setup claims used by that assembly. + +PR [#371](https://github.com/CrocSwap/integer-mult-bounds/pull/371), immutable +head `988ef67986c313445936fc7103908b6163b9d47e`, correctly keeps its rounding +correction conditional on the other proof obligations. The fetched historical +head's generator and upstream section 07 were compared with this audit's +base and match byte for byte; the generator SHA-256 is +`ce2013dc3a674b920ddacf25fd17329b262885af0a19279e084238318dff4760`. +The note differs only by the proposed correction. Therefore the PR body's +additional assertion that the referenced no-sort header is broader does +**not** describe either its own composed construction or the construction at +this audit's base. It reads the unmodified header without its replacement. + +## Universal arithmetic checks + +The following arguments use every integer `p>=101` and every integer +`2<=alpha2*(1/3+1/81)=56/81` imply `pi/ln(2)<891/196`. + Consequently `(891/196)*(121/400)<7/5`, + `(891/196)*(25/4)<29`, and `(891/196)/4<57/50`. + These respectively justify the displayed S' `Gamma=ceil(1.4p)`, + E `Gamma=29p`, and E input scale `B=ceil(1.14 alpha^2)` from the + exponents in the [note, lines 170–205](../../notes/fast-gaussian-resampling.tex#L170-L205). + The S' step uses `sqrt(p)+1 < 1.1 sqrt(p)` for `p>100`; the E step uses + `alpha*(2m+2)<=sqrt(p)+4alpha<5sqrt(p)`. Both Gammas satisfy `Gamma<=2P`. + +- **S' precision.** `L_A=3 alpha ceil(sqrt(p))+3 < 4p` for `p>=101`. + For each `p=101,102,103,104`, `4p<=2^(floor(p/4)-1)`. Increasing p by + four doubles the right side and adds only 16 to the left, proving the + same inequality in all four residue classes. Thus + `ceil(log2 L_A)<=p/4`, and the block requirement is at most + `p+(7p/5+1)+p/4+11=(53/20)p+12<3p`. + +- **E precision.** `m=ceil(sqrt(p)/(2alpha))<=sqrt(p)/4+1` implies + `L_A=3m+1<=3sqrt(p)/4+4<=p`. + Hence `ceil(log2 L_A)<=p-1`. Because B is an integer, + `ceil(log2(F L_A))=B+ceil(log2 L_A)` for `F=2^B`. + Using `B<=1.14p+1` gives the source's bound + `p+29p+(1.14p+1)+(p-1)+11=32.14p+11<34p`. + The weaker printed bound `F<=2^(1.15p)` alone would instead give + `32.15p+10`; that also suffices, but is not the derivation of `32.14p+11`. + See the [note, lines 197–213](../../notes/fast-gaussian-resampling.tex#L197-L213). + +- **PR #371's corrected final extraction.** Conditional on its internal + enclosure `h/4`, the exact normalization by `2alpha>=4` leaves at most + `h/16`, and precision-`3p` rational division adds less than + `sqrt(2)*2^(-3p)`. Their sum is below `h/4` for `p>=101`. + Since `sqrt(2)<3/2`, the complete displayed budgets are strictly below + `(1+1/4+3/2)h<3h` for S' and `(3+1/4+3/2)h<5h<(p/3)h` for E. + This corroborates the propagation of the predecessor correction; its + original final-grid counterexample is not a new finding of this audit. + +## Independent calculation and limits + +A separate Python standard-library calculation, without importing the +production numerical verifier, checked all 168,093 pairs +`101<=p<=4096`, `2<=alpha<=floor(sqrt(p-1))`. Integer square roots located +both windows; integer `bit_length` computed ceiling logarithms; rational +arithmetic checked the three exponential-growth bounds above. It checked +`L_A<4p` or `L_A<=p`, both precision requirements, `B<=1.15p`, and `m<2p`. +All passed. Minimum integer precision slack was 40 bits for S' at +`(p,alpha)=(101,8)`, and 277 bits for E at `(101,10)`. This finite replay is +supporting evidence only; the preceding arguments establish the stated +uniform arithmetic claims. + +The calculation is retained in +[`independent_budget_check.py`](independent_budget_check.py), independently +implemented from the main checker. From the repository root run: + +```sh +python3 -B research/gaussian-chirp-domain-audit/independent_budget_check.py +``` + +Expected first line: + +```text +PASS_INDEPENDENT_GAUSSIAN_BUDGETS pairs=168093 controls=5 +``` + +The following JSON line records the fixed domain, stopping rule and minimum +slacks above. Five negative controls reject `p=100`, `alpha^2=p`, the two +insufficient sufficient-precision choices `P=2p` and `P=31p`, and an E window +one integer too short at `(p,alpha)=(101,2)`. Runtime checks remain active +under `python3 -O`; the independent script imports no repository verifier. + +This review has not independently re-established Gaussian tail estimates, +transcendental approximation algorithms, exact packed multiplication, +multitape movement, the full Neumann theorem, or the selected multiplication +frontier. In particular, absence of a domain mismatch does not remove the +genuine final-grid defect that PR #371 addresses. + +Credit: eumemic's fast-Gaussian construction; icekylinx's shifted-input error +enclosure; Harvey and van der Hoeven's analytic interfaces; and Artus +Krohn-Grimberghe / PR #371's disclosed GPT-6 Pro and Codex rounding work. +Prepared with substantial OpenAI Codex assistance as a separate source and +arithmetic review in Effy's research sprint. No independent human peer review +or formal proof is claimed. diff --git a/research/gaussian-chirp-domain-audit/README.md b/research/gaussian-chirp-domain-audit/README.md new file mode 100644 index 0000000000..ade989c9c9 --- /dev/null +++ b/research/gaussian-chirp-domain-audit/README.md @@ -0,0 +1,182 @@ +# Audit: the generated Gaussian chirp domain closes PR #371's caveat + +**Research note and independent mathematical audit; no new kappa.** The +generated Gaussian construction supplies `alpha^-2 <= theta <= 1/4` to +`lem:chirped-gaussian`. Its integer windows and stated working precisions +`P=3p` and `P=34p` satisfy the audited arithmetic obligations throughout +that domain. The broader header left in `upstream/` is not the header used +by this construction. + +This resolves the specific domain caveat in the body of +[PR #371](https://github.com/CrocSwap/integer-mult-bounds/pull/371) at +`988ef67986c313445936fc7103908b6163b9d47e`. That PR's separate final-grid +rounding defect remains genuine and its correction is **not** incorporated +by this audit. Passing this package does not certify the containing lemma, +the selected construction or the full multiplication theorem. + +## Exact source and statement + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Assignment seed: **64**, adversarial mathematical audit. +The accepted certificate at this base is #626 with #543, +`kappa=51110230636731/31250000000000000`; it is unchanged. + +The audited statement is the use of the no-sort domain by +`lem:chirped-gaussian`, specifically its block windows, amplification +ceilings and sufficient precision inequality + +```text +P >= p + Gamma + ceil(log2(F L_A)) + 11. +``` + +The [source pins](SOURCES.json) identify the exact direct inputs, generated +manuscript digests and PR #371's source hashes. The base commit pins the +transitive generator dependencies. The source check executes the actual +`patched_files()` composition in memory; it writes nothing to `upstream/` +or existing certificates. It checks these links: + +1. [`make_fast_gaussian_patch.resampling`](../../scripts/make_fast_gaussian_patch.py#L23-L33) + replaces the original hypothesis `theta > p/alpha^4` by + `alpha^-2 <= theta <= 1/4`. +2. The same function [inserts the note](../../scripts/make_fast_gaussian_patch.py#L157-L161) + verbatim. The chirp lemma inherits that new header, including integer + `p>=101`, integer `2<=alpha p/alpha^4=101/16`. +For the **new chirp E algorithm**, however, + +```text +m = ceil(sqrt(101)/(2*2)) = 3, +L_B = 2m+2 = 8, +q_0 = 0, +q_1 = floor(19/2 + 1/2) = 10. +``` + +The first block contains outputs `ell=0,1`, but evaluates only local +correlation coordinates `0,...,7`. It misses `q_1=10`. The actual generated +header rejects this tuple because `theta>1/4`. + +This is a counterexample to applying the *new window recipe under only the +old hypotheses*. It is not a counterexample to the original slower +no-sort theorem, nor to the generated construction's restricted claim. +It shows why source composition is mathematically significant. + +## Uniform arithmetic argument + +The [separate review](INDEPENDENT-REVIEW.md) gives the window-containment +proofs and the uniform precision argument. A rational common enclosure is + +```text +pi/ln(2) < (22/7)/(56/81) = 891/196. +``` + +For completeness, `ln(2)>56/81` follows from the first two positive terms +of `ln(2)=2*sum_(k>=0) (1/3)^(2k+1)/(2k+1)`. +Also `22/7-pi = integral_0^1 x^4(1-x)^4/(1+x^2) dx > 0`: polynomial +division gives the integrand +`x^6-4x^5+5x^4-4x^2+4-4/(1+x^2)`. +These elementary analytic identities explain the enclosure; the finite +checker evaluates only its exact rational consequences. + +With `theta<=1/4`, `alpha^2100`, those consequences are + +| Obligation | Exact sufficient bound | +|---|---| +| Forward amplification | `(891/196)*(121/400) < 7/5`, so `Gamma=ceil(7p/5)` suffices | +| Correction amplification | `(891/196)*(25/4) < 29`, so `Gamma=29p` suffices | +| Correction input scale | `(891/196)/4 < 57/50`, so `B=ceil(57 alpha^2/50)` suffices | +| Forward precision | `(53/20)p+12 < 3p` for every `p>=101` | +| Correction precision | `(1607/50)p+11 < 34p` for every `p>=101` | + +The precision rows use `L_A<4p` for S', `L_A<=p` for E, and exact integer +ceiling-log bounds. For E, use the sharper `B<=1.14p+1` when deriving the +printed `32.14p+11` bound, rather than only `F<=2^(1.15p)`. + +## Reproduce + +From the repository root, using Python and its standard library (tested +with Python 3.14.7): + +```sh +python3 -B research/gaussian-chirp-domain-audit/verify.py +``` + +Expected output: + +```text +PASS_SCOPED_GAUSSIAN_CHIRP_DOMAIN_AUDIT +Exact parameter pairs: 21773 +Exact correction windows: 968049 +All 7 negative controls rejected; receipt matches +``` + +The deterministic [receipt](RECEIPT.json) records exact coverage, generated +source digests, minimum precision slacks and control outcomes. The command +recomputes its contents and rejects any mismatch. `--write` is available +only for deliberate regeneration after reviewing a change. + +This is exhaustive finite validation within the following domains, not a +search for a stronger construction: + +- Every `101<=p<=1088` and integer `2<=alpha= 101 and alpha >= 2 and alpha * alpha < p, "outside source domain") + root = isqrt(p) + m_s = (root + (root * root < p)) * alpha + # Independent of the main checker's nested ceiling formula: first m + # whose squared endpoint reaches p is one beyond floor(sqrt(p-1)/(2a)). + m_e = isqrt(p - 1) // (2 * alpha) + 1 + if correction_window is not None: + m_e = correction_window + require((2 * alpha * m_e) ** 2 >= p and + (2 * alpha * (m_e - 1)) ** 2 < p, "incorrect correction window") + l_s, l_e = 3 * m_s + 3, 3 * m_e + 1 + gamma_s = (7 * p + 4) // 5 + b = (57 * alpha * alpha + 49) // 50 + log_s, log_e = (l_s - 1).bit_length(), (l_e - 1).bit_length() + require(l_s < 4 * p and l_e <= p, "input length envelope") + require(4 * log_s <= p and log_e <= p - 1, "logarithm envelope") + require(100 * b <= 115 * p, "shifted input magnitude envelope") + require(m_s < 2 * p and m_e < 2 * p, "window size envelope") + p_s = 3 * p if forward_precision is None else forward_precision + p_e = 34 * p if correction_precision is None else correction_precision + require(gamma_s <= 2 * p_s and 29 * p <= 2 * p_e, "Gamma precondition") + slack_s = p_s - (p + gamma_s + log_s + 11) + slack_e = p_e - (p + 29 * p + b + log_e + 11) + require(slack_s >= 0 and slack_e >= 0, "insufficient sufficient precision") + return slack_s, slack_e + + +def must_reject(*args, **kwargs): + try: + check_pair(*args, **kwargs) + except ValueError: + return + raise ValueError("negative control was accepted") + + +def main(): + c = Q(891, 196) + require(2 * (Q(1, 3) + Q(1, 81)) == Q(56, 81), "log series arithmetic") + require(c * Q(121, 400) < Q(7, 5), "forward Gamma enclosure") + require(c * Q(25, 4) < 29, "correction Gamma enclosure") + require(c / 4 < Q(57, 50), "input scale enclosure") + for p in range(101, 105): + require(4 * p <= 2 ** (p // 4 - 1), "four-residue induction endpoint") + require(Q(53, 20) * 101 + 12 < 3 * 101, "forward uniform endpoint") + require(Q(1607, 50) * 101 + 11 < 34 * 101, "correction uniform endpoint") + + count = 0 + minimum_s = minimum_e = None + for p in range(101, 4097): + for alpha in range(2, isqrt(p - 1) + 1): + slack_s, slack_e = check_pair(p, alpha) + candidate_s, candidate_e = (slack_s, p, alpha), (slack_e, p, alpha) + minimum_s = candidate_s if minimum_s is None else min(minimum_s, candidate_s) + minimum_e = candidate_e if minimum_e is None else min(minimum_e, candidate_e) + count += 1 + require(count == 168093, "coverage changed") + require(minimum_s == (40, 101, 8) and minimum_e == (277, 101, 10), + "minimum precision slacks changed") + + # Insufficient-P controls reject a sufficient enclosure, not the actual + # numerical algorithm. The window control must fail its squared endpoint. + must_reject(100, 2) + must_reject(121, 11) + must_reject(101, 8, forward_precision=202) + must_reject(101, 10, correction_precision=3131) + must_reject(101, 2, correction_window=2) + result = { + "finite_only": True, + "p_inclusive": [101, 4096], + "alpha_domain": "2 <= alpha <= floor(sqrt(p-1)); integer", + "pairs_checked": count, + "minimum_forward_slack_bits_p_alpha": minimum_s, + "minimum_correction_slack_bits_p_alpha": minimum_e, + "negative_controls_rejected": 5, + "stopping_rule": "complete the fixed integer domain", + } + print("PASS_INDEPENDENT_GAUSSIAN_BUDGETS pairs=168093 controls=5") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/gaussian-chirp-domain-audit/verify.py b/research/gaussian-chirp-domain-audit/verify.py new file mode 100644 index 0000000000..c7fe9ae870 --- /dev/null +++ b/research/gaussian-chirp-domain-audit/verify.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +"""Source-bound, exact audit of the Gaussian chirp domain and block budgets. + +Only source composition uses the repository generator. All arithmetic and +window checks below are independent, standard-library implementations. +This is not a formal proof of the analytic or multitape theorems. +""" + +import argparse +from fractions import Fraction as Q +import hashlib +import json +from math import gcd, isqrt +from pathlib import Path +import re +import sys + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SEED = 64 +K_UPPER = Q(891, 196) # pi / ln(2) < (22/7) / (56/81); see README. + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def ceil_div(a, b): + return -(-a // b) + + +def ceil_sqrt(n): + r = isqrt(n) + return r + (r * r != n) + + +def ceil_log2(n): + require(n > 0, "logarithm requires a positive integer") + return (n - 1).bit_length() + + +def nearest(j, s, t): + # floor(t*j/s + 1/2), including negative j and ties rounded upward. + return (2 * t * j + s) // (2 * s) + + +def rejected(check, *args): + try: + check(*args) + except ValueError: + return True + raise ValueError("negative control was accepted") + + +def compact(text): + return re.sub(r"\s+", "", text) + + +def check_domain(text): + label = r"\label{lem:no-sort-resampling}" + require(text.count(label) == 1, "need one no-sort lemma") + statement = compact(text.split(label)[1].split(r"\end{lemma}")[0]) + for token in ( + r"p>100", r"2\leq\alpha<\sqrtp", "beintegers", + r"\gcd(s,t)=1", r"\alpha^{-2}\le\theta\le\tfrac14", + ): + require(token in statement, "missing domain token: " + token) + require(text.count(r"\label{lem:chirped-gaussian}") == 1, + "need one chirped Gaussian lemma") + require("AssumethehypothesesofLemma~\\ref{lem:no-sort-resampling}" in compact(text), + "chirp lemma no longer inherits no-sort domain") + + +def check_assembly(text): + text = compact(text) + for token in ( + r"\eta<\theta_i<2\eta/(1-2\eta)=1/(2d-1)\le1/4", + r"\alpha^2\theta_i>\fracb{16d}\cdot\frac1{4d}=\fracb{64d^2}\geq1", + r"b\geq64d^2", + ): + require(token in text, "missing assembly domain argument: " + token) + + +def check_sources(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for path, expected in pins["files_sha256"].items(): + actual = hashlib.sha256((ROOT / path).read_bytes()).hexdigest() + require(actual == expected, "source pin changed: " + path) + sys.path.insert(0, str(ROOT / "scripts")) + from make_fast_gaussian_patch import patched_files + + rendered = {} + for name, old, new in patched_files(): + if name.endswith(("07-resampling.tex", "08-assembly.tex")): + require(old == (ROOT / "upstream" / name).read_text(), + "generator did not start from pinned upstream: " + name) + rendered[name] = new + resampling = rendered["build/sections/07-resampling.tex"] + assembly = rendered["build/sections/08-assembly.tex"] + check_domain(resampling) + check_assembly(assembly) + require((ROOT / "notes/fast-gaussian-resampling.tex").read_text() in resampling, + "the audited note is not inserted verbatim") + hashes = {name: hashlib.sha256(text.encode()).hexdigest() + for name, text in rendered.items()} + require(hashes == pins["generated_sha256"], "generated source changed") + upper = r"\alpha^{-2}\le\theta\le\tfrac14" + controls = { + "removed_upper_domain_bound": rejected( + check_domain, resampling.replace(upper, r"\alpha^{-2}\le\theta")), + "removed_lower_domain_bound": rejected( + check_domain, resampling.replace(upper, r"0<\theta\le\tfrac14")), + "removed_assembly_upper_bound": rejected( + check_assembly, assembly.replace(r"1/(2d-1)\le1/4", r"1/(2d-1)")), + } + return {"generated_sha256": hashes, "negative_controls": controls} + + +def budget(p, alpha, forward_precision=None, correction_precision=None): + require(p >= 101 and 2 <= alpha and alpha * alpha < p, "invalid p, alpha") + m_s = ceil_sqrt(p) * alpha + # Smallest integer m with (2*alpha*m)^2 >= p: exact ceil(sqrt(p)/(2*alpha)). + m_e = ceil_div(ceil_sqrt(p), 2 * alpha) + l_s, l_e = 3 * m_s + 3, 3 * m_e + 1 + gamma_s, gamma_e = ceil_div(7 * p, 5), 29 * p + exponent_b = ceil_div(57 * alpha * alpha, 50) + require(gamma_s <= 2 * 3 * p and gamma_e <= 2 * 34 * p, "Gamma exceeds 2P") + require(m_s < 2 * p and m_e < 2 * p, "window exceeds cost envelope") + require(100 * exponent_b <= 115 * p, "input scale exceeds 1.15p bits") + require(l_s < 4 * p and l_e <= p, "length envelope failed") + require(4 * ceil_log2(l_s) <= p, "forward logarithm envelope failed") + require(ceil_log2(l_e) <= p - 1, "correction logarithm envelope failed") + require(K_UPPER * Q((m_s - 1) ** 2, 4 * alpha * alpha) < gamma_s, + "forward chirp amplification exceeds Gamma") + require(K_UPPER * Q(alpha * alpha * (2 * m_e + 1) ** 2, 4) < gamma_e, + "correction chirp amplification exceeds Gamma") + require(K_UPPER * Q(alpha * alpha, 4) < exponent_b, + "input amplification exceeds B") + need_s = p + gamma_s + ceil_log2(l_s) + 11 + need_e = p + gamma_e + exponent_b + ceil_log2(l_e) + 11 + slack_s = (3 * p if forward_precision is None else forward_precision) - need_s + slack_e = (34 * p if correction_precision is None else correction_precision) - need_e + require(slack_s >= 0 and slack_e >= 0, "insufficient certified precision") + return slack_s, slack_e + + +def check_arithmetic(): + # Exact endpoints used in the written uniform proof, not a finite theorem claim. + require(2 * (Q(1, 3) + Q(1, 81)) == Q(56, 81), "log lower bound") + require(K_UPPER * Q(121, 400) < Q(7, 5), "forward uniform amplification") + require(K_UPPER * Q(25, 4) < 29, "correction uniform amplification") + require(K_UPPER / 4 < Q(57, 50), "uniform input amplification") + for p in range(101, 105): + require(4 * p <= 2 ** (p // 4), "log-envelope induction base") + require(Q(53, 20) * 101 + 12 < 3 * 101, "forward uniform precision") + require(Q(1607, 50) * 101 + 11 < 34 * 101, "correction uniform precision") + + count = 0 + minima = {"forward": None, "correction": None} + for p in range(101, 1024 + SEED + 1): + for alpha in range(2, isqrt(p - 1) + 1): + slacks = budget(p, alpha) + count += 1 + for name, slack in zip(minima, slacks): + if minima[name] is None or slack < minima[name]["bits"]: + minima[name] = {"bits": slack, "p": p, "alpha": alpha} + controls = { + # These violate the published sufficient budget, not a necessary one. + "forward_P_equals_2p": rejected(budget, 101, 10, 202, None), + "correction_P_equals_31p": rejected(budget, 101, 10, None, 3131), + } + return {"p_inclusive": [101, 1024 + SEED], "all_integer_alpha": "2 <= alpha; alpha^2 < p", + "pairs_checked": count, "minimum_precision_slack": minima, + "negative_controls": controls} + + +def correction_window(s, t, m, start, length=None): + length = 2 * m + 2 if length is None else length + origin = nearest(start, s, t) + for offset in range(m): + b = nearest(start + offset, s, t) - origin + require(0 <= b < length, "selected coordinate outside correlation window") + # Entire inclusive |h|<=m window fits in [start-m, start+2m]. + require(start - m <= start + offset - m and + start + offset + m <= start + 2 * m, "correction input omitted") + + +def check_windows(): + pairs = blocks = outputs = 0 + for s in range(2, 64 + SEED + 1): + for t in range(s + 1, 5 * s // 4 + 1): + if gcd(s, t) != 1: + continue + pairs += 1 + for m in range(1, SEED // 8 + 2): + # All residues, seed-rotated, including negative periodic representatives. + for i in range(s): + start = (i + SEED) % s - s + correction_window(s, t, m, start) + blocks += 1 + outputs += m + # Every output residue for the forward map, also covering periodic boundaries. + for k0 in range(t): + j0 = (s * k0) // t - m + for b in range(m): + # Exact integer endpoints of |j - (k0+b)/sigma| < m. + first = (s * (k0 + b)) // t - m + 1 + last = ceil_div(s * (k0 + b), t) + m - 1 + require(j0 <= first <= last <= j0 + 3 * m + 2, + "forward input window omitted a truncated term") + + # Old upstream hypotheses permit this tuple; the GENERATED domain excludes it. + p, alpha, s, t = 101, 2, 2, 19 + theta = Q(t, s) - 1 + require(theta > Q(p, alpha ** 4) and gcd(s, t) == 1 and t < 2 ** p, + "old-header counterexample does not satisfy old hypotheses") + require(alpha * alpha < p and theta > Q(1, 4), "domain control is not separated") + m = ceil_div(ceil_sqrt(p), 2 * alpha) + require(nearest(1, s, t) == 10 and 2 * m + 2 == 8, + "wrong out-of-domain witness") + controls = { + "old_header_E_window": rejected(correction_window, s, t, m, 0), + "shortened_in_domain_E_window": rejected(correction_window, 4, 5, 3, 0, 3), + } + return {"s_inclusive": [2, 64 + SEED], "t_domain": "s < t <= 5*s/4, gcd(s,t)=1", + "m_inclusive": [1, SEED // 8 + 1], "coprime_pairs": pairs, + "correction_blocks": blocks, "correction_outputs": outputs, + "forward_residues": "all k0 in [0,t), all offsets in [0,m)", + "negative_controls": controls, + "old_header_witness": {"p": p, "alpha": alpha, "s": s, "t": t, + "theta": str(theta), "m": m, "L_B": 2 * m + 2, + "missing_q_1": 10}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="write the deterministic audit receipt") + args = parser.parse_args() + result = {"status": "PASS_SCOPED_GAUSSIAN_CHIRP_DOMAIN_AUDIT", "assignment_seed": SEED, + "sources": check_sources(), "arithmetic": check_arithmetic(), "windows": check_windows(), + "scope": "Source composition and exact bounded arithmetic/window replay; not the full analytic, rounding, tape or multiplication theorem."} + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + receipt = HERE / "RECEIPT.json" + if args.write: + receipt.write_text(encoded) + else: + require(receipt.read_text() == encoded, "receipt differs; inspect changes before regenerating") + print(result["status"]) + print("Exact parameter pairs:", result["arithmetic"]["pairs_checked"]) + print("Exact correction windows:", result["windows"]["correction_blocks"]) + print("All 7 negative controls rejected; receipt matches" if not args.write else + "All 7 negative controls rejected; receipt written") + + +if __name__ == "__main__": + main()