diff --git a/research/pr4326-bit-root-check/README.md b/research/pr4326-bit-root-check/README.md new file mode 100644 index 0000000000..b8e9c0ba07 --- /dev/null +++ b/research/pr4326-bit-root-check/README.md @@ -0,0 +1,77 @@ +# Independent check of #4326's BIT moment root + +**Claim type: an independent certified finite check. No new κ.** This +does not accept #4326, and it checks none of #4326's construction or caller +premises. + +## Object + +[PR #4326](https://github.com/CrocSwap/integer-mult-bounds/pull/4326) +(ai-nanachi, head `080f8c218d64c6d231ed6297987e39b7a912a4ef`) proposes a +conditional logical BIT supplier. + +- **Root.** It claims a surcharged BIT moment root strictly inside + `[1744853764761145849274, 1744853764761145849275]·10⁻²⁴`. That is 0.41562% + above PR4183's upper endpoint. +- **Majorant.** It claims `T(n,w) ≤ 200·C·n + 10⁷·C·n^(1−b)·w` at + `b = 0.00174481`. +- **Prior checks.** Its own checks are internal. No other PR or discussion + references it. + +The moment is the selected BIT moment's form: +`μ(a) = Σ n_r (r/64)^(1−a)/W + (32·64²/10¹⁶)·Σn·(1/64)^(1−a)/W`, with +`W = 28416`. + +## Results + +| Check | Result | +| --- | --- | +| Profile `{1:379872, 2:400000, 3:22464, 4:24416, 5:29376, 6:17088, 7:26496, 10:32, 42:672}` against the record | count 900,416 and rank mass 1,808,352, both equal to `RECORD.json` | +| `μ` across the claimed root bracket | `< 1` at the lower end, `> 1` at the upper end (certified) | +| `μ_1 < 199/200` (the 200C prefactor) | `μ_1 = 0.9943517737` | +| `μ_(1−b) < 1 − 10⁻⁷` (the 10⁷C prefactor) | `1 − μ_(1−b) = 1.42·10⁻⁷`, so it holds, but tightly | +| Gain over PR4183 | `0.415620%`, equal to the recorded `gain_lower` | +| Against the selected BIT saving `0.0017334270…` | `0.66%` higher | + +**Control.** The author rejects one variant: crediting the nine private +families to `W`. Under that variant the moment stays below 1 at the upper +end, so the root moves up. The bracket therefore depends on not crediting +them. + +**Not a κ change.** The selected κ is bound by the complex side, so a higher +BIT saving does not change it. + +## Not covered + +- Deriving the profile from #4326's word and remainders. The profile is + transcribed from its independent pricer and matched to the record's + aggregates. **Update:** + [#4349](https://github.com/CrocSwap/integer-mult-bounds/pull/4349) (ToikY) + has since rebuilt it from the literal word and owners. Its `full_profile` + equals the profile checked here exactly, and its idle histogram equals the + one implied by it. +- The logical supplier, fixed-tape lowering and caller premises. +- No proof-kernel check. + +## Reproduce + +```sh +python3.12 -B research/pr4326-bit-root-check/verify.py +``` + +It prints `PASS_PR4326_BIT_ROOT_CHECK` in under a second, using only the +standard library. `vendor/RECORD.json` is a byte-identical copy of #4326's +`research/bit-compact-carrier-retirement/RECORD.json` (blob `b6c69927…`); +its SHA256 is checked. The profile constant comes from +`independent_price.py` at the same head (blob `5b789483…`). + +## Open next questions + +None. The profile reconstruction asked for here is #4349; see "Not covered". + +## Credit + +The audited construction is ai-nanachi's #4326, building on Ross +Richardson's PR4183 and PR4021 and the retained BIT lineage. Prepared by +Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/pr4326-bit-root-check/SOURCES.json b/research/pr4326-bit-root-check/SOURCES.json new file mode 100644 index 0000000000..0cbf76d6e0 --- /dev/null +++ b/research/pr4326-bit-root-check/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + } + ] +} diff --git a/research/pr4326-bit-root-check/TASK.json b/research/pr4326-bit-root-check/TASK.json new file mode 100644 index 0000000000..203a49da92 --- /dev/null +++ b/research/pr4326-bit-root-check/TASK.json @@ -0,0 +1,94 @@ +{ + "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 certify #4326's surcharged BIT moment root bracket, its 200C and 10^7C majorant conditions and its gain over PR4183, from its record and profile.", + "scope_change_reason": "The card asks for independent coverage of a new paid-profile claim; #4326 had none outside its own package.", + "bottleneck_link": "#4326 raises the BIT saving above the selected supplier's; its moment claims must hold before its construction premises are worth review.", + "budget_minutes": 20, + "stop_rule": "Stop once each stated moment inequality is certified or fails.", + "outcome": "completed", + "evidence": "verify.py: moment straddles 1 across the 1e-24 bracket; mu_1 = 0.99435 < 199/200; 1 - mu_(1-b) = 1.42e-7 > 1e-7; gain over PR4183 0.415620% as recorded; profile aggregates equal RECORD.json; W+9 private-credit control moves the root.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, verifier implementation and writing; no independent human or proof-kernel review.", + "open_questions": [], + "no_open_questions_reason": "The profile reconstruction this asked for is #4349, whose rebuilt full_profile equals the checked profile." +} diff --git a/research/pr4326-bit-root-check/VERIFY.json b/research/pr4326-bit-root-check/VERIFY.json new file mode 100644 index 0000000000..6f4e246bd9 --- /dev/null +++ b/research/pr4326-bit-root-check/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Vendored RECORD.json hash; profile aggregates; certified moment bracket; 200C and 10^7C conditions; PR4183 gain; selected BIT comparison; private-credit control." + } + ] +} diff --git a/research/pr4326-bit-root-check/vendor/RECORD.json b/research/pr4326-bit-root-check/vendor/RECORD.json new file mode 100644 index 0000000000..b6c6992769 --- /dev/null +++ b/research/pr4326-bit-root-check/vendor/RECORD.json @@ -0,0 +1,54 @@ +{ + "status": "PROPOSED_CONDITIONAL_LOGICAL_BIT_SUPPLIER", + "source_head": "59a1d97a86ea82b4d62958d705709ea46d7509f1", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "moment_root": { + "lower": "872426882380572924637/500000000000000000000000", + "upper": "69794150590445833971/40000000000000000000000" + }, + "logical_b": "174481/100000000", + "logical_time": "T(n,w) <= 200 C n + 10000000 C n^(1-b) w", + "domain": "Fixed q>2^80; inherited canonical/root-coupled logicalp1 domain; R=t K^D(n) compatiblefreshrowstock.", + "ordinary_RAW": 658, + "helpers": 436, + "private_index": 658, + "query_count": 900416, + "rankmass": 1808352, + "W": 28416, + "private": 9, + "comparison": { + "PR": 4326, + "head": "09578fd3e23bc526be82c006abc5608739ac6668", + "previous_moment_upper": "871529681585030091971/500000000000000000000000", + "strict_moment_gain_lower": "897200795542832666/871529681585030091971", + "strict_logical_b_gain_over_previous_moment": "875318414969908029/871529681585030091971" + }, + "public_predecessor": { + "PR": 4183, + "head": "59a1d97a86ea82b4d62958d705709ea46d7509f1", + "upper": "434407954621501888371/250000000000000000000000", + "gain_lower": "3610973137569147895/868815909243003776742" + }, + "local_word_changed": true, + "fresh_cold_inverse_and_D0": true, + "removed_original_roles": [ + 464, + 469 + ], + "finite_positive_caps": [ + 192, + 320, + 640 + ], + "whole_kappa_changed": false, + "selected_record_changed": false, + "physical_tape_lowering_proved": false, + "publication": { + "PR": 4326, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4326", + "created_at": "2026-10-21T08:40:50Z", + "revision": "Scientific followup to the same PR; added commits do not count as a newPR." + }, + "validation_receipt": "VALIDATION.json; exact source commit, environment and actual outcomes", + "review_status": "Internal code-disjoint AI reviews; no independent human approval or maintainer acceptance claimed." +} diff --git a/research/pr4326-bit-root-check/verify.py b/research/pr4326-bit-root-check/verify.py new file mode 100644 index 0000000000..1a2b8425f6 --- /dev/null +++ b/research/pr4326-bit-root-check/verify.py @@ -0,0 +1,112 @@ +#!/usr/bin/env python3 +"""Independent certified check of #4326's BIT moment root and majorant constants. + +Standard library only; no code from #4326. The record is vendored byte-identically +(vendor/RECORD.json). The profile is transcribed from #4326's independent pricer and +cross-checked against the record's query count and rank mass. Exact rationals: ln by +atanh after reducing by powers of two, exp by Taylor with a Lagrange remainder. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +RECORD_SHA256 = "11b2446e3d714c366fe69a5c504e74fde4277d321ec3f7808c998bc1e229a180" +# research/bit-compact-carrier-retirement/independent_price.py at #4326 head 080f8c21, constant EXPECTED. +PROFILE = {1: 379872, 2: 400000, 3: 22464, 4: 24416, 5: 29376, 6: 17088, 7: 26496, 10: 32, 42: 672} +M = 64 +FALLBACK = Q(32 * M * M, 10**16) # per paid query, the surcharge of the selected BIT moment + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def atanh_ln(x, terms=45): + z = (x - 1) / (x + 1) + s = 2 * sum(z ** (2 * k + 1) / (2 * k + 1) for k in range(terms + 1)) + return s, s + 2 * z ** (2 * terms + 3) / ((2 * terms + 3) * (1 - z * z)) + + +def ln_bounds(x): + k = (x.numerator // x.denominator).bit_length() - 1 + a, b = atanh_ln(Q(2)) + c, d = atanh_ln(x / 2 ** k) + return k * a + c, k * b + d + + +def exp_bounds(y, terms=30): + s, term = Q(0), Q(1) + for k in range(terms + 1): + s += term + term = term * y / (k + 1) + return s, s + 3 * term + + +def moment(a, profile, W): + """sum_r n_r (r/M)^(1-a)/W + fallback * sum n * (1/M)^(1-a)/W, enclosed.""" + lo = hi = Q(0) + terms = list(profile.items()) + [(1, FALLBACK * sum(profile.values()))] + for r, n in terms: + if r == M: + lo, hi = lo + n, hi + n + continue + l_lo, l_hi = ln_bounds(Q(M, r)) + lo += n * Q(r, M) * exp_bounds(a * l_lo)[0] + hi += n * Q(r, M) * exp_bounds(a * l_hi)[1] + return lo / W, hi / W + + +def main(): + raw = (HERE / "vendor/RECORD.json").read_bytes() + need(hashlib.sha256(raw).hexdigest() == RECORD_SHA256, "vendored RECORD.json") + record = json.loads(raw) + W = record["W"] + need(sum(PROFILE.values()) == record["query_count"], "profile count = 900,416 paid queries") + need(sum(r * n for r, n in PROFILE.items()) == record["rankmass"], "profile rank mass = 1,808,352") + need(max(PROFILE) == 42 and W == 28416, "max child 42, W = 28416") + + lo, hi = Q(record["moment_root"]["lower"]), Q(record["moment_root"]["upper"]) + need(hi - lo == Q(1, 10**24), "adjacent 1e-24 bracket") + m_lo, m_hi = moment(lo, PROFILE, W), moment(hi, PROFILE, W) + need(m_lo[1] < 1 < m_hi[0], "moment straddles 1 across the claimed root bracket") + + b = Q(record["logical_b"]) + mu1 = moment(Q(0), PROFILE, W) + need(mu1[1] < Q(199, 200), "mu_1 < 199/200 gives the 200C linear prefactor") + mub = moment(b, PROFILE, W) + need(mub[1] < 1 - Q(1, 10**7), "mu_(1-b) < 1 - 1e-7 gives the 10^7 C prefactor") + need(b < lo, "separator below the root") + + prev = Q(record["public_predecessor"]["upper"]) + gain = (lo - prev) / prev + need(gain == Q(record["public_predecessor"]["gain_lower"]), "gain over PR4183 as recorded") + need(Q(41562, 10**7) < gain, "lower endpoint is more than 0.41562% above PR4183's upper endpoint") + + sel_path = ROOT / "research/e8-bit-p111-tuned/tune/EXPECTED.json" + pins = {row["path"]: row["sha256"] for row in json.loads((HERE / "SOURCES.json").read_text())["files"]} + need(hashlib.sha256(sel_path.read_bytes()).hexdigest() == pins["research/e8-bit-p111-tuned/tune/EXPECTED.json"], "selected BIT pin") + selected_bit = Q(json.loads(sel_path.read_text())["nine"]["bit_lower"]) + need(lo > selected_bit, "root above the selected BIT saving") + + # Control: crediting the nine private families as W (the author's rejected variant) moves the root. + need(moment(hi, PROFILE, W + record["private"])[1] < 1, "control: W + 9 private credit would shift the root up") + + print(json.dumps({ + "status": "PASS_PR4326_BIT_ROOT_CHECK", + "root_bracket": [str(lo), str(hi)], + "mu_1_upper": f"{float(mu1[1]):.10f}", + "mu_1_minus_b_gap": f"{float(1 - mub[1]):.4e}", + "gain_over_pr4183": f"{float(gain):.6%}", + "over_selected_bit": f"{float((lo - selected_bit) / selected_bit):.4%}", + "new_kappa_claimed": False, + }, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())