From ba0efeaac4e62d1757d7a9be6fd8aaf8f9bd35dc Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 01:07:32 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20#4416's=20paid-completi?= =?UTF-8?q?on=20tensor=20bound=20at=20kappa=200.00268647:=20proof=20steps?= =?UTF-8?q?=20and=20arithmetic=20hold;=20gamma=20margin=208e-6;=20least=20?= =?UTF-8?q?v=205745=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/pr4416-padding-check/README.md | 82 +++++++++ research/pr4416-padding-check/SOURCES.json | 18 ++ research/pr4416-padding-check/TASK.json | 100 ++++++++++ research/pr4416-padding-check/VERIFY.json | 18 ++ research/pr4416-padding-check/verify.py | 205 +++++++++++++++++++++ 5 files changed, 423 insertions(+) create mode 100644 research/pr4416-padding-check/README.md create mode 100644 research/pr4416-padding-check/SOURCES.json create mode 100644 research/pr4416-padding-check/TASK.json create mode 100644 research/pr4416-padding-check/VERIFY.json create mode 100644 research/pr4416-padding-check/verify.py diff --git a/research/pr4416-padding-check/README.md b/research/pr4416-padding-check/README.md new file mode 100644 index 0000000000..df64b5e098 --- /dev/null +++ b/research/pr4416-padding-check/README.md @@ -0,0 +1,82 @@ +# Independent check of #4416's paid-completion tensor bound + +**Claim type:** a written proof check plus certified exact arithmetic. **No new κ.** #4416 is not +accepted, and the native p7 audit and the outer premises are not re-checked. The object is +1337isnot1337's [#4416](https://github.com/CrocSwap/integer-mult-bounds/pull/4416) at head +`e9058860`, with `TENSOR.md` SHA256 prefix `b2eba86c` and `ENDPOINT.md` prefix `e7056020`. It +proposes conditional κ = 0.00268647 from zxv's p7 controller. The p7 controller is tensored +`v = 6240` times, small targets are completed to `11^v`, and paid jobs are split at `10^v`. + +## Proof check (`TENSOR.md` §1–3, §5) + +- **Product moments multiply.** + - Copy `j` of `U` runs at column `h_j`. + - Each paid position `l` of `U` makes one call to `V` at column `r_l`, whose role `j` delivers + rank `r_l h_j`. + - So the targets are `k_i h_j`, the paid ranks are `r_l s_a`, `T_τ(UV) = T_τ(U)T_τ(V)` and + `P_τ(UV) = P_τ(U)P_τ(V)`. +- **Completion.** Completing to rank `L` on disjoint axes is the canonical rank-`L` endpoint. + By concavity it loses moment, since `L^τ − K^τ < D^τ`. What it buys is the separation + `paid ≤ 10^v < 11^v ≤ target`. The bound conservatively keeps `T_τ^v` as the target moment. +- **Split tails.** `qJ^τ + r^τ ≤ RJ^{−C} + J^τ ≤ 2RJ^{−C}` holds for `R > J`. For completions, + `charge(D) ≤ (D + J)J^{−C} < 2L/J^C`. Together these give `α^v + 2γ^v + 2δ^v`. +- **Rank formula.** + - `r_max m^h < 2^{(111/26)v}` follows from `10 < 2⁴` and `121 < 2⁷`. + - `−log₂η < 1 + 7v(1−z0)` follows from `z0 > 1/2`. + - `θ < 25/26` follows from `10^26 < 11^25`. + - `H0 ≥ 7v` covers the base range `n < 121^v`. + +I found no gap in these steps. + +## Certified arithmetic + +| Quantity | This check | #4416 | +| --- | --- | --- | +| fields, paid calls, rank-one masses | 7,688; 55,998; 131,723 / 131,115 | same | +| `α = P_τ/T_τ` at `C = 0.00268648` | `< 0.999999984404` | `< 1 − 10⁻⁸` | +| `γ = P₁/(10^C T_τ)` | `< 0.99819171` | `< 4991/5000 = 0.9982` | +| `δ = 7688·11/(10^C T_τ)` | `< 0.64382471` | `< 2/3` | +| p7 mixed root | `(0.0026864890486, 0.0026864890492)` | above 0.00268648 | +| `α^v + 2γ^v + 2δ^v < 1` at `v = 6240` | holds (Bernoulli and direct) | holds | +| least `v` (direct certified route, `b = 11`, `c = 10`) | **5,745** | 6,240 used | +| `H0`, `H1` | 4,307,773,805,920 and 16,201,843,136,005,340,321 | same | + +The tight margin is `γ`: its bound sits only `8·10⁻⁶` below 4991/5000. The tested saving +0.00268648 is `9·10⁻⁹` below the p7 root. + +**A tighter rank from the same induction.** Using certified `−log₂η` and the exact +`log₂(r_max m^h)`, together with the best `θ̄ = 145/151` (from `10^151 < 11^145`, so +`h = 6/151`), gives `H1 = 15,370,312,178,898,752,926`. That is 5.4% below #4416's value. It is a +minor gain: the binding factor is `δ_gap = 1/1,400,000,000`, which is set by the choice of κ. + +## Not covered + +- The native p7 audit: contacts, phases, helpers and the all-column contract. +- The analytic, precision, tape and outer premises. +- The 209-profile screen in `FOLLOWUP.md`. +- Optimality of `(v, b, c)`. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/pr4416-padding-check --check-only +python3.12 -B scripts/research_package.py --package research/pr4416-padding-check +``` + +The verifier prints `PASS_PR4416_PADDING_ARITHMETIC` in about 10 seconds, using only the +standard library. + +## Open next questions + +1. **Which `(b, c)` minimizes `v`?** + - *Why it matters:* the least `v` with `(11, 10)` is 5,745. + - *First step:* scan `c < b < 121` with the direct certified route. + +## Credit + +- The construction and invoice are 1337isnot1337's (#4416, #4414, #4412). +- The native controller is 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/pr4416-padding-check/SOURCES.json b/research/pr4416-padding-check/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/pr4416-padding-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/pr4416-padding-check/TASK.json b/research/pr4416-padding-check/TASK.json new file mode 100644 index 0000000000..fc2d4177e7 --- /dev/null +++ b/research/pr4416-padding-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 #4416's paid-completion tensor bound and arithmetic at kappa 0.00268647.", + "scope_change_reason": "The card asks for independent coverage of a new paid-profile claim; #4416 is the largest open conditional claim and had no review.", + "bottleneck_link": "#4416's kappa rests on the p7 moment, the completion/split tails and the compiler rank.", + "budget_minutes": 30, + "stop_rule": "Stop at the tensor bound and arithmetic; do not audit the native p7 word.", + "outcome": "completed", + "evidence": "verify.py: alpha < 0.999999984404, gamma < 0.99819171 (margin 8e-6 to 4991/5000), delta < 0.6438; p7 root (0.0026864890486, 0.0026864890492); v=6240 inequality holds, least v 5745; #4416 H0/H1 reproduced; tighter H1 15370312178898752926.", + "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": "Which (b, c) minimizes the tensor power v?", + "why_it_matters": "The least v with (11,10) is 5745.", + "first_step": "Scan c= 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 ratios(C): + T = moment(TARGETS, C) + Pm = moment(PAID, C) + cC = exp_bounds(C * ln(C_CUT)[0], C * ln(C_CUT)[1]) + B = sum(TARGETS.values()) + P1 = sum(k * w for k, w in PAID.items()) + alpha = (Pm[0] / T[1], Pm[1] / T[0]) + gamma = (P1 / (cC[1] * T[1]), P1 / (cC[0] * T[0])) + delta = (B * B_FLOOR / (cC[1] * T[1]), B * B_FLOOR / (cC[0] * T[0])) + return alpha, gamma, delta + + +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 + + +def main(): + need(sum(TARGETS.values()) == 7688 and sum(PAID.values()) == 55998, "field and call counts") + T1, P1 = sum(k * w for k, w in TARGETS.items()), sum(k * w for k, w in PAID.items()) + need((T1, P1) == (131723, 131115), "rank-one masses") + need(max(PAID) < 121 and max(TARGETS) == 121, "ambient 121") + + alpha, gamma, delta = ratios(C_TEST) + need(alpha[1] < 1 - Q(1, 10**8), "alpha < 1 - 1e-8") + need(gamma[1] < Q(4991, 5000), "gamma < 4991/5000") + need(delta[1] < Q(2, 3), "delta < 2/3") + # p7 mixed root: alpha(C) = 1, alpha increasing in C + lo, hi = Q("0.00268"), Q("0.00269") + need(ratios(lo)[0][1] < 1 < ratios(hi)[0][0], "root bracket start") + 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 + root = (lo, hi) + need(root[0] > C_TEST, "C_test below the p7 mixed root") + + # Part B: #4416's sufficient route + need((Q(4991, 5000)) ** 390 < Q(1, 2) and Q(2, 3) ** 2 < Q(1, 2), "decay blocks") + need(1 / (1 + Q(V, 10**8)) + Q(4, 2 ** 16) < 1, "Bernoulli route at v = 6240") + # direct certified powers: ln(x^v) upper bounds, then compare via exp of a negative number + def total_upper(v): + la, lg, ld = pow_upper(alpha[1], v), pow_upper(gamma[1], v), pow_upper(delta[1], v) + # exp(x) <= 1/(1 - x) is false for x<0; use exp(x) <= 1/(1 + |x|) for the alpha term (Bernoulli-type) + ea = 1 / (1 - la) + def small(lx): # exp(lx) <= 2^-k when lx <= -k ln 2 + k = int(-lx / ln(2)[1]) + return Q(1, 2 ** k) if k > 0 else Q(1) + return ea + 2 * small(lg) + 2 * small(ld) + need(total_upper(V) < 1, "direct certified route at v = 6240") + least_v = next(v for v in range(1, V + 1) if total_upper(v) < 1) + + # Part C: compiler ranks + t = 1 - C_TEST + d = (C_TEST - KAPPA) / 7 + z = 1 - (KAPPA + 6 * d) + z0 = (t + z) / 2 + dl = z0 - t + need(d == Q(1, 700000000) and dl == Q(1, 1400000000), "slack family") + need(10 ** 26 < 11 ** 25, "theta < 25/26") + Bc, h = Q(111, 26) * V, Q(1, 26) + H0 = -((-(Bc * dl + 1 + 7 * V * (1 - z0))) // (h * dl)) + r = H0 * (1 - z0) / (z - z0) + H1 = r.numerator // r.denominator + 1 + need(H0 == 4307773805920 and H1 == 16201843136005340321 and H0 >= 7 * V, "#4416 ranks reproduced") + # tighter: certified log2 values, h from the best theta_bar = a/b with 10^b < 11^a + ln2 = ln(2) + log2_121_hi, log2_10_hi = ln(121)[1] / ln2[0], ln(10)[1] / ln2[0] + x = 1 - z0 + s, term = Q(0), x + for j in range(1, 30): + s += term / j + term *= x + neg_log2_z0_hi = (s + term / (1 - x)) / ln2[0] + neg_log2_eta = neg_log2_z0_hi + (1 - z0) * V * log2_121_hi + best = None + for den in range(26, 400): + # smallest a with 10^den < 11^a, i.e. theta = log 10 / log 11 < a/den + a = int(den * 0.9602) - 2 + while not 10 ** den < 11 ** a: + a += 1 + hh = 1 - Q(a, den) + B2 = V * (log2_10_hi + hh * log2_121_hi) + H0b = -((-(B2 * dl + neg_log2_eta)) // (hh * dl)) + if H0b < 7 * V: + continue + rb = H0b * (1 - z0) / (z - z0) + H1b = rb.numerator // rb.denominator + 1 + if best is None or H1b < best[0]: + best = (H1b, H0b, f"{a}/{den}") + print(json.dumps({ + "status": "PASS_PR4416_PADDING_ARITHMETIC", + "invoice": {"fields": 7688, "paid_calls": 55998, "rank_one": [131723, 131115]}, + "alpha_upper": f"{float(alpha[1]):.12f}", "gamma_upper": f"{float(gamma[1]):.8f}", + "delta_upper": f"{float(delta[1]):.8f}", + "p7_mixed_root": [f"{float(root[0]):.15f}", f"{float(root[1]):.15f}"], + "least_v_direct_route": least_v, + "ranks_4416": {"H0": H0, "H1": H1}, + "tighter_sufficient_rank": {"H1": best[0], "H0": best[1], "theta_bar": best[2], + "factor": f"{H1 / best[0]:.4f}"}, + "new_kappa_claimed": False, + }, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())