From 0a63873be8bb6a6e1ee682f46fb48be97447b2db Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 10:15:05 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20replay=20#4470's=20p16=20contro?= =?UTF-8?q?ller:=20exact=20diagonal=20for=20all=2032=20monomials,=20invoic?= =?UTF-8?q?e,=20controls=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/pr4470-controller-replay/README.md | 67 ++++++++ .../pr4470-controller-replay/SOURCES.json | 24 +++ research/pr4470-controller-replay/TASK.json | 100 ++++++++++++ research/pr4470-controller-replay/VERIFY.json | 20 +++ research/pr4470-controller-replay/verify.py | 150 ++++++++++++++++++ 5 files changed, 361 insertions(+) create mode 100644 research/pr4470-controller-replay/README.md create mode 100644 research/pr4470-controller-replay/SOURCES.json create mode 100644 research/pr4470-controller-replay/TASK.json create mode 100644 research/pr4470-controller-replay/VERIFY.json create mode 100644 research/pr4470-controller-replay/verify.py diff --git a/research/pr4470-controller-replay/README.md b/research/pr4470-controller-replay/README.md new file mode 100644 index 0000000000..af98777ac9 --- /dev/null +++ b/research/pr4470-controller-replay/README.md @@ -0,0 +1,67 @@ +# Independent Laurent replay of #4470's p16 controller + +**Claim type:** an independent literal replay by separately written code. **No new κ.** It covers the +p16 query-thinned complex controller of 1337isnot1337's +[#4470](https://github.com/CrocSwap/integer-mult-bounds/pull/4470) (conditional κ = 0.00302015). That is +the maintainers' next substantive review per `docs/research/pr-intake-checkpoint.json`. My #4478 checked +#4470's arithmetic but left this controller uncovered. + +## What is checked + +The verifier reads only `research/joint-helper-lattice/CONTROLLER.json`. Each of the 32 lines is replayed +as a linear combination of the initial lines, with exact Laurent coefficients in `Q, D_0, …, D_32`: + +| Event | Effect | +| --- | --- | +| `LOCAL` / `QUERY_SHEAR` on pair `(x, y)` (swapped when backward) | `y += Q^{−1}x` (or `y −= Q·x` backward); `LOCAL` then multiplies both lines by `D_stage` | +| `IDLE` | multiplies both lines of the pair by the selected `D_s` | +| `ADD` | adds a signed line | +| `SWAP` / `SIGNED_SWAP` | exchanges lines, with a sign | + +Results: + +1. **Event counts.** The word has 18 `LOCAL` (exactly the 18 thick stages), 15 `QUERY_SHEAR` (exactly the + thin stages), 15 `IDLE`, 90 `ADD` and 16 `SIGNED_SWAP`. +2. **The factorization.** For **every one of the 32 monomials**, `left · W_m · right` is exactly the + indicator of the declared diagonal entries equal to `m`. The central `Q` exponents are `+1` (16) and + `−1` (16), and no output credits a thin stage. +3. **The controller invoice.** + - main ranks `1 + 8·|stages|` × 112 ports: `{17…65: 448 each, 73: 224, 145: 224}`; + - whole-idle ranks `8·|stages|` × 2 lines × 112 ports: `{16…64: 448 each, 72: 224}`; + - 15 × 112 = 1,680 thin queries. + + All reproduce `CONTROLLER.json`. +4. **Controls.** Flipping one query's orientation changes the operator. Promoting a thin query to a full + stage is rejected. + +**Note.** `CONTROLLER.json`'s embedded `paid` and `targets` use the THREE-base local profile (for example +`paid[1] = 18·2487 + 1680 = 46446`). #4470's `RESULT.json` substitutes the new joint-helper profile +(`41946`). Its arithmetic is checked in #4478. + +## Not covered + +- The native word, meaning the physical contacts, phases and helper boundaries. #4504 audits the + chronological frames and local invoice. +- The BIT controller, which is unchanged from #4440. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/pr4470-controller-replay --check-only +python3.12 -B scripts/research_package.py --package research/pr4470-controller-replay +``` + +The verifier prints `PASS_PR4470_CONTROLLER_REPLAY` in about 2 seconds, using only the standard library. + +## Open next questions + +1. **An all-column native replay of #4470's patched word by a second implementation.** + - *First step:* apply `PATCH.json`'s 38/47/414 frame changes to the THREE-base word, and recount the + paid profile with nested-frame dimension gaps, as in #4475. + +## Credit + +- The controller construction is Cinna Davis's (1337isnot1337, #4440 and #4470). + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/pr4470-controller-replay/SOURCES.json b/research/pr4470-controller-replay/SOURCES.json new file mode 100644 index 0000000000..3df53e9984 --- /dev/null +++ b/research/pr4470-controller-replay/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + } + ] +} diff --git a/research/pr4470-controller-replay/TASK.json b/research/pr4470-controller-replay/TASK.json new file mode 100644 index 0000000000..0219bd7ded --- /dev/null +++ b/research/pr4470-controller-replay/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 literal Laurent replay of #4470's p16 query-thinned controller.", + "scope_change_reason": "Covers the controller part of the maintainers' next substantive review (#4470).", + "bottleneck_link": "Independent coverage of the strongest open conditional kappa claim.", + "budget_minutes": 30, + "stop_rule": "Stop at the controller; native word out of scope.", + "outcome": "completed", + "evidence": "154 events replayed; left*W*right equals the declared diagonal for all 32 monomials; central exponents 16x(+1), 16x(-1); main/idle/thin-query invoice reproduces; flipped query and promoted thin stage rejected.", + "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": "All-column native replay of #4470's patched word by a second implementation.", + "why_it_matters": "Completes independent coverage of #4470.", + "first_step": "Apply PATCH.json's frame changes and recount paid ranks via nested-frame gaps.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4470-controller-replay/VERIFY.json b/research/pr4470-controller-replay/VERIFY.json new file mode 100644 index 0000000000..c09e3dfae0 --- /dev/null +++ b/research/pr4470-controller-replay/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-helper-lattice/CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent Laurent replay of #4470's p16 controller: thick/thin stage discipline, left*W*right = declared diagonal for all 32 monomials, central exponents +-1, main/idle/thin-query invoice, two negative controls." + } + ] +} diff --git a/research/pr4470-controller-replay/verify.py b/research/pr4470-controller-replay/verify.py new file mode 100644 index 0000000000..e7318f2770 --- /dev/null +++ b/research/pr4470-controller-replay/verify.py @@ -0,0 +1,150 @@ +#!/usr/bin/env python3 +"""Independent literal Laurent replay of #4470's p16 query-thinned complex controller. + +Reads research/joint-helper-lattice/CONTROLLER.json only. Each of the 2p = 32 lines is a linear combination of the +initial lines with Laurent-polynomial coefficients in Q, D_0 .. D_(2p) (monomial = exponent tuple). Events: + LOCAL / QUERY_SHEAR (stage, pair, backward): with (x, y) = (2 pair, 2 pair + 1), swapped if backward, + y += s * Q^e * x with (e, s) = (+1, -1) if backward else (-1, +1); LOCAL then multiplies x and y by D_stage; + IDLE (pair, stages): multiply both lines of the pair by the product of D_s; + ADD (dst, src[, c]): dst += c src; SWAP / SIGNED_SWAP (x, y): (x, y) <- (y, +-x). +Checks: LOCAL stages are exactly the thick ones and QUERY_SHEAR stages the thin ones; for every monomial m, +left * W_m * right equals the indicator of the declared diagonal entries equal to m (rational, exact); central Q +exponents are +-1; no output credits a thin stage; main ranks 1 + 8|stages| x 112 ports, whole-idle ranks 8|stages| +x 2 lines x 112 ports and 15 x 112 thin queries reproduce CONTROLLER.json's invoice; flipping one query orientation +changes the operator and promoting one thin query to a full stage is rejected. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as F +import hashlib +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) + + +def replay(events, p, thick): + n, S = 2 * p, 2 * p + 1 + one = (0,) * (S + 1) + lines = [{i: {one: F(1)}} for i in range(n)] + + def mul(a, b): + return tuple(x + y for x, y in zip(a, b)) + + def scale(i, m): + lines[i] = {j: {mul(k, m): v for k, v in poly.items()} for j, poly in lines[i].items()} + + def add(dst, src, m, c): + for j, poly in lines[src].items(): + tgt = lines[dst].setdefault(j, {}) + for k, v in poly.items(): + kk = mul(k, m) + w = tgt.get(kk, 0) + c * v + if w: + tgt[kk] = w + else: + tgt.pop(kk, None) + if not tgt: + lines[dst].pop(j) + + for ev in events: + op = ev[0] + if op in ("LOCAL", "QUERY_SHEAR"): + _, stage, pair, back = ev + need((stage in thick) == (op == "LOCAL"), "LOCAL exactly on thick stages") + x, y = 2 * pair, 2 * pair + 1 + if back: + x, y = y, x + add(y, x, (1 if back else -1,) + (0,) * S, -1 if back else 1) + if op == "LOCAL": + d = (0,) + tuple(int(s == stage) for s in range(S)) + scale(x, d) + scale(y, d) + elif op == "IDLE": + _, pair, sel = ev + need(set(sel) <= thick, "idle only on thick stages") + d = (0,) + tuple(int(s in sel) for s in range(S)) + scale(2 * pair, d) + scale(2 * pair + 1, d) + elif op == "ADD": + _, dst, src, *c = ev + add(dst, src, one, c[0] if c else 1) + elif op in ("SWAP", "SIGNED_SWAP"): + _, x, y = ev + sg = -1 if op == "SIGNED_SWAP" else 1 + old = lines[x] + lines[x] = lines[y] + lines[y] = {j: {k: sg * v for k, v in poly.items()} for j, poly in old.items()} + else: + raise AssertionError("unknown event " + op) + return lines + + +def matmul(A, B): + return [[sum(A[i][k] * B[k][j] for k in range(len(B))) for j in range(len(B[0]))] for i in range(len(A))] + + +def diagonal_ok(lines, row, n): + L = [[F(x) for x in r] for r in row["boundaries"]["left"]] + R = [[F(x) for x in r] for r in row["boundaries"]["right"]] + diag = [tuple(k) for k in row["diagonal"]] + monos = {m for ln in lines for poly in ln.values() for m in poly} | set(diag) + for m in monos: + W = [[lines[i].get(j, {}).get(m, F(0)) for j in range(n)] for i in range(n)] + if matmul(matmul(L, W), R) != [[F(int(i == j and diag[i] == m)) for j in range(n)] for i in range(n)]: + return False, len(monos) + return True, len(monos) + + +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"]) + row = json.loads((ROOT / "research/joint-helper-lattice/CONTROLLER.json").read_bytes()) + p = row["pairs"] + need((row["kind"], p, row["prefix_pairs"], row["ambient_rank"]) == ("complex", 16, 7, 145), "controller parameters") + thick = {0, 2 * p, *range(1, 2 * p, 2)} + need(sorted(thick) == row["invoice"]["thick_stages"], "thick stages") + ev = row["physical_events"] + counts = Counter(e[0] for e in ev) + need(counts == Counter({"LOCAL": 18, "QUERY_SHEAR": 15, "IDLE": 15, "ADD": 90, "SIGNED_SWAP": 16}), "event counts") + ok, monos = diagonal_ok(replay(ev, p, thick), row, 2 * p) + need(ok, "left * W * right equals the declared diagonal for every monomial") + diag = [tuple(k) for k in row["diagonal"]] + need(Counter(d[0] for d in diag) == Counter({1: 16, -1: 16}), "central exponents +-1") + need(all(s in thick for d in diag for s, x in enumerate(d[1:]) if x), "no thin stage credited") + main_ranks = Counter() + for d in diag: + main_ranks[1 + 8 * sum(1 for x in d[1:] if x)] += 112 + need({str(k): v for k, v in main_ranks.items()} == row["invoice"]["main"], "main invoice") + idle = Counter() + for e in ev: + if e[0] == "IDLE": + idle[8 * len(e[2])] += 2 * 112 + need({str(k): v for k, v in idle.items()} == row["invoice"]["whole_idle"], "whole-idle invoice") + need(counts["QUERY_SHEAR"] * 112 == row["invoice"]["thin_queries"] == 1680, "thin queries 15 x 112") + bad = json.loads(json.dumps(ev)) + next(e for e in bad if e[0] == "QUERY_SHEAR")[3] = True + need(not diagonal_ok(replay(bad, p, thick), row, 2 * p)[0], "flipped query orientation rejected") + bad = json.loads(json.dumps(ev)) + i = next(k for k, e in enumerate(bad) if e[0] == "QUERY_SHEAR") + bad[i][0] = "LOCAL" + rejected = False + try: + replay(bad, p, thick) + except AssertionError as exc: + rejected = "thick" in str(exc) + need(rejected, "promoting a thin query to a full stage is rejected") + print(json.dumps({"status": "PASS_PR4470_CONTROLLER_REPLAY", "events": dict(counts), "monomials": monos, + "main_invoice": row["invoice"]["main"], "whole_idle": row["invoice"]["whole_idle"], + "thin_queries": 1680, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())