diff --git a/research/pr4483-chernoff-check/README.md b/research/pr4483-chernoff-check/README.md new file mode 100644 index 0000000000..f4ed2cc9ae --- /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), 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: + +| 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 + +- 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/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..445cf60843 --- /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) 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": "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.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..46018b8687 --- /dev/null +++ b/research/pr4483-chernoff-check/verify.py @@ -0,0 +1,195 @@ +#!/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, 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) + 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, formal=False): + 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 + 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 + 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: + 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: + 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: + 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(): + 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)): + 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 + + +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 = [] + 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}") + 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 + + +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())