Research: decoder source cosets save 244 R420 XORs (no new kappa)

research/r420-decoder-cosets/CLAIM.md

@@ -0,0 +1,34 @@
+# Sprint claim
+
+- Track: bit supplier; OS `secrets.randbelow(100)` assignment seed **3**.
+- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60` (origin/main).
+- Started: 2026-10-13 04:52 UTC; expected finish: 05:25 UTC.
+- No pinned coordination issue (GitHub GraphQL pinnedIssues returned empty).
+- Three candidates: resynthesize a phase-A quad; change decoder-total source
+  representations using the dead-register kernel; shorten full-frame cleanup.
+  Quad synthesis overlaps #691; cleanup overlaps #710. Choose decoder cosets.
+- Exact scope: the nine FULL-frame decoder totals in #543 R420. Enumerate
+  source-null dependencies among available dead-register values and use a
+  bounded seed-3 greedy descent to reduce the **complete** binary XOR count,
+  including changed frame-zero dirty compensation and literal cleanup.
+- Unlike #708, permit the helper-dirt operator to change and recompute D;
+  do not import its restored operand-pair sharing. No paid-moment or kappa
+  improvement is assumed. Stop if the complete optimistic cost does not help.
+- Deliverable: frozen replacement recipe, exact dirty-column verification,
+  negative controls, cost evidence and a scoped research construction or
+  negative result. Selected frontier and upstream remain unchanged.
+- Reviewed selected certificate, #626 review/construction dependencies, review
+  ledger, #543 construction/family limitations and open PR metadata through
+  #725. #711/#718 address scheduling, not decoder source cosets.
+
+## Completed handoff
+
+[PR #748](https://github.com/CrocSwap/integer-mult-bounds/pull/748): one
+index-3 decoder source-coset replacement saves 244 complete local binary XORs,
+including changed D and literal C. All 660 columns, original frame/interface
+checks, native counts/bounds and six rejection controls pass; no new κ.
+Search stopped at 32 trials / 2,997 scored candidates, five accepted moves.
+The final portion was reserved for exact verification, clean archive replay,
+source/optimized-mode controls, independent static AI review and handoff.
+Final overlap refreshed through #747, including distinct #731/#733/#742 work.
+No selected-frontier or upstream changes. See README and VALIDATION for limits.

research/r420-decoder-cosets/EXPECTED.json

@@ -0,0 +1,110 @@
+{
+  "canonical_word_sha256": "125a17ce601465f746297a7487acad670ff1ea4a44b4efb2d98e2c175117a9d5",
+  "changed_dirt_columns": 93,
+  "columns": 660,
+  "controls": [
+    "stale_compensation",
+    "stale_cleanup",
+    "missing_compensation_read",
+    "missing_cleanup_gate",
+    "corrupt_total_with_matched_cleanup",
+    "total_at_zero_frame"
+  ],
+  "counts_after": {
+    "A": 2394,
+    "B": 1077,
+    "C": 2991,
+    "D": 19642,
+    "scatter": 568,
+    "total": 26672
+  },
+  "counts_before": {
+    "A": 2376,
+    "B": 1077,
+    "C": 2973,
+    "D": 19922,
+    "scatter": 568,
+    "total": 26916
+  },
+  "identical_register_paths": 660,
+  "labels": {
+    "frames": 672,
+    "gram_det": 1,
+    "labels": 120,
+    "lattice_rank": 8
+  },
+  "native_after": {
+    "additions": 26672,
+    "bounds": [
+      144651,
+      2301524
+    ],
+    "copies": 9,
+    "erasures": 9,
+    "exporter_sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3",
+    "moves": 2940,
+    "payload_bits": 100,
+    "payload_upper": "1026066033413435005982928497664",
+    "rank_histogram": [
+      [
+        1,
+        1320
+      ],
+      [
+        2,
+        1440
+      ],
+      [
+        4,
+        60
+      ],
+      [
+        5,
+        120
+      ],
+      [
+        8,
+        9
+      ]
+    ],
+    "records": 29630
+  },
+  "native_before": {
+    "additions": 26916,
+    "bounds": [
+      144651,
+      2270064
+    ],
+    "copies": 9,
+    "erasures": 9,
+    "exporter_sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3",
+    "moves": 2940,
+    "payload_bits": 100,
+    "payload_upper": "998206739997057013039187410944",
+    "rank_histogram": [
+      [
+        1,
+        1320
+      ],
+      [
+        2,
+        1440
+      ],
+      [
+        4,
+        60
+      ],
+      [
+        5,
+        120
+      ],
+      [
+        8,
+        9
+      ]
+    ],
+    "records": 29874
+  },
+  "positive_forward_after": 144651,
+  "positive_forward_before": 144651
+}

research/r420-decoder-cosets/README.md

@@ -0,0 +1,129 @@
+# R420 decoder source cosets: 244 fewer local binary XORs
+
+**Status: finite bit-circuit research construction; no new κ.**
+
+Prepared by **Chinmay Khaladkar (@cxnmai)** with substantial OpenAI AI
+assistance, including a separate source-level reviewer agent. Apache-2.0.
+No independent human review or full multiplication theorem is claimed.
+
+## Result and reproduction
+
+Change just decoder total **index 3, host 583**, in eumemic's #543 R420 word.
+Its source expression is unchanged, but its helper-dirt expression changes
+in **93 columns**. Recompute frame-zero compensation D and literal cleanup C.
+The complete local primitive count falls **26,916 → 26,672**, saving **244**:
+
+| Section | Original binary XORs | Candidate |
+|---|---:|---:|
+| D: dirty compensation | 19,922 | 19,642 |
+| A | 2,376 | 2,394 |
+| scatter | 568 | 568 |
+| B | 1,077 | 1,077 |
+| C: restoration | 2,973 | 2,991 |
+
+The chosen total becomes **25 → 43** XORs: minimizing its own length would
+miss this improvement. Every new operand read and the extra cleanup is charged.
+There are no new helpers, recursive children, copies or frame changes. All 660
+register frame paths agree, including their final climbs. Rank mass remains
+5,112; the local histogram is `{1:1320, 2:1440, 4:60, 5:120, 8:9}`.
+
+Run from the repository root (Python 3.11+, standard library only):
+
+```sh
+python3 -B research/r420-decoder-cosets/verify.py
+```
+
+Expected final line:
+
+```text
+PASS_R420_DECODER_COSET total=26916->26672 saved=244 columns=660 controls=6 no_new_kappa
+```
+
+`--word /tmp/candidate.json.gz` also writes the complete candidate. Equality is
+by canonical JSON payload, not a regenerated gzip container hash. `RECIPE.json`
+freezes the search, operands and five accepted moves; `EXPECTED.json` freezes
+verification results. `--record` deliberately rewrites that receipt for authors;
+normal verification never rewrites repository files.
+
+## Mechanism and exact cost
+
+At the chosen gate let register r contain `X_r x + H_r s` over F2. Toggle an
+operand set N with `XOR_{r in N} X_r = 0`. Its dirt change is
+`d = XOR_{r in N} H_r`. Host 583 is not accessed by later A gates or B;
+its only downstream target use is scatter column 3. Therefore
+
+```
+K'_t = K_t XOR (scatter[t,3] * d)
+Delta = 2 (|operands'| - |operands|) + sum_t (wt(K'_t) - wt(K_t)).
+```
+
+Setting D to K' restores the same target map. C is regenerated as the literal
+reverse of all A/B non-target gates, so it restores arbitrary source/helper
+inputs. No target feeds a non-target. The unchanged original H1–H5 checker
+accepts the candidate, including frame legality and the exact J=I, D=K, U inverse
+obligations. This is a finite F2 identity, not an all-size analytic proof.
+
+## Bounded search and useful negative evidence
+
+Assignment seed **3** comes from OS randomness; index `3 mod 9` selects the
+fourth total, rather than another frequently resynthesized block.
+The 80 non-retained operands already used by the nine original totals have
+**source rank 80**: this pool has no source-null toggles. The evidence-driven
+expansion uses all 180 dead o2 registers from the first 180 phase-A D6 additions,
+minus the nine retained hosts. The resulting **171-register pool has rank 90
+and nullity 81** at the actual gate prefix. No pool register is accessed by B.
+
+`search.py` performs 32 seed-3 shuffled Gaussian-elimination bases, each followed
+by steepest strictly improving single-basis-vector descent until no such move
+helps. It completes **2,997 scored candidates**, accepting five moves. Ties use
+basis order. This searches neither all 2^81 null vectors nor all schedules;
+no optimality or impossibility theorem follows. The complete candidate is
+replayed, not trusted from the local cost formula.
+
+## Verification and limits
+
+- Independent set-valued replay covers all 660 dirty input columns.
+- Original #543 checker covers 120 E8 lines, all 672 frames and H1–H5.
+- Six negative controls reject stale D, stale C, missing D read, missing C gate,
+  corrupted total with matched C, and scalar-neutral illegal frame placement.
+- Original Dylan Crow exporter emits **29,874 → 29,630** records, with unchanged
+  2,940 MOVEs and nine COPY/ERASE pairs. Copy-aware positive integer bounds are
+  measured in both directions: forward **144,651 → 144,651**, reverse
+  **2,270,064 → 2,301,524**. The stock local envelope
+  `64 * forward^3 * reverse^2` remains 100 bits, below the 104-bit limit.
+
+The reverse bound increases: fewer XORs do **not** imply coefficient domination.
+The native bound calculation is Python, following `columns_k.cpp`; this package
+has not run that C++ multistage checker (Boost headers are unavailable), rebuilt
+the hosted parent, checked its global invoice, or assembled a changed-word κ.
+No repository-wide `make verify`, selected cold replay, Lean or remote CI pass
+is claimed. Only this new research package changes; therefore unrelated global
+artifacts are not regenerated. All-size/compiler/common-label/mutable-basis,
+whole-owner hosting, residual, precision/tape and analytic assumptions remain.
+The selected composition is complex-bound; local XOR savings alone do not
+change its recursive profile or imply a stronger exponent.
+
+## Pins, predecessors and overlap
+
+Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+Selected result at that base: #626 with #543, conditional κ
+`0.001635527380375392`; it is unchanged. Supplier #543 source head:
+`2065fe4f72a914d907f1046603f5a36f17018535`.
+The exact compressed input SHA256 is in `RECIPE.json`; the original checker
+SHA256 is enforced in `verify.py`; exporter SHA256 is in `EXPECTED.json`.
+All three input paths are in those scripts and resolved relative to this repo.
+
+Credit remains with eumemic's #543/#493 circuit, Dylan Crow's export/checker
+lineage, Zhihao Chen's #425 interface, #472's common-label realization, and
+all predecessors credited in `research/e8-bit-r420/README.md` and its notices.
+No pending contribution is imported. In particular Sagar Thakrar's #708 shares
+restored operands while preserving the full dirty operator. This construction
+changes that operator and wins mainly in D, using a different search class.
+#686/#694 change frame-zero bases; #710 shortens cleanup; #716 optimizes target
+pairs. Final overlap refresh through #747 also checked Joshua Snider's #731
+(rank/kernel of the **fixed correction matrix K**, not our decoder source map)
+and Scott Woolsey Biggart's #733 (two-sided basis composition preserving K).
+@ellipsi2's #742 likewise preserves K, using shared target donors.
+Our construction changes K; their savings must not be added to ours without a
+new composition audit. Those mechanisms are not combined here. The local claim
+records the candidate selection and absence of a pinned coordination issue.

research/r420-decoder-cosets/RECIPE.json

@@ -0,0 +1 @@
+{"affected_targets": [2, 3, 6, 7, 9, 11, 12, 14, 17, 19, 20, 22, 24, 27, 28, 31, 41, 43, 44, 46, 49, 51, 52, 54, 56, 59, 60, 63, 65, 66, 69, 70, 72, 74, 77, 79, 80, 82, 85, 87, 88, 91, 93, 94, 100, 101, 102, 103, 104, 106, 109, 111, 112, 114, 117, 119], "after": {"A": 2394, "B": 1077, "C": 2991, "D": 19642, "scatter": 568, "total": 26672}, "before": {"A": 2376, "B": 1077, "C": 2973, "D": 19922, "scatter": 568, "total": 26916}, "candidates_scored": 2997, "host": 583, "kernel_dimensions": [81], "moves": [{"delta_cost": -100, "toggle": [267, 310, 321, 324, 326, 376, 382, 398, 421, 456, 467, 505, 509, 521, 527, 534, 539, 557, 621], "trial": 0}, {"delta_cost": -98, "toggle": [291, 310, 321, 324, 326, 335, 343, 347, 376, 382, 398, 401, 411, 421, 431, 444, 460, 505, 506, 507, 509, 528, 534, 539, 601, 621, 622, 633], "trial": 0}, {"delta_cost": -18, "toggle": [305, 328, 333, 404, 421, 434, 435], "trial": 5}, {"delta_cost": -14, "toggle": [295, 333, 382, 404, 489, 505, 509, 634, 652], "trial": 12}, {"delta_cost": -14, "toggle": [533, 534, 565, 566, 576, 601, 613], "trial": 15}], "operands": [267, 291, 295, 299, 326, 328, 335, 339, 347, 356, 379, 401, 411, 415, 421, 444, 456, 467, 489, 497, 505, 509, 511, 513, 514, 516, 521, 527, 528, 529, 532, 533, 540, 557, 565, 566, 569, 576, 613, 622, 633, 634, 652], "original_operands": [299, 305, 326, 339, 343, 356, 379, 382, 415, 431, 434, 435, 460, 497, 506, 507, 511, 513, 514, 516, 529, 532, 534, 540, 569], "pool_size": 171, "seed": 3, "source_sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", "total_index": 3, "trials": 32}

research/r420-decoder-cosets/VALIDATION.md

@@ -0,0 +1,38 @@
+# Validation receipt
+
+2026-10-13, Linux, Python 3.14.7, standard-library Python only.
+Base `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+
+Passed after implementation:
+
+1. `python -B research/r420-decoder-cosets/verify.py`
+   reproduces the frozen 32-trial search, five moves, 2,997 candidate scores,
+   exact certificate and 244-XOR saving. All 660 columns, 672 closed frames,
+   original H1–H5, unchanged per-register paths and six negative controls pass.
+2. Original exporter, baseline and candidate: 29,874 / 29,630 native records;
+   copy-aware forward/reverse integer bounds and 100-bit local envelopes pass.
+3. Minimal `git archive` containing this package plus only its three input files,
+   extracted into a fresh `/tmp/` directory and invoked from outside the repo:
+   same PASS line, no untracked dependencies.
+4. `python -O -B research/r420-decoder-cosets/verify.py` exits nonzero with
+   `Assertions required: do not use python -O`.
+5. Appending corruption to the archived input gzip: verifier rejects its source
+   hash before search. This is an immutable source pin; candidate gzip output
+   is compared through canonical JSON instead.
+6. `git diff --check origin/main` passed; `git diff --exit-code origin/main --
+   upstream certificates/selected-result.json` passed.
+7. `make selected-record-check` passed with exact selected κ
+   `51110230636731/31250000000000000`.
+
+A separate AI reviewer checked the mathematical direction and cost formula,
+not execution, and prompted explicit source-kernel, downstream-host, changed
+D/C, frame-path and positive-growth checks. A second final static AI review
+read the completed code, recipe and receipts and reported no issues; it did
+not rerun commands or review a committed-range diff. This is not human peer review.
+
+Not run: repository-wide `make verify`, selected `frontier626-verify`, C++
+multistage replay, hosted-parent rebuild/global invoice, changed outer assembly,
+Lean or remote CI. Boost headers and NumPy are absent in this environment;
+the scoped stdlib verifier and unmodified exporter do not require either.
+No full theorem, stronger κ, global optimality or practical runtime speedup is
+inferred from these finite checks.

research/r420-decoder-cosets/checks.py

@@ -0,0 +1,64 @@
+# Apache-2.0; cxnmai with substantial OpenAI assistance.
+"""Set-valued dirty-input replay, paths, positive envelopes and controls."""
+import copy
+from model import INDEX, counts
+
+
+def replay(w):
+    n, v = 2*w['v']+w['R'], w['v']
+    values = [{r} for r in range(n)]
+    paths = [[f] for f in w['start']]
+    positive = [1]*n
+    peak = 1
+    for section in ('D', 'A', 'scatter', 'B', 'C'):
+        if section == 'scatter':
+            gates = [[0, v+t, [w['ret'][k] for k in row]]
+                     for t, row in enumerate(w['scatter'])]
+        else:
+            gates = w[section]
+        for frame, dst, srcs in gates:
+            if section != 'scatter':
+                assert dst not in srcs and len(srcs) == len(set(srcs))
+                for r in [dst]+srcs:
+                    if paths[r][-1] != frame:
+                        paths[r].append(frame)
+            for src in srcs:
+                values[dst] ^= values[src]
+                positive[dst] += positive[src]
+                peak = max(peak, positive[dst])
+    for r, f in enumerate(w['final']):
+        if paths[r][-1] != f:
+            paths[r].append(f)
+    expected = [{r, r-v} if v <= r < 2*v else {r} for r in range(n)]
+    assert values == expected, 'dirty-input map mismatch'
+    return paths, peak
+
+
+def controls(original, candidate):
+    rejected = []
+    variants = {}
+    bad = copy.deepcopy(candidate)
+    bad['D'] = original['D']
+    variants['stale_compensation'] = bad
+    bad = copy.deepcopy(candidate)
+    bad['C'] = original['C']
+    variants['stale_cleanup'] = bad
+    bad = copy.deepcopy(candidate)
+    bad['D'][0][2].pop()
+    variants['missing_compensation_read'] = bad
+    bad = copy.deepcopy(candidate)
+    bad['C'].pop()
+    variants['missing_cleanup_gate'] = bad
+    bad = copy.deepcopy(candidate)
+    bad['A'][-9+INDEX][2].pop()
+    bad['C'] = [[1, d, ss[:]] for _, d, ss in reversed(bad['A']+bad['B'])
+                if not 120 <= d < 240]
+    variants['corrupt_total_with_matched_cleanup'] = bad
+    for name, bad in variants.items():
+        try:
+            replay(bad)
+        except AssertionError:
+            rejected.append(name)
+        else:
+            raise AssertionError('control accepted: '+name)
+    return rejected