diff --git a/research/gaussian-section-chain-check/README.md b/research/gaussian-section-chain-check/README.md new file mode 100644 index 0000000000..bc24e8cef9 --- /dev/null +++ b/research/gaussian-section-chain-check/README.md @@ -0,0 +1,92 @@ +# One check of jwr404's p = 19 section chain, with the sharp two-power threshold + +**Claim type: an independent certified finite check of one section. No new +κ.** It covers 33 open PRs in one package, and adds the exact threshold that +their two-power steps approach. + +## Object + +The section is the one from #4319 and my +[#4336](https://github.com/CrocSwap/integer-mult-bounds/pull/4336): `p = 19`, +`β₀ = −1/2`, bandwidth 2, `t_i = i`. The interiors `3..6` are eliminated, and +the survivors `0, 1, 2, 7, 8, 9` are row-normalized to `H`. + +jwr404's chain then applies `HALO.md`'s polynomial inverse +`P = p⁻²⁰ Σ_{j p⁻⁴⁰` | exact, so the spectrum of `Q` lies in `(0, 1 − p⁻⁴⁰)` | +| `19⁻⁴⁰ · 19⁴² = 361` | exact, so `(1 − x)^N < e^(−xN) = e⁻³⁶¹` | +| The 27 two-power claims and #4401's negative | all hold, from `e³⁶¹` enclosed to 60 digits | + +**The sharp threshold.** `(319/100)e⁻³⁶¹ < 2^(−k)` holds exactly for +`k ≤ 519`, and fails at `k = 520`. The chain's step of 19 stops at 513 and +then fails at 532; the true boundary lies between them. + +**Two tight spots.** + +- The row and column sums of `H` clear `1226/625` by only `4.2·10⁻⁶`. The + largest sum is `1 + e^(−9π/722)`, from the forward step at vertex 0. +- The round ceilings `2.82 · 3.61 = 10.1802` exceed `3.19² = 10.1761`. + #4355's 2-norm bound therefore needs the certified norms, not the rounded + ones, as its own README notes. + +## Method and independence + +Nothing is imported from jwr404's packages, and the method differs from +theirs: + +- The entries come from `GAUGEFREE-INTERIORS.md`'s original form. +- `H⁻¹` comes from the quotient identity: the survivor block of `A⁻¹` times + `diag(S)`. +- `H` is the exact inverse of that, with one perturbation bound. + +The notes this reads are on main, pinned by SHA256 with phrase checks. + +## Not covered + +- Any other section, prime or bandwidth. +- `HALO.md`'s all-size claims. +- Whether `#4100`'s callers need more than the `2^(−C)` thresholds proved + here. + +## Reproduce + +```sh +python3.12 -B research/gaussian-section-chain-check/verify.py +``` + +It prints `PASS_GAUSSIAN_SECTION_CHAIN_CHECK` in about 10 seconds, using only +the standard library. + +## Open next questions + +None from this check. + +## Credit + +The chain, its section and its thresholds are jwr's (#4354, #4355, +#4361–#4401). The kernel and lemmas are `#4100`'s `GAUSSIAN.md`, `HALO.md`, +`INVERSE-CONDITIONING.md` and the vendored `GAUGEFREE-INTERIORS.md`. +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) +assistance. Apache-2.0. diff --git a/research/gaussian-section-chain-check/SOURCES.json b/research/gaussian-section-chain-check/SOURCES.json new file mode 100644 index 0000000000..017a97df2d --- /dev/null +++ b/research/gaussian-section-chain-check/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + }, + { + "path": "research/unconditional-batched-crt/INVERSE-CONDITIONING.md", + "usage": "input", + "git_blob": "3853ffac91dfed5421b05533eb274a8646741071", + "sha256": "be3e4b729481b15a5ccc286b297908e4f9cef94c0c9144a28ee1cf58950d142a" + }, + { + "path": "research/unconditional-batched-crt/vendor/GAUGEFREE-INTERIORS.md", + "usage": "input", + "git_blob": "20585e44fa4e49b13b5d8495bbf6ed254459a362", + "sha256": "d1423ac0ea0003521797209f4396e6981a66994bbee4f8b48026e5b95f8c5116" + } + ] +} diff --git a/research/gaussian-section-chain-check/TASK.json b/research/gaussian-section-chain-check/TASK.json new file mode 100644 index 0000000000..7514a58c1a --- /dev/null +++ b/research/gaussian-section-chain-check/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "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_status": "refined", + "actual_scope": "Independently certify every numerical claim of jwr404's p = 19 normalized-section chain (#4354, #4355, #4361, #4362, #4364, #4366-#4401) from exact section entries, and find the exact two-power threshold.", + "scope_change_reason": "The chain splits one section's conditioning and polynomial-inverse error into 33 open PRs with no outside check; one certified recomputation covers them together.", + "bottleneck_link": "HALO.md's polynomial inverse needs these conditioning and error bounds at #4100's precision caller.", + "budget_minutes": 30, + "stop_rule": "Stop once every claim is certified or fails.", + "outcome": "completed", + "evidence": "verify.py: ||H^-1||_1 = 2.8138 in (2.81, 2.82); ||H^-1||_2 <= 3.183 < 3.19; H row and column sums <= 1.9615957574 < 1226/625; Q spectrum in (0, 1-p^-40) and x N = 361 exact; e^361 enclosed to 60 digits proves all 27 claims (319/100) e^-361 < 2^-19C and #4401's negative; sharp threshold 519.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, verifier implementation and writing; no independent human or proof-kernel review.", + "open_questions": [], + "no_open_questions_reason": "Every chain claim holds and the sharp threshold is found." +} diff --git a/research/gaussian-section-chain-check/VERIFY.json b/research/gaussian-section-chain-check/VERIFY.json new file mode 100644 index 0000000000..5a03c0406a --- /dev/null +++ b/research/gaussian-section-chain-check/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/HALO.md", + "research/unconditional-batched-crt/INVERSE-CONDITIONING.md", + "research/unconditional-batched-crt/vendor/GAUGEFREE-INTERIORS.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned notes and phrases; alpha = 3; exact original-form entries; quotient-identity H^-1 and exact H with perturbation bounds; #4354 1-norm interval; #4355 2-norm bound; #4361 row and column sums; #4362 spectrum; #4364 exponent identity; 27 two-power claims and #4401's negative from a 60-digit e^361 enclosure; sharp threshold 519." + } + ] +} diff --git a/research/gaussian-section-chain-check/verify.py b/research/gaussian-section-chain-check/verify.py new file mode 100644 index 0000000000..e71141be79 --- /dev/null +++ b/research/gaussian-section-chain-check/verify.py @@ -0,0 +1,193 @@ +#!/usr/bin/env python3 +"""One independent check of jwr404's p = 19 normalized-section chain (#4354, #4355, #4361, #4362, #4364 and the +two-power PRs #4366-#4401), plus the sharp two-power threshold. + +The section (as in #4319 and my #4336): p = 19, beta0 = -1/2, bandwidth 2, t_i = i on 0..9, interiors 3..6 +eliminated, survivors 0,1,2,7,8,9, rows divided by their diagonals: H. Its inverse is the survivor block of +A^-1 times diag(S) (quotient identity); H is the exact inverse of that, with one perturbation bound. HALO's +polynomial inverse P = p^-20 sum_{j= 0: Taylor on y/2^k <= 1/2 with Lagrange remainder, then squaring""" + k = 0 + while y / 2 ** k > Q(1, 2): + k += 1 + z, s, term = y / 2 ** k, Q(0), Q(1) + for i in range(60): + s += term + term = term * z / (i + 1) + lo, hi = s, s + 2 * term + for _ in range(k): + lo, hi = lo * lo, hi * hi + lo, hi = Q(lo.numerator * 10**95 // lo.denominator, 10**95), Q(-(-hi.numerator * 10**95 // hi.denominator), 10**95) + return lo, hi + + +def snap(lo, hi): + return (lo / GRID).__floor__() * GRID, (hi / GRID).__ceil__() * GRID + + +def entries(pi_lo, pi_hi, alpha=3): + """dict (i, j) -> (lo, hi) for the 10x10 banded matrix""" + theta = Q(1, 4 * P * P) + rho, beta0 = 1 + theta, Q(-1, 2) + out = {} + for i in range(SIZE): + for j in range(SIZE): + h = j - i + if abs(h) > WIDTH: + continue + if h == 0: + out[i, j] = (Q(1), Q(1)) + continue + bi, bj = beta0 + theta * i, beta0 + theta * j + c = (rho * h + bi) ** 2 - bj ** 2 + need(c > 0, "every off-diagonal exponent is negative") + # cross-check against the gauge form: log N = (a/1444)(-1445 h^2 + 1444 h + i^2 - j^2) + need(c * 1444 == 1445 * h * h - 1444 * h - i * i + j * j, "original form equals gauge form") + e_lo = exp_pos(alpha ** 2 * pi_lo * c)[0] + e_hi = exp_pos(alpha ** 2 * pi_hi * c)[1] + out[i, j] = snap(1 / e_hi, 1 / e_lo) + return out + + +def inverse(m): + n = len(m) + w = [row[:] + [Q(int(r == c)) for c in range(n)] for r, row in enumerate(m)] + for c in range(n): + p = next(r for r in range(c, n) if w[r][c] != 0) + w[c], w[p] = w[p], w[c] + w[c] = [x / w[c][c] for x in w[c]] + for r in range(n): + if r != c and w[r][c] != 0: + f = w[r][c] + w[r] = [x - f * y for x, y in zip(w[r], w[c])] + return [row[n:] for row in w] + + +def inf_norm(m): + return max(sum(abs(x) for x in row) for row in m) + + +def perturbed(m_hat, radius_norm): + """inverse of the midpoint and a bound on ||M^-1 - inverse||_inf for ||M - midpoint||_inf <= radius_norm""" + x = inverse(m_hat) + nx = inf_norm(x) + need(nx * radius_norm < Q(1, 2), "perturbation is small") + return x, nx * nx * radius_norm / (1 - nx * radius_norm) + + + +PINS["HALO.md"] = "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" +PHRASES["HALO.md"] = ["Put Q_i=I-p^-20 H_i^* H_i and J=ceil(p^42)."] + + +def main(): + for name, sha in PINS.items(): + raw = (SRC / name).read_bytes() + need(hashlib.sha256(raw).hexdigest() == sha, f"pinned {name}") + for phrase in PHRASES[name]: + need(phrase in raw.decode(), f"{name}: {phrase}") + pi_lo, pi_hi = pi_bounds() + need(exp_pos(pi_hi)[1] < 304 <= exp_pos(Q(9, 4) * pi_lo)[0], "alpha = 3 at p = 19") + ent = entries(pi_lo, pi_hi) + mid = [[(ent[i, j][0] + ent[i, j][1]) / 2 if (i, j) in ent else Q(0) for j in range(SIZE)] for i in range(SIZE)] + rad = max(e[1] - e[0] for e in ent.values()) / 2 + x_hat, eta = perturbed(mid, 4 * rad) + y_hat = [[x_hat[i][j] for j in KEEP] for i in KEEP] + s_hat, eta_s = perturbed(y_hat, 6 * eta) + d_hat = [s_hat[k][k] for k in range(6)] + err = [[eta * (d_hat[j] + eta_s) + abs(y_hat[i][j]) * eta_s for j in range(6)] for i in range(6)] + ninv = [[y_hat[i][j] * d_hat[j] for j in range(6)] for i in range(6)] + e_inv = max(max(sum(err[i]) for i in range(6)), max(sum(err[i][j] for i in range(6)) for j in range(6))) + need(e_inv < Q(1, 10**40), "inverse error below 1e-40") + inv_inf = max(sum(abs(x) for x in r) for r in ninv) + inv_one = max(sum(abs(ninv[i][j]) for i in range(6)) for j in range(6)) + # H itself: exact inverse of the midpoint inverse, with the same perturbation lemma + h_hat, eta_h = perturbed(ninv, 6 * e_inv) + need(eta_h < Q(1, 10**35), "H error below 1e-35") + h_rows = [sum(abs(x) for x in r) + 6 * eta_h for r in h_hat] + h_cols = [sum(abs(h_hat[i][j]) for i in range(6)) + 6 * eta_h for j in range(6)] + need(all(abs(h_hat[k][k] - 1) < Q(1, 10**30) for k in range(6)), "H has unit diagonal") + + out = {} + # #4354: inverse 1-norm in (281/100, 282/100) + need(Q(281, 100) < inv_one - e_inv and inv_one + e_inv < Q(282, 100), "#4354 inverse 1-norm in (2.81, 2.82)") + # #4361: every absolute row and column sum of H below 1226/625, so ||H||_2 < 1226/625 + need(max(h_rows + h_cols) < Q(1226, 625), "#4361 row and column sums of H below 1226/625") + h2_sq = max(h_rows) * max(h_cols) + need(h2_sq < Q(1226, 625) ** 2 and Q(1226, 625) < 2 < 19 ** 10, "#4361 ||H||_2 < 1226/625 < 2 < 19^10") + # #4355: ||H^-1||_2^2 <= ||.||_1 ||.||_inf < (319/100)^2; the round ceilings 2.82 * 3.61 would not suffice + inv2_sq = (inv_one + e_inv) * (inv_inf + e_inv) + need(inv2_sq < Q(319, 100) ** 2 and 319 ** 2 < 101802 < 320 ** 2, "#4355 ||H^-1||_2 < 319/100") + # #4362: eigenvalues of Q in (0, 1 - p^-40) + p = 19 + need(Q(1, p ** 20) * Q(1226, 625) ** 2 < 1 and Q(1, p ** 20) * Q(100, 319) ** 2 > Q(1, p ** 40), "#4362 spectrum of Q inside (0, 1 - p^-40)") + # #4364: (1 - 19^-40)^(19^42) < exp(-361), since x N = 361 for x = 19^-40, N = 19^42, and ln(1 - x) < -x + need(Q(1, p ** 40) * p ** 42 == 361, "#4364 x N = 361") + # the two-power chain: (319/100) e^-361 < 2^-k exactly when e^361 > (319/100) 2^k + e_lo, e_hi = exp_pos(Q(361)) + need(e_hi / e_lo - 1 < Q(1, 10**60), "e^361 enclosed to 60 digits") + below = lambda k: e_lo > Q(319, 100) * 2 ** k # proves (319/100) e^-361 < 2^-k + not_below = lambda k: e_hi < Q(319, 100) * 2 ** k # proves it is not + chain = {4366 + i: 19 * (i + 1) for i in range(4)} + chain[4374] = 95 + chain.update({4379 + i: 19 * (6 + i) for i in range(22)}) + need(sorted(chain.values()) == [19 * c for c in range(1, 28)] and len(chain) == 27, "27 two-power PRs, C = 1..27") + need(all(below(k) for k in chain.values()), "every #4366-#4400 claim (319/100) e^-361 < 2^-19C holds") + need(not_below(532), "#4401: not below 2^-532") + need(below(519) and not_below(520), "sharp threshold: below 2^-519, not below 2^-520") + out = {"inverse_one_norm": f"{float(inv_one):.10f}", "inverse_inf_norm": f"{float(inv_inf):.10f}", + "inverse_two_norm_upper": f"{float(inv2_sq) ** 0.5:.6f}", "H_max_row_col_sum": f"{float(max(h_rows + h_cols)):.10f}", + "H_two_norm_upper": f"{float(h2_sq) ** 0.5:.6f}", "two_power_claims_checked": len(chain) + 1, + "sharp_two_power_exponent": 519} + print(json.dumps({"status": "PASS_GAUSSIAN_SECTION_CHAIN_CHECK", **out, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())