From 8ea8beb77bea590e492c61186f8f7d5ee88a2580 Mon Sep 17 00:00:00 2001 From: Matthieu Pascal Date: Tue, 13 Oct 2026 12:15:39 +0800 Subject: [PATCH 1/2] research: shorten R420 phase-A quad 13 with exact native evidence --- research/r420-quad13/CERTIFICATE.json | 329 ++++++++++++++++++++++++++ research/r420-quad13/CLAIM.md | 36 +++ research/r420-quad13/PROOF.md | 67 ++++++ research/r420-quad13/README.md | 129 ++++++++++ research/r420-quad13/SOURCES.json | 44 ++++ research/r420-quad13/VALIDATION.json | 39 +++ research/r420-quad13/WITNESS.json | 245 +++++++++++++++++++ research/r420-quad13/search.py | 60 +++++ research/r420-quad13/verify.py | 286 ++++++++++++++++++++++ 9 files changed, 1235 insertions(+) create mode 100644 research/r420-quad13/CERTIFICATE.json create mode 100644 research/r420-quad13/CLAIM.md create mode 100644 research/r420-quad13/PROOF.md create mode 100644 research/r420-quad13/README.md create mode 100644 research/r420-quad13/SOURCES.json create mode 100644 research/r420-quad13/VALIDATION.json create mode 100644 research/r420-quad13/WITNESS.json create mode 100644 research/r420-quad13/search.py create mode 100644 research/r420-quad13/verify.py diff --git a/research/r420-quad13/CERTIFICATE.json b/research/r420-quad13/CERTIFICATE.json new file mode 100644 index 0000000000..5a58156281 --- /dev/null +++ b/research/r420-quad13/CERTIFICATE.json @@ -0,0 +1,329 @@ +{ + "F2_matrix": [ + [ + 1, + 1, + 1, + 1, + 0, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 0, + 0, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 0, + 1, + 1, + 1 + ] + ], + "boolean_inputs": 64, + "columns": 660, + "controls_rejected": [ + "drop circuit gate", + "reverse circuit operand", + "F2-neutral positive-cost inflation", + "dropped cleanup", + "nonliteral original cleanup", + "illegal lower frame", + "missing dirty compensation", + "dropped exported quad ADD" + ], + "kappa_claim": "none; unchanged paid rank profile, no hosted replay", + "labels": { + "frames": 672, + "gram_det": 1, + "labels": 120, + "lattice_rank": 8 + }, + "native_records": { + "original": { + "adds": 26916, + "copies": 9, + "erasures": 9, + "moves": 2940, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "records": 29874, + "records_sha256": "f7e6cceaceb04d7bd70918981405dcead988a890cfca03b51e80d935f00a960f" + }, + "replacement": { + "adds": 26902, + "copies": 9, + "erasures": 9, + "moves": 2940, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "records": 29860, + "records_sha256": "de74714b1af2ea55eeda590b828deebdfaef3faa9db198ee1e074c738732d579" + } + }, + "new_gates": 12, + "new_phase_gates": { + "A": 2057, + "B": 837, + "C": 2654, + "D": 120 + }, + "old_gates": 19, + "old_phase_gates": { + "A": 2064, + "B": 837, + "C": 2661, + "D": 120 + }, + "positive_matrices": { + "forward": { + "original": [ + [ + 3, + 1, + 1, + 1, + 2, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 3, + 2, + 2, + 1, + 3, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 2, + 1, + 1, + 1, + 3, + 1 + ], + [ + 1, + 1, + 0, + 1, + 1, + 1 + ] + ], + "replacement": [ + [ + 3, + 1, + 1, + 1, + 2, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 3, + 2, + 2, + 1, + 3, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 2, + 1, + 1, + 1, + 3, + 1 + ], + [ + 1, + 1, + 0, + 1, + 1, + 1 + ] + ] + }, + "reverse": { + "original": [ + [ + 1, + 1, + 1, + 0, + 0, + 2 + ], + [ + 2, + 6, + 5, + 0, + 2, + 9 + ], + [ + 1, + 3, + 3, + 0, + 1, + 5 + ], + [ + 4, + 11, + 10, + 1, + 4, + 18 + ], + [ + 0, + 1, + 1, + 0, + 1, + 2 + ], + [ + 7, + 19, + 17, + 1, + 7, + 32 + ] + ], + "replacement": [ + [ + 1, + 1, + 1, + 0, + 0, + 0 + ], + [ + 0, + 2, + 1, + 0, + 0, + 1 + ], + [ + 1, + 3, + 3, + 0, + 1, + 1 + ], + [ + 0, + 1, + 0, + 1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 5, + 3, + 1, + 1, + 2 + ] + ] + } + }, + "quad": 13, + "reconstructed_word_sha256": "3cda40f1ad9a42c6fae002a00bc1ebe78cdeb66d937dd908457356ca8037b66b", + "saved_with_cleanup": 14, + "status": "PASS_R420_QUAD13" +} diff --git a/research/r420-quad13/CLAIM.md b/research/r420-quad13/CLAIM.md new file mode 100644 index 0000000000..d5d150d357 --- /dev/null +++ b/research/r420-quad13/CLAIM.md @@ -0,0 +1,36 @@ +# Sprint claim: bit supplier, seed 13 + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60` (main). +OS assignment: `secrets.randbelow(100)` returned **13** on 2026-10-13. +Contributor: @mtpsl, with substantial OpenAI Codex assistance. + +Three narrow candidates considered: + +1. Resynthesize phase-A quad 13's six-register circuit in the PR543 R420 word. +2. Resynthesize an unclaimed phase-B block. PR670 and PR674 already cover blocks + 3 and 5, making this the more crowded direction. +3. Investigate phase-A frame reassignment at quad 13. PR661's fixed-order + phase-B result does not cover it, but a circuit change gives a more directly + checkable bounded experiment. + +Selected scope: candidate 1, quad `13 mod 60 = 13`, frame 315, original A gates +873 through 891 (zero based), registers 267,347,349,376,467,491. Search only +commutations and three-to-at-most-two XOR rewrites whose forward and reversed +nonnegative transfer matrices are entrywise no larger. Seed 13 also fixes the +nomination order. Stop after 100 restarts of 1,000 attempted rewrites. + +Expected deliverable: a finite circuit replacement, exact transfer matrices, +whole-native-word replay and controls, or a scoped failed-search report. No +selected-frontier change and no new kappa without the full supplier pipeline. +Expected finish: 2026-10-13 12:30 Asia/Singapore. Reserve the last quarter of the +session for verification and handoff. + +Coordination: GitHub's pinnedIssues query returned no pinned issues; the only +open issue was #650 (requesting Discussions), with no comments. Claim recorded +locally rather than posting to an unrelated issue. PR metadata was inspected +through #685. Relevant ledger, negative results and predecessors read: PR543, +PR589, PR620 (decoder floors, not circuit lower bounds), PR661, PR670, PR674, +and the selected PR626 construction/review. PR661 explicitly excludes circuit +resynthesis; the two circuit PRs change phase B, whereas this changes phase A. + +Result: pending final verification and submission. diff --git a/research/r420-quad13/PROOF.md b/research/r420-quad13/PROOF.md new file mode 100644 index 0000000000..3ac4b39adf --- /dev/null +++ b/research/r420-quad13/PROOF.md @@ -0,0 +1,67 @@ +# Local substitution and complete native cost + +Let `g(d,s)` replace register d by its XOR with register s. All six registers +of the replaced contiguous A slice operate at frame 315. No target is among +these registers. The old and new ordered gate lists are in `WITNESS.json`. + +For a gate list L, let `F(L)` be its matrix over F2 and `P(L)` its nonnegative +integer transfer matrix, obtained by replacing each XOR update by addition. +The certificate exhibits exact integer matrices satisfying + +``` +P(new) = P(old), +P(reverse(new)) <= P(reverse(old)) entrywise. +``` + +The forward equality implies `F(new)=F(old)` by reduction modulo two. It is +an identity on all six inputs, including arbitrary incoming helper dirt, not +only on the clean-source projection. Each binary XOR is an involution, so +reversing either circuit realizes the inverse of this common F2 matrix. + +Substituting the new circuit in A therefore leaves every register's value at +the end of the slice unchanged. No external read occurs inside this contiguous +slice. All subsequent A operations, the retained COPY/scatter, B and initial D +can be kept. C is regenerated as the full-frame literal reverse of every +z-destination gate of A then B, exactly as required by PR543 hypothesis H4. +This retains H1-H5 and restores all source/helper inputs. The complete symbolic +replay checks the resulting target action `y_t -> y_t XOR x_t` on 660 columns. + +The replacement touches the same six registers, each at the same common frame, +and introduces no register or frame. A register's first touch inside this slice +may occur at a different instruction index, but it has not been changed by an +earlier operation in the slice before that first touch. Its incoming climb is +thus the same climb on the same input. Each register's ordered frame path, all +boundary frames, and all external operations coincide. The verifier compares +these paths for every register and checks nestedness using the exact E8 frames. + +For any nonnegative incoming bound vector u, the local forward terminal bound +is the same, `P(new)u=P(old)u`. Each addition only increases a coordinate, so +every local positive prefix lies componentwise below that local terminal bound. +In the full-frame cleanup slice the new terminal bound is componentwise no +larger for every u. Outside these two slices the nonnegative operations are +identical and monotone. Thus the substitution does not require larger +scalar cancellation-free prefix bounds in either traversal of the word. +This is a local monotonicity argument; it is not a newly replayed global hosted +invoice or a signed-integer restoration claim. Restoration is over F2. + +The complete cost difference is seven removed binary ADDs in A and seven in C. +Source accesses for the remaining gates are explicitly retained; no helper, +COPY, ERASE, frame move or recursive child is added. D and B are unchanged. +The official record exporter gives 26,902 ADDs instead of 26,916, with the same +2,940 MOVEs, nine COPYs and nine ERASEs. Counting each positive frame increment +and each retained COPY rank yields the unchanged histogram + +``` +H = {1:1320, 2:1440, 4:60, 5:120, 8:9}, +sum_r r H[r] = 5112. +``` + +Accordingly the finite scalar circuit improves, while its paid recursive +moment `sum_r H[r] r^p` is unchanged for every p. No improved c or kappa follows +from this contribution. No previously established fixed-profile ceiling is +challenged. Acceptance into a supplier still needs the inherited all-size and +physical interfaces and the supplier's full downstream checks. + +The exact circuit matrices, finite Boolean enumeration and native dirty-column +replay are checkable evidence for this finite substitution. They are not a +formalization of the all-size multiplication theorem. diff --git a/research/r420-quad13/README.md b/research/r420-quad13/README.md new file mode 100644 index 0000000000..c64f5ec7c4 --- /dev/null +++ b/research/r420-quad13/README.md @@ -0,0 +1,129 @@ +# R420 phase-A quad 13: 19 XORs become 12 + +**Finite circuit improvement; no new kappa claim.** A replacement for one +six-register phase-A quad in eumemic's PR543 R420 supplier reduces its circuit +from **19 to 12 binary XOR gates**. Rebuilding the required literal reverse +cleanup saves seven more: **26,916 to 26,902 native scalar ADDs** in total. +The exact forward integer transfer matrix is unchanged. The reversed +nonnegative transfer matrix decreases entrywise. All 660 symbolic input columns, +including 420 arbitrary dirty helpers, satisfy the original endpoint contract. + +No helper, COPY, frame, register, child or restoration step is omitted. Every +register follows the same ordered frame path. The local paid histogram remains +`{1:1320, 2:1440, 4:60, 5:120, 8:9}`, with rank mass **5112**. Consequently this +result supplies no improved recursive moment or integer-multiplication exponent. +The selected result is unchanged. + +## Reproduce + +From the repository root, using Python 3.10+ and only its standard library: + +```sh +python3 -B research/r420-quad13/verify.py +``` + +Expected final line: + +```text +PASS_R420_QUAD13 gates=19->12 native_adds=26916->26902 columns=660 rank_mass=5112 controls=8 +``` + +This checks source pins, reconstructs the improved word from `WITNESS.json`, +compares exact matrices and `CERTIFICATE.json`, replays the predecessor's +E8/frame/dirty-column/interface audit, enumerates all 64 local Boolean inputs, +and independently interprets the actual exported native records with set-valued +symbolic columns and MOVE/COPY/ERASE lifecycle checks. Eight corruptions must be +rejected, including a correct F2 endpoint with invalid literal cleanup and an +F2-neutral pair that increases the positive cost matrix. + +Use `--output /absolute/new/directory` to retain both reconstructed words and +record packages; the output directory must not already exist. With no output +argument, scratch files are temporary. `--write-certificate` explicitly rebuilds +only this package's certificate. The verifier's acceptance checks remain active +under optimized Python. + +The bounded nomination is separately reproducible: + +```sh +python3 -B research/r420-quad13/search.py +``` + +Expected: `PASS_QUAD13_SEARCH seed=13 attempts=100000 gates=19->12`. + +## Exact object and cost + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The selected record at that base consumes PR543 at +`2065fe4f72a914d907f1046603f5a36f17018535` in the PR626 assembly at +`660de893d27bb7abd1d5b01b1640207528a5c851`, with conditional +`kappa=51110230636731/31250000000000000`. + +The object is zero-based quad 13, frame 315, A gates `[873,892)`, on ordered +registers `[267,347,349,376,467,491]`. The six local indices in `WITNESS.json` +refer to this list. `SOURCES.json` pins source bytes and Git blobs at the base; +the word, independent auditor and exporter are the three execution inputs. +The remaining pins identify contextual provenance at the base, not dependencies +on future versions of the selected certificate. + +| Component | Original | Replacement | +|---|---:|---:| +| Quad gates at frame 315 | 19 | 12 | +| Corresponding cleanup gates at full frame | 19 | 12 | +| A gates (multi-source gates counted once) | 2064 | 2057 | +| C gates (multi-source gates counted once) | 2661 | 2654 | +| Native ADDs (one per source operand) | 26916 | 26902 | +| Helpers / retained COPYs | 420 / 9 | 420 / 9 | +| Paid rank mass | 5112 | 5112 | + +All other phases, retained totals, decoder scatter, source access, boundary +frames and recursive rank charges are unchanged. The complete restoration is +regenerated, not treated as free. See `PROOF.md` for the substitution argument. + +## Search, overlap and limitations + +OS seed **13** selected the bit-supplier track and quad `13 mod 60`. A seeded +search attempts 100 runs of 1,000 local rewrites. Each rewrite replaces three +gates by at most two with the same F2 map and no increase in either positive +transfer matrix; commuting neighboring transvections exposes other windows. +The first run ends at 14 gates, the second at 12, and the remaining 98 do not +improve it. This covers those **100,000 attempted rewrites**, not all six-wire +circuits. No minimum gate count or impossibility theorem is claimed. + +Concurrent PR670 and PR674 shorten phase-B blocks 3 and 5; this package changes +a distinct phase-A quad and depends on neither. Their composition with this +replacement is not tested. PR661's fixed-order phase-B moment bound explicitly +excludes circuit resynthesis. PR620's decoder floors concern a different expense +and are not reopened. `CLAIM.md` records the candidates and coordination checks. + +The submission refresh through PR690 also found Mikhail R. Gadelha's PR686 +(frame-zero D sharing) and Ali Romman's PR688 (composition and hosted replay of +PR670/674). Neither changes this phase-A quad. They are distinct concurrent +contributions; this package does not import their circuits or claim their +downstream verification coverage. + +The checked result stops at the complete native word. The multistage C++ formal +columns, hosted supplier invoice, global moment engines, outer assembly, +repository-wide `make verify`, Lean and remote CI were not run. This isolated +research addition does not alter the selected construction or its inputs; +integration into an accepted supplier requires its usual complete replay. +The inherited all-size compiler, common-label/mutable-basis realization, +whole-call hosting, precision, tape, exact-recovery and analytic assumptions +remain. Finite replay is not a formal proof of the multiplication theorem. + +## Credit and license + +Prepared for **@mtpsl** with substantial **OpenAI Codex** assistance in choosing +the circuit, writing the search, mathematical argument, checker and handoff. +No independent human review is claimed. New files are Apache-2.0 under the +repository's LICENSE. + +This builds on **eumemic's PR543/493** circuit, D4 partition and interleaved +scalar-interface checker; **Dylan Crow's PR370** E8 word format, decoder and +record exporter; **DreamingOfClouds' PR503/510** retained totals and nine-stage +pricing; **Zhihao Chen's PR425** interface argument; and the realization and +accounting lineage retained in +[`research/e8-bit-r420/NOTICE.md`](../e8-bit-r420/NOTICE.md), including Jacob +Sussman, icekylinx, chafreaky and DaysSky. The selected consuming composition +credits Chafik Boukhalfa's PR626 allocation, Jeremy Kothe's construction and +dispatch work, Rohan Arun's recurrence correction, and their cited predecessors. +This package claims only the new quad replacement and its evidence. diff --git a/research/r420-quad13/SOURCES.json b/research/r420-quad13/SOURCES.json new file mode 100644 index 0000000000..deeca329fd --- /dev/null +++ b/research/r420-quad13/SOURCES.json @@ -0,0 +1,44 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "source_pr543_commit": "2065fe4f72a914d907f1046603f5a36f17018535", + "selected_pr626_commit": "660de893d27bb7abd1d5b01b1640207528a5c851", + "files": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": { + "sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "git_blob": "0c63ca62759dc63d302be6552aeeee1ede70350f" + }, + "research/e8-bit-r420/code/xcheck.py": { + "sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "git_blob": "fbff8607e4c61e18481f696b99dd38a32444e90d" + }, + "research/e8-bit-r420/code/gen_l3.py": { + "sha256": "d5c802447c99255db1bdfcae62b2116bfc9612c9dc9000d41aa4f5f2fec9f2f2", + "git_blob": "6bbd36540c5527950a547b0e80d3aacdc653d497" + }, + "research/e8-bit-r420/README.md": { + "sha256": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "git_blob": "6751eba6f617292fc919e58d5a9f9f06ab037391" + }, + "research/e8-bit-r420/NOTICE.md": { + "sha256": "12ba6e0845f222e9940b00f6c60d261db104246a8d3143da267682973479f811", + "git_blob": "cb68783d7d76c3fc13faa571429e9b067a0db3f7" + }, + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": { + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350" + }, + "certificates/selected-result.json": { + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "git_blob": "92a10096dee76479af88a897714b3818d8263141" + }, + "docs/research/community-k492-review.md": { + "sha256": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "git_blob": "11efcd07ae2b9d93d355c6adaf773dca70dbce91" + } + }, + "execution_inputs": [ + "research/e8-bit-r420/data/bitE8mut-r420.json.gz", + "research/e8-bit-r420/code/xcheck.py", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py" + ] +} diff --git a/research/r420-quad13/VALIDATION.json b/research/r420-quad13/VALIDATION.json new file mode 100644 index 0000000000..9823241200 --- /dev/null +++ b/research/r420-quad13/VALIDATION.json @@ -0,0 +1,39 @@ +{ + "status": "PASS_SCOPED_FINITE_CIRCUIT", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "platform": "Darwin", + "machine": "arm64", + "python": "3.12.3", + "commands": [ + { + "command": "python3 -B research/r420-quad13/verify.py --write-certificate --output ../quad13-validation", + "result": "PASS_R420_QUAD13 gates=19->12 native_adds=26916->26902 columns=660 rank_mass=5112 controls=8" + }, + { + "command": "python3 -O -B research/r420-quad13/verify.py", + "result": "same PASS; acceptance checks remain active under optimization" + }, + { + "command": "python3 -B research/r420-quad13/search.py", + "result": "PASS_QUAD13_SEARCH seed=13 attempts=100000 gates=19->12" + }, + { + "command": "make selected-record-check", + "result": "PASS selected record, exact kappa, original source inventory and proof supplement: 51110230636731/31250000000000000" + }, + { + "command": "git diff --check", + "result": "PASS" + } + ], + "not_run": [ + "full make verify", + "frontier626 cold replay", + "multistage C++ column replay", + "hosted supplier invoice and moments", + "outer assembly", + "Lean", + "remote CI" + ], + "scope": "Isolated research addition; no existing supplier or selected-record file changed. No new kappa and no full multiplication proof." +} diff --git a/research/r420-quad13/WITNESS.json b/research/r420-quad13/WITNESS.json new file mode 100644 index 0000000000..6112423a46 --- /dev/null +++ b/research/r420-quad13/WITNESS.json @@ -0,0 +1,245 @@ +{ + "original": [ + [ + 5, + 3 + ], + [ + 5, + 1 + ], + [ + 5, + 4 + ], + [ + 5, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 4 + ], + [ + 3, + 0 + ], + [ + 1, + 2 + ], + [ + 1, + 4 + ], + [ + 1, + 0 + ], + [ + 2, + 4 + ], + [ + 2, + 0 + ], + [ + 0, + 5 + ], + [ + 0, + 2 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 2, + 5 + ], + [ + 2, + 1 + ] + ], + "replacement": [ + [ + 5, + 3 + ], + [ + 2, + 4 + ], + [ + 5, + 1 + ], + [ + 5, + 0 + ], + [ + 2, + 0 + ], + [ + 5, + 4 + ], + [ + 1, + 2 + ], + [ + 3, + 1 + ], + [ + 2, + 5 + ], + [ + 0, + 2 + ], + [ + 4, + 2 + ], + [ + 2, + 1 + ] + ], + "registers": [ + 267, + 347, + 349, + 376, + 467, + 491 + ], + "history": [ + 14, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12 + ], + "phase": "A", + "start": 873, + "stop": 892, + "frame": 315, + "quad": 13 +} diff --git a/research/r420-quad13/search.py b/research/r420-quad13/search.py new file mode 100644 index 0000000000..7a0d07c4ac --- /dev/null +++ b/research/r420-quad13/search.py @@ -0,0 +1,60 @@ +"""Bounded deterministic nomination; not a circuit optimality proof. + +Prepared for mtpsl with substantial OpenAI Codex assistance, Apache-2.0. +""" +import json +import random +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def transfer(ops, positive=False): + rows = [[int(i == j) for j in range(6)] for i in range(6)] + for a, b in ops: + rows[a] = [x + y if positive else x ^ y + for x, y in zip(rows[a], rows[b])] + return tuple(tuple(r) for r in rows) + + +def dominated(a, b): + return all(x <= y for r, s in zip(a, b) for x, y in zip(r, s)) + + +def nominate(original): + gates = [(a, b) for a in range(6) for b in range(6) if a != b] + small = {} + for a in gates: + small.setdefault(transfer([a]), []).append([a]) + for b in gates: + small.setdefault(transfer([a, b]), []).append([a, b]) + small[transfer([])] = [[]] + rng = random.Random(13) + best = [tuple(g) for g in original] + history = [] + for _ in range(100): + cur = list(best) + for _ in range(1000): + i = rng.randrange(len(cur) - 2) + window = cur[i:i + 3] + legal = [c for c in small.get(transfer(window), []) + if dominated(transfer(c, True), transfer(window, True)) + and dominated(transfer(c[::-1], True), transfer(window[::-1], True))] + if legal: + cur[i:i + 3] = min(legal, key=lambda x: (len(x), x)) + else: + a, b = cur[i:i + 2] + if a[0] != b[1] and b[0] != a[1]: + cur[i:i + 2] = [b, a] + if len(cur) < len(best): + best = list(cur) + history.append(len(best)) + return {"replacement": [list(g) for g in best], "history": history} + + +if __name__ == "__main__": + witness = json.loads((HERE / "WITNESS.json").read_text()) + result = nominate(witness["original"]) + if result != {k: witness[k] for k in result}: + raise SystemExit("REJECT search does not reproduce the frozen nomination") + print("PASS_QUAD13_SEARCH seed=13 attempts=100000 gates=19->12") diff --git a/research/r420-quad13/verify.py b/research/r420-quad13/verify.py new file mode 100644 index 0000000000..6721f8b461 --- /dev/null +++ b/research/r420-quad13/verify.py @@ -0,0 +1,286 @@ +"""Exact finite quad replacement and native-word checks; no new rate claim. + +Prepared for mtpsl with substantial OpenAI Codex assistance, Apache-2.0. +Python 3.10+, standard library only. No assertions are used for acceptance. +""" +import argparse +from collections import Counter +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import struct +import subprocess +import sys +import tempfile + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-r420/data/bitE8mut-r420.json.gz" +AUDITOR = "research/e8-bit-r420/code/xcheck.py" +EXPORTER = "research/e8-bit-carrier-skeleton/code/bit/export_records.py" + + +class Reject(Exception): + pass + + +def need(condition, reason): + if not condition: + raise Reject(reason) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def matrix(ops, positive=False): + # Each column is evolved separately; search.py evolves whole rows. + cols = [] + for j in range(6): + values = [int(i == j) for i in range(6)] + for d, s in ops: + need(type(d) is int and type(s) is int and 0 <= d < 6 and + 0 <= s < 6 and d != s, "invalid circuit gate") + values[d] = values[d] + values[s] if positive else values[d] ^ values[s] + cols.append(values) + return [list(r) for r in zip(*cols)] + + +def circuit_check(old, new): + need(matrix(old) == matrix(new), "circuit F2 map changed") + positive = {} + for direction, a, b in (("forward", old, new), ("reverse", old[::-1], new[::-1])): + before, after = matrix(a, True), matrix(b, True) + need(all(y <= x for rr, ss in zip(before, after) for x, y in zip(rr, ss)), + direction + " positive matrix increased") + positive[direction] = {"original": before, "replacement": after} + return positive + + +def cleanup(w): + return [[1, d, list(ss)] for _, d, ss in reversed(w["A"] + w["B"]) + if not 120 <= d < 240] + + +def build(base, recipe): + need((recipe["phase"], recipe["start"], recipe["stop"], recipe["frame"], recipe["quad"]) + == ("A", 873, 892, 315, 13), "unexpected circuit location") + regs = recipe["registers"] + need(regs == [267, 347, 349, 376, 467, 491], "unexpected circuit registers") + original = [[315, regs[d], [regs[s]]] for d, s in recipe["original"]] + need(base["A"][873:892] == original, "original gate slice mismatch") + circuit_check(recipe["original"], recipe["replacement"]) + out = copy.deepcopy(base) + out["A"][873:892] = [[315, regs[d], [regs[s]]] for d, s in recipe["replacement"]] + out["C"] = cleanup(out) + return out + + +def paths(w): + result = [[f] for f in w["start"]] + for sec in ("D", "A", "B", "C"): + for f, d, ss in w[sec]: + for r in [d] + ss: + if result[r][-1] != f: + result[r].append(f) + for r, f in enumerate(w["final"]): + if result[r][-1] != f: + result[r].append(f) + return result + + +def audit(w, module, geometry): + # Geometry is unchanged; reuse the baseline's already checked exact spaces. + obj = copy.copy(geometry) + obj.w = w + result = obj.full() + h, c, _ = obj.interface() + need(all(h.values()) and all(c.values()), "interface H1-H5 or decomposition failed") + return result + + +def records_check(directory, word): + """Independent set-valued interpreter of the actual exported instructions. + + This checks the scalar projection and literal MOVE/COPY/ERASE lifecycle, + not the multistage formal-column or hosted-recursion contracts. + """ + raw = (directory / "249-records.bin").read_bytes() + need(len(raw) % 24 == 0, "truncated record") + records = list(struct.iter_unpack("<6i", raw)) + dim = {int(k): v["dim"] for k, v in + json.loads((directory / "frames.json").read_text())["frames"].items()} + frames = list(word["start"]) + [None] + values = [{i} for i in range(660)] + [set()] + pths = [[f] for f in frames[:660]] + hist, counts = Counter(), Counter() + for op, a, b, c, d, e in records: + counts[op] += 1 + if op == 0: + need(a < 660 and frames[a] == b and dim[c] - dim[b] == d and d > 0, + "bad MOVE") + need(set(word["frames"][b]) <= set(word["frames"][c]), "MOVE not nested") + frames[a] = c + pths[a].append(c) + hist[d] += 1 + elif op == 1: + need(a != b and c == 1 and frames[a] == frames[b] == d, "bad ADD frame") + values[a] = values[a].symmetric_difference(values[b]) + elif op == 2: + need(b == 660 and not values[b] and frames[b] is None and frames[a] == c, + "COPY lifecycle") + need(d == 0 and e == dim[c], "COPY rank") + values[b] = set(values[a]) + frames[b] = d + hist[e] += 1 + elif op == 3: + need(b == 660 and frames[a] == c and frames[b] == d == 0 + and values[b] == values[a], "ERASE lifecycle") + values[b] = set() + frames[b] = None + else: + raise Reject("unknown record opcode") + expected = [{i} if not 120 <= i < 240 else {i, i - 120} for i in range(660)] + need(values[:660] == expected and not values[660], "record dirty-column endpoint") + need(frames[:660] == word["final"] and frames[660] is None, "record frame endpoint") + need(pths == paths(word), "record frame paths differ") + return {"records": len(records), "adds": counts[1], "moves": counts[0], + "copies": counts[2], "erasures": counts[3], + "paid_histogram": dict(sorted(hist.items())), + "rank_mass": sum(k * v for k, v in hist.items()), + "records_sha256": sha(raw)} + + +def rejected(label, fn, exceptions): + try: + fn() + except exceptions: + return label + raise Reject("negative control accepted: " + label) + + +def run(output, write_certificate): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for path in pins["execution_inputs"]: + pin = pins["files"][path] + need(sha((ROOT / path).read_bytes()) == pin["sha256"], "source hash mismatch: " + path) + base = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + recipe = json.loads((HERE / "WITNESS.json").read_text()) + revised = build(base, recipe) + positive = circuit_check(recipe["original"], recipe["replacement"]) + need(positive["forward"]["original"] == positive["forward"]["replacement"], + "integer forward map changed") + need(paths(base) == paths(revised), "physical frame path changed") + + spec = importlib.util.spec_from_file_location("predecessor_xcheck", ROOT / AUDITOR) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + geometry, labels, baseline, h, c, _ = module.check(base) + need(all(h.values()) and all(c.values()), "baseline interface failed") + revised_audit = audit(revised, module, geometry) + + # Independent exhaustive evaluation of the six-register Boolean map. + for bits in range(64): + endings = [] + for gates in (recipe["original"], recipe["replacement"]): + value = bits + for d, s in gates: + value ^= ((value >> s) & 1) << d + endings.append(value) + need(endings[0] == endings[1], "exhaustive six-bit map differs") + + evidence = {} + for name, word in (("original", base), ("replacement", revised)): + path = output / (name + ".json") + path.write_text(json.dumps(word, separators=(",", ":")) + "\n") + directory = output / name + subprocess.run([sys.executable, "-B", str(ROOT / EXPORTER), str(path), str(directory)], + check=True, capture_output=True, text=True) + evidence[name] = records_check(directory, word) + a, b = evidence["original"], evidence["replacement"] + need(a["adds"] == 26916 and b["adds"] == 26902, "unexpected native ADD count") + for key in ("moves", "copies", "erasures", "paid_histogram", "rank_mass"): + need(a[key] == b[key], "native cost changed: " + key) + need(b["rank_mass"] == 5112 and b["copies"] == 9, "incorrect native cost") + + controls = [] + fail = (Reject, module.Reject) + controls.append(rejected("drop circuit gate", lambda: circuit_check( + recipe["original"], recipe["replacement"][1:]), fail)) + wrong = copy.deepcopy(recipe["replacement"]) + wrong[0].reverse() + controls.append(rejected("reverse circuit operand", lambda: circuit_check( + recipe["original"], wrong), fail)) + inflated = recipe["replacement"] + [[0, 1], [0, 1]] + need(matrix(inflated) == matrix(recipe["replacement"]), "inflation control is not F2-neutral") + controls.append(rejected("F2-neutral positive-cost inflation", lambda: circuit_check( + recipe["original"], inflated), fail)) + bad = copy.deepcopy(revised) + bad["C"].pop() + controls.append(rejected("dropped cleanup", lambda: audit(bad, module, geometry), fail)) + bad = copy.deepcopy(revised) + bad["C"] = copy.deepcopy(base["C"]) + # Same endpoint but not the literal reverse required by H4. + obj = copy.copy(geometry) + obj.w = bad + obj.full() + controls.append(rejected("nonliteral original cleanup", lambda: audit(bad, module, geometry), fail)) + bad = copy.deepcopy(revised) + bad["A"][873][0] = 0 + controls.append(rejected("illegal lower frame", lambda: audit(bad, module, geometry), fail)) + bad = copy.deepcopy(revised) + bad["D"][0][2].pop() + controls.append(rejected("missing dirty compensation", lambda: audit(bad, module, geometry), fail)) + + # The record endpoint checker must see literal instruction corruption too. + directory = output / "replacement" + rawpath = directory / "249-records.bin" + raw = rawpath.read_bytes() + recs = list(struct.iter_unpack("<6i", raw)) + for i, rec in enumerate(recs): + if rec[0] == 1 and rec[5] == 2 and rec[4] == 315: + rawpath.write_bytes(raw[:24*i] + raw[24*(i+1):]) + break + try: + controls.append(rejected("dropped exported quad ADD", lambda: records_check(directory, revised), fail)) + finally: + rawpath.write_bytes(raw) + + cert = {"status": "PASS_R420_QUAD13", "quad": 13, "old_gates": 19, "new_gates": 12, + "saved_with_cleanup": 14, "labels": labels, "columns": revised_audit["columns"], + "old_phase_gates": baseline["gates"], "new_phase_gates": revised_audit["gates"], + "boolean_inputs": 64, "F2_matrix": matrix(recipe["replacement"]), + "positive_matrices": positive, "native_records": evidence, + "reconstructed_word_sha256": sha(canonical(revised)), "controls_rejected": controls, + "kappa_claim": "none; unchanged paid rank profile, no hosted replay"} + path = HERE / "CERTIFICATE.json" + if write_certificate: + path.write_text(json.dumps(cert, indent=2, sort_keys=True) + "\n") + else: + need(canonical(cert) == canonical(json.loads(path.read_text())), "certificate mismatch") + print("PASS_R420_QUAD13 gates=19->12 native_adds=26916->26902 columns=660 rank_mass=5112 controls=8") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="new directory for reconstructed word and records") + parser.add_argument("--write-certificate", action="store_true", help="regenerate this package's certificate") + args = parser.parse_args() + if args.output: + args.output.mkdir(parents=True, exist_ok=False) + run(args.output.resolve(), args.write_certificate) + else: + with tempfile.TemporaryDirectory(prefix="r420-quad13-") as temporary: + run(Path(temporary), args.write_certificate) + + +if __name__ == "__main__": + main() From ee6b9175fe006c11871802866c487b5ecc1a93a4 Mon Sep 17 00:00:00 2001 From: Matthieu Pascal Date: Tue, 13 Oct 2026 12:16:30 +0800 Subject: [PATCH 2/2] docs: record quad 13 sprint result and PR handoff --- research/r420-quad13/CLAIM.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/research/r420-quad13/CLAIM.md b/research/r420-quad13/CLAIM.md index d5d150d357..ddc2c8f05a 100644 --- a/research/r420-quad13/CLAIM.md +++ b/research/r420-quad13/CLAIM.md @@ -33,4 +33,15 @@ PR589, PR620 (decoder floors, not circuit lower bounds), PR661, PR670, PR674, and the selected PR626 construction/review. PR661 explicitly excludes circuit resynthesis; the two circuit PRs change phase B, whereas this changes phase A. -Result: pending final verification and submission. +Result: **completed finite circuit improvement**, submitted as +[PR691](https://github.com/CrocSwap/integer-mult-bounds/pull/691). Quad 13 uses +12 gates instead of 19; literal cleanup gives 14 fewer native ADDs overall. +The forward integer matrix agrees, the reverse positive matrix is dominated, +all 660 dirty-input columns restore, frame paths and rank mass 5112 agree, and +all eight rejection controls pass. No new kappa. `VALIDATION.json` records the +bounded checks and unreplayed downstream obligations. + +Final metadata refresh covered new PRs through #690 and found no phase-A quad +overlap. PR686 changes D, and PR688 composes phase-B blocks from PR670/674; +neither is imported here. Main still equals the recorded base. This is the +single result update to the local claim; no coordination thread was available.