From 5cc8d42370a1e0f8595b0c6d603cb9fcfc12c675 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 11:10:48 +0700 Subject: [PATCH 1/2] =?UTF-8?q?Sharper=20#4483=20witnesses:=20p16=20rank?= =?UTF-8?q?=202^1587000000=20(was=202^2800000000),=20p7=202^2253000000,=20?= =?UTF-8?q?same=20=CE=BA=20(compiler=20improvement,=20no=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/adaptive-witness-retune/README.md | 78 ++++++ research/adaptive-witness-retune/SOURCES.json | 48 ++++ research/adaptive-witness-retune/TASK.json | 100 +++++++ research/adaptive-witness-retune/VERIFY.json | 24 ++ .../adaptive-witness-retune/WITNESS-p16.json | 24 ++ .../adaptive-witness-retune/WITNESS-p7.json | 24 ++ research/adaptive-witness-retune/verify.py | 258 ++++++++++++++++++ 7 files changed, 556 insertions(+) create mode 100644 research/adaptive-witness-retune/README.md create mode 100644 research/adaptive-witness-retune/SOURCES.json create mode 100644 research/adaptive-witness-retune/TASK.json create mode 100644 research/adaptive-witness-retune/VERIFY.json create mode 100644 research/adaptive-witness-retune/WITNESS-p16.json create mode 100644 research/adaptive-witness-retune/WITNESS-p7.json create mode 100644 research/adaptive-witness-retune/verify.py diff --git a/research/adaptive-witness-retune/README.md b/research/adaptive-witness-retune/README.md new file mode 100644 index 0000000000..252d1871ef --- /dev/null +++ b/research/adaptive-witness-retune/README.md @@ -0,0 +1,78 @@ +# Sharper witnesses for #4483: p16 rank `2^1587000000`, p7 rank `2^2253000000` + +**Claim type:** a compiler improvement with certified finite witnesses. **No new κ.** It uses zxv's +[#4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483) theorem unchanged: the adaptive-height +direct compiler with its shifted-logarithmic majorant. It keeps each profile's raw native invoice, +uniform saving and κ, and changes only the free geometry of the witness: `p`, `c`, the height base `M`, +`ℓ₀`, `s`, `λ` and the rational guards. + +## Results + +| profile | κ (unchanged) | #4483 H | **new H** | exponent ratio | +| --- | ---: | ---: | ---: | ---: | +| p16 (#4470) | 0.00302015 | 2,800,000,000 | **1,587,000,000** | **1.764×** | +| p7 | 0.00268647 | 3,040,000,000 | **2,253,000,000** | 1.349× | + +Here the sufficient uniform rank is `N = 2^H`. Against p16's pre-#4483 rank `2^558100005581`, the new +exponent is about 352× smaller. + +The witnesses are `WITNESS-p16.json` and `WITNESS-p7.json`: + +| | t₀ | p | c | M | ℓ₀ | s | λ | t_hi | U | V | Q | d | β | η_min | +| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | +| p16 | .99697984 | 3/5 | 400 | 768 | 140 | 3/100 | 3/25 | .9974293 | .9848 | .9609 | 1.0017 | 1.04 | .5632 | .982 | +| p7 | .99731352 | 1/10 | 40 | 288 | 44 | 3/25 | 2/5 | .9976537 | .9436 | .7921 | 1.0012 | 1.72 | .321 | .9845 | + +**Why H drops.** The final funding (17) pays `ln A0 = (1−t₀) ln n₀ − p ln(c + ln n₀)` against +`(z − t₀) H ln 2`. A much smaller ordinary base `n₀ = m·M^{ℓ₀}` shrinks `A0`. Here `n₀` is `145·768^{140}` +instead of `145·1024^{650}` for p16, and `121·288^{44}` instead of `121·256^{100}` for p7. Larger `p` +and `c`, a smaller `s` and a larger `λ` keep the recurrence inequality (20) satisfied at that smaller `ℓ₀`. + +## Certification (`verify.py`, about 6 minutes) + +For each witness, separately written code re-certifies every finite gate of #4483's PROOF.md with its own +certified interval arithmetic (from my #4529): + +- the guards (18); +- the mirror guard (4) on every window and each of 20 t-slices; +- the recurrence inequality (20); +- the final funding (17). + +| | D (lower) | required | worst mirror ratio | τ(n₀) ≤ t_hi | final margin | +| --- | ---: | ---: | ---: | --- | ---: | +| p16 | 0.05144604 | 0.04297994 | 0.56312 | 0.9974292421 ≤ .9974293 | 0.00297292 | +| p7 | 0.02373829 | 0.02336096 | 0.32098 | 0.9976536953 ≤ .9976537 | 0.00011386 | + +At `H − 10⁶` each witness fails only the final funding, so each H is least at million granularity. Each +witness is also accepted by **#4483's own `compiler.certify`** on main. + +## Not covered + +- #4483's theorem itself, and its native and outer premises. The consumer points are unchanged because the + uniform saving is unchanged. +- Global optimality of the geometry. These are scan results, not optima. +- The native4453 witnesses, which were not retuned. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/adaptive-witness-retune --check-only +python3.12 -B scripts/research_package.py --package research/adaptive-witness-retune +python3.12 -B research/rank-convergence/compiler.py research/adaptive-witness-retune/WITNESS-p16.json +``` + +## Open next questions + +1. **How far can `H` fall?** + - *Why it matters:* the exponent of the explicit rank for κ = 0.00302015. + - *First step:* include `a, b > 1` and non-power-of-two `M`, and optimize `ℓ₀` jointly with the guards. + The binding constraint is (20) at small `ℓ₀`. +2. **Retune the native4453 witnesses the same way.** + +## Credit + +- The theorem, the compiler and the baseline witnesses are zxv's (#4483). +- The profiles come from #4470 / #4479 (p16) and the p7 lineage. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/adaptive-witness-retune/SOURCES.json b/research/adaptive-witness-retune/SOURCES.json new file mode 100644 index 0000000000..6042f44416 --- /dev/null +++ b/research/adaptive-witness-retune/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "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" + }, + { + "path": "research/compact-joint-compiler/arithmetic/RESULT.json", + "usage": "input", + "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff", + "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" + }, + { + "path": "research/higher-moment-strictification/RESULT.json", + "usage": "input", + "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a", + "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156" + }, + { + "path": "research/rank-convergence/BENCHMARKS.json", + "usage": "input", + "git_blob": "bc58c96abda014c28de91eca3ff10a7d4ec30b32", + "sha256": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850" + }, + { + "path": "research/rank-convergence/compiler.py", + "usage": "input", + "git_blob": "2a3bfcb3b3700a3e7b4f339084ba5a5a1a1996da", + "sha256": "71e8fc45ee3a22f8197fdb023c538f1f55730e389c982b8cab3586ddc8217b5f" + }, + { + "path": "research/rank-convergence/intervals.py", + "usage": "input", + "git_blob": "f3d990ab639ee49424226c202c92b9e1f390dcff", + "sha256": "91d079f43a082c3c23b76b8eb482066d0aeffe73de9fde0137ee033cf3b32250" + } + ] +} diff --git a/research/adaptive-witness-retune/TASK.json b/research/adaptive-witness-retune/TASK.json new file mode 100644 index 0000000000..e92df77597 --- /dev/null +++ b/research/adaptive-witness-retune/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "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": "Sharper certified witnesses for #4483's adaptive-height compiler (p16, p7) at unchanged uniform saving and kappa.", + "scope_change_reason": "Follow-up to my certified check of #4483 (#4529).", + "bottleneck_link": "Smaller explicit sufficient rank for the kappa 0.00302015 construction under review.", + "budget_minutes": 60, + "stop_rule": "Stop at certified witnesses from a parameter scan.", + "outcome": "completed", + "evidence": "p16 H 2.8e9 -> 1.587e9 (1.764x); p7 H 3.04e9 -> 2.253e9 (1.349x); certified by own interval checker and by #4483's compiler.certify; H-1e6 fails.", + "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": "How far can H fall?", + "why_it_matters": "Explicit rank exponent for kappa 0.00302015.", + "first_step": "Allow a,b>1 and other M; optimize ell0 with guards.", + "blocked_by": "None." + } + ] +} diff --git a/research/adaptive-witness-retune/VERIFY.json b/research/adaptive-witness-retune/VERIFY.json new file mode 100644 index 0000000000..dde8cf54f1 --- /dev/null +++ b/research/adaptive-witness-retune/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/compact-joint-compiler/arithmetic/RESULT.json", + "research/higher-moment-strictification/RESULT.json", + "research/rank-convergence/BENCHMARKS.json", + "research/rank-convergence/compiler.py", + "research/rank-convergence/intervals.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Two retuned #4483 witnesses (p16 H=1,587,000,000; p7 H=2,253,000,000) at unchanged uniform saving and kappa: certified guards (18), mirror (4), recurrence (20), funding (17); H-1e6 fails; #4483 compiler.certify accepts both." + } + ] +} diff --git a/research/adaptive-witness-retune/WITNESS-p16.json b/research/adaptive-witness-retune/WITNESS-p16.json new file mode 100644 index 0000000000..8e25146811 --- /dev/null +++ b/research/adaptive-witness-retune/WITNESS-p16.json @@ -0,0 +1,24 @@ +{ + "a": 1, + "b": 1, + "lambda": "3/25", + "mirror_slices": 20, + "t0": ".99697984", + "t_upper": ".9974293", + "p": "3/5", + "c": "400", + "s": "3/100", + "height_base": 768, + "ell0": 140, + "guards": { + "U": ".9848", + "V": ".9609", + "Q": "1.0017", + "d": "1.04", + "beta": ".5632", + "eta": ".982" + }, + "uniform_saving": "471898442219/156250001562500", + "kappa": ".00302015", + "H": 1587000000 +} diff --git a/research/adaptive-witness-retune/WITNESS-p7.json b/research/adaptive-witness-retune/WITNESS-p7.json new file mode 100644 index 0000000000..c76ac7320b --- /dev/null +++ b/research/adaptive-witness-retune/WITNESS-p7.json @@ -0,0 +1,24 @@ +{ + "a": 1, + "b": 1, + "lambda": "2/5", + "mirror_slices": 20, + "t0": ".99731352", + "t_upper": ".9976537", + "p": "1/10", + "c": "40", + "s": "3/25", + "height_base": 288, + "ell0": 44, + "guards": { + "U": ".9436", + "V": ".7921", + "Q": "1.0012", + "d": "1.72", + "beta": ".321", + "eta": ".9845" + }, + "uniform_saving": "376107/140000000", + "kappa": ".00268647", + "H": 2253000000 +} diff --git a/research/adaptive-witness-retune/verify.py b/research/adaptive-witness-retune/verify.py new file mode 100644 index 0000000000..3f1a153b42 --- /dev/null +++ b/research/adaptive-witness-retune/verify.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +"""Sharper witnesses for #4483's adaptive-height compiler at unchanged uniform saving and kappa. + + p16 (kappa .00302015): H = 1,587,000,000 instead of 2,800,000,000 (t0 .99697984, p 3/5, c 400, M 768, ell0 140, + s 3/100, lambda 3/25; guards U .9848, V .9609, Q 1.0017, d 1.04, beta .5632, eta .982, t_hi .9974293) + p7 (kappa .00268647): H = 2,253,000,000 instead of 3,040,000,000 (t0 .99731352, p 1/10, c 40, M 288, ell0 44, + s 3/25, lambda 2/5; guards U .9436, V .7921, Q 1.0012, d 1.72, beta .321, eta .9845, t_hi .9976537) +Each witness keeps #4483's raw profile, uniform saving and kappa; only the free geometry changes. This verifier +re-certifies every finite gate of #4483's PROOF.md (guards (18), mirror (4), recurrence (20), funding (17)) with its +own interval arithmetic (from research/rank-convergence-gates), shows H - 10^6 fails (17), and cross-checks each +witness with #4483's own compiler.certify on main. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +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 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 rat(x): + return Q(x) + + +def ln_real(lo, hi): + """certified ln on a positive rational interval [lo, hi]""" + return lnq(Q(lo))[0], lnq(Q(hi))[1] + + +def expi(lo, hi): + """certified exp on an interval, reducing large |x| by halving and squaring""" + k = 0 + while max(abs(lo), abs(hi)) > Q(1, 2): + lo, hi, k = lo / 2, hi / 2, k + 1 + a, b = exp_bounds(lo, hi) + for _ in range(k): + a, b = down(a * a), up(b * b) + return a, b + + +def mgf(h, t): + """certified sum_k w k^t""" + lo = hi = Q(0) + for k, w in h.items(): + l = ln(k) + a, b = expi(t * l[0], t * l[1]) + lo, hi = lo + w * a, hi + w * b + return lo, hi + + +def logmean(h, t): + nlo = nhi = Q(0) + for k, w in h.items(): + l = ln(k) + a, b = expi(t * l[0], t * l[1]) + nlo, nhi = nlo + w * a * l[0], nhi + w * b * l[1] + dlo, dhi = mgf(h, t) + return nlo / dhi, nhi / dlo + + +def profile(case): + d = json.loads((ROOT / case["source"]).read_text(encoding="utf-8")) + if case["profile_key"]: + d = d[case["profile_key"]] + return {int(k): v for k, v in d["targets"].items()}, {int(k): v for k, v in d["paid"].items()} + + +def check(case): + T, P = profile(case) + w, g = case["witness"], case["witness"]["guards"] + t0, th, p, c, s, lam = (rat(w[x]) for x in ("t0", "t_upper", "p", "c", "s", "lambda")) + a, b, M, ell0, slices = w["a"], w["b"], w["height_base"], w["ell0"], w["mirror_slices"] + U, V, Qg, d, beta, eta = (rat(g[x]) for x in ("U", "V", "Q", "d", "beta", "eta")) + gg, m = a + b, max(T) + need(min(T) >= 2 and max(P) < m and 1 in P, "profile premises") + need(mgf(T, t0)[0] > mgf(P, t0)[1], "T_t0 > P_t0") + need(logmean(T, t0)[0] - logmean(P, th)[1] >= d, "derivative guard d") + need(mgf(T, th)[1] / mgf(P, t0)[0] <= Qg, "Q guard") + lnM = ln(M) + Ms = expi(-s * lnM[1], -s * lnM[0])[1] + rT, rP = mgf(T, th + s)[1] / mgf(T, th)[0], mgf(P, th + s)[1] / mgf(P, th)[0] + need(Ms * rT ** a * rP ** b <= U, "U guard") + Ml = expi(lam * lnM[0], lam * lnM[1])[1] + need(Ml * (mgf(T, th - lam)[1] / mgf(P, t0)[0]) ** gg <= V, "V guard") + need(mgf(T, t0 + s)[0] / mgf(T, t0)[1] >= mgf(P, th + s)[1] / mgf(P, th)[0], "ratio ordering") + lm = ln(m) + need(t0 * expi((t0 - 1) * lm[1], (t0 - 1) * lm[0])[0] >= eta, "eta_min <= t0 m^(t0-1)") + need(c >= p / (1 - t0), "c >= p/(1-t0)") + ln_n0 = (lm[0] + ell0 * lnM[0], lm[1] + ell0 * lnM[1]) + tau_hi = t0 + p / (c + ln_n0[0]) + need(tau_hi <= th, "tau(n0) <= t_hi") + # mirror windows over t-slices + pts = sorted({Q(1, x) for x in list(T) + list(P)}) + worst = Q(0) + for i in range(slices): + ta, tb = t0 + (th - t0) * i / slices, t0 + (th - t0) * (i + 1) / slices + pw = {} + for r in P: + for k in T: + l = ln(r * k) + pw[r, k] = (expi(ta * l[0], ta * l[1])[0], expi(tb * l[0], tb * l[1])[1]) + for lo, hi in zip(pts, pts[1:]): + mid = (lo + hi) / 2 + E = sum(P[r] * T[k] * pw[r, k][1] for r in P for k in T if r > k and Q(1, r) < mid <= Q(1, k)) + S = sum(P[r] * T[k] * pw[r, k][0] for r in P for k in T if k > r and Q(1, k) < mid <= Q(1, r)) + if E: + need(S > 0 and E <= beta * S, f"mirror window slice {i}") + worst = max(worst, E / S) + # recurrence inequality (20) + l2 = ln(2) + den_hi = c + lm[1] + (ell0 + 1) * lnM[1] + l2[1] + x_lo = d * p * (a * ell0 + 1) / den_hi + e_lo = expi(x_lo, x_lo)[0] + D_lo = (1 - U ** ell0) * (e_lo - 1) - Qg * Ml * V ** ell0 + req = (1 - eta) / (eta - beta) + need(D_lo >= req, "recurrence inequality (20)") + # final funding (17) + z = 1 - rat(w["uniform_saving"]) + H = w["H"] + lnN = (H * l2[0], H * l2[1]) + lnc0 = ln_real(down(c + ln_n0[0]), up(c + ln_n0[1])) + lnA0_hi = (1 - t0) * ln_n0[1] - p * lnc0[0] + lncN = ln_real(down(c + lnN[0]), up(c + lnN[1])) + margin_lo = (z - t0) * lnN[0] - (lnA0_hi + p * lncN[1]) + need(margin_lo > 0, "final funding (17)") + return {"D_lower": f"{float(D_lo):.8f}", "required": f"{float(req):.8f}", "mirror_worst": f"{float(worst):.5f}", + "tau_n0_upper": f"{float(tau_hi):.10f}", "t_hi": str(w["t_upper"]), "final_margin_lower": f"{float(margin_lo):.8f}"} + + +def main(): + for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]: + need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"]) + cases = {c["name"]: c for c in json.loads((ROOT / "research/rank-convergence/BENCHMARKS.json").read_text(encoding="utf-8"))["cases"]} + spec = importlib.util.spec_from_file_location("rank_convergence_compiler", ROOT / "research/rank-convergence/compiler.py") + comp = importlib.util.module_from_spec(spec) + spec.loader.exec_module(comp) + out = {} + for name, old_H, new_H in (("p16", 2800000000, 1587000000), ("p7", 3040000000, 2253000000)): + base = cases[name] + need(base["witness"]["H"] == old_H, f"#4483's {name} witness") + witness = json.loads((HERE / f"WITNESS-{name}.json").read_text(encoding="utf-8")) + need(witness["uniform_saving"] == base["witness"]["uniform_saving"] and witness["kappa"] == base["witness"]["kappa"], + f"{name}: same uniform saving and kappa") + need(witness["H"] == new_H, f"{name}: new H") + case = dict(base, witness=witness) + res = check(case) + smaller = json.loads(json.dumps(case)) + smaller["witness"]["H"] = new_H - 10 ** 6 + try: + check(smaller) + need(False, "H - 10^6 must fail") + except AssertionError as exc: + need("(17)" in str(exc), f"{name}: H - 10^6 fails only the final funding") + src = json.loads((ROOT / base["source"]).read_text(encoding="utf-8")) + if base["profile_key"]: + src = src[base["profile_key"]] + theirs = comp.certify({"targets": src["targets"], "paid": src["paid"]}, witness) + need(theirs["status"] == "PASS_ADAPTIVE_HEIGHT_DIRECT_COMPILER" and theirs["H"] == new_H, f"{name}: #4483 compiler") + out[name] = {"H_new": new_H, "H_4483": old_H, "exponent_ratio": round(old_H / new_H, 4), "gates": res} + print(json.dumps({"status": "PASS_ADAPTIVE_WITNESS_RETUNE", "witnesses": out, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main()) From e9e9f244108ab4c21f0293cbfca9cfc3206e772a Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 11:38:11 +0700 Subject: [PATCH 2/2] Add retuned native4453 witnesses (713,000,000 and 2,580,000,000); split verifier into two commands Co-Authored-By: Claude Opus 5.5 --- research/adaptive-witness-retune/README.md | 16 +++++++++---- research/adaptive-witness-retune/TASK.json | 4 ++-- research/adaptive-witness-retune/VERIFY.json | 17 +++++++++++-- .../WITNESS-native4453-matched-uniform.json | 24 +++++++++++++++++++ .../WITNESS-native4453.json | 24 +++++++++++++++++++ research/adaptive-witness-retune/verify.py | 9 ++++++- 6 files changed, 84 insertions(+), 10 deletions(-) create mode 100644 research/adaptive-witness-retune/WITNESS-native4453-matched-uniform.json create mode 100644 research/adaptive-witness-retune/WITNESS-native4453.json diff --git a/research/adaptive-witness-retune/README.md b/research/adaptive-witness-retune/README.md index 252d1871ef..c19acbfc71 100644 --- a/research/adaptive-witness-retune/README.md +++ b/research/adaptive-witness-retune/README.md @@ -1,4 +1,4 @@ -# Sharper witnesses for #4483: p16 rank `2^1587000000`, p7 rank `2^2253000000` +# Sharper witnesses for #4483: p16 rank `2^1587000000`, native4453 `2^713000000`, p7 `2^2253000000` **Claim type:** a compiler improvement with certified finite witnesses. **No new κ.** It uses zxv's [#4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483) theorem unchanged: the adaptive-height @@ -12,23 +12,27 @@ uniform saving and κ, and changes only the free geometry of the witness: `p`, ` | --- | ---: | ---: | ---: | ---: | | p16 (#4470) | 0.00302015 | 2,800,000,000 | **1,587,000,000** | **1.764×** | | p7 | 0.00268647 | 3,040,000,000 | **2,253,000,000** | 1.349× | +| native4453 (#4453) | 0.00300120 | 1,300,000,000 | **713,000,000** | **1.823×** | +| native4453, matched uniform | 0.00300120 | 4,300,000,000 | **2,580,000,000** | 1.667× | Here the sufficient uniform rank is `N = 2^H`. Against p16's pre-#4483 rank `2^558100005581`, the new exponent is about 352× smaller. -The witnesses are `WITNESS-p16.json` and `WITNESS-p7.json`: +The witnesses are `WITNESS-p16.json`, `WITNESS-p7.json`, `WITNESS-native4453.json` and +`WITNESS-native4453-matched-uniform.json`: | | t₀ | p | c | M | ℓ₀ | s | λ | t_hi | U | V | Q | d | β | η_min | | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | | p16 | .99697984 | 3/5 | 400 | 768 | 140 | 3/100 | 3/25 | .9974293 | .9848 | .9609 | 1.0017 | 1.04 | .5632 | .982 | | p7 | .99731352 | 1/10 | 40 | 288 | 44 | 3/25 | 2/5 | .9976537 | .9436 | .7921 | 1.0012 | 1.72 | .321 | .9845 | +| native4453 (both) | 29909963/30000000 | 2/5 | 200 | 768 | 140 | 1/20 | 3/20 | .9973512 | .9817 | .9417 | 1.0013 | 1.02 | .5743 | .982 | **Why H drops.** The final funding (17) pays `ln A0 = (1−t₀) ln n₀ − p ln(c + ln n₀)` against `(z − t₀) H ln 2`. A much smaller ordinary base `n₀ = m·M^{ℓ₀}` shrinks `A0`. Here `n₀` is `145·768^{140}` instead of `145·1024^{650}` for p16, and `121·288^{44}` instead of `121·256^{100}` for p7. Larger `p` and `c`, a smaller `s` and a larger `λ` keep the recurrence inequality (20) satisfied at that smaller `ℓ₀`. -## Certification (`verify.py`, about 6 minutes) +## Certification (`verify.py`, two registered commands, about 6 minutes each) For each witness, separately written code re-certifies every finite gate of #4483's PROOF.md with its own certified interval arithmetic (from my #4529): @@ -42,6 +46,8 @@ certified interval arithmetic (from my #4529): | --- | ---: | ---: | ---: | --- | ---: | | p16 | 0.05144604 | 0.04297994 | 0.56312 | 0.9974292421 ≤ .9974293 | 0.00297292 | | p7 | 0.02373829 | 0.02336096 | 0.32098 | 0.9976536953 ≤ .9976537 | 0.00011386 | +| native4453 | 0.04714719 | 20/453 ≈ 0.04415 | 0.57424 | 0.9973511396 ≤ .9973512 | 0.00134278 | +| native4453, matched | 0.04714719 | 20/453 | 0.57424 | same | 0.00116679 | At `H − 10⁶` each witness fails only the final funding, so each H is least at million granularity. Each witness is also accepted by **#4483's own `compiler.certify`** on main. @@ -51,7 +57,6 @@ witness is also accepted by **#4483's own `compiler.certify`** on main. - #4483's theorem itself, and its native and outer premises. The consumer points are unchanged because the uniform saving is unchanged. - Global optimality of the geometry. These are scan results, not optima. -- The native4453 witnesses, which were not retuned. ## Reproduce @@ -67,7 +72,8 @@ python3.12 -B research/rank-convergence/compiler.py research/adap - *Why it matters:* the exponent of the explicit rank for κ = 0.00302015. - *First step:* include `a, b > 1` and non-power-of-two `M`, and optimize `ℓ₀` jointly with the guards. The binding constraint is (20) at small `ℓ₀`. -2. **Retune the native4453 witnesses the same way.** +2. **Allowing layer splits `a, b > 1` gives only about 3% more for p16 in a float scan.** The gain comes + from `n₀`, not from the layer split. ## Credit diff --git a/research/adaptive-witness-retune/TASK.json b/research/adaptive-witness-retune/TASK.json index e92df77597..5b33725379 100644 --- a/research/adaptive-witness-retune/TASK.json +++ b/research/adaptive-witness-retune/TASK.json @@ -80,13 +80,13 @@ ] }, "scope_status": "refined", - "actual_scope": "Sharper certified witnesses for #4483's adaptive-height compiler (p16, p7) at unchanged uniform saving and kappa.", + "actual_scope": "Sharper certified witnesses for #4483's adaptive-height compiler (p16, p7, native4453 x2) at unchanged uniform saving and kappa.", "scope_change_reason": "Follow-up to my certified check of #4483 (#4529).", "bottleneck_link": "Smaller explicit sufficient rank for the kappa 0.00302015 construction under review.", "budget_minutes": 60, "stop_rule": "Stop at certified witnesses from a parameter scan.", "outcome": "completed", - "evidence": "p16 H 2.8e9 -> 1.587e9 (1.764x); p7 H 3.04e9 -> 2.253e9 (1.349x); certified by own interval checker and by #4483's compiler.certify; H-1e6 fails.", + "evidence": "p16 H 2.8e9 -> 1.587e9 (1.764x); native4453 1.3e9 -> 7.13e8 (1.823x); native4453 matched 4.3e9 -> 2.58e9 (1.667x); p7 3.04e9 -> 2.253e9 (1.349x); certified by own interval checker and by #4483's compiler.certify; H-1e6 fails.", "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/adaptive-witness-retune/VERIFY.json b/research/adaptive-witness-retune/VERIFY.json index dde8cf54f1..0fa02756bd 100644 --- a/research/adaptive-witness-retune/VERIFY.json +++ b/research/adaptive-witness-retune/VERIFY.json @@ -15,10 +15,23 @@ "argv": [ "{python}", "-B", - "{package}/verify.py" + "{package}/verify.py", + "p16", + "p7" ], "timeout_seconds": 600, - "checks": "Two retuned #4483 witnesses (p16 H=1,587,000,000; p7 H=2,253,000,000) at unchanged uniform saving and kappa: certified guards (18), mirror (4), recurrence (20), funding (17); H-1e6 fails; #4483 compiler.certify accepts both." + "checks": "Retuned #4483 witnesses at unchanged uniform saving and kappa (p16 1,587,000,000; p7 2,253,000,000; native4453 713,000,000; native4453 matched 2,580,000,000): certified guards (18), mirror (4), recurrence (20), funding (17); H-1e6 fails; #4483 compiler.certify accepts." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "native4453", + "native4453-matched-uniform" + ], + "timeout_seconds": 600, + "checks": "Retuned #4483 witnesses at unchanged uniform saving and kappa (p16 1,587,000,000; p7 2,253,000,000; native4453 713,000,000; native4453 matched 2,580,000,000): certified guards (18), mirror (4), recurrence (20), funding (17); H-1e6 fails; #4483 compiler.certify accepts." } ] } diff --git a/research/adaptive-witness-retune/WITNESS-native4453-matched-uniform.json b/research/adaptive-witness-retune/WITNESS-native4453-matched-uniform.json new file mode 100644 index 0000000000..d009fcc5e0 --- /dev/null +++ b/research/adaptive-witness-retune/WITNESS-native4453-matched-uniform.json @@ -0,0 +1,24 @@ +{ + "a": 1, + "b": 1, + "lambda": "3/20", + "mirror_slices": 20, + "t0": "29909963/30000000", + "t_upper": ".9973512", + "p": "2/5", + "c": "200", + "s": "1/20", + "height_base": 768, + "ell0": 140, + "guards": { + "U": ".9817", + "V": ".9417", + "Q": "1.0013", + "d": "1.02", + "beta": ".5743", + "eta": ".982" + }, + "uniform_saving": "105043/35000000", + "kappa": ".00300120", + "H": 2580000000 +} diff --git a/research/adaptive-witness-retune/WITNESS-native4453.json b/research/adaptive-witness-retune/WITNESS-native4453.json new file mode 100644 index 0000000000..36beabf369 --- /dev/null +++ b/research/adaptive-witness-retune/WITNESS-native4453.json @@ -0,0 +1,24 @@ +{ + "a": 1, + "b": 1, + "lambda": "3/20", + "mirror_slices": 20, + "t0": "29909963/30000000", + "t_upper": ".9973512", + "p": "2/5", + "c": "200", + "s": "1/20", + "height_base": 768, + "ell0": 140, + "guards": { + "U": ".9817", + "V": ".9417", + "Q": "1.0013", + "d": "1.02", + "beta": ".5743", + "eta": ".982" + }, + "uniform_saving": "525213/175000000", + "kappa": ".00300120", + "H": 713000000 +} diff --git a/research/adaptive-witness-retune/verify.py b/research/adaptive-witness-retune/verify.py index 3f1a153b42..7665ff7281 100644 --- a/research/adaptive-witness-retune/verify.py +++ b/research/adaptive-witness-retune/verify.py @@ -5,6 +5,9 @@ s 3/100, lambda 3/25; guards U .9848, V .9609, Q 1.0017, d 1.04, beta .5632, eta .982, t_hi .9974293) p7 (kappa .00268647): H = 2,253,000,000 instead of 3,040,000,000 (t0 .99731352, p 1/10, c 40, M 288, ell0 44, s 3/25, lambda 2/5; guards U .9436, V .7921, Q 1.0012, d 1.72, beta .321, eta .9845, t_hi .9976537) + native4453 (kappa .00300120): H = 713,000,000 instead of 1,300,000,000, and the matched-uniform case + 2,580,000,000 instead of 4,300,000,000 (t0 29909963/30000000, p 2/5, c 200, M 768, ell0 140, s 1/20, + lambda 3/20; guards U .9817, V .9417, Q 1.0013, d 1.02, beta .5743, eta .982, t_hi .9973512) Each witness keeps #4483's raw profile, uniform saving and kappa; only the free geometry changes. This verifier re-certifies every finite gate of #4483's PROOF.md (guards (18), mirror (4), recurrence (20), funding (17)) with its own interval arithmetic (from research/rank-convergence-gates), shows H - 10^6 fails (17), and cross-checks each @@ -229,7 +232,11 @@ def main(): comp = importlib.util.module_from_spec(spec) spec.loader.exec_module(comp) out = {} - for name, old_H, new_H in (("p16", 2800000000, 1587000000), ("p7", 3040000000, 2253000000)): + wanted = set(sys.argv[1:]) + for name, old_H, new_H in (("p16", 2800000000, 1587000000), ("p7", 3040000000, 2253000000), + ("native4453", 1300000000, 713000000), ("native4453-matched-uniform", 4300000000, 2580000000)): + if wanted and name not in wanted: + continue base = cases[name] need(base["witness"]["H"] == old_H, f"#4483's {name} witness") witness = json.loads((HERE / f"WITNESS-{name}.json").read_text(encoding="utf-8"))