Tooling: 3.18× faster production R420 xcheck.rref via integer elimination with identical receipts

research/e8-bit-r420/MANIFEST.sha256

@@ -14,7 +14,7 @@ e2fd3429e2db4389ae8a5ab47dda89f551b0d0952c42fad5ac8d38a85d670594  code/mutants.p
 c0a687f61aed29455cea953d8a3e49a32136edb3cd4213c46880c146a6ca7fa3  code/planio.py
 aade757c1e4e2714207cbc80a9a60793d84b5f009de2cac79ee8d3239986fd2a  code/provenance.py
 afdf2e53648b417fcc49cd05e9a18ee9fff9ae41e791a6ffa333130e30f35feb  code/summary.py
-5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424  code/xcheck.py
+cd1d91b32831b4bd75290edf8b19f3a4378c5733bf4755ba59ed5161e2c468b9  code/xcheck.py
 9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784  data/bitE8mut-r420.json.gz
 ec81d67d8a82d41859ee33a4e387679b71e5ced15de074a71195d08969dd308a  data/complex-b.json
 3f4be566309841e00e842d5686f7937a355ae1a6a2eaa3ccb07bdf8a9ca604fb  data/complex/pr535/EXACT-ASSEMBLY-PR493.json

research/e8-bit-r420/code/xcheck.py

@@ -29,13 +29,18 @@
   J   the source part of every target's W0 output is its own source (J = I);
   K   the helper part of every target's W0 output equals the helper set D adds to it (D = -V^-1 K s over F2);
   Uinv  C applied to the W0 outputs of the z registers restores every z register (C = U^-1).
-Prepared by eumemic with substantial Anthropic Claude assistance; Apache-2.0."""
+Prepared by eumemic with substantial Anthropic Claude assistance; Apache-2.0.
+
+Production rref uses primitive-integer elimination (Aman PR367 / research/r420-rref-performance)
+and returns the same rational basis rows and pivot columns as the historical Fraction RREF.
+See research/r420-rref-production/ for equivalence evidence. No other checker stage changes."""
 import gzip
 import json
 import math
 import sys
 from collections import Counter
 from fractions import Fraction
+from math import gcd, lcm
 
 
 class Reject(Exception):
@@ -48,26 +53,65 @@ def need(cond, msg):
 
 
 # ------------------------------------------------------------------ exact linear algebra over Q and Z
-def rref(rows):
-    """reduced row echelon form over Q of integer rows; returns (basis rows, pivot columns)"""
-    m = [[Fraction(x) for x in r] for r in rows]
-    piv = []
-    rk = 0
-    ncol = len(m[0]) if m else 0
-    for col in range(ncol):
-        p = next((i for i in range(rk, len(m)) if m[i][col] != 0), None)
-        if p is None:
+def _primitive(row):
+    content = gcd(*row) if row else 0
+    return [x // content for x in row] if content > 1 else row
+
+
+def _integer_rows(matrix):
+    """Convert integer/Fraction rows to content-primitive integer rows; never mutate inputs."""
+    rows = []
+    for values in matrix:
+        row = list(values)
+        if all(isinstance(x, int) for x in row):
+            rows.append(_primitive(row))
+        else:
+            values = [Fraction(x) for x in row]
+            denominator = lcm(*(x.denominator for x in values)) if values else 1
+            rows.append(_primitive([x.numerator * (denominator // x.denominator)
+                                    for x in values]))
+    if rows and any(len(row) != len(rows[0]) for row in rows):
+        raise ValueError('matrix rows must have equal lengths')
+    return rows
+
+
+def _eliminate(matrix, reduced=False):
+    """Fraction-free integer elimination; returns primitive rows and pivot columns."""
+    rows = _integer_rows(matrix)
+    if not rows:
+        return rows, []
+    pivots = []
+    for column in range(len(rows[0])):
+        rank = len(pivots)
+        pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None)
+        if pivot is None:
             continue
-        m[rk], m[p] = m[p], m[rk]
-        inv = 1 / m[rk][col]
-        m[rk] = [a * inv for a in m[rk]]
-        for i in range(len(m)):
-            if i != rk and m[i][col] != 0:
-                f = m[i][col]
-                m[i] = [a - f * b for a, b in zip(m[i], m[rk])]
-        piv.append(col)
-        rk += 1
-    return m[:rk], piv
+        rows[rank], rows[pivot] = rows[pivot], rows[rank]
+        base = rows[rank]
+        targets = range(len(rows)) if reduced else range(rank + 1, len(rows))
+        for i in targets:
+            if i == rank or not rows[i][column]:
+                continue
+            row = rows[i]
+            divisor = gcd(base[column], row[column])
+            a, b = base[column] // divisor, row[column] // divisor
+            rows[i] = _primitive([a * x - b * y for x, y in zip(row, base)])
+        pivots.append(column)
+        if len(pivots) == len(rows):
+            break
+    return rows, pivots
+
+
+def rref(rows):
+    """Reduced row echelon form over Q; returns (basis rows, pivot columns).
+
+    Production form of research/r420-rref-performance/: primitive-integer elimination
+    followed by exact pivot scaling to Fractions. Identical rational row space and
+    pivot list to the historical per-entry Fraction RREF.
+    """
+    matrix, pivots = _eliminate(rows, reduced=True)
+    return [[Fraction(x, row[column]) for x in row]
+            for row, column in zip(matrix, pivots)], pivots
 
 
 def nullspace_int(rows, ncol=8):

research/r420-rref-production/NOTICE.md

@@ -0,0 +1,20 @@
+# Attribution and license
+
+Prepared by Wentao Li ([VictorLiwentao](https://github.com/VictorLiwentao),
+[@Is__Victor](https://x.com/Is__Victor), wentaol4@illinois.edu) with substantial
+AI assistance for orientation, overlap search, profiling, production wiring,
+packaging, benchmarking and writing. Not independent human peer review.
+Apache-2.0; see the repository root `LICENSE`.
+
+The primitive-integer RREF algorithm wired into production was introduced by
+**Aman** (PR367 / `research/frame-algebra-performance` lineage) and integrated as
+an opt-in adapter by the authors of
+`research/r420-rref-performance/` (merged tooling PR; prepared for @MrPink604
+with substantial AI assistance). That package's NOTICE.md and PROOF.md retain
+the exactness argument. This package wires an equivalent `rref` into the
+production `research/e8-bit-r420/code/xcheck.py` path used by
+`research/e8-bit-r420/verify.sh` step 2 and `mutants.py`.
+
+The original R420 checker, mutation harness, word and interleaved
+scalar-interface lemma are **eumemic**'s PR543, with substantial Anthropic Claude
+assistance. Upstream material retains its own source notices and license.

research/r420-rref-production/README.md

@@ -0,0 +1,90 @@
+# Production integer RREF for the R420 exact checker
+
+**Tooling improvement; no new kappa.** At base
+`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, production
+`research/e8-bit-r420/code/xcheck.py:rref` still paid a Fraction-per-entry
+elimination on every frame. The opt-in adapter
+`research/r420-rref-performance/` already proved an equivalent
+primitive-integer RREF with identical receipts and explicitly deferred
+production adoption. This package wires that equivalent check into the
+**production** `rref` used by `research/e8-bit-r420/verify.sh` step 2 and
+`mutants.py`.
+
+Only `research/e8-bit-r420/code/xcheck.py` and its
+`research/e8-bit-r420/MANIFEST.sha256` digest line change outside this
+directory. Label validation, HNF, determinant, F2 replay, H1–H5/dirty
+restoration, and every mutation control remain the historical implementations.
+Selected frontier untouched. Prior research packages that still pin the
+Fraction `xcheck.py` digest (including `research/r420-rref-performance/SOURCES.json`
+and other R420 follow-ons) are left as historical provenance, same pattern as
+earlier production promotions.
+
+## Reproduce
+
+Python **3.12**, standard library only, from the repository root:
+
+```sh
+python3.12 -I -B research/r420-rref-production/verify.py
+python3.12 -I -O -B research/r420-rref-production/verify.py
+python3.12 -B scripts/research_package.py --package research/r420-rref-production
+python3.12 -I -B research/r420-rref-production/benchmark.py --rounds 5 --write-result
+```
+
+Expected:
+
+```text
+PASS_R420_RREF_PRODUCTION frames=672 matrices=677 corruption=… certs=0 no_new_kappa
+PASS_REGISTERED_RESEARCH_PACKAGE research/r420-rref-production outcome=completed
+PASS_IDENTICAL_R420_RREF_PRODUCTION_RECEIPTS
+```
+
+Default verify is read-only. Timing is host-descriptive and is not a
+correctness gate. On Linux / CPython 3.12.3 (this host), five alternating
+fresh-process pairs gave:
+
+- check median **1.064 → 0.362 s (2.94×)**
+- mutants harness median **11.090 → 3.457 s (3.21×)**
+- stage-median sum **12.155 → 3.819 s (3.18×)**
+
+Retained samples are in [`RESULT.json`](RESULT.json).
+
+## Why the integer RREF is equivalent
+
+Aman’s primitive-integer elimination (`exact_rows._eliminate(..., reduced=True)`)
+computes a content-primitive integer row echelon form with the same pivot
+columns as the historical Fraction RREF. Scaling each pivot row by the
+reciprocal of its pivot entry returns lists of `Fraction` equal to the
+historical basis rows. The unchanged `nullspace_int` therefore emits the same
+integer annihilators. Finite evidence compares all **672** shipped frames plus
+five supplemental matrices, and byte-identical complete `xcheck` /
+`mutants` stdout. This supports the scoped kernel argument; it is not a formal
+proof of the multiplication theorem.
+
+## Overlap and credit
+
+Closest priors (different delivery):
+
+- `research/r420-rref-performance/` — opt-in integer RREF adapter; this package
+  is the production wiring.
+- [CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756)
+  — identical-receipt tooling quality bar.
+- Open leave-alone tooling on other objects (#1922 joint frames, #2054/#2150
+  shared/mixed-point, #2100 ternary, #2117 DisjointTensor.frame_data, #2194
+  production verify_factor, #2210 production leech_minor, #2231 production
+  sparse-fusion orbits, #2239 joint-dual replay, #2257 bit-frame
+  `frameopt.close`, #1861 parity-side, #1076 quadratic-affine) was not reopened.
+
+Credit **eumemic** (PR543 checker/harness/word), **Aman** (PR367 integer rows),
+and the authors of `research/r420-rref-performance/`. Prepared by **Wentao Li**
+with substantial AI assistance; see [NOTICE.md](NOTICE.md) and
+[TASK.json](TASK.json). Apache-2.0.
+
+## Open next questions
+
+1. **Should `research/r420-rref-performance/` note that production now ships the
+   same integer `rref`?** Its `SOURCES.json` still pins the historical Fraction
+   `xcheck.py` bytes. First step: one-line status note and pin refresh or relax.
+   Blocked on: maintainer preference for touching incorporated packages.
+2. **Should other packages that pin `research/e8-bit-r420/code/xcheck.py` refresh
+   that single digest?** Leaving old pins keeps this tooling change focused.
+   Blocked on: a dedicated provenance follow-up.

research/r420-rref-production/RESULT.json

@@ -0,0 +1,163 @@
+{
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "baseline_xcheck_sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424",
+  "check_speedup": 2.939734938471416,
+  "controls_speedup": 3.207916313783938,
+  "interpreter": "CPython 3.12.3",
+  "machine": "x86_64",
+  "no_new_kappa": true,
+  "platform": "Linux-6.12.94+-x86_64-with-glibc2.39",
+  "production_xcheck_sha256": "cd1d91b32831b4bd75290edf8b19f3a4378c5733bf4755ba59ed5161e2c468b9",
+  "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]",
+  "rounds": 5,
+  "stage_median_sum_seconds": {
+    "baseline": 12.154546371000038,
+    "production": 3.8191861049999716
+  },
+  "stage_median_sum_speedup": 3.182496489261847,
+  "status": "PASS_IDENTICAL_R420_RREF_PRODUCTION_RECEIPTS",
+  "suite_median_seconds": {
+    "baseline": 6.077273185500019
+  },
+  "timing_scope": "fresh subprocess wall time including imports; warm OS caches, not flushed; host-descriptive only; not a correctness gate",
+  "workloads": {
+    "check": {
+      "median_seconds": {
+        "baseline": 1.0641992050000226,
+        "production": 0.36200515600000926
+      },
+      "records": [
+        {
+          "engine": "baseline",
+          "pair": 0,
+          "seconds": 1.1395701070000541,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        },
+        {
+          "engine": "production",
+          "pair": 0,
+          "seconds": 0.33981653799992273,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        },
+        {
+          "engine": "production",
+          "pair": 1,
+          "seconds": 0.35975235000000794,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        },
+        {
+          "engine": "baseline",
+          "pair": 1,
+          "seconds": 0.989689956999996,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        },
+        {
+          "engine": "baseline",
+          "pair": 2,
+          "seconds": 1.0807330019999881,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        },
+        {
+          "engine": "production",
+          "pair": 2,
+          "seconds": 0.3831915519999711,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        },
+        {
+          "engine": "production",
+          "pair": 3,
+          "seconds": 0.4227107120000255,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        },
+        {
+          "engine": "baseline",
+          "pair": 3,
+          "seconds": 1.0547227089999751,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        },
+        {
+          "engine": "baseline",
+          "pair": 4,
+          "seconds": 1.0641992050000226,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        },
+        {
+          "engine": "production",
+          "pair": 4,
+          "seconds": 0.36200515600000926,
+          "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd"
+        }
+      ],
+      "speedup": 2.939734938471416
+    },
+    "controls": {
+      "median_seconds": {
+        "baseline": 11.090347166000015,
+        "production": 3.4571809489999623
+      },
+      "records": [
+        {
+          "engine": "baseline",
+          "pair": 0,
+          "seconds": 11.682598048000045,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        },
+        {
+          "engine": "production",
+          "pair": 0,
+          "seconds": 3.4433927389999326,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        },
+        {
+          "engine": "production",
+          "pair": 1,
+          "seconds": 3.5178037910000057,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        },
+        {
+          "engine": "baseline",
+          "pair": 1,
+          "seconds": 11.325159448000022,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        },
+        {
+          "engine": "baseline",
+          "pair": 2,
+          "seconds": 11.020422073999953,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        },
+        {
+          "engine": "production",
+          "pair": 2,
+          "seconds": 3.348689057999991,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        },
+        {
+          "engine": "production",
+          "pair": 3,
+          "seconds": 3.6446222680000346,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        },
+        {
+          "engine": "baseline",
+          "pair": 3,
+          "seconds": 10.93502884999998,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        },
+        {
+          "engine": "baseline",
+          "pair": 4,
+          "seconds": 11.090347166000015,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        },
+        {
+          "engine": "production",
+          "pair": 4,
+          "seconds": 3.4571809489999623,
+          "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8"
+        }
+      ],
+      "speedup": 3.207916313783938
+    }
+  }
+}