From a1b836c56b4cd40cdad8ca84691e0e59e5d19a45 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 10:48:46 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20certify=20#4483's=20finite=20ga?= =?UTF-8?q?tes=20(p16=202^2800000000,=20all=20four=20witnesses)=20and=20it?= =?UTF-8?q?s=20arbitrary-height=20flow=20identities=20(no=20new=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/rank-convergence-gates/README.md | 80 ++++ research/rank-convergence-gates/SOURCES.json | 48 +++ research/rank-convergence-gates/TASK.json | 100 +++++ research/rank-convergence-gates/VERIFY.json | 24 ++ research/rank-convergence-gates/verify.py | 371 +++++++++++++++++++ 5 files changed, 623 insertions(+) create mode 100644 research/rank-convergence-gates/README.md create mode 100644 research/rank-convergence-gates/SOURCES.json create mode 100644 research/rank-convergence-gates/TASK.json create mode 100644 research/rank-convergence-gates/VERIFY.json create mode 100644 research/rank-convergence-gates/verify.py diff --git a/research/rank-convergence-gates/README.md b/research/rank-convergence-gates/README.md new file mode 100644 index 0000000000..9f0cdb6847 --- /dev/null +++ b/research/rank-convergence-gates/README.md @@ -0,0 +1,80 @@ +# Independent certified check of #4483's finite gates and arbitrary-height flow + +**Claim type:** an independent certified recomputation by separately written code. **No new κ.** It covers +zxv's [#4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483) (`research/rank-convergence`). That +PR changes the direct flow's stopping height and closes the recursion with a shifted-logarithmic majorant, +reporting the p16 sufficient rank `2^2800000000` instead of `2^558100005581` at κ = 0.00302015. It is a +compiler follow-up in the maintainers' #4470 review plan, and it answers the obstruction my +#4459/#4465/#4467 described. + +## What is checked, for all four witnesses in `BENCHMARKS.json` + +Each raw profile is read from its pinned source. Everything uses certified interval logarithms and +exponentials (the helpers of my #4455), with exact rational powers for `U^{ℓ₀}` and `V^{ℓ₀}`. + +- **The guards (18) on `[t₀, t_hi]`:** + - `T_{t₀} > P_{t₀}`; + - `d ≤ μ_T(t₀) − μ_P(t_hi)`, where the μ are tilted log means; + - the bounds `Q`, `U` and `V`; + - the ratio ordering `T_{t₀+s}/T_{t₀} ≥ P_{t_hi+s}/P_{t_hi}`; + - `η_min ≤ t₀m^{t₀−1}` and `c ≥ p/(1−t₀)`; + - `τ(n₀) ≤ t_hi`. +- **The mirror guard (4)** on every elementary window, for each of the 20 t-slices, in the sufficient form + `E_J(t_b) ≤ β·S_J(t_a)`. +- **The recurrence inequality (20)** and the **final funding (17)** at `N = 2^H`. + +| witness | D (lower) | required | worst mirror ratio | τ(n₀) ≤ t_hi | final margin (lower) | +| --- | ---: | ---: | ---: | --- | ---: | +| p7 | 0.02858992 | 0.02336096 | 0.32091 | 0.9974809363 ≤ .997481 | 0.00003773 | +| native4453 | 0.05448611 | 0.04422604 | 0.57408 | 0.9971361473 ≤ .9971362 | 1.19575350 | +| native4453, matched uniform | 0.05448611 | 0.04422604 | 0.57408 | same | 0.32116914 | +| **p16** | **0.04854643** | **0.04306220** | 0.56287 | 0.9970659832 ≤ .997066 | **0.60862507** | + +All match #4483's stated values. Two margins are thin but certified positive: + +- p7's final margin of about 3.8·10⁻⁵; +- the `τ(n₀)` covers, with slack of about 2·10⁻⁸ to 7·10⁻⁸. + +PROOF.md's rejection control, `t_hi = .9974808` for p7, is rejected. + +## Arbitrary-height flow (#4483's open question 1) + +On raw p7 at `N = 500, 3000, 20000`, my independent #4436 flow is run with a forced height `G`, at every +`G = 0, …, G₀ + 2`. That range includes heights above the old minimum-target height, where root classes +are empty. Over these 13 cases: + +- the exact rank-one identity `Σ S·s − Σ X·e = 608·col` holds; +- every exit stays below `n`; +- the exact mirror identity of #4459 holds. + +So PROOF.md §1–2's flow identities do not depend on the old height. + +## Not covered + +- PROOF.md's theorem itself, including the Chernoff and majorant arguments. Only its finite gates are + recomputed here. +- The native suppliers and the outer consumer points. +- The stopping heights actually used inside the certificates, beyond `τ(n₀)`. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/rank-convergence-gates --check-only +python3.12 -B scripts/research_package.py --package research/rank-convergence-gates +``` + +The verifier prints `PASS_RANK_CONVERGENCE_GATES` in about 7 minutes, using only the standard library. + +## Open next questions + +1. **Can p7's 3.8·10⁻⁵ final margin be widened by a small change of `(t₀, c, ℓ₀)`?** + - *Why it matters:* it gives a more robust p7 witness. + - *First step:* scan `ℓ₀` and `c` with this certified checker, holding the consumer saving fixed. + +## Credit + +- The theorem, the witnesses and the adaptive height are zxv's (#4483). +- The flow is from #4436. The mirror identity is from my #4459. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/rank-convergence-gates/SOURCES.json b/research/rank-convergence-gates/SOURCES.json new file mode 100644 index 0000000000..6400555819 --- /dev/null +++ b/research/rank-convergence-gates/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "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/native-lattice-retiming/RESULT.json", + "usage": "input", + "git_blob": "93defc5ececebd542332fc42d6a78f0af222cd1c", + "sha256": "1ac2e581ea51e6448503a68caf4bf44aeb32470c2e2674c91f007af4a3abd2e3" + }, + { + "path": "research/rank-convergence/BENCHMARKS.json", + "usage": "input", + "git_blob": "bc58c96abda014c28de91eca3ff10a7d4ec30b32", + "sha256": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850" + }, + { + "path": "research/rank-convergence/PROOF.md", + "usage": "input", + "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e", + "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376" + } + ] +} diff --git a/research/rank-convergence-gates/TASK.json b/research/rank-convergence-gates/TASK.json new file mode 100644 index 0000000000..abd20d9ecd --- /dev/null +++ b/research/rank-convergence-gates/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "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": "refined", + "actual_scope": "Independent certified check of #4483's finite gates and arbitrary-height flow identities.", + "scope_change_reason": "Compiler follow-up named in the maintainers' #4470 review plan.", + "bottleneck_link": "Independent coverage of the compiler that removes tensor padding from the kappa 0.00302015 construction.", + "budget_minutes": 60, + "stop_rule": "Stop at the finite gates and flow identities.", + "outcome": "completed", + "evidence": "All four witnesses pass; p16 D >= 0.04854643 vs required 0.04306220, final margin >= 0.60862507; p7 margin 3.77e-5 certified; tau covers certified; rejection control rejects; arbitrary-height identities hold at 13 (N,G) pairs.", + "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": "Can p7's 3.8e-5 final margin be widened?", + "why_it_matters": "More robust p7 witness.", + "first_step": "Scan ell0 and c with this checker at fixed consumer saving.", + "blocked_by": "None." + } + ] +} diff --git a/research/rank-convergence-gates/VERIFY.json b/research/rank-convergence-gates/VERIFY.json new file mode 100644 index 0000000000..13a1084e53 --- /dev/null +++ b/research/rank-convergence-gates/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/compact-joint-compiler/arithmetic/RESULT.json", + "research/higher-moment-strictification/RESULT.json", + "research/native-lattice-retiming/RESULT.json", + "research/rank-convergence/BENCHMARKS.json", + "research/rank-convergence/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Certified recomputation of #4483's guards (18), mirror guard (4) over t-slices, recurrence inequality (20) and final funding (17) for all four witnesses; p7 rejection control; arbitrary-height flow identities (rank-one identity, exits < n, mirror identity) on raw p7 for G = 0..G0+2." + } + ] +} diff --git a/research/rank-convergence-gates/verify.py b/research/rank-convergence-gates/verify.py new file mode 100644 index 0000000000..b7a99a4d6d --- /dev/null +++ b/research/rank-convergence-gates/verify.py @@ -0,0 +1,371 @@ +#!/usr/bin/env python3 +"""Independent certified check of #4483's finite gates (adaptive height, shifted-log majorant) for all four witnesses. + +For each witness in research/rank-convergence/BENCHMARKS.json, with the raw profile read from its pinned source, this +recomputes with its own certified interval logarithms/exponentials (helpers of research/p17-b480-check) the guards +(18) of PROOF.md on [t0, t_hi]: + T_t0 > P_t0; d <= mu_T(t0) - mu_P(t_hi) (tilted log means); Q >= T_thi / P_t0; + U >= M^-s (T_(thi+s)/T_thi)^a (P_(thi+s)/P_thi)^b; V >= M^lambda (T_(thi-lambda)/P_t0)^g; + T_(t0+s)/T_t0 >= P_(thi+s)/P_thi; eta_min <= t0 m^(t0-1); c >= p/(1-t0); tau(n0) = t0 + p/(c + ln n0) <= t_hi; +the mirror guard (4) on every elementary window and each of the witness's t-slices [ta, tb] in the sufficient form +E_J(tb) <= beta S_J(ta); the single recurrence inequality (20) (U^ell0, V^ell0 exact rational powers); and the final +funding (17) at N = 2^H with z = 1 - uniform saving and A0 = n0^(1-t0) / (c + ln n0)^p. +It also checks, on raw p7, the arbitrary-height flow of PROOF.md section 1 (heights 0 .. G0+2, including empty root +classes): the exact rank-one identity sum S s - sum X e = 608 col, exits below n, and the exact mirror identity of +#4459 at every such height. It does not re-prove PROOF.md's theorem, the native supplier or the outer consumer. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +GRID = Q(1, 10**50) + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def down(x): + return (x / GRID).__floor__() * GRID + + +def up(x): + return (x / GRID).__ceil__() * GRID + + +def ln_bounds(n): + """certified ln n for integer n >= 1 (reduction to [1, 2) and the atanh series)""" + if n == 1: + return Q(0), Q(0) + k = n.bit_length() - 1 + y = Q(n, 2 ** k) + out = [Q(0), Q(0)] + for part, scale in ((y, 1), (Q(2), k)): + if part == 1 or scale == 0: + continue + u = (part - 1) / (part + 1) + s, term, j = Q(0), u, 0 + while True: + s += term / (2 * j + 1) + j += 1 + term *= u * u + tail = term / (2 * j + 1) / (1 - u * u) + if tail < GRID: + break + out[0] += scale * down(2 * s) + out[1] += scale * up(2 * (s + tail)) + return out[0], out[1] + + +def exp_bounds(x_lo, x_hi): + """certified exp on a small interval (|x| < 1)""" + def series(x): + s, term = Q(0), Q(1) + for i in range(70): + s += term + term = term * x / (i + 1) + return s, abs(term) * 2 + a, ea = series(x_lo) + b, eb = series(x_hi) + return down(a - ea), up(b + eb) + + +LN = {} + + +def ln(n): + if n not in LN: + LN[n] = ln_bounds(n) + return LN[n] + + +def moment(hist, C): + """bounds of sum count * k^(1-C)""" + lo = hi = Q(0) + for k, w in hist.items(): + e = exp_bounds(-C * ln(k)[1], -C * ln(k)[0]) + lo, hi = lo + w * k * e[0], hi + w * k * e[1] + return lo, hi + + +def lnq(x): + a, b = ln(x.numerator), ln(x.denominator) + return a[0] - b[1], a[1] - b[0] + + +def powq(base, e): + """certified base^e for integer base >= 1 and rational exponent e (|e ln base| < 1.2)""" + l = ln(base) + lo, hi = (e * l[0], e * l[1]) if e >= 0 else (e * l[1], e * l[0]) + return exp_bounds(lo, hi) + + + + +def rat(x): + return Q(x) + + +def ln_real(lo, hi): + """certified ln on a positive rational interval [lo, hi]""" + return lnq(Q(lo))[0], lnq(Q(hi))[1] + + +def expi(lo, hi): + """certified exp on an interval, reducing large |x| by halving and squaring""" + k = 0 + while max(abs(lo), abs(hi)) > Q(1, 2): + lo, hi, k = lo / 2, hi / 2, k + 1 + a, b = exp_bounds(lo, hi) + for _ in range(k): + a, b = down(a * a), up(b * b) + return a, b + + +def mgf(h, t): + """certified sum_k w k^t""" + lo = hi = Q(0) + for k, w in h.items(): + l = ln(k) + a, b = expi(t * l[0], t * l[1]) + lo, hi = lo + w * a, hi + w * b + return lo, hi + + +def logmean(h, t): + nlo = nhi = Q(0) + for k, w in h.items(): + l = ln(k) + a, b = expi(t * l[0], t * l[1]) + nlo, nhi = nlo + w * a * l[0], nhi + w * b * l[1] + dlo, dhi = mgf(h, t) + return nlo / dhi, nhi / dlo + + +def profile(case): + d = json.loads((ROOT / case["source"]).read_text(encoding="utf-8")) + if case["profile_key"]: + d = d[case["profile_key"]] + return {int(k): v for k, v in d["targets"].items()}, {int(k): v for k, v in d["paid"].items()} + + +def check(case): + T, P = profile(case) + w, g = case["witness"], case["witness"]["guards"] + t0, th, p, c, s, lam = (rat(w[x]) for x in ("t0", "t_upper", "p", "c", "s", "lambda")) + a, b, M, ell0, slices = w["a"], w["b"], w["height_base"], w["ell0"], w["mirror_slices"] + U, V, Qg, d, beta, eta = (rat(g[x]) for x in ("U", "V", "Q", "d", "beta", "eta")) + gg, m = a + b, max(T) + need(min(T) >= 2 and max(P) < m and 1 in P, "profile premises") + need(mgf(T, t0)[0] > mgf(P, t0)[1], "T_t0 > P_t0") + need(logmean(T, t0)[0] - logmean(P, th)[1] >= d, "derivative guard d") + need(mgf(T, th)[1] / mgf(P, t0)[0] <= Qg, "Q guard") + lnM = ln(M) + Ms = expi(-s * lnM[1], -s * lnM[0])[1] + rT, rP = mgf(T, th + s)[1] / mgf(T, th)[0], mgf(P, th + s)[1] / mgf(P, th)[0] + need(Ms * rT ** a * rP ** b <= U, "U guard") + Ml = expi(lam * lnM[0], lam * lnM[1])[1] + need(Ml * (mgf(T, th - lam)[1] / mgf(P, t0)[0]) ** gg <= V, "V guard") + need(mgf(T, t0 + s)[0] / mgf(T, t0)[1] >= mgf(P, th + s)[1] / mgf(P, th)[0], "ratio ordering") + lm = ln(m) + need(t0 * expi((t0 - 1) * lm[1], (t0 - 1) * lm[0])[0] >= eta, "eta_min <= t0 m^(t0-1)") + need(c >= p / (1 - t0), "c >= p/(1-t0)") + ln_n0 = (lm[0] + ell0 * lnM[0], lm[1] + ell0 * lnM[1]) + tau_hi = t0 + p / (c + ln_n0[0]) + need(tau_hi <= th, "tau(n0) <= t_hi") + # mirror windows over t-slices + pts = sorted({Q(1, x) for x in list(T) + list(P)}) + worst = Q(0) + for i in range(slices): + ta, tb = t0 + (th - t0) * i / slices, t0 + (th - t0) * (i + 1) / slices + pw = {} + for r in P: + for k in T: + l = ln(r * k) + pw[r, k] = (expi(ta * l[0], ta * l[1])[0], expi(tb * l[0], tb * l[1])[1]) + for lo, hi in zip(pts, pts[1:]): + mid = (lo + hi) / 2 + E = sum(P[r] * T[k] * pw[r, k][1] for r in P for k in T if r > k and Q(1, r) < mid <= Q(1, k)) + S = sum(P[r] * T[k] * pw[r, k][0] for r in P for k in T if k > r and Q(1, k) < mid <= Q(1, r)) + if E: + need(S > 0 and E <= beta * S, f"mirror window slice {i}") + worst = max(worst, E / S) + # recurrence inequality (20) + l2 = ln(2) + den_hi = c + lm[1] + (ell0 + 1) * lnM[1] + l2[1] + x_lo = d * p * (a * ell0 + 1) / den_hi + e_lo = expi(x_lo, x_lo)[0] + D_lo = (1 - U ** ell0) * (e_lo - 1) - Qg * Ml * V ** ell0 + req = (1 - eta) / (eta - beta) + need(D_lo >= req, "recurrence inequality (20)") + # final funding (17) + z = 1 - rat(w["uniform_saving"]) + H = w["H"] + lnN = (H * l2[0], H * l2[1]) + lnc0 = ln_real(down(c + ln_n0[0]), up(c + ln_n0[1])) + lnA0_hi = (1 - t0) * ln_n0[1] - p * lnc0[0] + lncN = ln_real(down(c + lnN[0]), up(c + lnN[1])) + margin_lo = (z - t0) * lnN[0] - (lnA0_hi + p * lncN[1]) + need(margin_lo > 0, "final funding (17)") + return {"D_lower": f"{float(D_lo):.8f}", "required": f"{float(req):.8f}", "mirror_worst": f"{float(worst):.5f}", + "tau_n0_upper": f"{float(tau_hi):.10f}", "t_hi": str(w["t_upper"]), "final_margin_lower": f"{float(margin_lo):.8f}"} + + +# ---- arbitrary-height flow (PROOF.md section 1; open question 1 of #4483) ---- +from math import factorial +def multis(n_types, size): + if n_types == 0: + if size == 0: yield () + return + for x in range(size + 1): + for rest in multis(n_types - 1, size - x): yield (x,) + rest +def flow(N, W, P, Gover=None): + ks = sorted(W); m = ks[-1]; kmin = ks[0] + 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 + G = 0 + while kmin ** (G + 1) <= N // m: G += 1 + if Gover is not None: G = Gover + 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) + S, X, BX = {}, {}, {} + col = units = matched = 0 + add = lambda D, k, v: D.__setitem__(k, D.get(k, 0) + v) + present = lambda rho, a: m * rho * c(a) <= N + 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 + units += cnt * u(b); col += cnt * u(b) * rho * c(b) + for r, pr in P.items(): + issued = cnt * pr * u(b); rank = r * rho * c(b) + if d == G: + add(X, rank, issued); 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)))) + matched += cnt * pr * D + if issued - cnt * pr * D: + add(X, rank, issued - cnt * pr * D); add(BX, rank, issued - cnt * pr * D) + for a in multis(len(ks), G): + if present(1, a): + for k in ks: add(S, k * c(a), W[k] * u(a)) + 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)): + add(S, rho * r * c(tuple(b)), cnt * pr * u(a) * W[k]) + return dict(G=G, S=S, X=X, BX=BX, col=col, units=units, matched=matched) + + +def mirror_identity(N, W, P, m, r): + """exact: BX and S equal the mirrored windows of the base measure mu(z), z = rho c(a)""" + ks = sorted(W) + G = r["G"] + F = [{1: 1}] + for d in range(1, G + 1): + nxt = {} + for rho, cnt in F[d - 1].items(): + for rr, pr in P.items(): + if m * rho * rr <= N: + nxt[rho * rr] = nxt.get(rho * rr, 0) + cnt * pr + F.append(nxt) + mu = {} + for d in range(G): + for rho, cnt in F[d].items(): + for a in multis(len(ks), G - d - 1): + c, u = 1, factorial(sum(a)) + for k, x in zip(ks, a): + c *= k ** x + u = u // factorial(x) * W[k] ** x + mu[rho * c] = mu.get(rho * c, 0) + cnt * u + bx, src = {}, {} + for z, w in mu.items(): + for rr in P: + for k in W: + if rr > k and N < m * z * rr and m * z * k <= N: + bx[rr * k * z] = bx.get(rr * k * z, 0) + P[rr] * W[k] * w + if k > rr and N < m * z * k and m * z * rr <= N: + src[rr * k * z] = src.get(rr * k * z, 0) + P[rr] * W[k] * w + for a in multis(len(ks), G): + c, u = 1, factorial(G) + for k, x in zip(ks, a): + c *= k ** x + u = u // factorial(x) * W[k] ** x + if m * c <= N: + for k in ks: + src[k * c] = src.get(k * c, 0) + W[k] * u + need(bx == {e: v for e, v in r["BX"].items() if v}, f"N={N}: boundary exits are the mirrored windows") + need(src == r["S"], f"N={N}: sources are the mirrored windows plus the top layer") + + + + +def arbitrary_height(): + W = {5: 420, 6: 270, 7: 840, 8: 1395, 9: 3195, 25: 448, 41: 448, 57: 448, 121: 224} + P = {1: 37305, 2: 10695, 3: 3360, 4: 1530, 5: 300, 8: 1464, 16: 448, 32: 448, 48: 448} + surplus = sum(k * x for k, x in W.items()) - sum(r * x for r, x in P.items()) + need(surplus == 608, "raw p7 rank-one surplus") + pairs = 0 + for N in (500, 3000, 20000): + G0 = 0 + while 5 ** (G0 + 1) <= N // 121: + G0 += 1 + for G in range(0, G0 + 3): + r = flow(N, W, P, G) + r["G"] = G + need(sum(s * x for s, x in r["S"].items()) - sum(e * x for e, x in r["X"].items()) == surplus * r["col"], + f"N={N}, G={G}: rank-one identity") + need(max(r["X"]) < N, f"N={N}, G={G}: exits below N") + mirror_identity(N, W, P, 121, r) + pairs += 1 + return pairs + + +def main(): + for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]: + need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"]) + cases = json.loads((ROOT / "research/rank-convergence/BENCHMARKS.json").read_text(encoding="utf-8"))["cases"] + need([c["name"] for c in cases] == ["p7", "native4453", "native4453-matched-uniform", "p16"], "four witnesses") + out = {c["name"]: check(c) for c in cases} + # rejection control from PROOF.md section 6: t_hi = .9974808 fails to cover tau(n0) for p7 + bad = json.loads(json.dumps(cases[0])) + bad["witness"]["t_upper"] = ".9974808" + try: + check(bad) + need(False, "the smaller p7 endpoint must be rejected") + except AssertionError as exc: + need("tau" in str(exc) or "mirror" in str(exc) or "guard" in str(exc), "smaller p7 endpoint rejected") + pairs = arbitrary_height() + print(json.dumps({"status": "PASS_RANK_CONVERGENCE_GATES", "witnesses": out, "arbitrary_height_pairs": pairs, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())