From 40f675338b7102ec38d858355a1db6cc051778e7 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 01:10:32 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20the=20#4412=20and=20#44?= =?UTF-8?q?14=20tensor=20endpoints:=20alpha/gamma=20bounds=20and=20ranks?= =?UTF-8?q?=20hold;=20least=20tensor=20powers=2010,714=20and=2060,701=20(n?= =?UTF-8?q?o=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/pr4412-pr4414-tensor-check/README.md | 77 +++++++ .../pr4412-pr4414-tensor-check/SOURCES.json | 18 ++ research/pr4412-pr4414-tensor-check/TASK.json | 100 ++++++++++ .../pr4412-pr4414-tensor-check/VERIFY.json | 18 ++ research/pr4412-pr4414-tensor-check/verify.py | 188 ++++++++++++++++++ 5 files changed, 401 insertions(+) create mode 100644 research/pr4412-pr4414-tensor-check/README.md create mode 100644 research/pr4412-pr4414-tensor-check/SOURCES.json create mode 100644 research/pr4412-pr4414-tensor-check/TASK.json create mode 100644 research/pr4412-pr4414-tensor-check/VERIFY.json create mode 100644 research/pr4412-pr4414-tensor-check/verify.py diff --git a/research/pr4412-pr4414-tensor-check/README.md b/research/pr4412-pr4414-tensor-check/README.md new file mode 100644 index 0000000000..7001b79cdd --- /dev/null +++ b/research/pr4412-pr4414-tensor-check/README.md @@ -0,0 +1,77 @@ +# Independent arithmetic check of the #4412 and #4414 tensor endpoints + +**Claim type:** certified exact arithmetic plus a written check of the split bound. **No new κ.** +Neither PR is accepted, and their native audits are not re-checked. The objects are +1337isnot1337's +[#4412](https://github.com/CrocSwap/integer-mult-bounds/pull/4412) (κ = 0.00247755, head +`9f0df9bf`, with `TENSOR.md`/`ENDPOINT.md` SHA256 prefixes `d65a3997`/`2b0d1524`) and +[#4414](https://github.com/CrocSwap/integer-mult-bounds/pull/4414) (κ = 0.00267987, head +`90da4b0a`, prefixes `96e4593f`/`3d17949e`). + +Both PRs tensor a native mixed unit `v` times and split each paid job at a cutoff `J` below the +smallest target rank: + +- #4412 tensors the all-fresh p3 unit with `J = 4^v`; +- #4414 tensors the p6 unit with `J = ⌊(19/4)^v⌋`. + +My [#4428](https://github.com/CrocSwap/integer-mult-bounds/pull/4428) checked their successor, +#4416. + +## Split bound + +For a paid rank `R > J`, the split satisfies `qJ^τ + r^τ ≤ 2RJ^{−C}`. That gives a normalized +paid moment below `α^v + 2γ^v`, where `α = P_τ/T_τ` and `γ = P₁/(c^C T_τ)`. For #4414, +`J ≥ (19/4)^v/2` doubles the tail, giving `α^v + 4γ^v`. The other requirements also hold: + +- **Exit exponents.** `4^8 < 5^7` gives `θ < 7/8` for #4412, and `19^32 < 4^32·5^31` gives + `θ < 31/32` for #4414. +- **Exit constants.** These are `B = (2 + 6h)v` for #4412 and `B = (79/32)v` for #4414, the latter + from `19^4 < 2^17`. Both hold. +- **Base range.** `H0 ≥ log₂m·v` covers it. + +## Results + +| | #4412 | #4414 | +| --- | --- | --- | +| tested saving | 0.00247756 | 0.00267988 | +| `α` upper (stated) | 0.999999996840 (`≤ 1 − 10⁻⁹`) | 0.999999982435 (`< 1 − 10⁻⁸`) | +| `γ` upper (stated) | 0.99896534 (`< 999/1000`) | 0.99986298 (`< 9999/10000`) | +| raw mixed root | (0.0024775616403, 0.0024775616409) | (0.0026798899695, 0.0026798899701) | +| tested saving below root by | `1.6·10⁻⁹` | `1.0·10⁻⁸` | +| tensor power used / **least** under the same certified bound | 15,000 / **10,714** | 150,000 / **60,701** | +| `H0`, `H1` reproduced | 2,508,580,090,000; 8,701,218,254,312,470,001 | 126,106,333,450,000; 473,129,651,134,046,950,001 | + +The `γ` margins are tight but certified: `3.5·10⁻⁵` and `3.7·10⁻⁵` under the stated bounds. The +least tensor powers are well below the ones used, at 0.71× and 0.40×. Smaller `v` shrinks every +tensor constant, though not the compiler rank, which is set by the slack gap `1/(1.4·10⁹)`. + +## Not covered + +- The native p3-fresh and p6 audits. +- The chronological tensor construction's native realization. +- The outer premises. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/pr4412-pr4414-tensor-check --check-only +python3.12 -B scripts/research_package.py --package research/pr4412-pr4414-tensor-check +``` + +The verifier prints `PASS_PR4412_PR4414_TENSOR_ARITHMETIC` in about 15 seconds, using only the +standard library. + +## Open next questions + +1. **Does a rational cutoff closer to the minimum target rank reduce `v` further?** + - *Example:* `(24/5)^v` for #4414's p6 unit. + - *First step:* scan rational `c` below 5 with the same certified `γ` and the floor factor. + +## Credit + +- The constructions and invoices are 1337isnot1337's (#4412, #4414). +- The native controllers 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/pr4412-pr4414-tensor-check/SOURCES.json b/research/pr4412-pr4414-tensor-check/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/pr4412-pr4414-tensor-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/pr4412-pr4414-tensor-check/TASK.json b/research/pr4412-pr4414-tensor-check/TASK.json new file mode 100644 index 0000000000..55340dfce6 --- /dev/null +++ b/research/pr4412-pr4414-tensor-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 the tensor-and-split endpoint arithmetic of #4412 (kappa 0.00247755) and #4414 (kappa 0.00267987).", + "scope_change_reason": "The card asks for independent coverage of new paid-profile claims; these two PRs had none.", + "bottleneck_link": "Their kappa claims rest on these moment bounds and compiler ranks before the native premises.", + "budget_minutes": 25, + "stop_rule": "Stop at the arithmetic; do not audit the native words.", + "outcome": "completed", + "evidence": "verify.py: alpha, gamma bounds certified (gamma margins 3.5e-5, 3.7e-5); roots 0.00247756164 / 0.00267988997; least v 10714 / 60701 vs used 15000 / 150000; stated 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": [ + { + "question": "Does a rational cutoff closer to the minimum target rank reduce v further?", + "why_it_matters": "Smaller v shrinks every tensor constant.", + "first_step": "Scan rational c < 5 with the certified gamma and floor factor.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4412-pr4414-tensor-check/VERIFY.json b/research/pr4412-pr4414-tensor-check/VERIFY.json new file mode 100644 index 0000000000..f5b0c97a15 --- /dev/null +++ b/research/pr4412-pr4414-tensor-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": "Printed #4412/#4414 invoices; certified alpha and gamma at the tested savings; raw mixed root brackets; tensor inequality at the used v and least v under the same certified bound; theta comparisons; stated H0/H1 reproduced." + } + ] +} diff --git a/research/pr4412-pr4414-tensor-check/verify.py b/research/pr4412-pr4414-tensor-check/verify.py new file mode 100644 index 0000000000..680fcb9681 --- /dev/null +++ b/research/pr4412-pr4414-tensor-check/verify.py @@ -0,0 +1,188 @@ +#!/usr/bin/env python3 +"""Independent arithmetic check of the tensor-and-split endpoints of #4412 (kappa 0.00247755) and #4414 (0.00267987). + +Both tensor a native mixed unit v times and split paid jobs at a cutoff c^v (#4412: c = 4; #4414: +floor((19/4)^v), which costs a factor 2 in the split tail). With alpha = P_tau/T_tau and +gamma = P_1/(c^C T_tau), the normalized paid moment is below alpha^v + 2 gamma^v (or + 4 gamma^v with the floor). +For each PR this verifier certifies alpha and gamma at the tested saving with its own interval logs, brackets the +raw mixed root, checks the stated v, finds the least v under the same certified bound, and reproduces the stated +compiler ranks H0, H1 from their rational formulas. Inputs are the printed invoices; nothing is imported. +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 + + + +CASES = { + "4412": {"targets": {5: 196, 6: 126, 7: 392, 8: 651, 9: 1491, 25: 448, 57: 224}, + "paid": {1: 17409, 2: 4991, 3: 1568, 4: 714, 5: 140, 8: 504, 16: 448}, + "C_test": Q("0.00247756"), "kappa": Q("0.00247755"), "v": 15000, "cut": Q(4), "floor": False, + "alpha_bound": 1 - Q(1, 10**9), "gamma_bound": Q(999, 1000), + "h": Q(1, 8), "theta_cmp": (4 ** 8, 5 ** 7), "B": lambda v, h: (2 + 6 * h) * v, "log2m": 6, + "H0": 2508580090000, "H1": 8701218254312470001}, + "4414": {"targets": {5: 364, 6: 234, 7: 728, 8: 1209, 9: 2769, 25: 448, 41: 448, 57: 224, 105: 224}, + "paid": {1: 32331, 2: 9269, 3: 2912, 4: 1326, 5: 260, 8: 1224, 16: 448, 32: 448, 48: 224}, + "C_test": Q("0.00267988"), "kappa": Q("0.00267987"), "v": 150000, "cut": Q(19, 4), "floor": True, + "alpha_bound": 1 - Q(1, 10**8), "gamma_bound": Q(9999, 10000), + "h": Q(1, 32), "theta_cmp": (19 ** 32, 4 ** 32 * 5 ** 31), "B": lambda v, h: Q(79, 32) * v, "log2m": 7, + "H0": 126106333450000, "H1": 473129651134046950001}, +} + + +def ln_q(x): + """certified ln of a positive rational p/q""" + a, b = ln(x.numerator), ln(x.denominator) + return a[0] - b[1], a[1] - b[0] + + +def analyse(name, cs): + T_hist, P_hist, C = cs["targets"], cs["paid"], cs["C_test"] + T1, P1 = sum(k * w for k, w in T_hist.items()), sum(k * w for k, w in P_hist.items()) + need(T1 > P1, f"{name}: positive rank-one surplus") + def ratios(Cx): + T = moment(T_hist, Cx) + Pm = moment(P_hist, Cx) + lc = ln_q(cs["cut"]) + cC = exp_bounds(Cx * lc[0], Cx * lc[1]) + return (Pm[0] / T[1], Pm[1] / T[0]), (P1 / (cC[1] * T[1]), P1 / (cC[0] * T[0])) + alpha, gamma = ratios(C) + need(alpha[1] <= cs["alpha_bound"] and gamma[1] < cs["gamma_bound"], f"{name}: alpha and gamma bounds") + lo, hi = C, C + Q(1, 10**5) + need(ratios(hi)[0][0] > 1, f"{name}: root bracket") + while hi - lo > Q(1, 10**12): + mid = (lo + hi) / 2 + a = ratios(mid)[0] + if a[1] < 1: + lo = mid + elif a[0] > 1: + hi = mid + else: + break + tail = 4 if cs["floor"] else 2 # floor(c^v) >= c^v / 2 doubles the split tail + def total_upper(v): + ea = 1 / (1 - pow_upper(alpha[1], v)) + lg = pow_upper(gamma[1], v) + k = int(-lg / ln(2)[1]) + return ea + tail * (Q(1, 2 ** k) if k > 0 else Q(1)) + v = cs["v"] + need(total_upper(v) < 1, f"{name}: tensor inequality at v = {v}") + least_v = None + lo_v, hi_v = 1, v + while lo_v < hi_v: # total_upper is decreasing in v once both decays bite + mid = (lo_v + hi_v) // 2 + if total_upper(mid) < 1: + hi_v = mid + else: + lo_v = mid + 1 + least_v = lo_v + need(total_upper(least_v) < 1 and not total_upper(least_v - 1) < 1, f"{name}: least v") + # ranks + t = 1 - C + d = (C - cs["kappa"]) / 7 + z = 1 - (cs["kappa"] + 6 * d) + z0 = (t + z) / 2 + dl = z0 - t + a_cmp, b_cmp = cs["theta_cmp"] + need(a_cmp < b_cmp, f"{name}: theta bound") + h = cs["h"] + B = cs["B"](v, h) + H0 = -((-(B * dl + 1 + cs["log2m"] * v * (1 - z0))) // (h * dl)) + r = H0 * (1 - z0) / (z - z0) + H1 = r.numerator // r.denominator + 1 + need(H0 == cs["H0"] and H1 == cs["H1"] and H0 >= cs["log2m"] * v, f"{name}: stated ranks reproduced") + return {"alpha_upper": f"{float(alpha[1]):.12f}", "gamma_upper": f"{float(gamma[1]):.8f}", + "gamma_stated_bound": str(cs["gamma_bound"]), + "mixed_root": [f"{float(lo):.13f}", f"{float(hi):.13f}"], + "C_test_gap_to_root": f"{float(lo - C):.2e}", "v_used": v, "least_v": least_v, + "H0": H0, "H1": H1} + + +def main(): + out = {"status": "PASS_PR4412_PR4414_TENSOR_ARITHMETIC", "new_kappa_claimed": False} + for name, cs in CASES.items(): + out[name] = analyse(name, cs) + print(json.dumps(out, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())