From 333d91cb7606f4bc783e279eb5d7769338632814 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:07:18 +0530 Subject: [PATCH 1/2] Research: certify two-XOR R420 cleanup conjugation --- research/r420-cleanup-commutation/CLAIM.json | 18 ++ research/r420-cleanup-commutation/README.md | 180 ++++++++++++++ .../r420-cleanup-commutation/VALIDATION.json | 45 ++++ .../r420-cleanup-commutation/certificate.json | 46 ++++ research/r420-cleanup-commutation/verify.py | 232 ++++++++++++++++++ 5 files changed, 521 insertions(+) create mode 100644 research/r420-cleanup-commutation/CLAIM.json create mode 100644 research/r420-cleanup-commutation/README.md create mode 100644 research/r420-cleanup-commutation/VALIDATION.json create mode 100644 research/r420-cleanup-commutation/certificate.json create mode 100644 research/r420-cleanup-commutation/verify.py diff --git a/research/r420-cleanup-commutation/CLAIM.json b/research/r420-cleanup-commutation/CLAIM.json new file mode 100644 index 0000000000..34e6d22917 --- /dev/null +++ b/research/r420-cleanup-commutation/CLAIM.json @@ -0,0 +1,18 @@ +{ + "track": "bit supplier", + "assignment_seed": 10, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "object": "PR543 R420 full-frame C cleanup, expanded into binary XORs", + "method": "Commute independent transvections and cancel identical pairs; exact symbolic replay on all dirty inputs; seed 10 selects deterministic traversal order", + "deliverable": "One finite cleanup circuit improvement or scoped negative certificate, with source pins and negative controls; no kappa claim", + "expected_finish_utc": "2026-10-13T04:59:00Z", + "coordination": "No pinned issues returned by GitHub GraphQL. Local claim; recent PR metadata checked through PR700 before recording.", + "candidate_tasks": [ + {"task": "phase-A quad synthesis", "decision": "deferred: PR691 already supplies exact synthesis on quad13"}, + {"task": "frame-zero helper sharing", "decision": "deferred: PR686 and PR694 cover single-pair and matching recipes"}, + {"task": "full-frame cleanup commutation", "decision": "selected: changes only cleanup, unlike the phase-A/B resynthesis and literal reverse cleanup in PR670/674/688/691"} + ], + "scope": "No upstream, selected certificate, forward circuit, COPY, frame, helper allocation, or assembly changes. Delegated audit stays within cleanup equivalence and its interface/accounting obligations.", + "status": "in progress" +} diff --git a/research/r420-cleanup-commutation/README.md b/research/r420-cleanup-commutation/README.md new file mode 100644 index 0000000000..85ba0da066 --- /dev/null +++ b/research/r420-cleanup-commutation/README.md @@ -0,0 +1,180 @@ +# Two fewer XORs in the R420 cleanup + +This finite bit-circuit construction replaces five cleanup XORs by three in +eumemic's PR543 R420 word. The complete local scalar ADD count falls from +26,916 to 26,914. Every source and dirty helper is restored, all register frame +paths are unchanged, and the reverse positive-prefix bound decreases. +There is no new supplier exponent or integer-multiplication kappa claim. + +The accompanying negative result closes commutation-only cancellation on this +specific cleanup: all 18 repeated-gate pairs have a noncommuting blocker. +The improvement uses an additional F2 conjugation identity. + +## Reproduce + +From the repository root, with Python 3.11 or later and its standard library: + +```sh +python3 -B research/r420-cleanup-commutation/verify.py +``` + +Expected final line: + +```text +PASS_R420_CLEANUP_CONJUGATION C=2973->2971 native_adds=26916->26914 columns=660 kappa=unchanged +``` + +The verifier checks the pinned baseline, reconstructs the candidate from +`certificate.json`, checks all 672 frames and 660 symbolic input columns, and +rejects six negative controls. It also exhausts the four-register identity on +all 16 Boolean inputs. These finite checks do not formalize the multiplication +theorem. All substantive checks remain active under `python3 -O`. + +To export the exact candidate as uncompressed JSON for downstream replay: + +```sh +python3 -B research/r420-cleanup-commutation/verify.py --emit-word /tmp/r420-cleanup.json +python3 -B research/e8-bit-carrier-skeleton/code/bit/export_records.py /tmp/r420-cleanup.json /tmp/r420-cleanup-records +``` + +The existing exporter reports 29,872 records. The candidate's canonical JSON +SHA-256 is `f87e4574addee69e4c9387f0d7139138454cf24e78e2c1358f239a52546b0abd`. +Source archive hashes are checked separately from canonical payload equality. + +## Object and exact substitution + +The base is `66849e1475c930fd7732b1a0067ffee7e1e95f60`. Its accepted conditional +result is kappa `51110230636731/31250000000000000`, or +`0.001635527380375392`, from #626 with #543. The construction and its remaining +assumptions are described in the [selected review](../../docs/research/community-k492-review.md). +This experiment uses the selected bit word from #543 at +`2065fe4f72a914d907f1046603f5a36f17018535`, not a larger pending PR claim. + +Expand each C gate's source list in its stored order into binary gates +`(destination, source)`. Indices below are zero-based in that original stream. +Every C gate has full-frame id 1. + +| Gate | Positions | Operation | +|---|---|---| +| A1 | 714, 1321 | helper 616 ^= helper 530 | +| A2 | 718, 1320 | helper 616 ^= helper 540 | +| B | 1071 | helper 466 ^= helper 616 | + +For each Ai, B is the only noncommuting gate strictly between its two copies. +A1 and A2 commute with each other. Commute the Ai copies toward B to obtain +`A1 A2 B A2 A1`. On the four registers this sequence leaves 616, 530 and 540 +unchanged and sends 466 to `466 + 616 + 530 + 540` over F2. It therefore equals +the three gates `B`, `(466,530)`, `(466,540)`. + +Delete original offsets 714, 718, 1320 and 1321. Insert the two correction gates +immediately after original offset 1071. All other binary gates retain their +order. The certificate records this complete construction. Expanding +multi-source gates changes the number of JSON records; counts here always +refer to binary XORs or exported native records, not JSON gate records. + +## Interface and complete local cost + +The historical [PR543 checker](../e8-bit-r420/code/xcheck.py) requires C to be +the literal reverse of the non-target gates in A and B. This candidate fails +that structural H4 check as expected. The original checker is unchanged. + +Use H4-prime instead: C touches only source/helper registers at the full frame, +each such register finishes at the full frame, and C induces the inverse of +the raw source/helper map U. The [PR543 interface proof](../e8-bit-r420/README.md) +then applies directly: the raw word sends `(z,y)` to `(Uz,y+Jx+Ks)`, and C sends +that to `(z,y+Jx+Ks)`. D, J, K and the target map are unchanged. Exact matrix +equality to the original cleanup establishes H4-prime for arbitrary helper +contents. The verifier reports the original H4 failure and checks H4-prime; +it does not weaken or patch the predecessor checker. + +| Complete local charge | Original | Candidate | +|---|---:|---:| +| Binary cleanup ADDs | 2,973 | 2,971 | +| All binary ADDs, including D and scatter | 26,916 | 26,914 | +| MOVE records | 2,940 | 2,940 | +| COPY / ERASE records | 9 / 9 | 9 / 9 | +| Helpers | 420 | 420 | +| Forward positive-prefix row bound | 144,651 | 144,651 | +| Reverse positive-prefix row bound | 2,270,064 | 2,266,968 | + +The four removed reads and two new reads are charged. All helpers already +exist; there is no scratch allocation, extra copy or omitted restoration. +Each register has exactly its original sequence of frame transitions, +including its final climb. Thus all recursive child ranks are unchanged. +The paid histogram, including the nine rank-8 copies, is +`{1:1320, 2:1440, 4:60, 5:120, 8:9}`, with rank mass 5,112. MOVE timing can +change; the claim is equality of each register's path, not of the global event +order. In the inherited local recurrence the child terms are identical and +the scalar ADD component of the node toll decreases by two. No new complete +hosted recurrence or assembled bound is asserted. + +The circuit identity is over F2, not equality of positive integer shears. +The cancellation-free bounds are checked separately on the actual forward +and reverse streams, including COPY/ERASE. The commutations are also valid +for the positive envelope, and replacing the joint sandwich lowers the +envelope on helper 616 while preserving the envelope on 466. This explains +why fewer gates do not hide a larger local coefficient bill. + +## Search coverage and controls + +The OS assignment seed was 10. Three candidates and the overlap decision are +recorded in `CLAIM.json`. The finite scan starts at binary cleanup offset 10 +and wraps once. It covers all 2,973 original gates, all 2,955 distinct binary +gates, and all 18 duplicate pairs. Each repeated gate occurs twice. +The stopping rule was one complete census, followed by testing every +one-blocker pair, with no further circuit resynthesis. Exactly two pairs +have one blocker and both are used in the joint substitution. + +Commuting swaps preserve the relative order of a gate and any noncommuting +blocker. If a first cancellation were possible after commuting swaps, its +two equal gates could not still have such a blocker between them. Every +duplicate pair has one, and none has yet been deleted before the hypothetical +first cancellation. Hence no first cancellation exists. This is an exact +obstruction for commuting swaps and pair deletion on the fixed word. It +does not exclude conjugation, insertion of neutral pairs, general linear +synthesis, changed forward circuits, or other cleanup words. + +Controls omit each correction separately, supply the wrong correction +source, introduce a second noncommuting blocker, try the uncorrected +three-to-one deletion, and put cleanup at an illegal lower frame. The first +two omissions and the uncorrected deletion fail exact F2 equality; the extra +blocker fails the rewrite premise. These are distinct from a failed search. + +## Validation boundary and attribution + +`VALIDATION.json` records the checks performed locally. A separate Codex +worker independently replayed the candidate using no repository optimizer +or checking imports and obtained the same columns, paths and prefix bounds. +The existing native exporter was also run on both words; its binary records +confirm the table above and identical frame/state descriptions. + +No C++ cohort replay was run because Boost headers were unavailable in this +environment. The recursive hosted-parent reconstruction, renamed-instruction +audits, residual-host checks and full invoice/outer assembly remain integration +work. The full `make verify` suite and selected cold replay were not run for +this standalone addition; no selected source, generator, certificate or +`upstream/` file changes. Uniform/compiler/common-label/mutable-basis, +hosting, signed-lift, precision/tape and analytic obligations remain inherited. + +Credit belongs to eumemic's #543 word and checker, the #493 carrier-skeleton +lineage, Dylan Crow's record exporter and original bit circuit, Zhihao Chen's +#425 cleanup interface, the #472 common-label realization, and the cumulative +contributors credited in those packages. Concurrent #670 by yongjae321, +#674 by x0hu, #688 by Ali Romman and #691 by mtpsl change forward blocks and +their literal reverse cleanup. #686 by Mikhail R. Gadelha and #694 by Greer +Guthrie change frame-zero compensation. Tuomo Kiiskinen's #661 fixes the +phase-B gate word and excludes cleanup synthesis. This result instead keeps +D/A/scatter/B fixed and changes only C. None of those pending patches is a +dependency, and compatibility with their changed cleanup words is untested. + +The final refresh through #709 also found [#708](https://github.com/CrocSwap/integer-mult-bounds/pull/708) +by @thakrarsagar at `2ec522a466ec448f148d4355dc43b51c0ef1e0b5`. It shares +phase-A decoder operands and regenerates literal reverse cleanup, saving 114 +ADDs while raising the measured prefix bounds. The present result uses a +different algebraic rewrite, changes C alone and lowers the reverse prefix +bound. It neither imports nor composes #708. #709 caches geometry checking; +it changes no circuit and is not used here. + +Prepared for GitHub account **@thakrarsagar** with substantial OpenAI Codex +assistance, including the separate audit worker. No independent human review +is claimed. New files are under the repository's Apache-2.0 license. diff --git a/research/r420-cleanup-commutation/VALIDATION.json b/research/r420-cleanup-commutation/VALIDATION.json new file mode 100644 index 0000000000..09d4fc0a3e --- /dev/null +++ b/research/r420-cleanup-commutation/VALIDATION.json @@ -0,0 +1,45 @@ +{ + "status": "finite circuit improvement; no new kappa", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "environment": "macOS, Python 3.14.8, standard library only", + "reproduce": "python3 -B research/r420-cleanup-commutation/verify.py", + "expected_last_line": "PASS_R420_CLEANUP_CONJUGATION C=2973->2971 native_adds=26916->26914 columns=660 kappa=unchanged", + "passed": [ + "Exact source archive/checker and canonical word pins", + "All 18 original duplicate pairs and both one-blocker identities", + "Complete 660-column cleanup matrix equality", + "Pinned E8 lattice and all 672 closed frames", + "Complete finite word replay with arbitrary source, target and helper inputs", + "All 660 register frame paths, including final climbs", + "H1/H2/H3/H5 and all scalar decomposition checks; original H4 intentionally false", + "Exact positive forward and reverse COPY/ERASE stream bounds", + "Six negative controls and all 16 local Boolean inputs", + "python3 -O -B research/r420-cleanup-commutation/verify.py", + "make selected-record-check", + "Independent Codex-worker scalar, frame-path and prefix replay without project imports", + "Existing native exporter on both words, with binary record count/path/prefix comparison", + "Minimal relocated Git archive with only this package and its two declared sources, Python -I -B", + "Both input Git blobs match GitHub PR543 at the declared source head", + "Staged whitespace check and unchanged upstream/selected-certificate paths" + ], + "native_exporter": { + "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "source_sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "records_before_after": [29874, 29872], + "move_records_before_after": [2940, 2940], + "copy_records_before_after": [9, 9], + "erase_records_before_after": [9, 9], + "binary_sha256_before": "f7e6cceaceb04d7bd70918981405dcead988a890cfca03b51e80d935f00a960f", + "binary_sha256_after": "13ba784c06ed0a5849a225c9f117613d69016363fa3aa41e95355a99467ceb1b", + "frame_and_state_json_equal": true, + "per_register_move_paths_equal": true, + "copy_erase_subsequence_equal": true + }, + "not_run": [ + "C++ native cohort replay: Boost headers unavailable", + "Hosted-parent reconstruction, renamed-instruction/residual-host audits and complete invoice/assembly", + "Repository-wide make verify and unchanged selected cold replay", + "Remote CI" + ], + "review_scope": "Finite computational evidence and written local algebra; not a formal proof of the multiplication theorem or independent human review" +} diff --git a/research/r420-cleanup-commutation/certificate.json b/research/r420-cleanup-commutation/certificate.json new file mode 100644 index 0000000000..b66ef5fe4d --- /dev/null +++ b/research/r420-cleanup-commutation/certificate.json @@ -0,0 +1,46 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "source_pr": 543, + "source_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "source_git_blobs": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "0c63ca62759dc63d302be6552aeeee1ede70350f", + "research/e8-bit-r420/code/xcheck.py": "fbff8607e4c61e18481f696b99dd38a32444e90d" + }, + "source_sha256": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "research/e8-bit-r420/code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" + }, + "canonical_input_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "canonical_candidate_sha256": "f87e4574addee69e4c9387f0d7139138454cf24e78e2c1358f239a52546b0abd", + "cleanup_binary_adds": [2973, 2971], + "native_adds": [26916, 26914], + "positive_prefix_before_after": [[144651, 2270064], [144651, 2266968]], + "recipe": { + "indexing": "Zero-based original C after expanding each source list in its stored order", + "delete": [714, 718, 1320, 1321], + "insert_after": 1071, + "insert_gates": [[466, 530], [466, 540]], + "full_frame_id": 1 + }, + "duplicate_census_columns": ["first", "second", "gate_dst_src", "blocker_count", "first_blocker"], + "duplicate_census": [ + [634, 1358, [598, 532], 3, 721], + [714, 1321, [616, 530], 1, 1071], + [718, 1320, [616, 540], 1, 1071], + [982, 2375, [658, 335], 8, 1361], + [985, 2393, [649, 307], 7, 1381], + [986, 2391, [650, 428], 7, 1514], + [989, 2385, [653, 417], 8, 1222], + [991, 2405, [643, 468], 7, 1269], + [992, 2403, [644, 257], 8, 1556], + [994, 2399, [646, 478], 8, 1245], + [998, 2415, [638, 277], 7, 1164], + [1003, 2429, [631, 272], 6, 1376], + [1012, 2435, [628, 249], 5, 1209], + [1015, 2453, [619, 295], 6, 1377], + [1060, 2531, [580, 321], 3, 1234], + [1078, 2567, [562, 333], 4, 1489], + [1083, 2581, [555, 297], 8, 1567], + [1084, 2579, [556, 460], 3, 1608] + ] +} diff --git a/research/r420-cleanup-commutation/verify.py b/research/r420-cleanup-commutation/verify.py new file mode 100644 index 0000000000..e135131586 --- /dev/null +++ b/research/r420-cleanup-commutation/verify.py @@ -0,0 +1,232 @@ +"""Exact finite cleanup experiment. @thakrarsagar / OpenAI Codex; Apache-2.0. + +Run from any directory with Python 3.11+. No third-party Python dependencies. +Optional --emit-word PATH writes the verified candidate for native replay. +""" +import argparse +from collections import Counter, defaultdict +from copy import deepcopy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":")).encode() + + +def expand(gates): + return [(d, s) for _, d, sources in gates for s in sources] + + +def commute(a, b): + return a[0] != b[1] and b[0] != a[1] + + +def census(gates): + positions = defaultdict(list) + # Seed 10 rotates the finite scan; sorting makes the certificate order canonical. + for i in list(range(10, len(gates))) + list(range(min(10, len(gates)))): + positions[gates[i]].append(i) + rows = [] + for a, indices in positions.items(): + indices.sort() + for i, j in zip(indices, indices[1:]): + blockers = [k for k in range(i + 1, j) if not commute(a, gates[k])] + rows.append([i, j, list(a), len(blockers), blockers[0] if blockers else None]) + return sorted(rows) + + +def rewrite(gates, recipe): + k = recipe["insert_after"] + removed = recipe["delete"] + need(len(removed) == len(set(removed)) == 4, "recipe deletion count") + pairs = [(removed[0], removed[3]), (removed[1], removed[2])] + replacements = [] + for i, j in pairs: + need(0 <= i < k < j < len(gates), "recipe indices") + a, b = gates[i], gates[k] + need(a == gates[j], "sandwich endpoints differ") + blockers = [q for q in range(i + 1, j) if not commute(a, gates[q])] + need(blockers == [k], "sandwich does not have exactly the declared blocker") + need(a[0] == b[1] and a[1] != b[0], "not the certified three-register chain") + replacements.append((b[0], a[1])) + need(replacements == [tuple(g) for g in recipe["insert_gates"]], "wrong conjugate gates") + need(commute(gates[removed[0]], gates[removed[1]]), "outer gates do not commute") + result = [] + for i, gate in enumerate(gates): + if i not in removed: + result.append(gate) + if i == k: + result.extend(replacements) + return result + + +def matrix(gates, n): + rows = [1 << r for r in range(n)] + for d, s in gates: + need(0 <= d < n and 0 <= s < n and d != s, "bad XOR operands") + rows[d] ^= rows[s] + return rows + + +def scalar_stream(word): + temp = 2 * word["v"] + word["R"] + stream = [("add", d, s) for name in ("D", "A") for d, s in expand(word[name])] + for k, q in enumerate(word["ret"]): + stream.append(("copy", temp, q)) + stream.extend(("add", word["v"] + t, temp) + for t, row in enumerate(word["scatter"]) if k in row) + stream.append(("erase", temp, q)) + stream.extend(("add", d, s) for name in ("B", "C") for d, s in expand(word[name])) + return stream + + +def prefix_bounds(stream, n): + bounds = [] + for reverse in (False, True): + norms = [1] * (n + 1) + largest, opened = 1, False + for kind, d, s in reversed(stream) if reverse else stream: + if reverse and kind != "add": + kind = "erase" if kind == "copy" else "copy" + if kind == "add": + norms[d] += norms[s] + largest = max(largest, norms[d]) + elif kind == "copy": + need(not opened, "nested COPY") + norms[d], opened = norms[s], True + else: + need(opened, "unmatched ERASE") + norms[d], opened = 0, False + need(not opened, "unclosed COPY") + bounds.append(largest) + return bounds + + +def frame_paths(word): + paths = [[f] for f in word["start"]] + for name in ("D", "A", "B", "C"): + for f, d, sources in word[name]: + for r in [d] + sources: + if paths[r][-1] != f: + paths[r].append(f) + for r, f in enumerate(word["final"]): + if paths[r][-1] != f: + paths[r].append(f) + return paths + + +def expect_rejection(call, message): + try: + call() + except ValueError: + return + raise ValueError("negative control accepted: " + message) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-word", type=Path) + args = parser.parse_args() + cert = json.loads((HERE / "certificate.json").read_text()) + for path, digest in cert["source_sha256"].items(): + need(hashlib.sha256((ROOT / path).read_bytes()).hexdigest() == digest, "source pin: " + path) + word = json.loads(gzip.decompress((ROOT / "research/e8-bit-r420/data/bitE8mut-r420.json.gz").read_bytes())) + need(hashlib.sha256(canonical(word)).hexdigest() == cert["canonical_input_sha256"], "input content pin") + before = expand(word["C"]) + rows = census(before) + need(rows == cert["duplicate_census"], "duplicate census mismatch") + need(all(row[3] > 0 for row in rows), "commutation-only cancellation exists") + need(sum(row[3] == 1 for row in rows) == 2, "one-blocker coverage changed") + after = rewrite(before, cert["recipe"]) + n = 2 * word["v"] + word["R"] + expected = matrix(before, n) + need(matrix(after, n) == expected, "cleanup matrix mismatch") + need([len(before), len(after)] == cert["cleanup_binary_adds"], "cleanup count") + candidate = deepcopy(word) + full = cert["recipe"]["full_frame_id"] + need(all(f == full for f, _, _ in word["C"]), "baseline C not at full frame") + candidate["C"] = [[full, d, [s]] for d, s in after] + need(hashlib.sha256(canonical(candidate)).hexdigest() == cert["canonical_candidate_sha256"], + "candidate content pin") + need(frame_paths(word) == frame_paths(candidate), "a paid register path changed") + + checker_path = ROOT / "research/e8-bit-r420/code/xcheck.py" + spec = importlib.util.spec_from_file_location("pinned_r420_xcheck", checker_path) + checker = importlib.util.module_from_spec(spec) + spec.loader.exec_module(checker) + baseline, labels, _, hypotheses, conclusion, _ = checker.check(word) + need(all(hypotheses.values()) and all(conclusion.values()), "baseline interface") + # Geometry is byte-identical; reuse the checked geometry for the candidate replay. + baseline.w = candidate + finite = baseline.full() + h, c, _ = baseline.interface() + need([k for k, v in h.items() if not v] == ["H4_C_literal_reverse_at_full"], "unexpected interface change") + need(all(c.values()), "candidate inverse/decomposition") + need(baseline.fdim[full] == 8, "replacement frame is not full") + need(all(not 120 <= r < 240 for gate in after for r in gate), "cleanup touches a target") + paths = frame_paths(candidate) + ranks = Counter(baseline.fdim[b] - baseline.fdim[a] for path in paths for a, b in zip(path, path[1:])) + ranks[8] += len(word["ret"]) + need(dict(ranks) == {1: 1320, 2: 1440, 4: 60, 5: 120, 8: 9}, "paid histogram") + streams = [scalar_stream(w) for w in (word, candidate)] + need([sum(k == "add" for k, _, _ in s) for s in streams] == cert["native_adds"], "native ADD count") + bounds = [prefix_bounds(s, n) for s in streams] + need(bounds == cert["positive_prefix_before_after"], "positive prefix receipt") + need(all(b <= a for a, b in zip(*bounds)), "positive prefix increased") + + # These controls address the changed identity, its blocker premise, and its price. + for added in cert["recipe"]["insert_gates"]: + broken = list(after) + broken.remove(tuple(added)) + need(matrix(broken, n) != expected, "missing conjugate not detected") + bad_recipe = deepcopy(cert["recipe"]) + bad_recipe["insert_gates"][0][1] = 531 + expect_rejection(lambda: rewrite(before, bad_recipe), "wrong conjugate source") + broken = list(before) + broken[800] = (530, 0) + expect_rejection(lambda: rewrite(broken, cert["recipe"]), "extra noncommuting blocker") + need(matrix([(616, 530), (466, 616), (616, 530)], n) + != matrix([(466, 616)], n), "unpaid conjugate not detected") + illegal = deepcopy(candidate) + illegal["C"][0][0] = 0 + baseline.w = illegal + try: + baseline.full() + except checker.Reject: + pass + else: + raise ValueError("negative control accepted: illegal cleanup descent") + baseline.w = candidate + # Exhaust the local identity independently as a four-bit truth table. + for bits in range(16): + x = [(bits >> i) & 1 for i in range(4)] + y = list(x) + for d, s in [(0, 2), (0, 3), (1, 0), (0, 3), (0, 2)]: + x[d] ^= x[s] + for d, s in [(1, 0), (1, 2), (1, 3)]: + y[d] ^= y[s] + need(x == y, "local truth table") + print(json.dumps({"labels": labels, "columns": finite["columns"], + "duplicate_pairs": len(rows), "paid_histogram": dict(sorted(ranks.items())), + "positive_prefix_before_after": bounds, + "candidate_content_sha256": hashlib.sha256(canonical(candidate)).hexdigest(), + "controls_rejected": 6, "local_truth_table_inputs": 16}, sort_keys=True)) + if args.emit_word: + args.emit_word.write_bytes(canonical(candidate)) + print("PASS_R420_CLEANUP_CONJUGATION C=2973->2971 native_adds=26916->26914 columns=660 kappa=unchanged") + + +if __name__ == "__main__": + main() From d97c8d20a8b885271a24c5a4e8446ac7f5697d5c Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:08:59 +0530 Subject: [PATCH 2/2] Record completed cleanup sprint handoff --- research/r420-cleanup-commutation/CLAIM.json | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/research/r420-cleanup-commutation/CLAIM.json b/research/r420-cleanup-commutation/CLAIM.json index 34e6d22917..5c3952f82c 100644 --- a/research/r420-cleanup-commutation/CLAIM.json +++ b/research/r420-cleanup-commutation/CLAIM.json @@ -14,5 +14,10 @@ {"task": "full-frame cleanup commutation", "decision": "selected: changes only cleanup, unlike the phase-A/B resynthesis and literal reverse cleanup in PR670/674/688/691"} ], "scope": "No upstream, selected certificate, forward circuit, COPY, frame, helper allocation, or assembly changes. Delegated audit stays within cleanup equivalence and its interface/accounting obligations.", - "status": "in progress" + "status": "completed: finite circuit improvement and commutation-only negative result", + "finished_utc": "2026-10-13T04:38:41Z", + "result": "C 2973->2971; complete native ADDs 26916->26914; 660 symbolic columns and paid frame paths preserved; reverse positive bound 2270064->2266968; no new kappa", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/710", + "final_overlap_refresh": "Open PR metadata through #709 immediately before submission; no pinned issue. #708 changes decoder totals and literal reverse cleanup, while this contribution keeps the forward word fixed and changes cleanup by conjugation. No composition is claimed.", + "main_at_final_refresh": "66849e1475c930fd7732b1a0067ffee7e1e95f60" }