From eb80ed386cd3b6442d2cca012ea24c47768b5d7e Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 10:06:36 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20recount=20#4505's=20installed?= =?UTF-8?q?=20adapters:=20one=20logically=20identical=20segment,=20allowan?= =?UTF-8?q?ce=20=E2=88=92100=20per=20orientation=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/native-splice-recount/README.md | 62 ++++++++++++ research/native-splice-recount/SOURCES.json | 30 ++++++ research/native-splice-recount/TASK.json | 100 +++++++++++++++++++ research/native-splice-recount/VERIFY.json | 21 ++++ research/native-splice-recount/verify.py | 105 ++++++++++++++++++++ 5 files changed, 318 insertions(+) create mode 100644 research/native-splice-recount/README.md create mode 100644 research/native-splice-recount/SOURCES.json create mode 100644 research/native-splice-recount/TASK.json create mode 100644 research/native-splice-recount/VERIFY.json create mode 100644 research/native-splice-recount/verify.py diff --git a/research/native-splice-recount/README.md b/research/native-splice-recount/README.md new file mode 100644 index 0000000000..1a672a3dd2 --- /dev/null +++ b/research/native-splice-recount/README.md @@ -0,0 +1,62 @@ +# Independent recount of #4505: the installed borrowed adapters + +**Claim type:** an independent logical recount by separately written code. **No new κ.** It covers +Dugongue's [#4505](https://github.com/CrocSwap/integer-mult-bounds/pull/4505). That PR installs #4502's +borrowed rank-one adapters into the complete THREE-base native word and reports a scalar-allowance saving of +100 per orientation. + +## What is checked, in both orientations + +The verifier reads the pinned original native word and #4505's `NATIVE.json`. + +1. **Nothing paid moves.** Every non-scalar event (climb, center, warp, adapter, residual adapter, phase) is + identical and in the same order. So the paid profile `{1:2487, 2:713, 3:232, 4:102, 5:28}`, the + transports and the warps are unchanged by construction. +2. **The change is local and logically exact.** All differences lie inside **one** maximal scalar segment: + the same segment (index 4,984) in both orientations, with 4,208 scalars before and 4,210 after. Replaying + ADD, SCALE, CLEAR and COPY as exact rational linear maps, the old and new segments have the **identical + effect on all 411 fields they touch**. Borrowed fields are therefore restored, and no field is left dirty. +3. **The tariff.** The scalar allowance is re-implemented from its stated rule: + + | Operation | Allowance | + | --- | --- | + | CLEAR, COPY | 2 | + | dyadic unit SCALE | `2(|bitlen n − bitlen d| + [q<0])` | + | ADD | `2(3 + bitlen n − 1 + popcount n + bitlen d − 1)` | + + It gives + + | Orientation | Original | Rewritten | Saving | + | --- | ---: | ---: | ---: | + | forward | 158,120 | 158,020 | 100 | + | backward | 158,168 | 158,068 | 100 | + + This matches #4505. + +## Not covered + +- Physical frames, phases and the prefix envelope. #4505's own retained-interpreter replay covers those. +- Any cost model beyond the stated scalar tariff. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/native-splice-recount --check-only +python3.12 -B scripts/research_package.py --package research/native-splice-recount +``` + +The verifier prints `PASS_NATIVE_SPLICE_RECOUNT` in about a second, using only the standard library. + +## Open next questions + +1. **Can the same segment-level linear-map comparison audit #4510's suffix error weights?** + - *First step:* propagate a unit defect through each scalar event with the same free-word replay, and + compare with #4510's 1,328 δ forward and 4,879 δ backward totals. + +## Credit + +- The adapters and the installer are Dugongue's (#4502, #4505). +- The native word comes from the retained THREE-base lineage. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/native-splice-recount/SOURCES.json b/research/native-splice-recount/SOURCES.json new file mode 100644 index 0000000000..7a2e438cf2 --- /dev/null +++ b/research/native-splice-recount/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "usage": "input", + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39" + }, + { + "path": "research/native-splice-replay/NATIVE.json", + "usage": "input", + "git_blob": "8e8fcbc0c6b5d40322ed71e9de48a2687ef66e0b", + "sha256": "e71e6fdf04f73a7c3ac77afcf037e0a88bb204765aeec24f72dda7b5e527af47" + } + ] +} diff --git a/research/native-splice-recount/TASK.json b/research/native-splice-recount/TASK.json new file mode 100644 index 0000000000..12ea512460 --- /dev/null +++ b/research/native-splice-recount/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": "Independent logical recount of #4505's installed borrowed adapters.", + "scope_change_reason": "Independent coverage of a fresh native-word change.", + "bottleneck_link": "Side result: second implementation of the native scalar-allowance accounting.", + "budget_minutes": 30, + "stop_rule": "Stop at the logical recount.", + "outcome": "completed", + "evidence": "Non-scalar events identical; one changed scalar segment (4,208->4,210) with identical linear effect on 411 fields; allowance saving exactly 100 per orientation.", + "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 segment-level free-word replay audit #4510's suffix error weights?", + "why_it_matters": "Independent coverage of the error budgets.", + "first_step": "Propagate unit defects through each scalar event and compare totals.", + "blocked_by": "None." + } + ] +} diff --git a/research/native-splice-recount/VERIFY.json b/research/native-splice-recount/VERIFY.json new file mode 100644 index 0000000000..dfb3be76f6 --- /dev/null +++ b/research/native-splice-recount/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/native-splice-replay/NATIVE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "#4505 recount: identical non-scalar events, one changed scalar segment with identical exact linear effect on all touched fields, scalar allowance 158,120->158,020 / 158,168->158,068 from the stated tariff." + } + ] +} diff --git a/research/native-splice-recount/verify.py b/research/native-splice-recount/verify.py new file mode 100644 index 0000000000..b516fd2c69 --- /dev/null +++ b/research/native-splice-recount/verify.py @@ -0,0 +1,105 @@ +#!/usr/bin/env python3 +"""Independent recount of #4505: borrowed rank-one adapters installed in the complete THREE-base word. + +Separately written code reads the pinned original native word and #4505's rewritten NATIVE.json and checks, in +both orientations: + * every non-scalar event (climb, center, warp, adapter, residual_adapter, phase) is identical and in the same + order, so paid profile, transports and warps are unchanged; + * all changes lie inside one maximal scalar segment, and that segment computes the identical exact linear map + on every field it touches (fields as rational combinations of their entry values; ADD/SCALE/CLEAR/COPY); + * the scalar allowance, re-implemented from the stated tariff (CLEAR/COPY 2; dyadic unit SCALE + 2(|bitlen n - bitlen d| + [q<0]); ADD 2(3 + bitlen n - 1 + popcount n + bitlen d - 1)), is 158,120 -> 158,020 + forward and 158,168 -> 158,068 backward: a saving of exactly 100 each. +This is a logical (free-word) check; physical frames and phases are #4505's own replay. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +OLD = "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz" +NEW = "research/native-splice-replay/NATIVE.json" +EXPECT = {"forward": (158120, 158020), "backward": (158168, 158068)} + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def allowance(op): + if op[0] in ("clear", "copy"): + return 2 + q = Q(op[3], op[4]) if op[0] == "add" else Q(op[2], op[3]) + n, d = abs(q.numerator), q.denominator + need(n and d & (d - 1) == 0, "nonzero dyadic scalar") + if op[0] == "scale": + need(n & (n - 1) == 0, "dyadic unit scale") + return 2 * (abs(n.bit_length() - d.bit_length()) + (q < 0)) + need(op[0] == "add", "known scalar op") + return 2 * (3 + n.bit_length() - 1 + bin(n).count("1") + d.bit_length() - 1) + + +def segments(word): + out = [[]] + for e in word: + if e[0] == "scalar": + out[-1].append(e) + else: + out.append([]) + return out + + +def linear_effect(seg): + st = {} + get = lambda f: st.setdefault(f, {f: Q(1)}) + for e in seg: + op = e[1] + if op[0] == "add": + dst, src, q = tuple(op[1]), tuple(op[2]), Q(op[3], op[4]) + v = dict(get(dst)) + for k, c in get(src).items(): + v[k] = v.get(k, 0) + q * c + st[dst] = {k: c for k, c in v.items() if c} + elif op[0] == "scale": + f, q = tuple(op[1]), Q(op[2], op[3]) + st[f] = {k: q * c for k, c in get(f).items()} + elif op[0] == "clear": + st[tuple(op[1])] = {} + elif op[0] == "copy": + st[tuple(op[1])] = dict(get(tuple(op[2]))) + else: + raise AssertionError(f"unknown scalar op {op[0]}") + return st + + +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"]) + old = json.loads(gzip.decompress((ROOT / OLD).read_bytes())) + new = json.loads((ROOT / NEW).read_bytes()) + out = {} + for o in ("forward", "backward"): + need([e for e in old[o] if e[0] != "scalar"] == [e for e in new[o] if e[0] != "scalar"], f"{o}: non-scalar events") + A, B = segments(old[o]), segments(new[o]) + need(len(A) == len(B), f"{o}: segment count") + changed = [i for i in range(len(A)) if A[i] != B[i]] + need(len(changed) == 1, f"{o}: one changed scalar segment") + i = changed[0] + ea, eb = linear_effect(A[i]), linear_effect(B[i]) + for f in set(ea) | set(eb): + need(ea.get(f, {f: Q(1)}) == eb.get(f, {f: Q(1)}), f"{o}: field {f} has the same linear effect") + cost = tuple(sum(allowance(e[1]) for e in w[o] if e[0] == "scalar") for w in (old, new)) + need(cost == EXPECT[o], f"{o}: scalar allowance {cost}") + out[o] = {"allowance": list(cost), "saving": cost[0] - cost[1], "changed_segment": i, + "segment_scalars": [len(A[i]), len(B[i])], "fields_compared": len(set(ea) | set(eb))} + print(json.dumps({"status": "PASS_NATIVE_SPLICE_RECOUNT", **out, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())