diff --git a/research/pr4405-refill-check/README.md b/research/pr4405-refill-check/README.md new file mode 100644 index 0000000000..db8aa817c8 --- /dev/null +++ b/research/pr4405-refill-check/README.md @@ -0,0 +1,97 @@ +# Independent check of #4405's refined template ranks and endpoint family + +**Claim type:** an independent exact check plus a quantitative lever analysis. **No new κ.** It +checks 1337isnot1337's [#4405](https://github.com/CrocSwap/integer-mult-bounds/pull/4405), at head +`873d1b3c96a83b701a5c0bba8e37a861e6672fef`. That PR refines zxv's #4359: + +- `TEMPLATE.md` (SHA256 prefix `3778e49c`) gives smaller explicit uniform ranks; +- `ENDPOINT.md` (`9b8d08cd`) gives a parameter family that admits every rational κ below the + complex mixed root. + +My #4404 audited #4359's original rank chain. Nothing is imported from #4405 or #4359, and the +invoices are embedded as printed in #4359. + +## Results + +**Part A: the refined ranks reproduce.** The refined induction requires only that the exit +coefficient satisfy `(16·n^{−h})^δ ≤ η = z0·m^{z0−1}`, not that it be at most `1/8 < η/2`. The +step is `L(n) ≤ A(n^{z0} − ηS + ηS)`, which is valid. With its own certified logarithms, the +verifier recomputes: + +| | `H0` | `H1` | #4359's `H1` | +| --- | --- | --- | --- | +| Complex | 335,449 | 1,546,084,442 | 276,540,184,361 | +| BIT | 69,740 | 42,843,607 | 6,552,928,412 | + +Both match #4405. Each `H0` is certified minimal, since one less fails for every value in the +log enclosure, and each `H1` is minimal. The endpoint's sufficient complex rank exponent, +2,099,384,703,303,215,709, also reproduces. + +**Part B: #4405's suggested levers.** These answer `TEMPLATE.md`'s "next quantitative questions": + +- **The intermediate `z0`.** A 199-point rational grid over `(t, z)` finds no `H1` below the + midpoint's, in either family. The leading factor is `1/((z0−t)(z−z0))`, which is minimized at + the midpoint, so optimizing `z0` gains nothing. +- **The exit constant 16.** Its `4δ` term is `1.2·10⁻⁴` of `H0` (complex) and `9.2·10⁻⁴` (BIT). + Sharpening it is negligible. +- **The uniform saving.** This is the real lever. `H1` scales like `1/δ²`, where `δ` is half the + gap between the tested mixed saving and the uniform saving: + + | Uniform saving | complex `H1` | BIT `H1` | + | --- | --- | --- | + | 0.002300 | 61,765,945 | 13,943 | + | 0.002302 | 171,679,856 | 14,073 | + | 0.002303 | 386,399,233 | 14,139 | + | as used (0.002304 / 0.002760) | 1,546,084,442 | 42,843,607 | + + #4359 admits BIT at 0.0027 only so that it does not cap the complex supplier. A BIT uniform + saving much closer to the complex one would therefore shrink the BIT rank to about `2^14000`. + That would hold only if the cover fallback and conversion still leave BIT above the complex + saving, which is not checked here. + +**Part C: the endpoint family.** + +- **The root bound.** The complex mixed moment at `C_test = 0.00230509019` is certified positive, + about `4.7·10⁻⁷`, so `C_test < C*`. It is negative at 0.002306, so `C* < 0.002306`. +- **The gap identities.** These are all exact identities with strictly positive values at + `κ = 0.00230509` and at 24 further rational κ between 10⁻⁷ and 0.0023: + - `ξ = 29/32 + (1−d)q` and `εq = κ + d(3−q)`; + - `λ−τ = d/2`, `λ−σ = 3d/2` and `λ'−λ = d/2`; + - `(1−stop)b − a = d(1−b)`; + - `ε − ξ = 3/32 − d − (1−d)q`; + - `1 − (2ξ−2) − r0 − β = 3/16 − 2(1−d)q + 29d/10`; + - the parameter order and the geometric gaps. + +## Not covered + +- The nine outer cost-row formulas themselves. Only the self-contained identities are checked. +- Native closure, adapters, the delayed cover and the BIT cover fallback. +- Whether a smaller uniform saving is admissible at the outer layer. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/pr4405-refill-check --check-only +python3.12 -B scripts/research_package.py --package research/pr4405-refill-check +``` + +The verifier prints `PASS_PR4405_REFILL_INDEPENDENT_CHECK` in about one second, using only the +standard library. + +## Open next questions + +1. **What is the smallest BIT uniform saving that still clears the complex binding row after the + cover fallback and conversion?** + - *Why it matters:* the BIT rank would drop from `2^42843607` to about `2^14000`. + - *First step:* recompute #4359's BIT fallback bill as a function of the uniform saving and + of `N`. + - *Blocked by:* the fallback formula in `DELAYED-COVER-BRIDGE.md`. + +## Credit + +- The refinement and endpoint family are 1337isnot1337's (#4405). +- The construction and invoices are zxv's (#4359). +- Theorem 1G is Jacob Alan Sussman's (#4268). + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/pr4405-refill-check/SOURCES.json b/research/pr4405-refill-check/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/pr4405-refill-check/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/pr4405-refill-check/TASK.json b/research/pr4405-refill-check/TASK.json new file mode 100644 index 0000000000..4707356476 --- /dev/null +++ b/research/pr4405-refill-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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 #4405's refined template ranks and endpoint slack family for #4359, and quantify its suggested levers.", + "scope_change_reason": "The card asks for independent coverage of a new paid-profile claim; #4405 refines the largest open conditional claim and had no review.", + "bottleneck_link": "#4359/#4405's uniform savings rest on these explicit-rank and slack-family steps.", + "budget_minutes": 30, + "stop_rule": "Stop at self-contained arithmetic; do not audit outer row formulas or native closure.", + "outcome": "completed", + "evidence": "verify.py: H0/H1 reproduced and minimal for both families and the endpoint; midpoint z0 optimal on a 199-point grid; exit constant 16 is 1e-4..1e-3 of H0; H1 falls to 61,765,945 (complex) / 13,943 (BIT) at uniform saving 0.0023; C_test < C* < 0.002306 certified; gap identities exact at 25 kappa.", + "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": "What is the smallest BIT uniform saving that still clears the complex row after cover fallback and conversion?", + "why_it_matters": "The BIT rank would fall from 2^42843607 to about 2^14000.", + "first_step": "Recompute #4359's BIT fallback bill as a function of the uniform saving and N.", + "blocked_by": "The fallback formula in DELAYED-COVER-BRIDGE.md." + } + ] +} diff --git a/research/pr4405-refill-check/VERIFY.json b/research/pr4405-refill-check/VERIFY.json new file mode 100644 index 0000000000..1a9cdd0e85 --- /dev/null +++ b/research/pr4405-refill-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": 120, + "checks": "Embedded #4359 invoices; certified log2(eta) enclosure; #4405 H0/H1 (complex 335449/1546084442, BIT 69740/42843607) reproduced and minimal; endpoint H1 2099384703303215709; z0 grid, exit-constant share and uniform-saving curve; mixed moment sign at C_test and 0.002306; ENDPOINT.md gap identities at 25 rational kappa." + } + ] +} diff --git a/research/pr4405-refill-check/verify.py b/research/pr4405-refill-check/verify.py new file mode 100644 index 0000000000..9fd5cc8dd9 --- /dev/null +++ b/research/pr4405-refill-check/verify.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +"""Independent check of #4405's refined template ranks and endpoint slack family (refining #4359). + +Part A the refined induction needs only exit coefficient <= eta = z0 m^(z0-1). With certified logarithms, + H0 = least integer with h delta H0 >= 4 delta - log2(eta), H1 = floor(H0 (1-z0)/(z-z0)) + 1; + recompute #4405's (335449, 1546084442) complex and (69740, 42843607) BIT, both minimal, and the + endpoint rank exponent 2099384703303215709. +Part B levers: (i) the intermediate z0 -- scan a rational grid and compare with the midpoint; + (ii) the exit constant 16 -- its share of H0; (iii) the uniform saving -- H1 as it varies. +Part C endpoint family at kappa = 0.00230509: the tested mixed moment is positive at C_test (so + C_test < C*), and the self-contained gap identities of ENDPOINT.md hold exactly, also on a sweep of + rational kappa. +Separately written; imports nothing from #4405 or #4359. Invoices embedded as printed in #4359. +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**45) +CASES = { + "complex": {"targets": {6: 192, 7: 56, 8: 93, 9: 1229, 25: 448, 57: 224}, + "paid": {1: 17623, 2: 5065, 3: 1738, 4: 714, 5: 254}, + "tested": Q(461, 200000), "uniform": Q(36, 15625), "h": Q(1, 10), + "H0": 335449, "H1": 1546084442, "old_H1": 276540184361}, + "BIT": {"targets": {8: 3073, 22: 444, 50: 222}, + "paid": {1: 9261, 2: 9394, 3: 553, 4: 308, 5: 714, 6: 77, 7: 1465}, + "tested": Q(2769, 1000000), "uniform": Q(69, 25000), "h": Q(1, 16), + "H0": 69740, "H1": 42843607, "old_H1": 6552928412}, +} + + +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(k): + y = Q(k - 1, k + 1) + s, term, n = Q(0), y, 0 + while True: + s += term / (2 * n + 1) + n += 1 + term *= y * y + tail = term / (2 * n + 1) / (1 - y * y) + if tail < GRID: + return down(2 * s), up(2 * (s + tail)) + + +def exp_small(lo, hi): + def series(x): + s, term = Q(0), Q(1) + for i in range(60): + s += term + term = term * x / (i + 1) + return s, abs(term) * 2 + a, ea = series(lo) + b, eb = series(hi) + return down(a - ea), up(b + eb) + + +def balance(case, saving, logs): + """bounds of sum W k^(1-C) - sum p r^(1-C)""" + lo = hi = Q(0) + for k, w in case["targets"].items(): + e = exp_small(-saving * logs[k][1], -saving * logs[k][0]) + lo, hi = lo + w * k * e[0], hi + w * k * e[1] + for r, pr in case["paid"].items(): + e = exp_small(-saving * logs[r][1], -saving * logs[r][0]) + lo, hi = lo - pr * r * e[1], hi - pr * r * e[0] + return lo, hi + + +def ranks(t, z0, z, h, m, logs): + """least H0 certified to give (16 2^(-h H0))^delta <= eta, and H1""" + delta = z0 - t + ln2 = logs[2] + # log2 eta = log2 z0 + (z0 - 1) log2 m ; z0 close to 1: log z0 = -sum (1-z0)^j / j + x = 1 - z0 + s, term = Q(0), x + for j in range(1, 40): + s += term / j + term *= x + ln_z0 = (-(s + term / (1 - x)), -s) + l2_lo = ln_z0[0] / ln2[0] + (z0 - 1) * logs[m][1] / ln2[0] + l2_hi = ln_z0[1] / ln2[1] + (z0 - 1) * logs[m][0] / ln2[1] + need(l2_lo <= l2_hi < 0, "log2 eta enclosure") + need_lo = 4 * delta - l2_hi # smallest possible requirement + need_hi = 4 * delta - l2_lo # largest possible requirement + H0 = -((-need_hi) // (h * delta)) # ceil: certified sufficient + certain_fail = h * delta * (H0 - 1) < need_lo + ratio = H0 * (1 - z0) / (z - z0) + H1 = ratio.numerator // ratio.denominator + 1 + need(H1 * (z - z0) > H0 * (1 - z0) and not (H1 - 1) * (z - z0) > H0 * (1 - z0), "H1 minimal") + return H0, H1, certain_fail, (4 * delta) / need_hi + + +def main(): + logs = {k: ln_bounds(k) for k in (2, 3, 4, 5, 6, 7, 8, 9, 22, 25, 50, 57)} + logs[1] = (Q(0), Q(0)) + out = {"status": "PASS_PR4405_REFILL_INDEPENDENT_CHECK", "new_kappa_claimed": False, "cases": {}} + for name, case in CASES.items(): + m = max(case["targets"]) + t, z = 1 - case["tested"], 1 - case["uniform"] + z0 = (t + z) / 2 + H0, H1, minimal, share16 = ranks(t, z0, z, case["h"], m, logs) + need(H0 == case["H0"] and H1 == case["H1"] and minimal, f"{name}: #4405 H0/H1 reproduced and minimal") + need(case["old_H1"] // H1 > 150, "factor > 150 over #4359") + # lever (i): z0 grid + best = (H1, z0) + for j in range(1, 200): + zz = t + (z - t) * j / 200 + _, h1, _, _ = ranks(t, zz, z, case["h"], m, logs) + if h1 < best[0]: + best = (h1, zz) + # lever (iii): uniform saving + curve = [] + for u in (Q(23, 10000), Q(2302, 1000000), Q(2303, 1000000), case["uniform"]): + if u >= case["tested"]: + continue + zu = 1 - u + _, h1u, _, _ = ranks(t, (t + zu) / 2, zu, case["h"], m, logs) + curve.append({"uniform_saving": str(u), "H1": h1u}) + out["cases"][name] = { + "H0": H0, "H1": H1, "midpoint_H1": H1, + "best_grid_z0_H1": best[0], "z0_gain": f"{1 - best[0] / H1:.4%}", + "exit_constant_16_share_of_H0": f"{float(share16):.2e}", + "H1_vs_uniform_saving": curve, + } + + # Part C: endpoint + cx = CASES["complex"] + kappa, c_test = Q("0.00230509"), Q("0.00230509019") + bal = balance(cx, c_test, logs) + need(bal[0] > 0, "mixed moment positive at C_test, so C_test < C*") + bal_hi = balance(cx, Q("0.002306"), logs) + need(bal_hi[1] < 0, "C* < 0.002306") + sweep = [kappa] + [Q(k, 10**7) for k in range(1, 23051, 997)] + for kap in sweep: + ct = c_test if kap == kappa else (kap + Q("0.00230509")) / 2 if kap < Q("0.00230509") else None + if ct is None: + continue + d = (ct - kap) / 7 + uniform, b, a, q = kap + 6 * d, kap + 5 * d, kap + 4 * d, kap + 3 * d + eps, beta, r0, stop, layout = 1 - d, 1 - 3 * d, d / 10, d, d + xi = eps * (1 + q) - Q(3, 32) + layout + need(xi == Q(29, 32) + (1 - d) * q, "xi identity") + need(eps * q == kap + d * (3 - q) and eps * q > kap, "main-transform saving") + lam, lam_p, tau, sigma = 1 - (q + a) / 2, 1 - q, 1 - a, 1 - b + need(lam - tau == d / 2 and lam - sigma == 3 * d / 2 and lam_p - lam == d / 2, "stopped-supplier gaps") + need((1 - stop) * b - a == d * (1 - b) > 0, "stop gap") + need(eps - xi == Q(3, 32) - d - (1 - d) * q > 0, "epsilon - xi") + need(1 - (2 * xi - 2) - r0 - beta == Q(3, 16) - 2 * (1 - d) * q + Q(29, 10) * d > 0, "precision guard gap") + need(0 < d < Q(1, 3000) and 0 < q < a < b < uniform < ct, "parameter order") + need(Q(1, 2) < xi < eps < 1 and 0 < beta < eps and b < Q(1, 32), "geometric gaps") + # endpoint rank + d = (c_test - kappa) / 7 + z = 1 - (kappa + 6 * d) + t = 1 - c_test + _, H1e, _, _ = ranks(t, (t + z) / 2, z, cx["h"], 57, logs) + need(H1e == 2099384703303215709, "#4405 endpoint rank exponent") + out["endpoint"] = {"kappa": str(kappa), "C_test": str(c_test), "moment_at_C_test": f"{float(bal[0]):.3e}", + "H1": H1e, "kappa_sweep_points": len(sweep)} + print(json.dumps(out, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())