From 2a60ff2c097624e493a6a88b18a713deada7e4c8 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 15:37:33 +0700 Subject: [PATCH 1/2] =?UTF-8?q?Independently=20check=20#4483's=20identity?= =?UTF-8?q?=20(2)=20and=20Chernoff=20bounds=20(7)-(9)=20on=20actual=20flow?= =?UTF-8?q?s=20(p7,=20p16):=20all=20hold=20with=20wide=20margins=20(no=20n?= =?UTF-8?q?ew=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- research/pr4483-chernoff-check/README.md | 60 ++++++++ research/pr4483-chernoff-check/SOURCES.json | 36 +++++ research/pr4483-chernoff-check/TASK.json | 100 ++++++++++++++ research/pr4483-chernoff-check/VERIFY.json | 22 +++ research/pr4483-chernoff-check/verify.py | 143 ++++++++++++++++++++ 5 files changed, 361 insertions(+) create mode 100644 research/pr4483-chernoff-check/README.md create mode 100644 research/pr4483-chernoff-check/SOURCES.json create mode 100644 research/pr4483-chernoff-check/TASK.json create mode 100644 research/pr4483-chernoff-check/VERIFY.json create mode 100644 research/pr4483-chernoff-check/verify.py diff --git a/research/pr4483-chernoff-check/README.md b/research/pr4483-chernoff-check/README.md new file mode 100644 index 0000000000..fa05453ee4 --- /dev/null +++ b/research/pr4483-chernoff-check/README.md @@ -0,0 +1,60 @@ +# Independent check of #4483 §2–3 on actual flows: identity (2) and Chernoff bounds (7)–(9) + +**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.** + +zxv's #4483, `research/rank-convergence/PROOF.md` (pinned), controls the arbitrary-height flow with three results: +- the exact potential identity `I_t + R_t = B_t + F_t + (T−P)H_t`, eq. (2); +- the two Chernoff bounds, (7) `(T−P)H_t ≥ (1−u_t^ℓ)P^(G+1)(q^(aℓ+1)−1)` and (8) `R_t ≤ q M^λ v_t^ℓ P^(G+1)`; +- their consequence (9), `A_t ≥ D_ℓ(t) P^(G+1)`. + +#4532's critical-root funding inherits these, and with it #4535 and #4568. My #4529 checked #4483's gates and its rank-one identity at `t = 1`. This package checks (2), (7), (8) and (9) **on actual flows** at real exponents. + +## Method + +My own flow code builds the arbitrary-height flow at #4483's height `G = (a+b)·⌊log_M ⌊N/m⌋⌋` and computes, from the flow's classes, five potentials: +- the unit-column potential `H_t`; +- root sources `R_t`; +- inner sources `I_t`; +- boundary exits `B_t`; +- leaf exits `F_t`. + +`u_t`, `v_t` and `q` follow #4483's (6). There are two cases: +- **raw p7** with #4483's p7 geometry: `M = 256`, `a = b = 1`, `s = λ = 1/10`; +- **p16** (#4470) with #4532's p16 geometry: `M = 1024`, `a = b = 1`, `s = 1/20`, `λ = 1/10`. + +Both profiles are read from main (SHA256-pinned). The exponents lie above each profile's moment crossing, since `T > P` is (7)'s premise: the guard exponents `t0` and `t_upper`, plus `0.999`. + +## Results + +All 15 cases pass: +- **Identity (2).** It holds to `10^−9` relative at every rank and exponent. +- **Ratio ordering.** It holds, as does `q > 1`. +- **(7), (8), (9).** They hold with the following slack: + +| profile | ranks `N` (height `G`) | `(T−P)H_t / rhs(7)` | `R_t / rhs(8)` | +|---|---|---|---| +| p7 | 10^5 (2), 10^7 (4), 3·10^9 (6) | 28.0 → 13.5 → 9.97 | 0.304 → 0.123 → 0.096 | +| p16 | 2·10^5 (2), 2·10^8 (4) | 25.2 → 16.1 | 0.267 → 0.237 | + +So (7) holds with a factor of at least 9.97, and (8) with at most 0.31 of the bound. The (7) slack shrinks as the height grows, as expected for a Chernoff tail bound, and stays well above 1 at every tested height. (9) follows, and is checked directly. + +**Scope note.** Below the moment crossing, where `T < P` (for example `t = 0.9` for p7), both sides of (7) are negative and the inequality is not claimed. #4483 states it only for `T > P`. + +## Verify + +```text +python3 -B research/pr4483-chernoff-check/verify.py +``` + +This runs in about 30 s with the standard library only. + +## Limitations + +- **Finite heights.** These are finite heights (`G ≤ 6`) and finitely many exponents. #4483's (7)–(9) are proved for all heights by the written Chernoff argument, which these checks corroborate on actual flows. The asymptotic ranks of #4535 (`N = 2^(10^12)` and beyond) are far outside direct computation. +- **Floating point.** Comparisons use floats. The margins (≥ 9.97 and ≤ 0.31) far exceed rounding. + +## Open next questions + +- An exact-rational version at rational `t`, using certified powers `r^t` as in my #4580 check, to make the identity check exact. First step: replace the float powers by certified intervals at `t = t0`. + +Credit: zxv (#4483), Dillon (#4532), Cinna Davis (#4470), Jacob Alan Sussman (Pascal matching). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4483-chernoff-check/SOURCES.json b/research/pr4483-chernoff-check/SOURCES.json new file mode 100644 index 0000000000..8c00209ade --- /dev/null +++ b/research/pr4483-chernoff-check/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/compact-joint-compiler/arithmetic/RESULT.json", + "usage": "input", + "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff", + "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" + }, + { + "path": "research/higher-moment-strictification/RESULT.json", + "usage": "input", + "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a", + "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156" + }, + { + "path": "research/rank-convergence/PROOF.md", + "usage": "input", + "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e", + "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376" + } + ] +} diff --git a/research/pr4483-chernoff-check/TASK.json b/research/pr4483-chernoff-check/TASK.json new file mode 100644 index 0000000000..ec709ea309 --- /dev/null +++ b/research/pr4483-chernoff-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "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.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "unchanged", + "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "scope_change_reason": null, + "bottleneck_link": "Independent coverage, on actual flows, of the Chernoff inequalities that every #4483/#4532-based kappa claim (#4535, #4568) inherits.", + "budget_minutes": 40, + "stop_rule": "Stop at heights G <= 6 (p7) and 4 (p16).", + "outcome": "completed", + "evidence": "Own flow potentials at #4483's height: identity (2) to 1e-9; (7) slack ratio >= 9.97; (8) ratio <= 0.31; (9) and ratio ordering; 15 cases on p7 and p16 above their crossings.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Exact-rational version with certified powers.", + "why_it_matters": "Would make the identity check exact.", + "first_step": "Certified r^t intervals at t = t0.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4483-chernoff-check/VERIFY.json b/research/pr4483-chernoff-check/VERIFY.json new file mode 100644 index 0000000000..a54dda479a --- /dev/null +++ b/research/pr4483-chernoff-check/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/compact-joint-compiler/arithmetic/RESULT.json", + "research/higher-moment-strictification/RESULT.json", + "research/rank-convergence/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Own arbitrary-height flow potentials at #4483's height for p7 and p16: identity (2), Chernoff (7), (8), (9), ratio ordering; binding to pinned PROOF.md." + } + ] +} diff --git a/research/pr4483-chernoff-check/verify.py b/research/pr4483-chernoff-check/verify.py new file mode 100644 index 0000000000..a996ab3b7e --- /dev/null +++ b/research/pr4483-chernoff-check/verify.py @@ -0,0 +1,143 @@ +#!/usr/bin/env python3 +"""Independent check of PR #4483 (zxv), research/rank-convergence/PROOF.md sections 2-3, on actual flows. + +For the arbitrary-height flow at #4483's height G = (a+b) floor(log_M floor(N/m)), this file's own flow code computes, +at real exponents t, the unit-column potential H_t, root-source potential R_t, inner-source potential I_t, +boundary-exit potential B_t and leaf-exit potential F_t, and checks + (2) I_t + R_t = B_t + F_t + (T - P) H_t (relative error < 1e-9, floats) + (7) (T - P) H_t >= (1 - u_t^ell) P^(G+1) (q^(a ell + 1) - 1) + (8) R_t <= q M^lambda v_t^ell P^(G+1) + (9) A_t = (T - P) H_t - R_t >= D_ell(t) P^(G+1) + and the ratio-ordering premise T(t+s)/T(t) >= P(t+s)/P(t), +with u_t, v_t, q as in #4483 (6), for the raw p7 profile with #4483's p7 geometry (M = 256, a = b = 1, s = lambda = 1/10) +and the p16 (#4470) profile with #4532's p16 geometry (M = 1024, a = b = 1, s = 1/20, lambda = 1/10), at several +ranks (heights G up to 6 for p7 and 4 for p16) and exponents above each profile's moment crossing (T > P is (7)'s premise). Profiles are read from main (sha256-pinned); the proof's +equations are bound verbatim to the pinned PROOF.md. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import hashlib +import json +import math +from math import factorial +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +P7 = ROOT / "research/higher-moment-strictification/RESULT.json" +P16 = ROOT / "research/compact-joint-compiler/arithmetic/RESULT.json" +PROOF = ROOT / "research/rank-convergence/PROOF.md" +PINS = {P7: "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156", P16: "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091", PROOF: "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376"} + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def multis(n, size): + if n == 1: + yield (size,); return + for k in range(size + 1): + for rest in multis(n - 1, size - k): yield (k,) + rest +def potentials(N, W, P, G, t): + ks = sorted(W); m = ks[-1] + def c(a): + v = 1 + for k, x in zip(ks, a): v *= k ** x + return v + def u(a): + v = factorial(sum(a)) + for k, x in zip(ks, a): v = v // factorial(x) * W[k] ** x + return v + F = [{1: 1}] + for d in range(1, G + 1): + nxt = {} + for rho, cnt in F[d - 1].items(): + for r, pr in P.items(): + if m * rho * r <= N: nxt[rho * r] = nxt.get(rho * r, 0) + cnt * pr + F.append(nxt) + present = lambda rho, a: m * rho * c(a) <= N + H = R = I = B = Fl = 0.0 + for d in range(G + 1): + for rho, cnt in F[d].items(): + for b in multis(len(ks), G - d): + if not present(rho, b): continue + H += cnt * u(b) * (rho * c(b)) ** t + for r, pr in P.items(): + issued = cnt * pr * u(b); rank = r * rho * c(b) + if d == G: Fl += issued * rank ** t; continue + D = sum(W[k] * u(tuple(x - (i == j) for j, x in enumerate(b))) + for i, k in enumerate(ks) if b[i] > 0 and present(rho * r, tuple(x - (i == j) for j, x in enumerate(b)))) + if issued - cnt * pr * D: B += (issued - cnt * pr * D) * rank ** t + for a in multis(len(ks), G): + if present(1, a): + for k in ks: R += W[k] * u(a) * (k * c(a)) ** t + for d in range(1, G + 1): + for rho, cnt in F[d - 1].items(): + for r, pr in P.items(): + for a in multis(len(ks), G - d): + if not present(rho * r, a): continue + for i, k in enumerate(ks): + b = list(a); b[i] += 1 + if not present(rho, tuple(b)): I += cnt * pr * u(a) * W[k] * (rho * r * c(tuple(b))) ** t + return H, R, I, B, Fl + + +def mom(h, t): + return sum(x * k ** t for k, x in h.items()) + + +def check_case(name, W, P, M, a, b, s, lam, ranks, exponents): + m = max(W) + rows = [] + for t in exponents: + T, Pt = mom(W, t), mom(P, t) + q = T / Pt + need(q > 1, f"{name}: (7) premise T(t) > P(t) at t={t}") + need(mom(W, t + s) / T >= mom(P, t + s) / Pt, f"{name}: ratio ordering at t={t}") + u_t = M ** (-s) * (mom(W, t + s) / T) ** a * (mom(P, t + s) / Pt) ** b + v_t = M ** lam * (mom(W, t - lam) / Pt) ** (a + b) + for N in ranks: + C = N // m + ell = 0 + while M ** (ell + 1) <= C: + ell += 1 + G = (a + b) * ell + H, R, I, B, Fl = potentials(N, W, P, G, t) + lhs2, rhs2 = I + R, B + Fl + (T - Pt) * H + need(abs(lhs2 - rhs2) <= 1e-9 * abs(rhs2), f"{name}: identity (2) at N={N}, t={t}") + A = (T - Pt) * H - R + rhs7 = (1 - u_t ** ell) * Pt ** (G + 1) * (q ** (a * ell + 1) - 1) + rhs8 = q * M ** lam * v_t ** ell * Pt ** (G + 1) + D = (1 - u_t ** ell) * (q ** (a * ell + 1) - 1) - q * M ** lam * v_t ** ell + need((T - Pt) * H >= rhs7 * (1 - 1e-12), f"{name}: (7) at N={N}, t={t}") + need(R <= rhs8 * (1 + 1e-12), f"{name}: (8) at N={N}, t={t}") + need(A >= D * Pt ** (G + 1) - 1e-9 * abs(D * Pt ** (G + 1)), f"{name}: (9) at N={N}, t={t}") + rows.append({"t": t, "N": N, "ell": ell, "G": G, "ratio7": round(((T - Pt) * H) / rhs7, 4) if rhs7 > 0 else None, + "ratio8": round(R / rhs8, 4)}) + return rows + + +def main(): + for path, digest in PINS.items(): + need(hashlib.sha256(path.read_bytes()).hexdigest() == digest, f"pinned {path.name}") + o7 = json.loads(P7.read_bytes())["invoice_oracle"] + W7 = {int(k): v for k, v in o7["targets"].items()} + P7h = {int(k): v for k, v in o7["paid"].items()} + d16 = json.loads(P16.read_bytes()) + W16 = {int(k): v for k, v in d16["targets"].items()} + P16h = {int(k): v for k, v in d16["paid"].items()} + text = PROOF.read_text(encoding="utf-8") + for s_ in ("I_t+R_t = B_t+F_t+(T_t-P_t)H_t.", "(T-P)H_t >=(1-u_t^ell)P^(G+1)(q^(a*ell+1)-1).", + "<=q*M^lambda*v_t^ell*P^(G+1).", "D_ell(t)=(1-u_t^ell)(q^(a*ell+1)-1)-q*M^lambda*v_t^ell."): + need(s_ in text, f"PROOF.md states: {s_}") + p7 = check_case("p7", W7, P7h, 256, 1, 1, 0.1, 0.1, (10 ** 5, 10 ** 7, 3 * 10 ** 9), (0.99731352, 0.997481, 0.999)) + p16 = check_case("p16", W16, P16h, 1024, 1, 1, 0.05, 0.1, (2 * 10 ** 5, 2 * 10 ** 8), (0.99697984, 0.997066, 0.999)) + print(json.dumps({"status": "PASS_PR4483_CHERNOFF_CHECK", "p7": p7, "p16": p16, + "min_ratio7": min(r["ratio7"] for r in p7 + p16 if r["ratio7"]), + "max_ratio8": max(r["ratio8"] for r in p7 + p16), "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main()) From 84c0fb3a39bcb1e4b8c48892bfdd8a6e7ae58a50 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 16:10:37 +0700 Subject: [PATCH 2/2] Check identity (2) exactly as formal power sums (every t at once), with a rejection control Co-Authored-By: Claude Opus 5.5 --- research/pr4483-chernoff-check/README.md | 4 +- research/pr4483-chernoff-check/TASK.json | 8 +-- research/pr4483-chernoff-check/verify.py | 70 +++++++++++++++++++++--- 3 files changed, 67 insertions(+), 15 deletions(-) diff --git a/research/pr4483-chernoff-check/README.md b/research/pr4483-chernoff-check/README.md index fa05453ee4..f4ed2cc9ae 100644 --- a/research/pr4483-chernoff-check/README.md +++ b/research/pr4483-chernoff-check/README.md @@ -27,7 +27,7 @@ Both profiles are read from main (SHA256-pinned). The exponents lie above each p ## Results All 15 cases pass: -- **Identity (2).** It holds to `10^−9` relative at every rank and exponent. +- **Identity (2), exactly.** At every rank checked, both sides are compared as **formal power sums** `Σ_x c_x·x^t` with integer coefficients, from 245 up to 16,252 distinct bases `x`. They are identical, so (2) holds **exactly, for every exponent `t` at once**. A rejection control drops one root source and is detected. Numerically it also holds to `10^−9` at each tested `t`. - **Ratio ordering.** It holds, as does `q > 1`. - **(7), (8), (9).** They hold with the following slack: @@ -55,6 +55,6 @@ This runs in about 30 s with the standard library only. ## Open next questions -- An exact-rational version at rational `t`, using certified powers `r^t` as in my #4580 check, to make the identity check exact. First step: replace the float powers by certified intervals at `t = t0`. +- Certified (interval) versions of (7) and (8). (2) is now exact. First step: certified powers `r^t` at `t = t0`, as in my #4580 check. Credit: zxv (#4483), Dillon (#4532), Cinna Davis (#4470), Jacob Alan Sussman (Pascal matching). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4483-chernoff-check/TASK.json b/research/pr4483-chernoff-check/TASK.json index ec709ea309..445cf60843 100644 --- a/research/pr4483-chernoff-check/TASK.json +++ b/research/pr4483-chernoff-check/TASK.json @@ -86,14 +86,14 @@ "budget_minutes": 40, "stop_rule": "Stop at heights G <= 6 (p7) and 4 (p16).", "outcome": "completed", - "evidence": "Own flow potentials at #4483's height: identity (2) to 1e-9; (7) slack ratio >= 9.97; (8) ratio <= 0.31; (9) and ratio ordering; 15 cases on p7 and p16 above their crossings.", + "evidence": "Own flow potentials at #4483's height: identity (2) EXACT as formal power sums (up to 16,252 bases) with a rejection control; (7) slack ratio >= 9.97; (8) ratio <= 0.31; (9) and ratio ordering; 15 cases on p7 and p16 above their crossings.", "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", "open_questions": [ { - "question": "Exact-rational version with certified powers.", - "why_it_matters": "Would make the identity check exact.", - "first_step": "Certified r^t intervals at t = t0.", + "question": "Certified interval versions of (7) and (8).", + "why_it_matters": "(2) is exact; (7)/(8) use floats with wide margins.", + "first_step": "Certified r^t at t = t0.", "blocked_by": "None." } ] diff --git a/research/pr4483-chernoff-check/verify.py b/research/pr4483-chernoff-check/verify.py index a996ab3b7e..46018b8687 100644 --- a/research/pr4483-chernoff-check/verify.py +++ b/research/pr4483-chernoff-check/verify.py @@ -4,7 +4,8 @@ For the arbitrary-height flow at #4483's height G = (a+b) floor(log_M floor(N/m)), this file's own flow code computes, at real exponents t, the unit-column potential H_t, root-source potential R_t, inner-source potential I_t, boundary-exit potential B_t and leaf-exit potential F_t, and checks - (2) I_t + R_t = B_t + F_t + (T - P) H_t (relative error < 1e-9, floats) + (2) I_t + R_t = B_t + F_t + (T - P) H_t, EXACTLY as an identity of formal power sums sum_x c_x x^t with integer + coefficients (hence for every t at once), with a dropped-source rejection control, and numerically at each t (7) (T - P) H_t >= (1 - u_t^ell) P^(G+1) (q^(a ell + 1) - 1) (8) R_t <= q M^lambda v_t^ell P^(G+1) (9) A_t = (T - P) H_t - R_t >= D_ell(t) P^(G+1) @@ -40,7 +41,7 @@ def multis(n, size): yield (size,); return for k in range(size + 1): for rest in multis(n - 1, size - k): yield (k,) + rest -def potentials(N, W, P, G, t): +def potentials(N, W, P, G, t, formal=False): ks = sorted(W); m = ks[-1] def c(a): v = 1 @@ -58,21 +59,43 @@ def u(a): if m * rho * r <= N: nxt[rho * r] = nxt.get(rho * r, 0) + cnt * pr F.append(nxt) present = lambda rho, a: m * rho * c(a) <= N - H = R = I = B = Fl = 0.0 + if formal: + H, R, I, B, Fl = {}, {}, {}, {}, {} + + def acc(d, base, coeff): + d[base] = d.get(base, 0) + coeff + else: + H = R = I = B = Fl = 0.0 for d in range(G + 1): for rho, cnt in F[d].items(): for b in multis(len(ks), G - d): if not present(rho, b): continue - H += cnt * u(b) * (rho * c(b)) ** t + if formal: + acc(H, rho * c(b), cnt * u(b)) + else: + H += cnt * u(b) * (rho * c(b)) ** t for r, pr in P.items(): issued = cnt * pr * u(b); rank = r * rho * c(b) - if d == G: Fl += issued * rank ** t; continue + if d == G: + if formal: + acc(Fl, rank, issued) + else: + Fl += issued * rank ** t + continue D = sum(W[k] * u(tuple(x - (i == j) for j, x in enumerate(b))) for i, k in enumerate(ks) if b[i] > 0 and present(rho * r, tuple(x - (i == j) for j, x in enumerate(b)))) - if issued - cnt * pr * D: B += (issued - cnt * pr * D) * rank ** t + if issued - cnt * pr * D: + if formal: + acc(B, rank, issued - cnt * pr * D) + else: + B += (issued - cnt * pr * D) * rank ** t for a in multis(len(ks), G): if present(1, a): - for k in ks: R += W[k] * u(a) * (k * c(a)) ** t + for k in ks: + if formal: + acc(R, k * c(a), W[k] * u(a)) + else: + R += W[k] * u(a) * (k * c(a)) ** t for d in range(1, G + 1): for rho, cnt in F[d - 1].items(): for r, pr in P.items(): @@ -80,7 +103,11 @@ def u(a): if not present(rho * r, a): continue for i, k in enumerate(ks): b = list(a); b[i] += 1 - if not present(rho, tuple(b)): I += cnt * pr * u(a) * W[k] * (rho * r * c(tuple(b))) ** t + if not present(rho, tuple(b)): + if formal: + acc(I, rho * r * c(tuple(b)), cnt * pr * u(a) * W[k]) + else: + I += cnt * pr * u(a) * W[k] * (rho * r * c(tuple(b))) ** t return H, R, I, B, Fl @@ -88,6 +115,29 @@ def mom(h, t): return sum(x * k ** t for k, x in h.items()) +def exact_identity(W, P, N, G): + """(2) as an identity of formal power sums sum_x coeff_x x^t, exact for every t at once.""" + H, R, I, B, Fl = potentials(N, W, P, G, None, formal=True) + lhs, rhs = dict(I), dict(B) + for x, v in R.items(): + lhs[x] = lhs.get(x, 0) + v + for x, v in Fl.items(): + rhs[x] = rhs.get(x, 0) + v + for x, v in H.items(): # (T - P) H = sum_k W_k (k x)^t - sum_r P_r (r x)^t + for k, w in W.items(): + rhs[k * x] = rhs.get(k * x, 0) + w * v + for r, q in P.items(): + rhs[r * x] = rhs.get(r * x, 0) - q * v + lhs = {x: v for x, v in lhs.items() if v} + rhs = {x: v for x, v in rhs.items() if v} + need(lhs == rhs, f"exact formal identity (2) at N={N}, G={G}") + x0 = min(R) # rejection control: dropping one root source must break the identity + bad = dict(lhs) + bad[x0] -= R[x0] + need({x: v for x, v in bad.items() if v} != rhs, "control: a dropped root source is detected") + return len(lhs) + + def check_case(name, W, P, M, a, b, s, lam, ranks, exponents): m = max(W) rows = [] @@ -114,7 +164,9 @@ def check_case(name, W, P, M, a, b, s, lam, ranks, exponents): need((T - Pt) * H >= rhs7 * (1 - 1e-12), f"{name}: (7) at N={N}, t={t}") need(R <= rhs8 * (1 + 1e-12), f"{name}: (8) at N={N}, t={t}") need(A >= D * Pt ** (G + 1) - 1e-9 * abs(D * Pt ** (G + 1)), f"{name}: (9) at N={N}, t={t}") - rows.append({"t": t, "N": N, "ell": ell, "G": G, "ratio7": round(((T - Pt) * H) / rhs7, 4) if rhs7 > 0 else None, + if t == exponents[0]: + bases = exact_identity(W, P, N, G) + rows.append({"t": t, "N": N, "ell": ell, "G": G, "exact_identity_bases": bases, "ratio7": round(((T - Pt) * H) / rhs7, 4) if rhs7 > 0 else None, "ratio8": round(R / rhs8, 4)}) return rows