From 4e8f77031b1a936d6739b2cd84f378dcf1eb5635 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 06:15:27 -0400 Subject: [PATCH] Research: independent audit of PR1786's fine-prime transfer lemmas (no new kappa) Exact stdlib re-derivation of FINE-PRIME-PADDING.md sections 1-3, 5 and 7 at PR1786 head c52345ca, against the cited PR1673/PR1758 bounds. No gap found in scope; column-gap analogue added; outer headroom on the PR1699 supplier is (1-eps)q ~ 1.68e-10. Co-Authored-By: Claude Opus 5.5 --- .../README.md | 112 ++++++ .../SOURCES.json | 18 + .../TASK.json | 65 ++++ .../VERIFY.json | 20 + .../verify.py | 361 ++++++++++++++++++ 5 files changed, 576 insertions(+) create mode 100644 research/pr1786-fine-prime-transfer-audit/README.md create mode 100644 research/pr1786-fine-prime-transfer-audit/SOURCES.json create mode 100644 research/pr1786-fine-prime-transfer-audit/TASK.json create mode 100644 research/pr1786-fine-prime-transfer-audit/VERIFY.json create mode 100644 research/pr1786-fine-prime-transfer-audit/verify.py diff --git a/research/pr1786-fine-prime-transfer-audit/README.md b/research/pr1786-fine-prime-transfer-audit/README.md new file mode 100644 index 0000000000..20b390d9a5 --- /dev/null +++ b/research/pr1786-fine-prime-transfer-audit/README.md @@ -0,0 +1,112 @@ +# Audit of PR1786's fine-prime transfer (no new kappa) + +**No gap found in the audited scope. No new bound is claimed, and the selected record is unchanged.** + +This is an independent check of the written transfer lemmas in +[PR1786](https://github.com/CrocSwap/integer-mult-bounds/pull/1786) (chafreaky, +"Conditional κ = 0.001679754788150048 from fine source-prime padding"). It answers +that package's Open next questions 1 and 2 for the explicit inequalities only. + +| Audited text | Commit | SHA256 | +|---|---|---| +| `research/fine-prime-padding/FINE-PRIME-PADDING.md` | PR1786 head `c52345caa318fc6b1b6e2659c57d746317a72823` | `47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce` | +| `research/fine-prime-padding/vendor/pr1758/outer/GAUGEFREE-INTERIORS.md` (PR1758, byte-preserved) | same | `d1423ac0ea0003521797209f4396e6981a66994bbee4f8b48026e5b95f8c5116` | +| `research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md` (PR1673) | PR1673 head `2569871ff906d2a2abfc86e97126ab9afe2e4a5a` | `e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272` | +| `research/capped-phase-fusion/FORWARD-SMALL-A-AUDIT.md` (PR1673) | same | `e37aaa30b15671a1dff00676b14572213efaaac99df202dbba5e09f57af487c0` | + +`verify.py` is written from the prose. It neither imports nor reads PR1786's +checkers, `LEDGER.json` or `CLAIM.json`. Exact rationals decide every PASS. Thresholds +marked INFORMATIONAL use floating point and are reported, not certified. + +## Findings + +1. **Section 1 (prime interval).** For `s` in `((1-2η)t, (1-η)t]` with `η = 1/(4p²)`, + `θ = t/s - 1` lies in `(1/(4p²), 1/(2p²-1)]`, and `S/T > 1/2` whenever `d ≤ p`. + Checked exactly for p = 2..2000. The Trudgian step is sound: + - the main term is at least `ηx/log x`; + - both endpoint errors are at most `2f(x)`, since `f` increases once `log y ≥ 2`; + - at least `x/(8p² log x)` primes survive once `4.472 p² u^{1/4} e^{-√(u/6.455)} ≤ 1`, where `u = log x`. + + If `log x = c·p^(1-ε)` at ε = 0.9999999, that condition needs `ln p ≈ 4.3·10⁸` + (3.8·10⁸ to 4.8·10⁸ for c from 100 down to 0.01). This is consistent with the PR's + disclaimer that it claims no practical cutoff, and it quantifies the cutoff. +2. **Section 2 (conditioning).** The cited bounds do state the θ-dependence the transfer + substitutes: + - PR1673 LOG-A §1: `‖N-I‖∞ ≤ e^{-2aθ} + 5e^{-2a}` holds for every θ > 0. Only its + numeric margin `1/(8p)` assumed `θ ≥ 1/(4p)`. + - FORWARD-SMALL-A §1–2: explicit in θ for 0 < θ ≤ 1. + - PR1758 §3: the accretive gap is `≥ θ/2` (narrow) and `≥ θ` (broad). + + The new margin `1/(8p²)` holds for every p ≥ 1, checked exactly to 5000; the argument + is uniform in p. + + **Column analogue.** LOG-A does not write it out; §5's spectral norms need it. For + column j and `G = q_j - q_i`, the exponent is `G(G + 2β_j)`. The two in-cell + neighbours have `1 ± 2β_j ≥ 2θ` and these sum to 2, so + `‖N-I‖₁ ≤ e^{-2aθ} + e^{-2a(1-θ)} + 4e^{-2a}`, the same polynomial gap. A Decimal + fixture (p = 8, 3000 points, 12 cell cuts) gives a maximum row sum and column sum of + 0.7995, against the bound 0.8018. A control shows that the old `1/(8p)` margin really fails at the new θ, + so the PR is right not to reuse it. The "eventually" steps start at p ≥ 1.05·10⁶ + (`e^{aρ/3} ≤ p²`) and p ≥ 1.9·10²³ (`a ≤ 5 log 16p`). +3. **Section 3 (setup vs online precision).** The bound `a ≤ 16⌈log₂ p⌉` holds for every + p ≥ 3 (exact α to 4096; a continuous bound beyond). Then + `2^{-P_setup} e^{a/(4θ)} < 2^{-Cp}` with slack factor 64 ln 2/16 ≈ 2.77 in the p² L_p + term. Control: with C = 128, the old Cp-bit absolute weight precision rounds some + weight to zero at every p in 32..4096, not only at the PR's p = 32 witness. +4. **Section 5 (locality).** The stated error `p^10 e^{-p²}` is sharp for the exact + identity `H⁻¹ - σΣ_{j 0`. +5. **Section 7 (ledger).** All nine rows were re-derived from the prose table: + - the minimum is `εq`, and the boundary row equals main + 10⁻⁶⁴; + - the Gaussian row exceeds main by exactly `δ(1-2q)`; + - every side condition is positive, including the chirp guard `0.1841409904237`; + - the headline is below `εq` and exceeds PR1758 by 9.279348·10⁻⁹. + + Controls that must fail, and do: the old `θ ~ 1/d` guard, a `θ ~ 1/p` guard, + `β = 1-δ/2`, and `ε = 1`. +6. **Saturation of this outer on this supplier.** Along the whole family + `ε = 1-δ, β = 1-3δ, ξ = ε(1+q) - 3/32 + s` (checked for δ = 10⁻⁴..10⁻³⁷), the binding row + stays `εq < q`, where `q` is PR1699's certified complex endpoint + `b_cert = 0.001679754956125544521335` minus 2·10⁻⁶⁴. No reparametrization of this + nine-row ledger can reach `b_cert`. The remaining outer-only headroom is + `(1-ε)q ≈ 1.68·10⁻¹⁰`. Larger gains on this line need a better certified complex + supplier, which is the PR's own Open question 3. + +## Not checked + +- SHALLOW-TOEPLITZ and the accretive circuit theorem (PR1758 §4). Its proof is cited, not + re-derived here. +- The derivation of each cost row's exponent. +- The union schedule and microbox layout. +- §4's normalization accounting, beyond the `O(d log p) = o(p)` arithmetic. +- The supplier admission (no native replay). +- The all-size compiler and every other inherited hypothesis that PR1786 lists. + +## Reproduce + +```sh +python3 scripts/research_package.py --package research/pr1786-fine-prime-transfer-audit --check-only +python3.12 scripts/research_package.py --package research/pr1786-fine-prime-transfer-audit +# or directly: python3 -B research/pr1786-fine-prime-transfer-audit/verify.py +``` + +The verifier is stdlib-only, runs in under one second, and passes on Python 3.10, 3.12 and 3.14. + +## Open next questions + +1. **Can the accretive Toeplitz theorem (PR1758 §4) be independently re-derived?** It is + the largest cited input left unchecked. First step: check §4(a)'s quotient identity + `(T_b/T_a)/(T_m/T_a) = T_b/T_m` and §4(d)'s recursion. Blocked only by reviewer time. +2. **Can the supplier endpoint be raised?** Finding 6 shows that is the only remaining + lever on this outer line. First step: price candidate suppliers with the same paid + moment. That requires a complete native word and admission. + +## Credit + +The audited mathematics is by Chafik Boukhalfa (PR1786, with OpenAI Codex assistance), +Vlado Vojdanovski (PR1673), and IdeaOuter and the PR1758 contributors. Tim Trudgian proved +the cited prime theorem. The supplier lineage is retained by PR1699. This audit was +prepared in a Claude Code (Anthropic Claude Opus) session donated by JosieElliston. +It is new work under Apache-2.0. diff --git a/research/pr1786-fine-prime-transfer-audit/SOURCES.json b/research/pr1786-fine-prime-transfer-audit/SOURCES.json new file mode 100644 index 0000000000..681d42c93a --- /dev/null +++ b/research/pr1786-fine-prime-transfer-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + } + ] +} diff --git a/research/pr1786-fine-prime-transfer-audit/TASK.json b/research/pr1786-fine-prime-transfer-audit/TASK.json new file mode 100644 index 0000000000..6f8bc2c0ef --- /dev/null +++ b/research/pr1786-fine-prime-transfer-audit/TASK.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "independent-moment", + "question": "Can one selected pricing or assembly claim be checked by a genuinely independent exact implementation?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Recompute one small part of the ledger or one certified enclosure using an independent implementation.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent audit of the written transfer lemmas of pending PR1786 (head c52345ca): FINE-PRIME-PADDING.md sections 1-3, 5 and 7, and whether the cited PR1673 (LOG-A-PHASE-SCHUR-AUDIT s1-3, FORWARD-SMALL-A-AUDIT s1-2) and PR1758 (GAUGEFREE-INTERIORS s2-5) bounds state the theta-dependence substituted at theta ~ 1/(4p^2). Exact stdlib re-derivation of every explicit inequality and of the nine-row cost table from the prose.", + "scope_change_reason": "The selected ledger already has several independent moment/pricing checks (PR1293, PR1577, PR1632 and packages such as frontier1094-emitted-ledger-seed78). The newest pending pricing claim, PR1786, had no independent check and asks for one in its Open next questions 1-2.", + "bottleneck_link": "PR1786 would raise the conditional kappa above the selected record; an independent check of its new transfer lemmas is needed before any maintainer adoption. The saturation finding (outer headroom (1-eps)q ~ 1.68e-10 on the PR1699 supplier) redirects further effort on this outer line to the complex supplier endpoint.", + "budget_minutes": 60, + "stop_rule": "Stop at 60 minutes; report unchecked cited theorems rather than re-deriving SHALLOW-TOEPLITZ or the cost rows.", + "outcome": "completed", + "evidence": "verify.py: exact checks of sections 1-3, 5, 7 (theta interval p=2..2000, row gap p<=5000, setup precision a<=16L_p for p>=3, Neumann tail identity and bandwidth on a banded fixture, nine rows and side conditions), a Decimal column-gap fixture, seven rejecting controls, and informational eventual thresholds (Trudgian step needs ln p ~ 4.3e8 at c=1).", + "author": "Claude Code (Opus) donated session for JosieElliston", + "ai_assistance": "Prepared end to end by Claude Code (Anthropic Claude Opus) in a session donated by JosieElliston; no human review.", + "open_questions": [ + { + "question": "Is the accretive Toeplitz circuit theorem (PR1758 GAUGEFREE-INTERIORS s4) correct as stated, including the descendant bound?", + "why_it_matters": "It is the largest cited input to PR1758/PR1786 not independently re-derived; the theta ~ p^-2 transfer relies on it with Lambda/mu = p^O(1).", + "first_step": "Check the quotient identity (T_b/T_a)/(T_m/T_a)=T_b/T_m and the prefix-norm recursion of s4(d) on exact small shifted-Gaussian sections.", + "blocked_by": "Reviewer time only." + }, + { + "question": "Can the certified complex supplier endpoint on this outer line be raised above 0.001679754956125544521335?", + "why_it_matters": "On this nine-row ledger every parameter choice has kappa < eps*q < q; outer-only headroom is (1-eps)q ~ 1.68e-10.", + "first_step": "Price candidate supplier words with the same paid moment before building any outer change.", + "blocked_by": "A complete paid native word and fresh admission." + } + ] +} diff --git a/research/pr1786-fine-prime-transfer-audit/VERIFY.json b/research/pr1786-fine-prime-transfer-audit/VERIFY.json new file mode 100644 index 0000000000..eff2bdc287 --- /dev/null +++ b/research/pr1786-fine-prime-transfer-audit/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact re-derivation of PR1786 transfer inequalities (sections 1-3, 5, 7), column-gap fixture, seven rejecting controls (old 1/(8p) margin, old Cp weight precision, halo p^40, old theta~1/d and theta~1/p guards, beta=1-delta/2, eps=1), saturation along delta->0; informational eventual thresholds." + } + ] +} diff --git a/research/pr1786-fine-prime-transfer-audit/verify.py b/research/pr1786-fine-prime-transfer-audit/verify.py new file mode 100644 index 0000000000..13cda9d788 --- /dev/null +++ b/research/pr1786-fine-prime-transfer-audit/verify.py @@ -0,0 +1,361 @@ +#!/usr/bin/env python3 +"""Independent audit checks for PR1786's written fine-prime transfer. + +Audited text: research/fine-prime-padding/FINE-PRIME-PADDING.md at PR1786 head +c52345caa318fc6b1b6e2659c57d746317a72823 (SHA256 in README.md). Every +quantity below is re-derived from that prose and from the cited PR1673/PR1758 +statements. Nothing is imported or read from PR1786's checkers or ledger. + +Exact rational arithmetic decides every PASS condition except the parts marked +INFORMATIONAL (eventual thresholds, computed in floating point and reported only). +Standard library only. Claude Code (Opus) donated session; Apache-2.0. +""" +import json +import math +import sys +from decimal import Decimal, getcontext +from fractions import Fraction as F +from pathlib import Path + +if not __debug__: + raise SystemExit('assertions must be enabled') +ROOT = Path(__file__).resolve().parents[2] +getcontext().prec = 60 +report = {} + + +def dec_ln(n): + return Decimal(n).ln() + + +# Rigorous rational bounds: 3.14159 < pi < 3.1416 and 0.6931 < ln 2 < 0.6932. +PI_LO, PI_HI = F(314159, 100000), F(31416, 10000) +LN2_LO, LN2_HI = F(6931, 10000), F(6932, 10000) + + +def alpha_of(p): + """alpha = ceil(sqrt((4/pi) log(16p))); refuse if the ceiling is ambiguous.""" + v = (Decimal(4) / Decimal('3.14159265358979323846264338327950288')) * dec_ln(16 * p) + r = v.sqrt() + a = int(r) + (0 if r == int(r) else 1) + assert abs(r - Decimal(a)) > Decimal('1e-30') and abs(r - Decimal(a - 1)) > Decimal('1e-30') + return a + + +# ---------------------------------------------------------------- section 1 +# s in ((1-2eta)t, (1-eta)t], eta = 1/(4p^2); theta = t/s - 1 is decreasing in s. +def theta_range(p): + eta = F(1, 4 * p * p) + lo = 1 / (1 - eta) - 1 # attained at s = (1-eta)t + hi = 1 / (1 - 2 * eta) - 1 # approached as s -> (1-2eta)t (excluded) + return eta, lo, hi + + +for p in range(2, 2001): + eta, lo, hi = theta_range(p) + assert lo > F(1, 4 * p * p) # strict lower bound of section 1 + assert hi == F(1, 2 * p * p - 1) and hi <= F(1, p * p) + # capacity: (1-2eta)^d >= 1-2d*eta > 1/2 for every d <= p (Bernoulli; d=p worst) + assert 1 - 2 * p * eta > F(1, 2) +# exact Bernoulli spot checks, d = p +for p in (2, 3, 5, 17, 64): + assert (1 - F(1, 2 * p * p)) ** p >= 1 - F(p, 2 * p * p) > F(1, 2) +report['section1_theta_interval'] = 'PASS: 1/(4p^2) < theta <= 1/(2p^2-1) <= 1/p^2 and S/T > 1/2 (d<=p), p=2..2000 exact' + + +# INFORMATIONAL: eventual threshold of the Trudgian-based count. +# Count >= eta x/log x - 2 f(x) with f(y)=0.2795 y (log y)^(-3/4) exp(-sqrt(log y/6.455)) +# increasing for log y >= 2. Half the main term survives iff +# 4*0.2795*u^(1/4)*exp(-sqrt(u/6.455)) <= 1/(4p^2), u = log x = c p^(1-eps). +def count_ok(L, c, one_minus_eps): + lu = math.log(c) + one_minus_eps * L + if lu > 600: # sqrt(u/6.455) > e^299 dwarfs 2L + log(u)/4 + 3 for every L <= 1e13 tested + return True + u = math.exp(lu) + if u < math.log(229): + return False + lhs = math.log(4 * 0.2795 * 4) + 2 * L + 0.25 * math.log(u) - math.sqrt(u / 6.455) + return lhs <= 0 + + +def threshold(c, one_minus_eps): + lo, hi = 1.0, 1e13 + assert count_ok(hi, c, one_minus_eps) + for _ in range(200): + mid = (lo + hi) / 2 + if count_ok(mid, c, one_minus_eps): + hi = mid + else: + lo = mid + # condition is monotone past the threshold: spot-check a geometric grid above it + assert all(count_ok(hi * k, c, one_minus_eps) for k in (1.0001, 1.5, 3, 10, 100)) + return hi + + +report['section1_eventual_threshold_INFORMATIONAL'] = { + 'meaning': 'smallest log(p) (natural) from which the cited Trudgian bound leaves half the main term, if log x = c p^(1-eps), eps = 9999999/10000000', + **{f'c={c}': f'{threshold(c, 1e-7):.4g}' for c in (0.01, 1, 100)}, +} + +# ---------------------------------------------------------------- section 2 +# LOG-A-PHASE-SCHUR-AUDIT s1: ||N-I||_inf <= exp(-2a theta) + 5 exp(-2a), any theta>0. +# Claim: theta >= 1/(4p^2), a >= 4 log(16p) => row gap >= 1/(8p^2). +# Proof used here: x = 2a theta >= a/(2p^2); if x<=1 then 1-e^-x >= x/2 >= a/(4p^2) +# >= log(16p)/p^2 >= 2/p^2 ... (16p >= e^2 for p >= 1); if x>1, 1-e^-x > 1/2. +# And 5 e^(-2a) <= 5 (16p)^(-8). Check gap >= 1/(8p^2) exactly using ln(16p) >= 2. +for p in range(1, 5001): + lower_first = min(F(1, 2), F(2, p * p)) # uses log(16p) >= log 16 > 2 + assert lower_first - F(5, (16 * p) ** 8) >= F(1, 8 * p * p) +report['section2_row_gap'] = 'PASS: gap >= 1/(8p^2) for p=1..5000 (exact; the argument is uniform in p)' + +# Control: PR1673's old numeric margin 1/(8p) cannot be reused at the new theta. +# At theta = 1/(2p^2-1) (largest new theta) and a <= 5 log(16p)+pi+2 sqrt(4 pi log 16p), +# 1 - e^{-2a theta} <= 2a theta < 1/(8p) once p is large: exhibit it exactly at p=2^20. +p = 2 ** 20 +a_hi = PI_HI * alpha_of(p) ** 2 +assert 2 * a_hi * F(1, 2 * p * p - 1) < F(1, 8 * p) +report['control_old_row_margin_1_over_8p_fails'] = f'PASS (rejects): at p=2^20 the new-theta gap is below 1/(8p)' + +# Column analogue (not written in LOG-A s1): for column j and source offset i=j-h with +# G=q_j-q_i, the exponent is (rho h+beta_i)^2-beta_j^2 = G(G+2beta_j). In-cell neighbours give +# 1+2beta_j >= 2theta and 1-2beta_j > 2theta, summing to 2, and |G|>=2 gives >= G^2/2, so +# ||N-I||_1 <= e^{-2a theta} + e^{-2a(1-theta)} + 4e^{-2a}: the same polynomial gap as rows. +# Finite fixture: build N on 3000 source points (several cells) at p=8, theta just above +# 1/(4p^2), a = pi*alpha^2, |h|<=8, and compare row and column off-diagonal sums (Decimal). +def n_fixture(p, npts=3000, hmax=8): + theta = Decimal(1) / Decimal(4 * p * p) * Decimal('1.0001') + rho = 1 + theta + a = Decimal('3.14159265358979323846264338327950288') * alpha_of(p) ** 2 + qv = [int((rho * j + Decimal('0.5')).to_integral_value(rounding='ROUND_FLOOR')) for j in range(npts)] + bv = [rho * j - qv[j] for j in range(npts)] + assert all(Decimal('-0.5') <= x < Decimal('0.5') for x in bv) + rows = [Decimal(0)] * npts + cols = [Decimal(0)] * npts + for i in range(npts): + for h in range(-hmax, hmax + 1): + k = i + h + if h == 0 or not 0 <= k < npts: + continue + e = (-a * ((rho * h + bv[i]) ** 2 - bv[k] ** 2)).exp() + rows[i] += e + cols[k] += e + inner = range(hmax, npts - hmax) + return theta, a, max(rows[i] for i in inner), max(cols[i] for i in inner), sum(1 for j in range(1, npts) if qv[j] - qv[j - 1] == 2) + + +getcontext().prec = 40 +th, a8, rmax, cmax, cuts = n_fixture(8) +bound = (-2 * a8 * th).exp() + (-2 * a8 * (1 - th)).exp() + 4 * (-2 * a8).exp() +assert cuts >= 3 and rmax <= bound and cmax <= bound and 1 - cmax >= Decimal(1) / (8 * 64) +getcontext().prec = 60 +report['section2_column_gap_fixture'] = (f'PASS: p=8, {cuts} cell cuts, max row off-diag {float(rmax):.6f}, ' + f'max column off-diag {float(cmax):.6f}, both <= {float(bound):.6f}; column gap >= 1/(8p^2)') + +# FORWARD-SMALL-A-AUDIT s1-2: ||K^-1|| <= alpha e^{3b/4} c_b^{-4} (1-e^{-b rho theta})^{-2}, +# c_b^{-4} <= e^{a rho/3}, (1-e^{-x})^{-1} <= 2/x for 0= 1/(4p^2) gives a polynomial bound. +# INFORMATIONAL eventual thresholds used by section 2's "eventually". +def first_p(pred, lo=2, hi=2**200): + assert pred(hi) + while hi - lo > 1: + mid = (lo + hi) // 2 + lo, hi = (lo, mid) if pred(mid) else (mid, hi) + return hi + + +def a_upper_continuous(p): + l = float(dec_ln(16 * p)) + return 4 * l + 2 * math.sqrt(4 * math.pi * l) + math.pi + + +p_a5 = first_p(lambda p: a_upper_continuous(p) <= 5 * float(dec_ln(16 * p))) +p_exp = first_p(lambda p: (5 / 3) * (1 + 1 / p**2) * float(dec_ln(16 * p)) <= 2 * float(dec_ln(p))) +report['section2_eventual_thresholds_INFORMATIONAL'] = { + 'a<=5log(16p) (continuous alpha bound)': f'p >= {p_a5:.4g}', + 'exp(a rho/3)<=p^2 given a<=5log(16p)': f'p >= {p_exp:.4g}', +} + +# ---------------------------------------------------------------- section 3 +# Claim: a <= 16 L_p eventually, L_p = ceil(log2 p); then with P_setup = Cp + 64 p^2 L_p, +# 2^-P_setup e^{a/(4 theta)} < 2^-Cp because a/(4theta) < a p^2 <= 16 p^2 L_p and +# e^X < 2^{2X}. Exact alpha for p <= 4096, continuous alpha bound beyond (monotone gap). +first_ok = None +for p in range(2, 4097): + a_hi_p = PI_HI * alpha_of(p) ** 2 + L = (p - 1).bit_length() + ok = a_hi_p <= 16 * L + if ok and first_ok is None: + first_ok = p + if not ok: + first_ok = None + if first_ok is not None: + # precision inequality, exact: need 64 p^2 L > (a p^2)/ln 2, i.e. a < 64 L ln 2 + assert a_hi_p < 64 * L * LN2_LO +assert first_ok is not None +# beyond 4096: for 2^(k-1) < p <= 2^k, L_p = k and a <= a_upper_continuous(p) <= a_upper_continuous(2^k), +# so checking a_upper_continuous(2^k) < 16k covers every such p (and 16 log2 p outgrows 4 ln p beyond 2^400) +for k in range(12, 400): + p = 2 ** k + assert a_upper_continuous(p) + 1e-9 < 16 * k +report['section3_setup_precision'] = f'PASS: a <= 16 L_p for all p >= {first_ok} (exact alpha to 4096, continuous bound to 2^400); setup inequality holds with factor 64 ln2/16 = {float(64*LN2_LO/16):.3f} slack' + +# Control: the old O(p)-bit absolute weight precision underflows for every p >= 32: +# the narrow weight nearest beta=0 has -log w >= a(1/4 - theta^2)/theta > C p log 2 with C=128. +for p in range(32, 4097): + theta_hi = F(1, 2 * p * p - 1) + a_lo = 4 * F(int(dec_ln(16 * p) * 10**6), 10**6) + assert a_lo * (F(1, 4) - theta_hi ** 2) / theta_hi > 128 * p * LN2_HI +report['control_old_Cp_weight_precision_underflows'] = 'PASS (rejects): C=128, every p in 32..4096' + +# ---------------------------------------------------------------- section 5 +# Generic locality: Q = I - sigma H^T H, sigma = p^-20. Exact identity +# H^-1 - sigma sum_{j radius, core p^128 > halo; gA/L -> 0 iff 128-48-beta>0. +norm_pow, scale_pow = 10, 20 +gap_pow = 2 * scale_pow +iter_pow = gap_pow + 2 +radius_pow = iter_pow + 1 +assert (gap_pow, iter_pow, radius_pow) == (40, 42, 43) and 48 > radius_pow and 128 - 48 - 1 > 0 +report['section5_neumann_locality'] = 'PASS: exact tail identity and bandwidth 2W(J-1)+W on a banded fixture; exponents 40/42/43 < halo 48 < core 128' +# Control: a halo of p^40 would not cover the radius p^43. +assert not 40 > radius_pow +report['control_halo_p40_rejected'] = 'PASS (rejects)' + +# ---------------------------------------------------------------- section 7 +# Re-derive the nine paid rows from the prose table (not from LEDGER.json). +b_cert = F(335950991225108904267, 200000000000000000000000) +b = b_cert - F(1, 10**64) +q = b - F(1, 10**64) +a_eff = (q + b) / 2 +r0, s = F(1, 10**64), F(1, 10**64) +eps, beta, delta = F(9999999, 10**7), F(9999997, 10**7), F(1, 10**7) +c = (3 - F(45, 16)) / 2 +xi = eps * (1 + q) - F(3, 32) + s +assert 7**16 < 2**45 and c == F(3, 32) + + +def savings(eps, beta, xi, q, a_eff): + return { + 'main_transforms': eps * q, + 'global_coordinate_router': a_eff, + 'fused_gaussian_groups': 1 - eps + q * beta, + 'group_bit_router': 1 - eps + a_eff * beta, + 'group_scans': 1 - eps + beta, + 'strassen_boundary': c + xi - eps, + 'radix_union_movement': xi + F(1, 2) - eps, + 'polynomial_products': eps, + 'core_face_corrections': 1 - (eps + beta + 48 - 128 + 2), + } + + +sv = savings(eps, beta, xi, q, a_eff) +kmin = min(sv.values()) +assert kmin == sv['main_transforms'] == eps * q +assert sv['strassen_boundary'] == eps * q + s +assert sv['fused_gaussian_groups'] - eps * q == delta * (1 - 2 * q) > 0 +headline = F('0.001679754788150048') +assert headline < kmin +side = { + '1-beta': 1 - beta, '1-beta-2(1-eps)': 1 - beta - 2 * (1 - eps), 'eps-beta': eps - beta, + '1-eps-r0': 1 - eps - r0, 'chirp guard 1-(2xi-2)-r0-beta': 1 - (2 * xi - 2) - r0 - beta, + 'xi-1/2': xi - F(1, 2), 'eps-xi': eps - xi, '2-xi': 2 - xi, '128-48-beta': 128 - 48 - beta, +} +assert all(v > 0 for v in side.values()) +g_ = side['chirp guard 1-(2xi-2)-r0-beta'] +assert F('0.184140990423') < g_ < F('0.184140990424') +assert side['1-beta-2(1-eps)'] == delta +pr1758 = F('0.001679745508802299051546533685199973672313473419790800679752457380932784242972585600630181672224983') +assert headline - pr1758 > F('9.2793e-9') +selected = F(json.loads((ROOT / 'certificates/selected-result.json').read_text())['kappa']) +assert headline > selected +# Control: the old chirp guard (theta ~ 1/d, exponent beta+2xi-eps) fails at this point. +assert 1 - (2 * xi - eps) - r0 - beta < 0 +# Control: theta ~ 1/p (theta power 1) would also fail the guard at this point. +assert 1 - (2 * xi - 1) - r0 - beta < 0 +# Control: a group size beta = 1 - delta/2 breaks the membership row 1-beta-2(1-eps). +assert 1 - (1 - delta / 2) - 2 * (1 - eps) < 0 +# Control: eps = 1 removes the superpolynomial source axis (1-eps-r0 < 0). +assert 1 - 1 - r0 < 0 +report['section7_ledger'] = { + 'status': 'PASS: nine rows re-derived; minimum is eps*q; boundary = main + 1e-64; all side conditions positive', + 'kappa_headline': '0.001679754788150048', + 'eps_q_decimal': f'{Decimal(kmin.numerator) / Decimal(kmin.denominator):.30f}', + 'chirp_guard': f'{Decimal(g_.numerator) / Decimal(g_.denominator):.15f}', + 'gain_over_pr1758': f'{float(headline - pr1758):.6e}', + 'controls': 'old theta~1/d guard, theta~1/p guard, beta=1-delta/2 and eps=1 all fail (rejects)', +} + +# Saturation: along the whole one-parameter family delta -> 0 (eps=1-delta, beta=1-3delta, +# xi=eps(1+q)-3/32+s) the minimum row is eps*q < q. So no outer-only reparametrization of +# this ledger, on this supplier, can reach q; the remaining outer headroom is (1-eps) q. +for k in range(4, 40, 3): + d = F(1, 10**k) + e_, be_ = 1 - d, 1 - 3 * d + x_ = e_ * (1 + q) - F(3, 32) + s + sv_ = savings(e_, be_, x_, q, a_eff) + assert min(sv_.values()) == e_ * q < q + assert 1 - (2 * x_ - 2) - r0 - be_ > 0 and x_ < e_ and x_ > F(1, 2) +headroom = q - headline +report['saturation'] = { + 'status': 'PASS: for delta=1e-4..1e-37 the binding row stays eps*q < q', + 'b_cert_PR1699': f'{Decimal(b_cert.numerator) / Decimal(b_cert.denominator):.24f}', + 'q': 'b_cert - 2e-64', + 'headroom_q_minus_headline': f'{float(headroom):.6e}', + 'meaning': 'outer-only changes to this ledger on the PR1699 supplier can add at most this much; larger gains need a better certified complex supplier endpoint', +} + +report['status'] = 'PASS_PR1786_TRANSFER_AUDIT_SCOPED' +report['scope'] = ('Explicit inequalities of FINE-PRIME-PADDING.md sections 1-3, 5, 7 and the theta-dependence ' + 'of the cited PR1673/PR1758 bounds. Not checked: SHALLOW-TOEPLITZ circuit theorem, union ' + 'schedule, layout/cost-row derivations, supplier admission, all-size compiler.') +print(json.dumps(report, indent=2))