From bce939b6eeb7d65b8161ca0a4204267e4e1e88a0 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 05:24:16 +0700 Subject: [PATCH 1/7] =?UTF-8?q?Independently=20check=20#4447=20and=20#4453?= =?UTF-8?q?=20(kappa=20~0.0030012):=20the=20B/480=20invoice=20is=20#4441?= =?UTF-8?q?=20+=2019=20swaps;=20strictification,=20root=20and=20compiler?= =?UTF-8?q?=20ranks=20hold=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/p17-b480-check/README.md | 77 ++++++++++ research/p17-b480-check/SOURCES.json | 18 +++ research/p17-b480-check/TASK.json | 100 ++++++++++++ research/p17-b480-check/VERIFY.json | 18 +++ research/p17-b480-check/verify.py | 217 +++++++++++++++++++++++++++ 5 files changed, 430 insertions(+) create mode 100644 research/p17-b480-check/README.md create mode 100644 research/p17-b480-check/SOURCES.json create mode 100644 research/p17-b480-check/TASK.json create mode 100644 research/p17-b480-check/VERIFY.json create mode 100644 research/p17-b480-check/verify.py diff --git a/research/p17-b480-check/README.md b/research/p17-b480-check/README.md new file mode 100644 index 000000000..0015fa27a --- /dev/null +++ b/research/p17-b480-check/README.md @@ -0,0 +1,77 @@ +# Independent arithmetic check of the p17 B/480 patch (#4447, #4453) + +**Claim type:** an independent certified arithmetic check. **No new κ, and neither PR is +accepted.** The native contact replay is not re-run. Two PRs report the same patch, made at phase B +scalar contact 480 on #4441's p17 invoice: + +- 1337isnot1337's [#4447](https://github.com/CrocSwap/integer-mult-bounds/pull/4447), at κ = 0.00300123 + (head `322e0ec7`); +- zxv's [#4453](https://github.com/CrocSwap/integer-mult-bounds/pull/4453), at κ = 0.00300120 + (head `de6869e2`). + +The patch replaces frame 732 by a three-dimensional span, which changes the four incident paid ranks +from `[2,2,1,3]` to `[1,1,2,4]`. Since `(1,4)` majorizes `(2,3)` and `x^τ` is strictly concave, +`1 + 4^τ < 2^τ + 3^τ` holds for every `0 < τ < 1`, by Karamata. + +## Results + +**The invoice.** The shared p17 invoice equals #4441's invoice plus exactly 19 per-call swaps: +paid ranks 1 and 4 rise by 19 each, ranks 2 and 3 fall by 19 each, and the targets are unchanged. +That gives 11,560 productive fields, 69,273 paid calls and rank surplus `260,798 − 259,998 = 800`. + +**The raw root.** It lies in `(0.0030012390168, 0.0030012390174)`, certified. + +**Strictification.** Each PR uses main's higher-moment theorem: `α = P_t/T_t`, +`γ_u = P_{t+u}/(c^u T_t)`, `δ = B·b/(c^C T_t)`, and the bound `α^v + 2γ_u^v + 2δ^v`. The split +bound `2RJ^{−C} ≤ 2R^{t+u}J^{−u}` for `R > J` was checked by hand: it needs `u ≥ C`. + +| | #4447 | #4453 | +| --- | --- | --- | +| `(C, v, c, b, u)` | (0.003001235, 1024, 20, 21, 1/5) | (0.00300122, 675, 18, 22, 3/25) | +| `α` upper (stated limit) | 0.999999995876755 (`1 − 10⁻⁹`) | 0.999999980480395 (`0.999999981`) | +| `γ_u` upper (stated limit) | 0.969136675521 (`97/100`) | 0.981971727000 (`491/500`) | +| `δ` upper (stated limit) | 0.932537504514 (`19/20`) | 0.977253011856 (`391/400`) | +| tensor bound | 0.9999989760 | 0.9999970702 | +| compiler `θ̄`, power `p` | 63/64, 1000 | 15/16, 160 | +| stated `H` / **least certified `H`** | 64,215,200,000,000 / **64,215,171,181,937** | 2,299,850,000,000 / **2,299,613,602,047** | + +All three ratios agree with the PRs' printed intervals to every printed digit. + +**The compiler conditions.** These hold at ambient `153^v`, with `r_max = c^v` and `k_min = b^v`: + +- `c^b < b^a` gives `θ < θ̄ = a/b`; +- `2^{b−a}r_max^b ≤ m^a`; +- `θ̄^p < η = t·m^{t−1}`, which is tight for #4453: `(15/16)^160 ≈ 3.27·10⁻⁵` against `η ≈ 3.74·10⁻⁵`; +- `m^{1−t} < 2^p`; +- `z − t = d = (C − κ)/7`. + +## Not covered + +- The native replay of the new contact, its transports and phases. +- #4441's predecessor native work, which mihir-s-05's #4448 audits separately. +- The outer ledgers. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/p17-b480-check --check-only +python3.12 -B scripts/research_package.py --package research/p17-b480-check +``` + +The verifier prints `PASS_PR4447_PR4453_ARITHMETIC` in about 3 seconds, using only the standard +library. + +## Open next questions + +1. **Does a second missing span exist at another contact?** + - *Why it matters:* the same concavity gain would apply. + - *First step:* rerun #4453's line/hyperplane min-cut discovery with the B/480 contact fixed. + +## Credit + +- The patch and constructions are 1337isnot1337's (#4447, #4440, #4441) and zxv's (#4453, #4359). +- The higher-moment theorem and the polylog majorant are on main (`higher-moment-strictification`). +- Theorem 1G is Jacob Alan Sussman's. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/p17-b480-check/SOURCES.json b/research/p17-b480-check/SOURCES.json new file mode 100644 index 000000000..9124bb10f --- /dev/null +++ b/research/p17-b480-check/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "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" + } + ] +} diff --git a/research/p17-b480-check/TASK.json b/research/p17-b480-check/TASK.json new file mode 100644 index 000000000..7748739d4 --- /dev/null +++ b/research/p17-b480-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "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": "Independently check the arithmetic of #4447 and #4453's shared p17 B/480 patch: invoice accounting, raw root, higher-moment strictification and polylog compiler ranks.", + "scope_change_reason": "The card asks for independent coverage of new paid-profile claims; these two kappa ~0.0030012 PRs had none.", + "bottleneck_link": "The proposed kappa 0.0030012 rests on this invoice, its strictification and compiler rank before native premises.", + "budget_minutes": 30, + "stop_rule": "Stop at the arithmetic; do not replay native contacts.", + "outcome": "completed", + "evidence": "verify.py: invoice is #4441 + 19 swaps; root (0.0030012390168, 0.0030012390174); alpha/gamma_u/delta match both PRs' intervals; tensor bounds 0.999998976 / 0.999997070; least H 64,215,171,181,937 / 2,299,613,602,047 below the stated ranks.", + "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": "Does a second missing span exist at another contact?", + "why_it_matters": "The same concavity gain would apply.", + "first_step": "Rerun #4453's min-cut discovery with the B/480 contact fixed.", + "blocked_by": "None." + } + ] +} diff --git a/research/p17-b480-check/VERIFY.json b/research/p17-b480-check/VERIFY.json new file mode 100644 index 000000000..04a2e54e7 --- /dev/null +++ b/research/p17-b480-check/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Invoice = #4441 + 19 swaps; rank surplus 800; certified raw root bracket; per PR: alpha, gamma_u, delta below stated limits, tensor bound < 1, polylog compiler conditions, stated and least certified H." + } + ] +} diff --git a/research/p17-b480-check/verify.py b/research/p17-b480-check/verify.py new file mode 100644 index 000000000..6c085c72b --- /dev/null +++ b/research/p17-b480-check/verify.py @@ -0,0 +1,217 @@ +#!/usr/bin/env python3 +"""Independent arithmetic check of #4447 (kappa 0.00300123) and #4453 (kappa 0.00300120). + +Both report the same B/480 contact patch on #4441's p17 invoice. This verifier checks, with its own certified +interval logarithms: the invoice is #4441's plus exactly 19 per-call swaps [2,2,1,3] -> [1,1,2,4]; the raw root +bracket; for each PR the higher-moment strictification (main's research/higher-moment-strictification theorem: +alpha = P_t/T_t, gamma_u = P_(t+u)/(c^u T_t), delta = B b/(c^C T_t), bound alpha^v + 2 gamma_u^v + 2 delta^v < 1) +at the PR's own (C, v, c, b, u) and stated rational limits; the polylog compiler conditions (theta, the shifted +exit condition, theta_bar^p < eta, m^(1-t) < 2^p) at ambient 153^v; and the least H with (1+H)^p < 2^((z-t)H). +Invoices and parameters are as printed in the PRs; nothing is imported from them. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import json +import sys + +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 pow_upper(x, v): + """certified upper bound of x^v for 0 < x < 1 rational: exp(v ln x) with ln x <= -(1-x) - (1-x)^2/2""" + y = 1 - x + lnx_hi = -(y + y * y / 2) + return lnx_hi * v + + + +T = {153: 224, 17: 448, 25: 448, 33: 448, 4: 494, 41: 448, 49: 448, 5: 38, 57: 448, 65: 448, 7: 551, 73: 448, 8: 798, 9: 5871} +P = {1: 44618, 16: 448, 2: 9766, 24: 448, 3: 8436, 32: 448, 4: 1957, 40: 448, 48: 448, 5: 760, 56: 448, 64: 448, 72: 448, 8: 152} +P4441 = {1: 44599, 16: 448, 2: 9785, 24: 448, 3: 8455, 32: 448, 4: 1938, 40: 448, 48: 448, 5: 760, 56: 448, 64: 448, 72: 448, 8: 152} +CASES = { + "4447": {"kappa": Q("0.00300123"), "C": Q(600247, 200000000), "v": 1024, "c": 20, "b": 21, "u": Q(1, 5), + "limits": (1 - Q(1, 10**9), Q(97, 100), Q(19, 20)), "theta_bar": Q(63, 64), "p": 1000, "H": 64215200000000}, + "4453": {"kappa": Q(7503, 2500000), "C": Q(150061, 50000000), "v": 675, "c": 18, "b": 22, "u": Q(3, 25), + "limits": (Q(999999981, 10**9), Q(491, 500), Q(391, 400)), "theta_bar": Q(15, 16), "p": 160, "H": 2299850000000}, +} + + +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 mom(hist, expo): + lo = hi = Q(0) + for k, w in hist.items(): + e = powq(k, expo - 1) + lo, hi = lo + w * k * e[0], hi + w * k * e[1] + return lo, hi + + +def log2_upper_of_H1(H): + """certified upper bound of log2(1+H)""" + n = H + 1 + l = ln(n) if n < 2**60 else None + return l + + +def ln_int(n): + k = n.bit_length() - 1 + y = Q(n, 2 ** k) + u = (y - 1) / (y + 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 u else Q(0) + if tail < Q(1, 10**40): + break + l2 = ln(2) + return 2 * s + k * l2[0], 2 * (s + tail) + k * l2[1] + + +def main(): + from collections import Counter + d = Counter(P4441) + d.update({1: 19, 4: 19}) + d.subtract({2: 19, 3: 19}) + need(+d == Counter(P), "invoice = #4441 + 19 swaps [2,2,1,3] -> [1,1,2,4]") + need(sum(T.values()) == 11560 and sum(P.values()) == 69273, "fields and calls") + need((sum(k * w for k, w in T.items()), sum(k * w for k, w in P.items())) == (260798, 259998), "rank surplus 800") + need(all((1 + 4 ** x) < 2 ** x + 3 ** x for x in (0.1, 0.5, 0.9)), "concavity spot checks") + # raw root bracket + def alpha(C): + tl, th = mom(T, 1 - C) + pl, ph = mom(P, 1 - C) + return pl / th, ph / tl + lo, hi = Q("0.0030012390168"), Q("0.0030012390174") + need(alpha(lo)[1] < 1 < alpha(hi)[0], "root bracket (0.0030012390168, 0.0030012390174)") + out = {"status": "PASS_PR4447_PR4453_ARITHMETIC", "new_kappa_claimed": False, + "invoice": {"fields": 11560, "paid_calls": 69273, "rank_surplus": 800}, "root_bracket": [str(lo), str(hi)]} + B = sum(T.values()) + for name, cs in CASES.items(): + C, v, c, b, u = cs["C"], cs["v"], cs["c"], cs["b"], cs["u"] + t = 1 - C + need(u >= C and t + u >= 1 and 1 < c < b < 153, f"{name}: theorem hypotheses") + tl, th = mom(T, t) + pl, ph = mom(P, t) + a_hi = ph / tl + g_num = mom(P, t + u)[1] + cu = powq(c, u)[0] + g_hi = g_num / (cu * tl) + cC = powq(c, C)[0] + d_hi = B * b / (cC * tl) + la, lg, ld = cs["limits"] + need(a_hi < la and g_hi < lg and d_hi < ld, f"{name}: alpha, gamma_u, delta below the stated limits") + total = 1 / (1 + v * (1 - la)) + 2 * lg ** v + 2 * ld ** v + need(total < 1, f"{name}: alpha^v + 2 gamma^v + 2 delta^v < 1") + # compiler (polylog majorant): m = 153^v, r_max = c^v, k_min = b^v + tb, p = cs["theta_bar"], cs["p"] + A_, Bd = tb.numerator, tb.denominator + need(c ** Bd < b ** A_, f"{name}: theta = log c / log b < theta_bar") + need((Bd - A_) + Bd * v * ln(c)[1] / ln(2)[0] <= A_ * v * ln(153)[0] / ln(2)[1], f"{name}: 2^(b-a) r^b <= m^a") + # eta = t * 153^(v (t-1)); need theta_bar^p < eta and m^(1-t) < 2^p (logs) + ln_eta_lo = lnq(t)[0] - v * C * ln(153)[1] + need(p * lnq(tb)[1] < ln_eta_lo, f"{name}: theta_bar^p < eta") + need(v * C * ln(153)[1] < p * ln(2)[0], f"{name}: m^(1-t) < 2^p") + dgap = (C - cs["kappa"]) / 7 + z = 1 - (cs["kappa"] + 6 * dgap) + zt = z - t + need(zt == dgap, f"{name}: z - t = d") + H = cs["H"] + def ok(Hx): + l = ln_int(Hx + 1) + return p * l[1] < zt * Hx * ln(2)[0] + need(ok(H), f"{name}: (1+H)^p < 2^((z-t)H) at stated H") + lo_h, hi_h = 1, H + while lo_h < hi_h: + mid = (lo_h + hi_h) // 2 + if ok(mid): + hi_h = mid + else: + lo_h = mid + 1 + out[name] = {"alpha_upper": f"{float(a_hi):.15f}", "gamma_u_upper": f"{float(g_hi):.12f}", + "delta_upper": f"{float(d_hi):.12f}", "stated_limits": [str(x) for x in cs["limits"]], + "tensor_bound": f"{float(total):.10f}", "stated_H": H, "least_certified_H": lo_h} + print(json.dumps(out, indent=1)) + + +if __name__ == "__main__": + sys.exit(main()) From 67b4ef8a858ceb5d5ad37cb0fee7ba00a5da2638 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 05:26:06 +0700 Subject: [PATCH 2/7] Extend the p17 check to predecessors #4441 and #4440 Co-Authored-By: Claude Opus 5.5 --- research/p17-b480-check/README.md | 22 +++++++++++++++++++- research/p17-b480-check/TASK.json | 4 ++-- research/p17-b480-check/VERIFY.json | 2 +- research/p17-b480-check/verify.py | 32 +++++++++++++++++++++++++++-- 4 files changed, 54 insertions(+), 6 deletions(-) diff --git a/research/p17-b480-check/README.md b/research/p17-b480-check/README.md index 0015fa27a..f20ca5a90 100644 --- a/research/p17-b480-check/README.md +++ b/research/p17-b480-check/README.md @@ -1,4 +1,4 @@ -# Independent arithmetic check of the p17 B/480 patch (#4447, #4453) +# Independent arithmetic check of the p17 chain: #4440, #4441, #4447, #4453 **Claim type:** an independent certified arithmetic check. **No new κ, and neither PR is accepted.** The native contact replay is not re-run. Two PRs report the same patch, made at phase B @@ -45,6 +45,26 @@ All three ratios agree with the PRs' printed intervals to every printed digit. - `m^{1−t} < 2^p`; - `z − t = d = (C − κ)/7`. +## Predecessors #4441 and #4440 + +The same engine also checks the predecessors. + +**#4441** (κ = 0.00300105) uses its own invoice and the same tail parameters as #4447. Its ratios +match its printed intervals: `α < 0.999999997758999`, `γ_u < 0.969126930834` and +`δ < 0.932537400875`. Its stated `H` = 165,315,500,000,000 is certified, and the least passing value +is 165,312,667,114,238. + +**#4440** (κ = 0.00296) consists of two query-thinned units, both at `v = 1024` and `u = 1/5`. Only +their strictification ratios are checked here. The compiler is #4440's older power majorant and is +not re-derived. + +| Unit | `α` upper | `γ_u` upper | `δ` upper | tensor bound | +| --- | --- | --- | --- | --- | +| complex (`c = 20`, `b = 21`) | 0.999999952117241 | 0.967466409565 | 0.941649713485 | `< 0.99995098` | +| BIT (`c = 17`, `b = 18`) | 0.999995735238060 | 0.957429821066 | 0.949707924145 | `< 0.99565187` | + +All six ratios match #4440's printed interval endpoints to within `10⁻²⁸`. + ## Not covered - The native replay of the new contact, its transports and phases. diff --git a/research/p17-b480-check/TASK.json b/research/p17-b480-check/TASK.json index 7748739d4..bf8f470a2 100644 --- a/research/p17-b480-check/TASK.json +++ b/research/p17-b480-check/TASK.json @@ -80,13 +80,13 @@ ] }, "scope_status": "refined", - "actual_scope": "Independently check the arithmetic of #4447 and #4453's shared p17 B/480 patch: invoice accounting, raw root, higher-moment strictification and polylog compiler ranks.", + "actual_scope": "Independently check the arithmetic of #4447 and #4453's shared p17 B/480 patch: invoice accounting, raw root, higher-moment strictification and polylog compiler ranks. Also checks predecessors #4441 (strictification and compiler) and #4440 (complex and BIT strictification ratios).", "scope_change_reason": "The card asks for independent coverage of new paid-profile claims; these two kappa ~0.0030012 PRs had none.", "bottleneck_link": "The proposed kappa 0.0030012 rests on this invoice, its strictification and compiler rank before native premises.", "budget_minutes": 30, "stop_rule": "Stop at the arithmetic; do not replay native contacts.", "outcome": "completed", - "evidence": "verify.py: invoice is #4441 + 19 swaps; root (0.0030012390168, 0.0030012390174); alpha/gamma_u/delta match both PRs' intervals; tensor bounds 0.999998976 / 0.999997070; least H 64,215,171,181,937 / 2,299,613,602,047 below the stated ranks.", + "evidence": "verify.py: invoice is #4441 + 19 swaps; root (0.0030012390168, 0.0030012390174); alpha/gamma_u/delta match both PRs' intervals; tensor bounds 0.999998976 / 0.999997070; least H 64,215,171,181,937 / 2,299,613,602,047 below the stated ranks. #4441: ratios match, least H 165,312,667,114,238; #4440 complex/BIT ratios match to 1e-28 with tensor bounds < 1.", "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": [ diff --git a/research/p17-b480-check/VERIFY.json b/research/p17-b480-check/VERIFY.json index 04a2e54e7..f3a2ecbeb 100644 --- a/research/p17-b480-check/VERIFY.json +++ b/research/p17-b480-check/VERIFY.json @@ -12,7 +12,7 @@ "{package}/verify.py" ], "timeout_seconds": 300, - "checks": "Invoice = #4441 + 19 swaps; rank surplus 800; certified raw root bracket; per PR: alpha, gamma_u, delta below stated limits, tensor bound < 1, polylog compiler conditions, stated and least certified H." + "checks": "Invoice = #4441 + 19 swaps; rank surplus 800; certified raw root bracket; per PR: alpha, gamma_u, delta below stated limits, tensor bound < 1, polylog compiler conditions, stated and least certified H. Predecessors: #4441 strictification and compiler on its own invoice; #4440 complex and BIT strictification ratios matched to 1e-28." } ] } diff --git a/research/p17-b480-check/verify.py b/research/p17-b480-check/verify.py index 6c085c72b..0a64abcf7 100644 --- a/research/p17-b480-check/verify.py +++ b/research/p17-b480-check/verify.py @@ -93,12 +93,22 @@ def pow_upper(x, v): +# #4440's query-thinned units (strictification only; its compiler uses the older power majorant) +T4440C = {153: 224, 17: 448, 25: 448, 33: 448, 41: 448, 49: 448, 5: 532, 57: 448, 6: 342, 65: 448, 7: 1064, 73: 448, 8: 1767, 9: 4047} +P4440C = {1: 49045, 16: 448, 2: 13547, 24: 448, 3: 4256, 32: 448, 4: 1938, 40: 448, 48: 448, 5: 380, 56: 448, 64: 448, 72: 448, 8: 152} +T4440B = {127: 222, 15: 444, 22: 444, 29: 444, 36: 444, 43: 444, 50: 444, 57: 444, 64: 222, 8: 7902} +P4440B = {1: 25479, 14: 444, 2: 24156, 21: 444, 28: 444, 3: 1422, 35: 444, 4: 792, 42: 444, 49: 444, 5: 1836, 56: 444, 6: 198, 63: 222, 7: 342} +EXPECT4440 = {"complex": ("0.999999952117240859760145478346", "0.967466409565147920980822933860", "0.941649713484853845388929204841"), + "BIT": ("0.999995735238059506641600561768", "0.957429821066420278606254392111", "0.949707924144871179442776557219")} T = {153: 224, 17: 448, 25: 448, 33: 448, 4: 494, 41: 448, 49: 448, 5: 38, 57: 448, 65: 448, 7: 551, 73: 448, 8: 798, 9: 5871} P = {1: 44618, 16: 448, 2: 9766, 24: 448, 3: 8436, 32: 448, 4: 1957, 40: 448, 48: 448, 5: 760, 56: 448, 64: 448, 72: 448, 8: 152} P4441 = {1: 44599, 16: 448, 2: 9785, 24: 448, 3: 8455, 32: 448, 4: 1938, 40: 448, 48: 448, 5: 760, 56: 448, 64: 448, 72: 448, 8: 152} CASES = { "4447": {"kappa": Q("0.00300123"), "C": Q(600247, 200000000), "v": 1024, "c": 20, "b": 21, "u": Q(1, 5), "limits": (1 - Q(1, 10**9), Q(97, 100), Q(19, 20)), "theta_bar": Q(63, 64), "p": 1000, "H": 64215200000000}, + "4441": {"kappa": Q("0.00300105"), "C": Q(750263, 250000000), "v": 1024, "c": 20, "b": 21, "u": Q(1, 5), + "limits": (1 - Q(1, 10**9), Q(97, 100), Q(19, 20)), "theta_bar": Q(63, 64), "p": 1000, "H": 165315500000000, + "invoice": "P4441"}, "4453": {"kappa": Q(7503, 2500000), "C": Q(150061, 50000000), "v": 675, "c": 18, "b": 22, "u": Q(3, 25), "limits": (Q(999999981, 10**9), Q(491, 500), Q(391, 400)), "theta_bar": Q(15, 16), "p": 160, "H": 2299850000000}, } @@ -168,12 +178,13 @@ def alpha(C): B = sum(T.values()) for name, cs in CASES.items(): C, v, c, b, u = cs["C"], cs["v"], cs["c"], cs["b"], cs["u"] + Pinv = P4441 if cs.get("invoice") == "P4441" else P t = 1 - C need(u >= C and t + u >= 1 and 1 < c < b < 153, f"{name}: theorem hypotheses") tl, th = mom(T, t) - pl, ph = mom(P, t) + pl, ph = mom(Pinv, t) a_hi = ph / tl - g_num = mom(P, t + u)[1] + g_num = mom(Pinv, t + u)[1] cu = powq(c, u)[0] g_hi = g_num / (cu * tl) cC = powq(c, C)[0] @@ -210,6 +221,23 @@ def ok(Hx): out[name] = {"alpha_upper": f"{float(a_hi):.15f}", "gamma_u_upper": f"{float(g_hi):.12f}", "delta_upper": f"{float(d_hi):.12f}", "stated_limits": [str(x) for x in cs["limits"]], "tensor_bound": f"{float(total):.10f}", "stated_H": H, "least_certified_H": lo_h} + # #4440: strictification ratios against the printed upper ends + for name, (Tx, Px, C, c, b) in {"4440-complex": (T4440C, P4440C, Q(29603, 10000000), 20, 21), + "4440-BIT": (T4440B, P4440B, Q(173, 50000), 17, 18)}.items(): + u, v, t = Q(1, 5), 1024, 1 - C + need(sum(k * w for k, w in Tx.items()) > sum(k * w for k, w in Px.items()), f"{name}: rank surplus") + tl, th = mom(Tx, t) + a_hi = mom(Px, t)[1] / tl + g_hi = mom(Px, t + u)[1] / (powq(c, u)[0] * tl) + d_hi = sum(Tx.values()) * b / (powq(c, C)[0] * tl) + ea, eg, ed = (Q(x) for x in EXPECT4440[name.split("-")[1]]) + need(abs(a_hi - ea) < Q(1, 10**28) and abs(g_hi - eg) < Q(1, 10**28) and abs(d_hi - ed) < Q(1, 10**28), + f"{name}: ratios match the printed intervals") + lnb = lambda x: -(1 - x) - (1 - x) ** 2 / 2 + bound = 1 / (1 - v * lnb(a_hi)) + 2 * Q(1, 2 ** int(-v * lnb(g_hi) / ln(2)[1])) + 2 * Q(1, 2 ** int(-v * lnb(d_hi) / ln(2)[1])) + need(bound < 1, f"{name}: tensor bound at v = 1024") + out[name] = {"alpha_upper": f"{float(a_hi):.15f}", "gamma_u_upper": f"{float(g_hi):.12f}", + "delta_upper": f"{float(d_hi):.12f}", "tensor_bound_upper": f"{float(bound):.10f}"} print(json.dumps(out, indent=1)) From e02ca27f9a30b9aeb5e2eb701bf2eb0a27d4e193 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 05:27:59 +0700 Subject: [PATCH 3/7] Add #4446 to the p17 chain check Co-Authored-By: Claude Opus 5.5 --- research/p17-b480-check/README.md | 21 +++++++++++++++- research/p17-b480-check/TASK.json | 2 +- research/p17-b480-check/verify.py | 40 +++++++++++++++++++++++++++++++ 3 files changed, 61 insertions(+), 2 deletions(-) diff --git a/research/p17-b480-check/README.md b/research/p17-b480-check/README.md index f20ca5a90..8de54fead 100644 --- a/research/p17-b480-check/README.md +++ b/research/p17-b480-check/README.md @@ -1,4 +1,4 @@ -# Independent arithmetic check of the p17 chain: #4440, #4441, #4447, #4453 +# Independent arithmetic check of the p17 chain: #4440, #4441, #4446, #4447, #4453 **Claim type:** an independent certified arithmetic check. **No new κ, and neither PR is accepted.** The native contact replay is not re-run. Two PRs report the same patch, made at phase B @@ -65,6 +65,25 @@ not re-derived. All six ratios match #4440's printed interval endpoints to within `10⁻²⁸`. +## #4446 + +**#4446** (κ = 0.003001053) uses #4441's invoice with the rank-one tail of #4416, where +`γ = P₁/(c^C T_t)`. Its parameters are `v = 17160`, cutoff `18^v`, target floor `19^v` and ambient +`281^v`. Its ratios match the 36-digit printed intervals to `10⁻³⁰`: + +- `α < 0.999999999811973`; +- `γ < 0.999071242992`, against the limit 9991/10000; +- `δ < 0.843991137666`, against the limit 6/7. + +The tensor bound is 0.99999876. Its compiler is #4405's refined power majorant. Each conservative +constant it uses dominates the true quantity: + +- the exit constant 88,608 exceeds the actual `log₂(r_max·m^h) = 74,093.9`; +- the bound `−log₂η ≤ 464.483` exceeds the actual value, 418.912; +- `18^55 < 19^54` gives `θ < 54/55`. + +The stated `H0` = 357,651,736,794,440 and `H1` = 15,026,650,096,742,881,962,201 reproduce exactly. + ## Not covered - The native replay of the new contact, its transports and phases. diff --git a/research/p17-b480-check/TASK.json b/research/p17-b480-check/TASK.json index bf8f470a2..93a455fb7 100644 --- a/research/p17-b480-check/TASK.json +++ b/research/p17-b480-check/TASK.json @@ -86,7 +86,7 @@ "budget_minutes": 30, "stop_rule": "Stop at the arithmetic; do not replay native contacts.", "outcome": "completed", - "evidence": "verify.py: invoice is #4441 + 19 swaps; root (0.0030012390168, 0.0030012390174); alpha/gamma_u/delta match both PRs' intervals; tensor bounds 0.999998976 / 0.999997070; least H 64,215,171,181,937 / 2,299,613,602,047 below the stated ranks. #4441: ratios match, least H 165,312,667,114,238; #4440 complex/BIT ratios match to 1e-28 with tensor bounds < 1.", + "evidence": "verify.py: invoice is #4441 + 19 swaps; root (0.0030012390168, 0.0030012390174); alpha/gamma_u/delta match both PRs' intervals; tensor bounds 0.999998976 / 0.999997070; least H 64,215,171,181,937 / 2,299,613,602,047 below the stated ranks. #4441: ratios match, least H 165,312,667,114,238; #4440 complex/BIT ratios match to 1e-28 with tensor bounds < 1. #4446: ratios match to 1e-30, tensor bound 0.99999876, conservative compiler constants dominate the true ones, H0/H1 reproduced.", "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": [ diff --git a/research/p17-b480-check/verify.py b/research/p17-b480-check/verify.py index 0a64abcf7..a75413b29 100644 --- a/research/p17-b480-check/verify.py +++ b/research/p17-b480-check/verify.py @@ -238,6 +238,46 @@ def ok(Hx): need(bound < 1, f"{name}: tensor bound at v = 1024") out[name] = {"alpha_upper": f"{float(a_hi):.15f}", "gamma_u_upper": f"{float(g_hi):.12f}", "delta_upper": f"{float(d_hi):.12f}", "tensor_bound_upper": f"{float(bound):.10f}"} + # #4446: rank-one tail (gamma = P_1/(c^C T)), v = 17160, c = 18, b = 19, ambient 281^v; power-majorant compiler + C, v, c, b, kap = Q(1500527, 500000000), 17160, 18, 19, Q(3001053, 10**9) + t = 1 - C + tl, th = mom(T, t) + a_hi = mom(P4441, t)[1] / tl + P1 = sum(k * w for k, w in P4441.items()) + g_hi = P1 / (powq(c, C)[0] * tl) + d_hi = sum(T.values()) * b / (powq(c, C)[0] * tl) + for got, want in ((a_hi, "0.99999999981197332875426410809243317"), (g_hi, "0.99907124299228386730839393376721824"), + (d_hi, "0.84399113766577138522456189514008498")): + need(abs(got - Q(want)) < Q(1, 10**30), "#4446: ratio matches its printed interval") + la, lg, ld = 1 - Q(1, 10**10), Q(9991, 10000), Q(6, 7) + need(a_hi < la and g_hi < lg and d_hi < ld, "#4446: below stated limits") + need(lg ** 780 < Q(1, 2) and ld ** 5 < Q(1, 2), "#4446: decay blocks") + bound = 1 / (1 + v * (1 - la)) + 2 * Q(1, 2 ** 22) + 2 * Q(1, 2 ** (v // 5)) + need(bound < 1, "#4446: alpha^v + 2 gamma^v + 2 delta^v < 1") + need(18 ** 55 < 19 ** 54, "#4446: theta = log 18 / log 19 < 54/55") + h, d = Q(1, 55), (C - kap) / 7 + z = 1 - (kap + 6 * d) + z0 = (t + z) / 2 + dl = z0 - t + need(dl == Q(1, 14000000000), "#4446: delta gap") + Bexit, negl2eta = Q(88608), Q(32513793811, 70000000) + l2 = ln(2) + true_B = v * (ln(18)[1] + h * ln(281)[1]) / l2[0] + need(true_B < Bexit, "#4446: exit constant dominates log2(r_max m^h) at ambient 281^v") + s_, term = Q(0), 1 - z0 + for j in range(1, 30): + s_ += term / j + term *= (1 - z0) + true_negl2eta = (s_ + term / z0) / l2[0] + (1 - z0) * v * ln(281)[1] / l2[0] + need(true_negl2eta < negl2eta, "#4446: -log2(eta) upper bound dominates") + H0 = -((-(Bexit * dl + negl2eta)) // (h * dl)) + r = H0 * (1 - z0) / (z - z0) + H1 = r.numerator // r.denominator + 1 + need(H0 == 357651736794440 and H1 == 15026650096742881962201, "#4446: H0, H1 reproduced") + out["4446"] = {"alpha_upper": f"{float(a_hi):.15f}", "gamma_upper": f"{float(g_hi):.12f}", + "delta_upper": f"{float(d_hi):.12f}", "tensor_bound": f"{float(bound):.10f}", + "exit_constant": [f"{float(true_B):.1f}", 88608], "neg_log2_eta": [f"{float(true_negl2eta):.3f}", f"{float(negl2eta):.3f}"], + "H0": H0, "H1": H1} print(json.dumps(out, indent=1)) From 089b5972dea86417a3cac5a4d36c15b64009ce5f Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 06:52:24 +0700 Subject: [PATCH 4/7] p17 chain check: reproduce #4440's power-majorant compiler constants exactly Co-Authored-By: Claude Opus 5.5 --- research/p17-b480-check/README.md | 14 ++++++++++++-- research/p17-b480-check/verify.py | 20 ++++++++++++++++++++ 2 files changed, 32 insertions(+), 2 deletions(-) diff --git a/research/p17-b480-check/README.md b/research/p17-b480-check/README.md index 8de54fead..8db11a0da 100644 --- a/research/p17-b480-check/README.md +++ b/research/p17-b480-check/README.md @@ -55,8 +55,7 @@ match its printed intervals: `α < 0.999999997758999`, `γ_u < 0.969126930834` a is 165,312,667,114,238. **#4440** (κ = 0.00296) consists of two query-thinned units, both at `v = 1024` and `u = 1/5`. Only -their strictification ratios are checked here. The compiler is #4440's older power majorant and is -not re-derived. +their strictification ratios and its power-majorant compiler are checked here. | Unit | `α` upper | `γ_u` upper | `δ` upper | tensor bound | | --- | --- | --- | --- | --- | @@ -65,6 +64,17 @@ not re-derived. All six ratios match #4440's printed interval endpoints to within `10⁻²⁸`. +**#4440's compiler** is defined in its PROOF.md §3 with `h = 1/64`, `v = 1024` and `z0 = (t+z)/2`. It +reproduces exactly: + +| Unit | `H0` | `H1` | uniform saving | +| --- | --- | --- | --- | +| complex | 75,415,467,350 | 10,418,370,291,022,217 | `κ + 6d = 103609/35000000`, with `κ = 0.00296` | +| BIT | 3,755,884,544 | 25,986,965,159,937 | 0.003459 | + +The Bernoulli surpluses also match exactly, and so do `c^64 < b^63` and the decay blocks +`(31/32)^128, (19/20)^128 < 1/16`. + ## #4446 **#4446** (κ = 0.003001053) uses #4441's invoice with the rank-one tail of #4416, where diff --git a/research/p17-b480-check/verify.py b/research/p17-b480-check/verify.py index a75413b29..919c92a6b 100644 --- a/research/p17-b480-check/verify.py +++ b/research/p17-b480-check/verify.py @@ -278,6 +278,26 @@ def ok(Hx): "delta_upper": f"{float(d_hi):.12f}", "tensor_bound": f"{float(bound):.10f}", "exit_constant": [f"{float(true_B):.1f}", 88608], "neg_log2_eta": [f"{float(true_negl2eta):.3f}", f"{float(negl2eta):.3f}"], "H0": H0, "H1": H1} + # #4440's power-majorant compiler (PROOF.md section 3): h = 1/64, v = 1024, z0 = (t + z)/2 + def compiler4440(tested, uniform): + hh, vv = Q(1, 64), 1024 + t_, z_ = 1 - tested, 1 - uniform + z0_ = (t_ + z_) / 2 + gap = z0_ - t_ + x = (gap * (5 + 8 * hh) * vv + 1 + 8 * vv * (1 - z0_)) / (hh * gap) + h0 = -((-x.numerator) // x.denominator) + x = h0 * (1 - z0_) / (z_ - z0_) + return h0, x.numerator // x.denominator + 1 + k4440, tc = Q(37, 12500), Q(29603, 10000000) + uc = k4440 + 6 * (tc - k4440) / 7 + need(uc == Q(103609, 35000000), "#4440: complex uniform saving kappa + 6d") + need(compiler4440(tc, uc) == (75415467350, 10418370291022217), "#4440: complex H0, H1") + need(compiler4440(Q(173, 50000), Q(3459, 1000000)) == (3755884544, 25986965159937), "#4440: BIT H0, H1") + for g_, s_ in ((Q(1, 30000000), Q(8589700209, 251666829934592)), (Q(1, 250000), Q(68719461047, 16845935476736))): + need(1 - 1 / (1 + 1024 * g_) - Q(4, 2 ** 32) == s_ > 0, "#4440: Bernoulli surplus") + need(20 ** 64 < 21 ** 63 and 17 ** 64 < 18 ** 63 and Q(31, 32) ** 128 < Q(1, 16) and Q(19, 20) ** 128 < Q(1, 16), + "#4440: exit exponent h = 1/64 and tail decay blocks") + out["4440_compiler"] = {"complex": [75415467350, 10418370291022217], "BIT": [3755884544, 25986965159937]} print(json.dumps(out, indent=1)) From 9c155a693fda59dcc6affa070092ce9d12d5d7e8 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 07:00:44 +0700 Subject: [PATCH 5/7] p17 chain check: #4446's separate p6 BIT supplier (masses, raw root, alpha) Co-Authored-By: Claude Opus 5.5 --- research/p17-b480-check/README.md | 7 +++++++ research/p17-b480-check/verify.py | 12 ++++++++++++ 2 files changed, 19 insertions(+) diff --git a/research/p17-b480-check/README.md b/research/p17-b480-check/README.md index 8db11a0da..5d2678fd9 100644 --- a/research/p17-b480-check/README.md +++ b/research/p17-b480-check/README.md @@ -94,6 +94,13 @@ constant it uses dominates the true quantity: The stated `H0` = 357,651,736,794,440 and `H1` = 15,026,650,096,742,881,962,201 reproduce exactly. + +**#4446's separate p6 BIT supplier**, which supplies the ordinary BIT premise, is also checked: + +- the rank masses are 102,419 (paid) and 102,932 (target), with surplus 513; +- the raw root lies in `(0.00314, 0.00315)`, above the admitted 0.00312; +- `α < 99999/100000` at the tested saving `157/50000` (computed upper bound 0.9999882). + ## Not covered - The native replay of the new contact, its transports and phases. diff --git a/research/p17-b480-check/verify.py b/research/p17-b480-check/verify.py index 919c92a6b..b998493f9 100644 --- a/research/p17-b480-check/verify.py +++ b/research/p17-b480-check/verify.py @@ -297,6 +297,18 @@ def compiler4440(tested, uniform): need(1 - 1 / (1 + 1024 * g_) - Q(4, 2 ** 32) == s_ > 0, "#4440: Bernoulli surplus") need(20 ** 64 < 21 ** 63 and 17 ** 64 < 18 ** 63 and Q(31, 32) ** 128 < Q(1, 16) and Q(19, 20) ** 128 < Q(1, 16), "#4440: exit exponent h = 1/64 and tail decay blocks") + # #4446's separate p6 BIT supplier (ordinary BIT premise): invoice, raw root and alpha at the tested saving + Pb = {1: 17199, 2: 17446, 3: 1027, 4: 572, 5: 1326, 6: 143, 7: 1357, 14: 444, 28: 444, 42: 222} + Tb = {8: 5707, 22: 444, 36: 444, 50: 222, 92: 222} + need(sum(k * w for k, w in Pb.items()) == 102419 and sum(k * w for k, w in Tb.items()) == 102932, "#4446 BIT: rank masses") + tl, _ = moment(Tb, Q(157, 50000)) + _, ph = moment(Pb, Q(157, 50000)) + need(ph / tl < Q(99999, 100000), "#4446 BIT: alpha < 99999/100000 at the tested saving 157/50000") + lo_t, _ = moment(Tb, Q(314, 100000)); _, hi_p = moment(Pb, Q(314, 100000)) + _, hi_t = moment(Tb, Q(315, 100000)); lo_p, _ = moment(Pb, Q(315, 100000)) + need(lo_t > hi_p and hi_t < lo_p, "#4446 BIT: raw root in (0.00314, 0.00315), above the admitted 0.00312") + out["4446_BIT_supplier"] = {"rank_masses": [102419, 102932], "surplus": 513, "alpha_upper": f"{float(ph / tl):.9f}", + "raw_root_bracket": ["0.00314", "0.00315"]} out["4440_compiler"] = {"complex": [75415467350, 10418370291022217], "BIT": [3755884544, 25986965159937]} print(json.dumps(out, indent=1)) From 02b7e88fc6283f55c0dde80697eb3066dcefc3b1 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 07:01:53 +0700 Subject: [PATCH 6/7] p17 chain check: #4446 BIT supplier gamma, finite moment, compiler and cover Co-Authored-By: Claude Opus 5.5 --- research/p17-b480-check/README.md | 7 ++++++- research/p17-b480-check/verify.py | 16 ++++++++++++++++ 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/research/p17-b480-check/README.md b/research/p17-b480-check/README.md index 5d2678fd9..13e333b36 100644 --- a/research/p17-b480-check/README.md +++ b/research/p17-b480-check/README.md @@ -99,7 +99,12 @@ The stated `H0` = 357,651,736,794,440 and `H1` = 15,026,650,096,742,881,962,201 - the rank masses are 102,419 (paid) and 102,932 (target), with surplus 513; - the raw root lies in `(0.00314, 0.00315)`, above the admitted 0.00312; -- `α < 99999/100000` at the tested saving `157/50000` (computed upper bound 0.9999882). +- `α < 99999/100000` at the tested saving `157/50000` (computed upper bound 0.9999882); +- the rank-one tail `γ = P_1/(7^C T_t) < 999/1000` (upper bound 0.998596); +- the finite paid moment `1/(1 + 6000/100000) + 2·2^{−6} = 1653/1696`; +- the separation `7^{16} < 8^{15}`; +- the compiler, `H0 = 850,090,000` and `H1 = 1,066,862,950,001`; +- the delayed-cover gap `1/200000`. ## Not covered diff --git a/research/p17-b480-check/verify.py b/research/p17-b480-check/verify.py index b998493f9..ab1694681 100644 --- a/research/p17-b480-check/verify.py +++ b/research/p17-b480-check/verify.py @@ -309,6 +309,22 @@ def compiler4440(tested, uniform): need(lo_t > hi_p and hi_t < lo_p, "#4446 BIT: raw root in (0.00314, 0.00315), above the admitted 0.00312") out["4446_BIT_supplier"] = {"rank_masses": [102419, 102932], "surplus": 513, "alpha_upper": f"{float(ph / tl):.9f}", "raw_root_bracket": ["0.00314", "0.00315"]} + # gamma (rank-one tail at cutoff 7), the finite paid moment at power 6000, the compiler and the delayed cover + Cb, Ub, Cov, POW = Q(157, 50000), Q(627, 200000), Q(313, 100000), 6000 + e7 = exp_bounds(-Cb * ln(7)[1], -Cb * ln(7)[0]) # 7^(-C) bounds + gamma_hi = Q(102419) * e7[1] / tl # P1 / (7^C T_t), upper bound via 7^(-C) upper and T_t lower + need(gamma_hi < Q(999, 1000) and Q(999, 1000) ** 1000 < Q(1, 2), "#4446 BIT: gamma < 999/1000 and decay block") + need(Q(1, 1) / (1 + Q(POW, 100000)) + 2 * Q(1, 2) ** (POW // 1000) == Q(1653, 1696), "#4446 BIT: finite paid moment 1653/1696") + need(7 ** 16 < 8 ** 15 and 92 < 2 ** 7, "#4446 BIT: separation and ambient") + tb, zb = 1 - Cb, 1 - Ub + z0b = (tb + zb) / 2 + db, hb = z0b - tb, Q(1, 16) + x = ((3 + 7 * hb) * POW * db + 1 + 7 * POW * (1 - z0b)) / (hb * db) + H0b = -((-x.numerator) // x.denominator) + x = H0b * (1 - z0b) / (zb - z0b) + need((H0b, x.numerator // x.denominator + 1) == (850090000, 1066862950001), "#4446 BIT: compiler H0, H1") + need(Ub - Cov == Q(1, 200000) and (1 + (Ub - Cov) / 4) / (1 + (Ub - Cov) / 2) < 1, "#4446 BIT: delayed cover gap") + out["4446_BIT_supplier"].update({"gamma_upper": f"{float(gamma_hi):.6f}", "H0_H1": [850090000, 1066862950001]}) out["4440_compiler"] = {"complex": [75415467350, 10418370291022217], "BIT": [3755884544, 25986965159937]} print(json.dumps(out, indent=1)) From f848f014d4ca9dfc3beef0d4b615b572a7301605 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 07:08:47 +0700 Subject: [PATCH 7/7] p17 chain check: all five outer ledgers reproduce from printed parameters Co-Authored-By: Claude Opus 5.5 --- research/p17-b480-check/README.md | 27 +++++++++++++++++++++++++++ research/p17-b480-check/verify.py | 15 +++++++++++++++ 2 files changed, 42 insertions(+) diff --git a/research/p17-b480-check/README.md b/research/p17-b480-check/README.md index 13e333b36..ecf85bd2b 100644 --- a/research/p17-b480-check/README.md +++ b/research/p17-b480-check/README.md @@ -75,6 +75,33 @@ reproduces exactly: The Bernoulli surpluses also match exactly, and so do `c^64 < b^63` and the decay blocks `(31/32)^128, (19/20)^128 < 1/16`. +## Outer ledgers of all five κ PRs + +For #4440, #4441, #4446, #4447 and #4453, all nine outer rows reproduce **exactly** from each PR's printed +parameters. The FINE-PRIME row formulas are used: + +| Row | Formula | +| --- | --- | +| main transform | `εq` | +| global router | `a` | +| fused Gaussian | `1−ε+qβ` | +| group bit router | `1−ε+aβ` | +| group scans | `1−ε+β` | +| polynomial products | `ε` | +| sparse union movement | `ξ+1/2−ε` | +| micro-box faces | `79−ε−β` | +| boundary algebraic matrix | `3/32+ξ−ε` | + +In every case the binding row is the main transform. Its margin above κ is: + +| PR | Margin above κ | +| --- | --- | +| #4440 | `1.3·10⁻⁷` | +| #4441 | `8.6·10⁻¹⁰` | +| #4446 | `4.3·10⁻¹⁰` | +| #4447 | `2.1·10⁻⁹` | +| #4453 | `8.6·10⁻⁹` | + ## #4446 **#4446** (κ = 0.003001053) uses #4441's invoice with the rank-one tail of #4416, where diff --git a/research/p17-b480-check/verify.py b/research/p17-b480-check/verify.py index ab1694681..e115efbe3 100644 --- a/research/p17-b480-check/verify.py +++ b/research/p17-b480-check/verify.py @@ -325,6 +325,21 @@ def compiler4440(tested, uniform): need((H0b, x.numerator // x.denominator + 1) == (850090000, 1066862950001), "#4446 BIT: compiler H0, H1") need(Ub - Cov == Q(1, 200000) and (1 + (Ub - Cov) / 4) / (1 + (Ub - Cov) / 2) < 1, "#4446 BIT: delayed cover gap") out["4446_BIT_supplier"].update({"gamma_upper": f"{float(gamma_hi):.6f}", "H0_H1": [850090000, 1066862950001]}) + # outer ledgers of all five kappa PRs: printed parameters and margins against the FINE-PRIME row formulas + OUTER = {"4441": {"parameters": {"epsilon": "3499999999/3500000000", "q": "5251839/1750000000", "a": "10503679/3500000000", "beta": "3499999997/3500000000", "cap_xi": "5569162686494748161/6125000000000000000", "kappa": "60021/20000000"}, "margins": {"boundary_algebraic_matrix": "18381438244748161/6125000000000000000", "fused_gaussian": "18381438234244483/6125000000000000000", "global_coordinate_router": "10503679/3500000000", "group_bit_router": "36762879968488963/12250000000000000000", "group_scans": "1749999999/1750000000", "main_transform": "18381436494748161/6125000000000000000", "microbox_face_corrections": "67375000001/875000000", "polynomial_products": "3499999999/3500000000", "sparse_union_movement": "2506662688244748161/6125000000000000000"}}, "4447": {"parameters": {"epsilon": "1399999999/1400000000", "q": "168069/56000000", "a": "2100863/700000000", "beta": "1399999997/1400000000", "cap_xi": "71285296599831931/78400000000000000", "kappa": "300123/100000000"}, "margins": {"boundary_algebraic_matrix": "235296655831931/78400000000000000", "fused_gaussian": "235296655495793/78400000000000000", "global_coordinate_router": "2100863/700000000", "group_bit_router": "2941208893697411/980000000000000000", "group_scans": "699999999/700000000", "main_transform": "235296599831931/78400000000000000", "microbox_face_corrections": "26950000001/350000000", "polynomial_products": "1399999999/1400000000", "sparse_union_movement": "32085296655831931/78400000000000000"}}, "4453": {"parameters": {"epsilon": "349999999/350000000", "q": "1050423/350000000", "a": "131303/43750000", "beta": "349999997/350000000", "cap_xi": "111383273048949577/122500000000000000", "kappa": "7503/2500000"}, "margins": {"boundary_algebraic_matrix": "367648398949577/122500000000000000", "fused_gaussian": "367648396848731/122500000000000000", "global_coordinate_router": "131303/43750000", "group_bit_router": "45956093356091/15312500000000000", "group_scans": "174999999/175000000", "main_transform": "367648048949577/122500000000000000", "microbox_face_corrections": "6737500001/87500000", "polynomial_products": "349999999/350000000", "sparse_union_movement": "50133273398949577/122500000000000000"}}, "4440": {"parameters": {"epsilon": "69999997/70000000", "q": "207209/70000000", "a": "51803/17500000", "beta": "69999991/70000000", "cap_xi": "4455129629378373/4900000000000000", "kappa": "37/12500"}, "margins": {"boundary_algebraic_matrix": "14504839378373/4900000000000000", "fused_gaussian": "14504838135119/4900000000000000", "global_coordinate_router": "51803/17500000", "group_bit_router": "3626262033773/1225000000000000", "group_scans": "34999997/35000000", "main_transform": "14504629378373/4900000000000000", "microbox_face_corrections": "1347500003/17500000", "polynomial_products": "69999997/70000000", "sparse_union_movement": "2005129839378373/4900000000000000"}}, "4446": {"parameters": {"epsilon": "6999999999/7000000000", "q": "10503687/3500000000", "a": "168059/56000000", "beta": "6999999997/7000000000", "cap_xi": "22276650808989496313/24500000000000000000", "kappa": "3001053/1000000000"}, "margins": {"boundary_algebraic_matrix": "73525812489496313/24500000000000000000", "fused_gaussian": "73525812468488939/24500000000000000000", "global_coordinate_router": "168059/56000000", "group_bit_router": "1176413055495823/392000000000000000", "group_scans": "3499999999/3500000000", "main_transform": "73525808989496313/24500000000000000000", "microbox_face_corrections": "134750000001/1750000000", "polynomial_products": "6999999999/7000000000", "sparse_union_movement": "10026650812489496313/24500000000000000000"}}} + outer_min = {} + for n, rec in OUTER.items(): + P_ = {k: Q(x) for k, x in rec["parameters"].items()} + M_ = {k: Q(x) for k, x in rec["margins"].items()} + e, q_, a_, be, xi, kap = P_["epsilon"], P_["q"], P_["a"], P_["beta"], P_["cap_xi"], P_["kappa"] + rows = {"main_transform": e * q_, "global_coordinate_router": a_, "fused_gaussian": 1 - e + q_ * be, + "group_bit_router": 1 - e + a_ * be, "group_scans": 1 - e + be, "polynomial_products": e, + "sparse_union_movement": xi + Q(1, 2) - e, "microbox_face_corrections": 1 - (e + be + 48 - 128 + 2), + "boundary_algebraic_matrix": Q(3, 32) + xi - e} + need(rows == M_, f"#{n}: all nine outer rows reproduce") + need(min(M_, key=M_.get) == "main_transform" and min(M_.values()) > kap, f"#{n}: binding row above kappa") + outer_min[n] = f"{float(min(M_.values()) - kap):.3e}" + out["outer_ledgers_min_minus_kappa"] = outer_min out["4440_compiler"] = {"complex": [75415467350, 10418370291022217], "BIT": [3755884544, 25986965159937]} print(json.dumps(out, indent=1))