From 76613f8d29b664e386f29f30153f74087f462953 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 01:03:20 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20review=20#4411's=20logarithmic?= =?UTF-8?q?=20majorant:=20proof=20holds,=20arithmetic=20certified,=20least?= =?UTF-8?q?=20ranks=20slightly=20below=20stated,=20exact=20L(N)=20<=3D=20F?= =?UTF-8?q?(N)=20to=20N=20=3D=206000=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/pr4411-majorant-review/README.md | 77 +++++++ research/pr4411-majorant-review/SOURCES.json | 18 ++ research/pr4411-majorant-review/TASK.json | 100 +++++++++ research/pr4411-majorant-review/VERIFY.json | 18 ++ research/pr4411-majorant-review/verify.py | 220 +++++++++++++++++++ 5 files changed, 433 insertions(+) create mode 100644 research/pr4411-majorant-review/README.md create mode 100644 research/pr4411-majorant-review/SOURCES.json create mode 100644 research/pr4411-majorant-review/TASK.json create mode 100644 research/pr4411-majorant-review/VERIFY.json create mode 100644 research/pr4411-majorant-review/verify.py diff --git a/research/pr4411-majorant-review/README.md b/research/pr4411-majorant-review/README.md new file mode 100644 index 0000000000..a52369f977 --- /dev/null +++ b/research/pr4411-majorant-review/README.md @@ -0,0 +1,77 @@ +# Independent review of #4411's logarithmic majorant + +**Claim type:** a written proof check, certified exact arithmetic and an independent flow +simulation. **No new κ.** It reviews zxv's +[#4411](https://github.com/CrocSwap/integer-mult-bounds/pull/4411) at head `ec2c9505`, with README +SHA256 prefix `3b74b9b2`, as that PR's open question asks. #4411 replaces #4359's power majorant +with + + L(n) = P_n/B_n ≤ F(n) = n^t (1 + log₂ n)^{1/q}, + +and specifies ranks `2^465000` (complex) and `2^7100` (BIT) at κ = 0.0023. Those supersede my +own #4413 ranks, `2^268300549` and `2^14664`. #4411 and #4413 were posted in parallel. + +## Proof check + +The induction is checked line by line, and it holds. + +- **Base, `n < m`.** For `2 ≤ n < m`, `n^{q(1−t)} < m^{q(1−t)} < 2 ≤ 1 + log₂ n`, using (4). +- **Exit contraction (6).** Since `θ < θ̄` and `n ≥ m`, `log₂ E ≤ log₂ r_max + θ̄(log₂ n − log₂ m)`. + Then `1 + log₂ E ≤ θ̄(1 + log₂ n)` is equivalent to `2^{1−θ̄} r_max ≤ m^{θ̄}`, which is (2). So + `C(e) ≤ θ̄^{1/q}C(n)`, and (1) gives `Σ x_e F(e) ≤ θ̄^{1/q}C(n)Σ w_s s^t`. +- **Complements (7).** `C` is increasing, so `F(n−s) ≤ (n−s)^t C(n)`, with `F(0) = 0`. With + `1 − (1−y)^t ≥ η y^t` on `(1/m, 1]`, this gives `F(n) − Σ w_s F(n−s) ≥ η C(n) Σ w_s s^t`. +- **Induction.** Condition (3), `θ̄ < η^q`, makes (6) smaller than (7). Strong induction then + gives `L(n) ≤ F(n)` for all `n ≥ 1`, with constant 1. +- **Final rank test.** `L(N) < N^z` holds iff `1 + H < 2^{q(z−t)H}`. + +## Certified arithmetic + +| | complex | BIT | +| --- | --- | --- | +| `θ < θ̄` | `5^10 < 6^9` | `7^16 < 8^15` | +| (2) `2^{b−a} r_max^b ≤ m^a` | holds | holds | +| (3) `η^q − θ̄` | 0.000646856868 (matches #4411) | 0.009533387925 (matches) | +| (4) `m^{q(1−t)} < 2` | holds | holds | +| stated / **least** `H`, original savings | 2,352,000 / **2,351,697** | 529,000 / **528,066** | +| stated / **least** `H`, κ-preserving savings | 465,000 / **464,850** | 7,100 / **7,091** | + +Every stated `H` is certified. #4411's values are rounded up from the least `H` that passes the +same sufficient test; that least value is computed here by bisection with certified logarithms. + +## Flow simulation + +The separate aggregated lockstep-flow simulator from my #4404 computes exact rational `L(N)` for +every `N ≤ 6000` in both families. At every rank it checks the source range, the exit bound and +the exact rank-one potential identity, and that `L(N) ≤ F(N)`. The largest ratio `L(N)/F(N)` is +0.927 (complex) and 0.843 (BIT), so the majorant holds with room on all simulated ranks. + +## Not covered + +- #4411's retuned consumer point (`b = 0.0023004`, `a = 0.0023003`) and its 63 + 22 predicates. +- Native closure, the delayed cover and outer transfer. +- Ranks above 6000 in the simulation. The proof, not the simulation, covers all `n`. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/pr4411-majorant-review --check-only +python3.12 -B scripts/research_package.py --package research/pr4411-majorant-review +``` + +The verifier prints `PASS_PR4411_MAJORANT_REVIEW` in about 30 seconds, using only the standard +library. + +## Open next questions + +1. **Can the `(1 + log₂ n)^{1/q}` factor be replaced by a smaller slowly varying factor?** + - *Why it matters:* the simulated ratio `L/F` is well below 1. + - *First step:* fit the simulated `L(N)/N^t` against `log N`. + +## Credit + +The majorant, ranks and consumer retuning are zxv's (#4411). The compiler is #4359's, and the +lockstep flow is Jacob Alan Sussman's Theorem 1G (#4268). + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/pr4411-majorant-review/SOURCES.json b/research/pr4411-majorant-review/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/pr4411-majorant-review/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/pr4411-majorant-review/TASK.json b/research/pr4411-majorant-review/TASK.json new file mode 100644 index 0000000000..dc088d43c8 --- /dev/null +++ b/research/pr4411-majorant-review/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 review #4411's logarithmic majorant and explicit ranks: proof check, certified arithmetic, least ranks, exact flow simulation.", + "scope_change_reason": "#4411's own open question asks for independent review of the new majorant.", + "bottleneck_link": "#4359/#4411's finite uniform templates are specified by these ranks.", + "budget_minutes": 30, + "stop_rule": "Stop at the majorant and ranks; do not audit the consumer retuning or native premises.", + "outcome": "completed", + "evidence": "verify.py: conditions (2)-(4) certified, eta^q - theta_bar = 0.000646856868 / 0.009533387925; least certified H 2351697, 464850 (complex) and 528066, 7091 (BIT), each below the stated rounded value; exact L(N) <= F(N) for N <= 6000 with max ratio 0.927 / 0.843.", + "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 the (1+log2 n)^(1/q) factor be replaced by a smaller slowly varying factor?", + "why_it_matters": "The simulated L/F ratio is well below 1.", + "first_step": "Fit simulated L(N)/N^t against log N.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4411-majorant-review/VERIFY.json b/research/pr4411-majorant-review/VERIFY.json new file mode 100644 index 0000000000..bfcd1e84d7 --- /dev/null +++ b/research/pr4411-majorant-review/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": "Embedded invoices; certified theta= 1, by reduction to [1, 2)""" + 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 < GRID: + break + l2 = LN2 + return down(2 * s + k * l2[0]), up(2 * (s + tail) + k * l2[1]) + + +def passes(H, g, certain): + """(1 + H) < 2^(g H) decided by certified logs; certain=True requires the inequality to be proven""" + lo, hi = ln_big(1 + H) + if certain: + return hi < g * H * LN2[0] + return lo < g * H * LN2[1] + + +def exp_bounds(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 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): + ks = sorted(W) + m = ks[-1] + def c(a): + v = 1 + for k, x in zip(ks, a): + v *= k ** x + return v + def u(a): + v = factorial(sum(a)) + for k, x in zip(ks, a): + v = v // factorial(x) * W[k] ** x + return v + G = 0 + while any(m * c(a) <= N for a in multis(len(ks), G + 1)): + G += 1 + F = [{1: 1}] # F[d][rho]: number of length-d paid sequences with dilation rho + 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) + surplus = sum(k * w for k, w in W.items()) - sum(r * p for r, p in P.items()) + S, X, col_mass = {}, {}, 0 + for d in range(G + 1): + for rho, cnt in F[d].items(): + for a in multis(len(ks), G - d): + col = rho * c(a) + if m * col > N: + continue + col_mass += cnt * u(a) * col + if d == G: + for r, pr in P.items(): + X[r * col] = X.get(r * col, 0) + cnt * u(a) * pr + for a in multis(len(ks), G): # top class: every target is a source + if m * c(a) <= N: + for k in ks: + S[k * c(a)] = S.get(k * c(a), 0) + W[k] * u(a) + for d in range(1, G + 1): # child targets whose parent unit is absent + for rho, cnt in F[d - 1].items(): + for r, pr in P.items(): + for a in multis(len(ks), G - d): + if m * rho * r * c(a) > N: + continue + for i, k in enumerate(ks): + b = list(a) + b[i] += 1 + if m * rho * c(b) > N: + S[rho * r * c(b)] = S.get(rho * r * c(b), 0) + cnt * pr * u(a) * W[k] + return G, S, X, col_mass * surplus + + + + +def simulate(case): + W, P = case["targets"], case["paid"] + m = max(W) + t, qq = float(case["t"]), case["q"] + L = [Q(0), Q(1)] + worst = 0.0 + for N in range(2, NMAX + 1): + if N < m: + val = Q(N) + else: + G, S, X, pot = flow(N, W, P) + need(all(m * s > N and s <= N for s in S) and all(e < N for e in X), f"N={N}: ranks") + need(sum(s * v for s, v in S.items()) - sum(e * v for e, v in X.items()) == pot, f"N={N}: potential") + tot = sum(S.values()) + val = (sum(v * L[N - s] for s, v in S.items()) + sum(v * L[e] for e, v in X.items())) / tot + F = N ** t * (1 + log(N, 2)) ** (1 / qq) + need(float(val) <= F * (1 - 1e-9), f"N={N}: L(N) <= F(N)") + worst = max(worst, float(val) / F) + L.append(val) + return worst + + +def main(): + global LN2 + LN2 = ln_bounds(2) + out = {"status": "PASS_PR4411_MAJORANT_REVIEW", "new_kappa_claimed": False, "cases": {}} + for name, case in CASES.items(): + W, P = case["targets"], case["paid"] + m, kmin, rmax = max(W), min(W), max(P) + t, tb, qq = case["t"], case["theta_bar"], case["q"] + a, b = tb.numerator, tb.denominator + need(rmax ** b < kmin ** a, "theta < theta_bar") + need(2 ** (b - a) * rmax ** b <= m ** a, "condition (2)") + lnm = ln_bounds(m) + # eta^q = t^q exp(q (t-1) ln m); lower bound uses the upper bound of ln m + eta_q_lo = t ** qq * exp_bounds(qq * (t - 1) * lnm[1], qq * (t - 1) * lnm[1])[0] + need(eta_q_lo > tb, "condition (3): theta_bar < eta^q") + eta_q_hi = t ** qq * exp_bounds(qq * (t - 1) * lnm[0], qq * (t - 1) * lnm[0])[1] + need(exp_bounds(qq * (1 - t) * lnm[1], qq * (1 - t) * lnm[1])[1] < 2, "condition (4)") + ranks = [] + for z, H in case["ranks"]: + g = qq * (z - t) # need 1 + H < 2^(g H) + num, den = g.numerator, g.denominator + need(passes(H, g, True), f"rank H={H} certified") + lo_h, hi_h = 1, H # least certified H, by bisection on the monotone test + while lo_h < hi_h: + mid = (lo_h + hi_h) // 2 + if passes(mid, g, True): + hi_h = mid + else: + lo_h = mid + 1 + need(not passes(lo_h - 1, g, False) or lo_h == 1, "one less is certified to fail") + ranks.append({"stated_H": H, "least_H": lo_h}) + worst = simulate(case) + out["cases"][name] = {"eta_q_minus_theta_bar": [f"{float(eta_q_lo - tb):.12f}", f"{float(eta_q_hi - tb):.12f}"], + "ranks_H": ranks, "flows_to": NMAX, "max_L_over_F": f"{worst:.4f}"} + print(json.dumps(out, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())