From b0796249cb54351804f6a9301d16ca1152b8f3d7 Mon Sep 17 00:00:00 2001 From: martinxxx9 <341803289+martinxxx9@users.noreply.github.com> Date: Tue, 13 Oct 2026 19:55:27 +0200 Subject: [PATCH 1/2] Add finite R480 Q-node5 circuit with full local invoice --- research/r480-qnode5-seed05/CANDIDATE.json | 360 ++++++++++++++++++ research/r480-qnode5-seed05/CERTIFICATE.json | 184 +++++++++ research/r480-qnode5-seed05/CLAIM.md | 14 + research/r480-qnode5-seed05/OVERLAP.json | 150 ++++++++ research/r480-qnode5-seed05/PROOF.md | 28 ++ research/r480-qnode5-seed05/README.md | 50 +++ research/r480-qnode5-seed05/SOURCES.json | 32 ++ research/r480-qnode5-seed05/VALIDATION.md | 30 ++ research/r480-qnode5-seed05/search.py | 182 +++++++++ research/r480-qnode5-seed05/test_package.py | 79 ++++ research/r480-qnode5-seed05/verify.py | 374 +++++++++++++++++++ 11 files changed, 1483 insertions(+) create mode 100644 research/r480-qnode5-seed05/CANDIDATE.json create mode 100644 research/r480-qnode5-seed05/CERTIFICATE.json create mode 100644 research/r480-qnode5-seed05/CLAIM.md create mode 100644 research/r480-qnode5-seed05/OVERLAP.json create mode 100644 research/r480-qnode5-seed05/PROOF.md create mode 100644 research/r480-qnode5-seed05/README.md create mode 100644 research/r480-qnode5-seed05/SOURCES.json create mode 100644 research/r480-qnode5-seed05/VALIDATION.md create mode 100644 research/r480-qnode5-seed05/search.py create mode 100644 research/r480-qnode5-seed05/test_package.py create mode 100644 research/r480-qnode5-seed05/verify.py diff --git a/research/r480-qnode5-seed05/CANDIDATE.json b/research/r480-qnode5-seed05/CANDIDATE.json new file mode 100644 index 0000000000..9731ea4e39 --- /dev/null +++ b/research/r480-qnode5-seed05/CANDIDATE.json @@ -0,0 +1,360 @@ +{ + "assignment_seed": 5, + "best": { + "forward": 176135, + "gates": [ + [ + 487, + 40, + [ + 35 + ] + ], + [ + 487, + 19, + [ + 24 + ] + ], + [ + 487, + 95, + [ + 84 + ] + ], + [ + 487, + 100, + [ + 40 + ] + ], + [ + 487, + 100, + [ + 111 + ] + ], + [ + 487, + 111, + [ + 65 + ] + ], + [ + 487, + 65, + [ + 74 + ] + ], + [ + 487, + 24, + [ + 111 + ] + ], + [ + 487, + 111, + [ + 24 + ] + ], + [ + 487, + 24, + [ + 111 + ] + ], + [ + 487, + 35, + [ + 40 + ] + ], + [ + 487, + 40, + [ + 35 + ] + ], + [ + 487, + 35, + [ + 40 + ] + ], + [ + 487, + 54, + [ + 74 + ] + ], + [ + 487, + 74, + [ + 54 + ] + ], + [ + 487, + 54, + [ + 74 + ] + ], + [ + 487, + 65, + [ + 95 + ] + ], + [ + 487, + 95, + [ + 65 + ] + ], + [ + 487, + 65, + [ + 95 + ] + ], + [ + 487, + 84, + [ + 95 + ] + ], + [ + 487, + 95, + [ + 84 + ] + ], + [ + 487, + 84, + [ + 95 + ] + ], + [ + 487, + 24, + [ + 74 + ] + ], + [ + 487, + 35, + [ + 19 + ] + ], + [ + 487, + 54, + [ + 56 + ] + ], + [ + 487, + 24, + [ + 95 + ] + ], + [ + 487, + 24, + [ + 40 + ] + ], + [ + 487, + 24, + [ + 111 + ] + ], + [ + 487, + 56, + [ + 74 + ] + ], + [ + 487, + 54, + [ + 19 + ] + ], + [ + 487, + 111, + [ + 19 + ] + ], + [ + 487, + 56, + [ + 84 + ] + ], + [ + 487, + 19, + [ + 65 + ] + ], + [ + 487, + 65, + [ + 56 + ] + ], + [ + 487, + 65, + [ + 100 + ] + ], + [ + 487, + 84, + [ + 35 + ] + ], + [ + 487, + 54, + [ + 65 + ] + ], + [ + 487, + 35, + [ + 65 + ] + ], + [ + 487, + 100, + [ + 35 + ] + ], + [ + 487, + 56, + [ + 54 + ] + ], + [ + 487, + 19, + [ + 65 + ] + ] + ], + "payload": 4824956153877587673775933824000, + "reverse": 3714396, + "trial": 1897 + }, + "format": "r480-qnode5-boolean-search-v1", + "frame": 487, + "full_precision_candidates": 9, + "histogram": { + "41": 2, + "42": 1, + "44": 3, + "45": 11, + "46": 28, + "47": 32, + "48": 32, + "49": 72, + "50": 100, + "51": 101, + "52": 198, + "53": 210, + "54": 188, + "55": 210, + "56": 207, + "57": 160, + "58": 153, + "59": 110, + "60": 78, + "61": 54, + "62": 27, + "63": 16, + "64": 3, + "65": 2, + "66": 2 + }, + "registers": [ + 19, + 24, + 35, + 40, + 54, + 56, + 65, + 74, + 84, + 95, + 100, + 111 + ], + "search_seed": 2026101305, + "start": 2409, + "stop": 2460, + "target": [ + 3327, + 2390, + 4083, + 4, + 3935, + 4015, + 4092, + 16, + 207, + 256, + 1023, + 1 + ], + "trials": 2000 +} diff --git a/research/r480-qnode5-seed05/CERTIFICATE.json b/research/r480-qnode5-seed05/CERTIFICATE.json new file mode 100644 index 0000000000..fe3512f53f --- /dev/null +++ b/research/r480-qnode5-seed05/CERTIFICATE.json @@ -0,0 +1,184 @@ +{ + "Boolean_inputs": 4096, + "all_register_frame_paths_preserved": 720, + "assignment_seed": 5, + "base": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "block_gates": [ + 51, + 41 + ], + "complete_adds": [ + 33958, + 33938 + ], + "copy_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "endpoint_sha256": "900eeb83e7b68ae3474e74bdb5fa3cb64668877289fe540aa691450aac683bcf", + "format": "r480-qnode5-finite-certificate-v1", + "full_dirty_columns": 720, + "no_new_kappa": true, + "paid_profile": { + "1": 1200, + "2": 1440, + "4": 180, + "6": 120, + "8": 9 + }, + "precision": [ + { + "forward": 176135, + "payload": "4921056267806722187755121024000", + "payload_bits": 102, + "reverse": 3751204 + }, + { + "forward": 176135, + "payload": "4824956153877587673775933824000", + "payload_bits": 102, + "reverse": 3714396 + } + ], + "rank_mass": 5592, + "raw_records_sha256": "7d3edbc649309fedcf551b9ac0c26accfc3aeca163a2a3859fa5b7f2c932f7b5", + "rejected_controls": [ + "omit gate 0", + "omit gate 1", + "omit gate 2", + "omit gate 3", + "omit gate 4", + "omit gate 5", + "omit gate 6", + "omit gate 7", + "omit gate 8", + "omit gate 9", + "omit gate 10", + "omit gate 11", + "omit gate 12", + "omit gate 13", + "omit gate 14", + "omit gate 15", + "omit gate 16", + "omit gate 17", + "omit gate 18", + "omit gate 19", + "omit gate 20", + "omit gate 21", + "omit gate 22", + "omit gate 23", + "omit gate 24", + "omit gate 25", + "omit gate 26", + "omit gate 27", + "omit gate 28", + "omit gate 29", + "omit gate 30", + "omit gate 31", + "omit gate 32", + "omit gate 33", + "omit gate 34", + "omit gate 35", + "omit gate 36", + "omit gate 37", + "omit gate 38", + "omit gate 39", + "omit gate 40", + "bad frame", + "endpoint-valid stale cleanup contract", + "missing dirt compensation", + "endpoint-valid precision overflow", + "omit bridge 2/0", + "omit bridge 2/1", + "omit bridge 2/2", + "omit bridge 2/3", + "omit bridge 2/4", + "omit bridge 2/5", + "omit bridge 4/0", + "omit bridge 4/1", + "omit bridge 4/2", + "omit bridge 4/3", + "omit bridge 4/4", + "omit bridge 4/5", + "omit bridge 4/6", + "omit bridge 4/7", + "omit bridge 4/8", + "omit bridge 4/9", + "omit bridge 4/10", + "omit bridge 4/11", + "omit bridge 4/12", + "omit bridge 4/13", + "omit bridge 4/14", + "omit bridge 4/15", + "omit bridge 4/16", + "omit bridge 4/17", + "omit bridge 5/0", + "omit bridge 5/1", + "omit bridge 5/2", + "omit bridge 5/3", + "omit bridge 5/4", + "omit bridge 5/5", + "omit bridge 5/6", + "omit bridge 5/7", + "omit bridge 5/8", + "omit bridge 5/9", + "omit bridge 5/10", + "omit bridge 5/11", + "omit bridge 5/12", + "omit bridge 5/13", + "omit bridge 5/14", + "omit bridge 5/15", + "omit bridge 5/16", + "omit bridge 5/17", + "omit bridge 5/18", + "omit bridge 5/19", + "omit bridge 5/20", + "omit bridge 5/21", + "omit bridge 5/22", + "omit bridge 5/23" + ], + "stage_replays": [ + [ + { + "bridges": 6, + "columns": 960, + "stages": 5 + }, + { + "bridges": 18, + "columns": 1440, + "stages": 9 + }, + { + "bridges": 24, + "columns": 1680, + "stages": 11 + } + ], + [ + { + "bridges": 6, + "columns": 960, + "stages": 5 + }, + { + "bridges": 18, + "columns": 1440, + "stages": 9 + }, + { + "bridges": 24, + "columns": 1680, + "stages": 11 + } + ] + ], + "word_content_sha256": "0f2b9457b8cebb037ec9e3a393745b60ff119c6ebf7db7d0ca145142dc5ac099" +} diff --git a/research/r480-qnode5-seed05/CLAIM.md b/research/r480-qnode5-seed05/CLAIM.md new file mode 100644 index 0000000000..65646de5ee --- /dev/null +++ b/research/r480-qnode5-seed05/CLAIM.md @@ -0,0 +1,14 @@ +# Local sprint claim + +- Track: bit supplier; fresh OS assignment seed: **5** (`RandomNumberGenerator.GetInt32(100)`). +- Base: `abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`. +- Object: zero-based Q-node 5, frame 487, A[2409:2460], in the historical PR503/510 R480 word. Its twelve source registers have a fixed complete Boolean transfer. +- Method: 2,000 seeded two-sided Boolean elimination trajectories, including explicit permutation repair; select by complete ADD count and chronological positive precision bounds. No free output relabeling or helper allocation. +- Deliverable: one finite circuit witness, exact full-boundary replay and precision invoice, or a scoped search census if no admissible saving is found. No new kappa claimed. +- Expected finish: 2026-10-13 20:07 Europe/Madrid (18:07 UTC); final quarter reserved for verification. + +Three candidates considered: Q-node 5 resynthesis, six-wire quad 5 resynthesis, retained-total accumulation rescheduling. Seed 5 selects Q-node 5. PR1003 at `b0eda846c34413dabd1e75402b8ad730f8940ff2` covers Q-node 2; PR1027 covers quad12; neither source code is imported. PR823/754 precede local resynthesis. PR1048 concerns the selected R439 paid profile. This is a distinct historical circuit, and does not reopen an exhausted selected-profile search. + +Open PR metadata through #1069 and all-state GitHub searches for `R480 Q-node5` and `R480 Qnode` were checked before this claim. The two open issues (#913 and #650) are not sprint coordination issues; no pinned sprint issue was visible, so this claim is local. The system Git credential manager subsequently authenticated as `martinxxx9`; GitHub CLI is unavailable. + +Prepared for `martinxxx9` by OpenAI Codex, with substantial AI assistance in research, implementation, verification and writing. No independent human review is implied. New material: Apache-2.0. diff --git a/research/r480-qnode5-seed05/OVERLAP.json b/research/r480-qnode5-seed05/OVERLAP.json new file mode 100644 index 0000000000..68a377c97a --- /dev/null +++ b/research/r480-qnode5-seed05/OVERLAP.json @@ -0,0 +1,150 @@ +{ + "checked_at_utc": "2026-10-13T17:52:20.9140427Z", + "latest_open_pr": 1086, + "searches": [ + { + "query": "repo:CrocSwap/integer-mult-bounds R480", + "results": [ + { + "number": 597, + "title": "[Lean] Verify current R480 scalar boundaries", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/597" + }, + { + "number": 823, + "title": "Research construction: shorten historical R480 quad 1 by 12 XORs (no new kappa)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/823" + }, + { + "number": 1003, + "title": "Finite bit construction: R480 Q-node2 saves 18 ADDs (no new kappa)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1003" + }, + { + "number": 1027, + "title": "Finite R480 construction: 252 shortest quad12 circuits, 24 fewer ADDs (no new kappa)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1027" + }, + { + "number": 1034, + "title": "Research: a common dual for mixed owner assembly across 71 provider records", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1034" + }, + { + "number": 843, + "title": "Research construction: reuse R439 source sum for 2,880 fewer hosted instructions (no new kappa)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/843" + }, + { + "number": 510, + "title": "Bit word R480 at nine stages: c = 0.001587447106092548137108 (+1.41% over #493)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/510" + }, + { + "number": 503, + "title": "Bit word R480: totals on dead registers, c = 0.001574753352953808650916 (+0.595% over #493)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/503" + }, + { + "number": 1045, + "title": "Finite bit construction: exact R439 four-helper fusion below the pair floor", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1045" + }, + { + "number": 542, + "title": "Conditional kappa 0.001587467473762886: PR541 trace plus sliced R480 frames", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/542" + }, + { + "number": 589, + "title": "Bit c = 0.001733427039589844: two A-section transports on #555's punctured R439 word (+0.0216%, κ unchanged)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/589" + }, + { + "number": 539, + "title": "Conditional kappa 0.001584931113695072: literal bit bad-class charge on PR535", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/539" + }, + { + "number": 546, + "title": "Conditional kappa 0.001587480974500277: static44 global admission plus PR542 bit", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/546" + }, + { + "number": 590, + "title": "[Lean] Verify historical bit scalar boundaries", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/590" + }, + { + "number": 545, + "title": "Punctured star bit unit: bit c = 0.00165947204563779652541 (+4.54% over #510)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/545" + }, + { + "number": 535, + "title": "Post-center rank-four kernels for conditional κ = 0.001584931111785787", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/535" + }, + { + "number": 543, + "title": "Conditional κ = 0.001587467473762886: an E8 bit word with 420 helpers, c = 0.001653826988 (+4.18% over #510)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/543" + }, + { + "number": 541, + "title": "Conditional kappa 0.001587212454640692: trace refinement with a curvature-cone certificate", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/541" + }, + { + "number": 612, + "title": "[Lean] Verify current R420 boundaries and B-XOR interfaces", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/612" + }, + { + "number": 925, + "title": "Finite bit construction: R439 frame 267 reaches a 12-ADD positive-transfer minimum (no new kappa)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/925" + }, + { + "number": 548, + "title": "Conditional kappa 0.001590591090759927: observable pruning, Steinberg cancellation and response-owner composition", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/548" + }, + { + "number": 555, + "title": "Bit c = 0.001733052823: #545's punctured unit on the R420 skeleton (111 live ports, +4.79% over #543)", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/555" + } + ], + "total": 22 + }, + { + "query": "repo:CrocSwap/integer-mult-bounds \"Q-node5\"", + "results": [], + "total": 0 + }, + { + "query": "repo:CrocSwap/integer-mult-bounds \"Q-node 5\"", + "results": [ + { + "number": 5, + "title": "Faster Gaussian resampling for a conditional 1479/10^12 > 2^-30 bound", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5" + } + ], + "total": 1 + } + ], + "related_heads": [ + { + "number": 1027, + "title": "Finite R480 construction: 252 shortest quad12 circuits, 24 fewer ADDs (no new kappa)", + "head": "ebc027e26a7018b73a5a452eae269a9bfeaabce9" + }, + { + "number": 1003, + "title": "Finite bit construction: R480 Q-node2 saves 18 ADDs (no new kappa)", + "head": "b0eda846c34413dabd1e75402b8ad730f8940ff2" + } + ] +} diff --git a/research/r480-qnode5-seed05/PROOF.md b/research/r480-qnode5-seed05/PROOF.md new file mode 100644 index 0000000000..f5854b272b --- /dev/null +++ b/research/r480-qnode5-seed05/PROOF.md @@ -0,0 +1,28 @@ +# Finite substitution and exact accounting + +Let `W` be the immutable R480 word pinned in `SOURCES.json`. Its A[2409:2460] gates all act at frame 487 on the twelve registers +`(19,24,35,40,54,56,65,74,84,95,100,111)`. Their ordered Boolean row masks are +`(3327,2390,4083,4,3935,4015,4092,16,207,256,1023,1)`. + +Each candidate gate is the elementary shear `r_d <- r_d XOR r_s` at that same frame. The verifier evaluates the original and replacement on every one of the 4,096 Boolean inputs and requires every **ordered** output to agree. Since all later gates have unchanged ordered operands and are linear over F2, replacing this subword preserves its subsequent Boolean action on every source, target and dirty-helper column. The finite complete-word replay independently checks this implication rather than relying on it alone. + +The search uses `L M R = P`, where L is a product of row shears, R a product of right shears, and P an explicitly recovered permutation matrix. Its emitted chronological operations are the recorded right shears, the XOR-swap realization of P, then the reversed left shears. Every swap costs three ADDs. The verifier imports no search code and checks the resulting transfer directly; this description is not used as a certificate acceptance shortcut. + +All operands remain source registers in the same rank-four frame. The verifier reconstructs the complete frame chronology and requires every one of the 720 individual frame paths to equal the frozen word's path. It checks strict frame nesting and independently computes exact rational frame ranks. Thus the multiset of paid MOVE ranks remains unchanged. The COPY ranks are nine eights, and all copied-source lifetimes and external-work closures are checked. No helper is allocated, relocated, omitted or silently restored. + +C is rebuilt as the literal reverse of all source/helper-destination gates in A followed by B, at the rank-eight full frame. The block saves ten A ADDs and ten C ADDs. D, B, retained totals and scatter remain unchanged. The new invoice explicitly counts all scatter ADDs and cleanup ADDs and yields **33,938**, from **33,958**. The unchanged exporter produces exactly the same six-int raw records as the new independent reconstruction. The paid histogram is `{1:1200,2:1440,4:180,6:120,8:9}`, of rank mass 5,592. + +An old C circuit may remain a Boolean inverse of the new block, but fails the required literal-cleanup predicate and has a different invoice. Accordingly, the stale-cleanup control first passes the complete Boolean endpoint and is then rejected by the literal contract. This separates endpoint correctness from this source-bound implementation contract. + +For the integer lift, elementary ADDs in the signed inverse have coefficient -1. Reversing the candidate's signed shears restores its twelve inputs exactly over Z; the verifier checks its integer matrix against the identity. This does **not** imply that the original and new integer forward matrices agree, or that the complete signed multiplication construction is proved. + +Following the pinned `columns_h.cpp`/`columns_k.cpp` rule, initialize every persistent row-norm bound to one. An ADD updates `u_d <- u_d + |c| u_s`; COPY initializes external work from its unchanged original center; ERASE closes it to zero. Reverse traversal interchanges COPY and ERASE and negates ADD coefficients, leaving their absolute values one. Compute the maximum row bound in both orientations. Exact results are: + +- Original: `F=176135`, `B=3751204`, `64 F^3 B^2=4921056267806722187755121024000`. +- Candidate: `F=176135`, `B=3714396`, `64 F^3 B^2=4824956153877587673775933824000`. + +Both payloads are strictly below `2^104` and have bit length 102. No unpriced precision increase is required. A separate endpoint-valid 1,000-gate neutral insertion demonstrates that Boolean equality alone cannot admit a circuit: it passes the endpoint, but its chronological positive invoice exceeds the cap and is rejected. + +The new set-valued local engine covers all 720 formal columns, including arbitrary helper dirt. A separate integer-bitset implementation executes the literal PR363 bridged schedules with 2, 4 and 5 bank pairs on both words, covering 960, 1,440 and 1,680 formal columns respectively. Every bridge omission is rejected on the candidate. The unchanged inherited `xcheck_p.py` checks labels, all 672 closed frames, endpoint, H1-H5 and their U/J/K/restoration conclusions; the PR425 interface checker independently checks its more specialized hypotheses. These are finite checks and source-bound accounting, not a formal proof of a uniform compiler or of the full multiplication theorem. + +The selected PR589 R439 supplier is a different word. The new witness is not composed with it, PR1003's Q-node2 or PR1027's quad12. Neither an improved moment nor a new kappa follows from these twenty finite scalar ADDs. Inherited physical, hosting, precision/tape, all-size/compiler and analytic obligations remain as listed in the README. diff --git a/research/r480-qnode5-seed05/README.md b/research/r480-qnode5-seed05/README.md new file mode 100644 index 0000000000..4ba6e871f3 --- /dev/null +++ b/research/r480-qnode5-seed05/README.md @@ -0,0 +1,50 @@ +# Finite R480 Q-node 5 construction (no new kappa) + +The historical PR503/510 R480 word's zero-based Q-node **5**, frame **487**, has a **41-XOR** fixed-output replacement for its original **51-XOR** circuit. Rebuilding the required literal reverse cleanup reduces complete local ADDs from **33,958 to 33,938**. The twelve source registers, all 480 arbitrary dirty helpers, all 720 register frame paths, nine COPY/ERASE pairs and paid recursive profile are preserved. This package is a finite bit-circuit construction, not a selected supplier or a new exponent claim. + +| Complete local quantity | Frozen original | Replacement | +|---|---:|---:| +| Q-node XORs | 51 | 41 | +| ADDs including cleanup and scatter | 33,958 | 33,938 | +| Forward positive bound F | 176,135 | 176,135 | +| Reverse positive bound B | 3,751,204 | 3,714,396 | +| `64 F^3 B^2` bit length | 102 | 102 | +| Paid rank mass | 5,592 | 5,592 | + +The paid histogram remains `{1:1200, 2:1440, 4:180, 6:120, 8:9}`. The replacement preserves the full Boolean map on each physical output register; **positive integer-transfer equality with the original is not asserted**. The complete chronological precision bound, rather than a local gate-count comparison, admits the replacement under the inherited strict `64 F^3 B^2 < 2^104` rule. [PROOF.md](PROOF.md) explains the finite substitution and its limits. + +## Reproduction + +From the repository root, with Python 3.11+ and its standard library: + +```sh +python3 -I -B research/r480-qnode5-seed05/verify.py --replay-search +``` + +Expected final line: + +```text +PASS_R480_QNODE5_SEED05 gates=51->41 ADDs=33958->33938 columns=720 payload_bits=102 controls=93 rank_mass=5592 no_new_kappa +``` + +The command verifies source pins and the exact certificate, regenerates the bounded search into a temporary file, compares its bytes with `CANDIDATE.json`, and runs the pinned inherited checkers unchanged. `--output /absolute/path/outside/package` retains the rebuilt word, literal raw records, checker logs and report. Without it, a temporary output directory is created. Generated gzip containers are compared through canonical decompressed word content; the committed source gzip is an immutable input and has an exact SHA-256 pin. + +Validation covers all **4,096 Boolean block inputs** and their inverse, a signed integer forward/inverse identity for the replacement alone, complete **720-column arbitrary-dirt** endpoints by a new set-valued engine and the inherited `xcheck_p.py`, every frame climb and paid rank, byte-identical raw records against the unchanged exporter, H1-H5 and PR425 hypotheses, and literal **5/9/11-stage** Boolean scalar schedules on both words (**960/1,440/1,680 columns**). The 93 controls reject all 41 single-gate omissions, a bad frame, missing dirt compensation, endpoint-valid stale cleanup, endpoint-valid precision overflow, and all 48 candidate bridge omissions. This new Python schedule implementation follows the pinned C++ rule; native C++ execution is **not** claimed. + +## Search domain and completed coverage + +Assignment seed **5** was drawn once from OS randomness, selecting the bit-supplier track and zero-based object 5. The search fixes twelve registers and all twelve ordered output values. It runs exactly **2,000** trajectories with `random.Random(2026101305)`, using strictly weight-decreasing left/right Boolean eliminations, randomized sparse pivot choices, and paid three-XOR permutation repair. Trial **1897** supplies the selected precision-admitted 41-gate program; two 41-gate programs were encountered. The complete gate-count histogram and number of priced candidates are in `CANDIDATE.json`. Selection is by gate count, then full precision payload, then lexicographic program order. There is no early success stop. + +This is a bounded heuristic in a specified class, not an exhaustive search of all XOR circuits. It proves neither that 41 gates are minimal nor that a better supplier is impossible. No previously exhausted selected-profile search is reopened. + +## Pins, overlap and attribution + +Exact base: **`abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`**. The consumed source word, unchanged checker/exporter sources, precision/schedule reference sources and selected record are bound in [SOURCES.json](SOURCES.json). Exact witness and finite receipt are [CANDIDATE.json](CANDIDATE.json) and [CERTIFICATE.json](CERTIFICATE.json). The selected record at this base remains Jonathan Capalbo's #942 conditional **kappa 0.001661960547713947**, with DreamingOfClouds' unchanged #589 bit supplier on eumemic's #555. + +Credit eumemic for PR493's mutable-source skeleton; DreamingOfClouds for PR503/510's R480 totals/hosting and PR589; Dylan Crow for the literal record/export and formal-column contracts; DaysSky for PR363's bridged schedule; Zhihao Chen for PR425's mutable-source interface; and the retained E8 construction lineage. Jeffrey Cox's PR754 and Hao Yan's PR823 precede local circuit resynthesis. ToikY's pending **PR1003**, head **`b0eda846c34413dabd1e75402b8ad730f8940ff2`**, already establishes a 52-to-43 Q-node **2** replacement and the complete-prefix admission precedent; its implementation is not imported. PR1027, head `ebc027e26a7018b73a5a452eae269a9bfeaabce9`, concerns **quad12** integer-transfer minima. This contribution adds another object, its witness and independent finite evidence; their savings are not composed. The overlap search and local claim are recorded in [CLAIM.md](CLAIM.md). + +Prepared for **@martinxxx9** with substantial **OpenAI Codex assistance** in mathematics, implementation, verification and writing. The search and verifier were written separately by the same AI agent; no separate-agent or independent human peer review is claimed. New material is **Apache-2.0**, under the repository license; predecessor notices and sources remain unchanged. + +## Remaining obligations + +No selected-record edit, whole-hosted parent invoice, supplier binding, moment-root improvement, outer assembly, native C++ run, Lean proof, remote CI pass or measured multiplication speedup is claimed. A full hosted adoption and assembly would be separate work. All inherited all-size/compiler, common-label and mutable-source realization, correlated whole-call hosting, physical projector/routing, precision/tape/recovery and analytic assumptions remain. Finite replay is not formal verification of the multiplication theorem. `upstream/` and all consumed predecessor packages are unchanged. diff --git a/research/r480-qnode5-seed05/SOURCES.json b/research/r480-qnode5-seed05/SOURCES.json new file mode 100644 index 0000000000..448e270c12 --- /dev/null +++ b/research/r480-qnode5-seed05/SOURCES.json @@ -0,0 +1,32 @@ +{ + "base": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "candidate_sha256": "ca8cd1ad1911815db7ac7c90800c46b99f650916ba519f6d5ff2fbeb5f4c08e2", + "files": { + "certificates/selected-result.json": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp": "d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-carrier-skeleton/code/bit/independent/interface.py": "2c63a039f97e3a11ce5a6b83302d4f5beda160c1db14164a5a9b0855aeb19d3c", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz": "92e399e9a486b55229b5624632ac54f800dd9e022f2aee97f1e5f264bbc0ef5c" + }, + "git_blobs": { + "certificates/selected-result.json": "3d7529d77a5f22d8c6f64f98bd5a0e71b8eee892", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp": "00c5a3a5d81d083582f60f33dd2e7bea5049c37f", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": "42bb232fbec4de703e70cc13dc2f39a3b43a3a01", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "3632d370486a02f5456f7643ced03f8c925b2350", + "research/e8-bit-carrier-skeleton/code/bit/independent/interface.py": "8beb87c39a07e389c8f83f32ab9d17f8097ed9b1", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz": "8e59c4b5380d522b1c1cb930029a71556b2fa65f" + }, + "selected_prs": [ + 942, + 589, + 555 + ], + "source_prs": [ + 493, + 503, + 510 + ] +} diff --git a/research/r480-qnode5-seed05/VALIDATION.md b/research/r480-qnode5-seed05/VALIDATION.md new file mode 100644 index 0000000000..5eed5ff4f3 --- /dev/null +++ b/research/r480-qnode5-seed05/VALIDATION.md @@ -0,0 +1,30 @@ +# Verification record + +Environment: CPython **3.12.14**, Windows 11, standard library only for the new package and all three invoked inherited Python checks. Base and refreshed origin/main both **`abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`**. No consumed dependency or selected-record change was found on refresh. + +Completed commands from the repository root: + +```sh +python3 -I -B research/r480-qnode5-seed05/search.py +python3 -I -B research/r480-qnode5-seed05/verify.py --replay-search +python3 -I -B research/r480-qnode5-seed05/test_package.py +python3 -B scripts/verify_selected_result.py +python3 -B -m unittest discover -s tests -p test_selected_result.py +git diff --cached --check +``` + +The search completed 2,000 trajectories; 9 candidates were fully priced; two had 41 gates; trial 1897 won by the specified complete-payload tie-break. Regeneration matches `CANDIDATE.json` byte for byte (SHA-256 `ca8cd1ad1911815db7ac7c90800c46b99f650916ba519f6d5ff2fbeb5f4c08e2`). This is completed coverage of that deterministic heuristic, not exhaustive coverage of all circuits. + +The independent verifier passes the complete exact certificate: 4,096 block inputs; 720 arbitrary-dirt columns; complete ADDs 33,958 -> 33,938; rank mass 5,592; all 720 per-register frame paths; full positive payload 102 bits; 5/9/11-stage finite scalar schedules on both words; 93 rejected controls. The reference xcheck validates 120 E8 labels and all 672 closed frames, original H1-H5 and U/J/K/restoration conclusions. The PR425 checker passes unchanged. Independently reconstructed literal raw records equal the unchanged exporter byte for byte. + +Five package test groups pass, including a minimal relocated checkout under `python -I -O -B`, complete search regeneration, and adversarial source/candidate corruption rejected with optimization enabled. Five selected-record test groups pass and the accepted kappa remains unchanged. The new verifier uses explicit exceptions for acceptance conditions, so optimization cannot erase them; inherited assertion-based checkers run in unoptimized subprocesses. + +A development test exposed that Python's integer histogram keys were compared with JSON's string keys. This caused a safe certificate-drift rejection, not a false acceptance. Report keys were canonicalized and the complete normal and relocated/optimized runs were repeated successfully. No failed receipt was edited into a pass. + +Final staging exposed Windows text-mode CRLF output in the witness generator. Output is now explicitly LF, the witness SHA pin is updated to those portable bytes, and a minimal checkout reconstructed from the exact Git index (18 files) passes complete verification and byte-identical search regeneration. The frozen input files are copied from their exact staged blobs; no line-ending relaxation is used in acceptance. + +`make verify` was attempted once and could not start: **`make` is not installed/on PATH**. No C++ compiler was available on PATH, so the native C++ legality/5/9/11-stage executables were not built or run. The corresponding finite schedule rule is pinned and replayed by the new Python engine; this does not imply a native, repository-wide, remote CI, hosted-parent, selected-frontier cold replay, or full theorem pass. No selected construction or shared generator was changed, and no unrelated artifacts were regenerated. + +Final metadata was refreshed through open PR **#1086**. All-state R480 results still include PR1003's Q-node2 and PR1027's quad12; their heads are unchanged. The explicit `Q-node5` query had zero results. The quoted `Q-node 5` query returned unrelated PR5 (a GitHub search tokenization false positive), which is not treated as evidence of circuit overlap. [OVERLAP.json](OVERLAP.json) preserves the concrete query/results snapshot. No priority, newest-record, or best-known-circuit claim is made. + +The final quarter of the actual work is reserved for verification, refresh and handoff. The local claim will be updated once with the submitted result and PR link. Contributor and AI-assistance disclosure are in README/CLAIM. New files are Apache-2.0. diff --git a/research/r480-qnode5-seed05/search.py b/research/r480-qnode5-seed05/search.py new file mode 100644 index 0000000000..fe887b1f26 --- /dev/null +++ b/research/r480-qnode5-seed05/search.py @@ -0,0 +1,182 @@ +"""Bounded fixed-output Boolean resynthesis; Apache-2.0, OpenAI Codex assistance.""" +import collections +import argparse +import gzip +import json +import random +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / 'research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz' +FRAME, START, STOP = 487, 2409, 2460 +REGS = [19, 24, 35, 40, 54, 56, 65, 74, 84, 95, 100, 111] +TRIALS, SEED = 2000, 2026101305 + + +def load_word(): + return json.loads(gzip.decompress(SOURCE.read_bytes())) + + +def matrix(gates): + index = {r: i for i, r in enumerate(REGS)} + rows = [1 << i for i in range(12)] + for f, d, sources in gates: + if f != FRAME: + raise ValueError('unexpected block frame') + for s in sources: + rows[index[d]] ^= rows[index[s]] + return rows + + +def synthesize(target, rng): + """L M R = P; emit R^-1, P, L^-1 chronologically, paying swaps.""" + rows = target[:] + left, right = [], [] + active_r, active_c = list(range(12)), list(range(12)) + for _ in range(12): + # Strictly weight-decreasing row/column moves on the active minor. + while True: + columns = {c: sum(((rows[r] >> c) & 1) << r for r in active_r) + for c in active_c} + best, choices = 0, [] + for a in active_r: + for b in active_r: + if a == b: + continue + gain = rows[a].bit_count() - (rows[a] ^ rows[b]).bit_count() + if gain > best: + best, choices = gain, [('row', a, b)] + elif gain == best and gain > 0: + choices.append(('row', a, b)) + for a in active_c: + for b in active_c: + if a == b: + continue + gain = columns[b].bit_count() - (columns[b] ^ columns[a]).bit_count() + if gain > best: + best, choices = gain, [('col', a, b)] + elif gain == best and gain > 0: + choices.append(('col', a, b)) + if not choices: + break + kind, a, b = rng.choice(choices) + if kind == 'row': + rows[a] ^= rows[b] + left.append((a, b)) + else: + for r in active_r: + if rows[r] >> a & 1: + rows[r] ^= 1 << b + right.append((a, b)) + # Choose a sparse pivot and clear its column and row. + pivots = [(rows[r].bit_count() + sum(rows[x] >> c & 1 for x in active_r), r, c) + for r in active_r for c in active_c if rows[r] >> c & 1] + score = min(p[0] for p in pivots) + _, r, c = rng.choice([p for p in pivots if p[0] == score]) + for x in active_r: + if x != r and rows[x] >> c & 1: + rows[x] ^= rows[r] + left.append((x, r)) + for y in active_c: + if y != c and rows[r] >> y & 1: + for x in active_r: + if rows[x] >> c & 1: + rows[x] ^= 1 << y + right.append((c, y)) + active_r.remove(r) + active_c.remove(c) + if sorted(rows) != [1 << i for i in range(12)]: + raise ValueError('elimination did not reach a permutation') + perm = [1 << i for i in range(12)] + swaps = [] + for i in range(12): + if perm[i] != rows[i]: + j = perm.index(rows[i]) + swaps.extend([(i, j), (j, i), (i, j)]) + perm[i], perm[j] = perm[j], perm[i] + ops = right + swaps + left[::-1] + gates = [[FRAME, REGS[a], [REGS[b]]] for a, b in ops] + if matrix(gates) != target: + raise ValueError('synthesis orientation error') + return gates + + +def replace(word, gates): + w = dict(word) + w['A'] = word['A'][:START] + gates + word['A'][STOP:] + w['C'] = [[1, d, list(ss)] for _, d, ss in reversed(w['A'] + w['B']) + if d < w['v'] or d >= 2 * w['v']] + return w + + +def stream(w): + result = [] + for phase in ('D', 'A'): + result.extend(('add', d, s) for _, d, ss in w[phase] for s in ss) + temp = 2 * w['v'] + w['R'] + for k, q in enumerate(w['ret']): + result.append(('copy', temp, q)) + result.extend(('add', w['v'] + t, temp) for t, row in enumerate(w['scatter']) if k in row) + result.append(('erase', temp, q)) + for phase in ('B', 'C'): + result.extend(('add', d, s) for _, d, ss in w[phase] for s in ss) + return result + + +def bounds(w): + events = stream(w) + peaks = [] + for reverse in (False, True): + norms = [1] * (2 * w['v'] + w['R'] + 1) + peak = 1 + for kind, d, s in (reversed(events) if reverse else events): + if reverse and kind != 'add': + kind = 'erase' if kind == 'copy' else 'copy' + if kind == 'add': + norms[d] += norms[s] + peak = max(peak, norms[d]) + elif kind == 'copy': + norms[d] = norms[s] + else: + norms[d] = 0 + peaks.append(peak) + f, b = peaks + return f, b, 64 * f ** 3 * b ** 2 + + +def run_search(): + word = load_word() + target = matrix(word['A'][START:STOP]) + rng = random.Random(SEED) + histogram = collections.Counter() + best = None + candidates = 0 + for trial in range(TRIALS): + gates = synthesize(target, rng) + histogram[len(gates)] += 1 + if best is not None and len(gates) > len(best['gates']): + continue + f, b, payload = bounds(replace(word, gates)) + candidates += 1 + if payload >= 1 << 104: + continue + key = (len(gates), payload, gates) + if best is None or key < (len(best['gates']), best['payload'], best['gates']): + best = dict(trial=trial, gates=gates, forward=f, reverse=b, payload=payload) + if best is None: + raise ValueError('no precision-admitted candidate') + return dict(format='r480-qnode5-boolean-search-v1', assignment_seed=5, + search_seed=SEED, trials=TRIALS, frame=FRAME, start=START, stop=STOP, + registers=REGS, target=target, histogram=dict(sorted(histogram.items())), + full_precision_candidates=candidates, best=best) + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path, default=HERE / 'CANDIDATE.json') + args = parser.parse_args() + result = run_search() + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n', encoding='utf-8', newline='\n') + print('SEARCH_COMPLETE trials=%s gates=51->%s trial=%s payload_bits=%s' % + (TRIALS, len(result['best']['gates']), result['best']['trial'], result['best']['payload'].bit_length())) diff --git a/research/r480-qnode5-seed05/test_package.py b/research/r480-qnode5-seed05/test_package.py new file mode 100644 index 0000000000..4b84f27ec4 --- /dev/null +++ b/research/r480-qnode5-seed05/test_package.py @@ -0,0 +1,79 @@ +"""Fail-closed package checks. Apache-2.0; substantial OpenAI Codex assistance.""" +import copy +import importlib.util +import json +import shutil +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('qnode5_verifier', HERE / 'verify.py') +verifier = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verifier) + + +class PackageChecks(unittest.TestCase): + def test_dense_boolean_transfer_preserves_order(self): + candidate = json.loads((HERE / 'CANDIDATE.json').read_text())['best']['gates'] + changed = copy.deepcopy(candidate) + changed[0][1] = 24 + with self.assertRaises(verifier.Reject): + verifier.need(all(verifier.block_map(candidate, 1 << i) == + verifier.block_map(changed, 1 << i) for i in range(12)), 'wrong output') + + def test_self_source_rejected(self): + with self.assertRaises(verifier.Reject): + verifier.block_map([[487, 19, [19]]], 1) + + def test_out_of_scope_register_rejected(self): + with self.assertRaises(verifier.Reject): + verifier.block_map([[487, 19, [120]]], 1) + + def test_source_pins_and_candidate_fail_closed(self): + root = verifier.ROOT + with tempfile.TemporaryDirectory(prefix='qnode5-controls-') as temp: + copy_root = Path(temp) + package = copy_root / 'research/r480-qnode5-seed05' + shutil.copytree(HERE, package) + pins = json.loads((package / 'SOURCES.json').read_text()) + for relative in pins['files']: + destination = copy_root / relative + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(root / relative, destination) + source = copy_root / verifier.SOURCE + source.write_bytes(source.read_bytes() + b'corruption') + failed = subprocess.run([sys.executable, '-I', '-O', '-B', package / 'verify.py'], + capture_output=True, text=True) + self.assertNotEqual(failed.returncode, 0) + self.assertIn('source pin:', failed.stderr) + shutil.copyfile(root / verifier.SOURCE, source) + candidate = package / 'CANDIDATE.json' + candidate.write_bytes(candidate.read_bytes() + b' ') + failed = subprocess.run([sys.executable, '-I', '-O', '-B', package / 'verify.py'], + capture_output=True, text=True) + self.assertNotEqual(failed.returncode, 0) + self.assertIn('candidate digest', failed.stderr) + + def test_relocated_optimized_full_replay(self): + with tempfile.TemporaryDirectory(prefix='qnode5-relocated-') as temp: + root = Path(temp) + package = root / 'research/r480-qnode5-seed05' + shutil.copytree(HERE, package) + pins = json.loads((package / 'SOURCES.json').read_text()) + for relative in pins['files']: + destination = root / relative + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verifier.ROOT / relative, destination) + result = subprocess.run([sys.executable, '-I', '-O', '-B', package / 'verify.py', + '--replay-search', '--output', root / 'out'], capture_output=True, text=True) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn('controls=93', result.stdout) + self.assertEqual(json.loads((root / 'out/REPORT.json').read_text()), + json.loads((HERE / 'CERTIFICATE.json').read_text())) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/r480-qnode5-seed05/verify.py b/research/r480-qnode5-seed05/verify.py new file mode 100644 index 0000000000..ec11f315b7 --- /dev/null +++ b/research/r480-qnode5-seed05/verify.py @@ -0,0 +1,374 @@ +"""Independent finite verifier; no search imports. Apache-2.0; Codex assistance.""" +import argparse +import collections +import copy +import gzip +import hashlib +import json +import struct +import subprocess +import sys +import tempfile +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = 'research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz' +REGS = [19, 24, 35, 40, 54, 56, 65, 74, 84, 95, 100, 111] +FRAME, START, STOP = 487, 2409, 2460 + + +class Reject(ValueError): + pass + + +def need(condition, label): + if not condition: + raise Reject(label) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def rank(vectors): + pivots = {} + for vector in vectors: + row = list(map(Fraction, vector)) + for k in sorted(pivots): + scale = row[k] + row = [a - scale * b for a, b in zip(row, pivots[k])] + k = next((i for i, x in enumerate(row) if x), None) + if k is not None: + pivots[k] = [x / row[k] for x in row] + return len(pivots) + + +def block_map(gates, value): + values = {r: (value >> i) & 1 for i, r in enumerate(REGS)} + for f, d, sources in gates: + need(f == FRAME and d in values and len(sources) == 1, + 'block gate shape/frame') + s = sources[0] + need(s in values and d != s, 'block source/destination') + values[d] ^= values[s] + return sum(values[r] << i for i, r in enumerate(REGS)) + + +def make_word(base, gates): + w = copy.deepcopy(base) + w['A'][START:STOP] = copy.deepcopy(gates) + w['C'] = [[1, d, list(ss)] for _, d, ss in reversed(w['A'] + w['B']) + if d < w['v'] or d >= 2 * w['v']] + return w + + +def records(w, dimensions, check_cleanup=True): + """Reconstruct the exact raw six-int contract, including every MOVE.""" + v, n = w['v'], 2 * w['v'] + w['R'] + need(len(w['start']) == len(w['final']) == n, 'boundary frame count') + if check_cleanup: + literal = [[1, d, list(ss)] for _, d, ss in reversed(w['A'] + w['B']) + if d < v or d >= 2 * v] + need(w['C'] == literal, 'literal cleanup contract') + current = w['start'][:] + masks = [set(f) for f in w['frames']] + trails = [[f] for f in current] + result = [] + paid = collections.Counter() + copies = [] + + def move(r, frame): + need(0 <= r < n and 0 <= frame < len(masks), 'register/frame range') + old = current[r] + if old != frame: + need(masks[old] < masks[frame] and dimensions[old] < dimensions[frame], + 'strict nested frame climb') + charge = dimensions[frame] - dimensions[old] + result.append((0, r, old, frame, charge, 0)) + paid[charge] += 1 + current[r] = frame + trails[r].append(frame) + + def phase(name, number): + for frame, d, sources in w[name]: + need(len({d, *sources}) == 1 + len(sources), 'distinct operands') + for r in [d, *sources]: + move(r, frame) + result.extend((1, d, s, 1, frame, number) for s in sources) + + phase('D', 1) + phase('A', 2) + need(all(current[v + t] == 0 for t in range(v)), 'targets before scatter') + for k, q in enumerate(w['ret']): + need(2 * v <= q < n, 'retained total register') + frame = current[q] + charge = dimensions[frame] + result.append((2, q, n, frame, 0, charge)) + copies.append(charge) + paid[charge] += 1 + for t, row in enumerate(w['scatter']): + need(len(row) == len(set(row)) and all(0 <= i < len(w['ret']) for i in row), + 'scatter indices') + if k in row: + result.append((1, v + t, n, 1, 0, 3)) + result.append((3, q, n, frame, 0, 0)) + phase('B', 4) + phase('C', 5) + for r, frame in enumerate(w['final']): + move(r, frame) + return result, trails, dict(sorted(paid.items())), copies + + +def events(raw): + return [(op, a, b, c) for op, a, b, c, _, _ in raw if op != 0] + + +def positive_bounds(raw, n): + """Exact cancellation-free row-l1 recurrence of columns_h/k.cpp.""" + peaks = [] + for reverse in (False, True): + norms, peak, center = [1] * (n + 1), 1, None + seq = raw[::-1] if reverse else raw + for op, a, b, coefficient, _, _ in seq: + if not op: + continue + if op == 1: + need(a != n and a != b and (b != n or center is not None), 'ADD shape/temp') + need(a != center, 'copied center must stay immutable') + norms[a] += abs(coefficient) * norms[b] + peak = max(peak, norms[a]) + elif (op == 2) != reverse: + need(center is None and b == n, 'COPY opening') + center = a + norms[n] = norms[a] + else: + need(center == a and b == n, 'ERASE source binding') + center = None + norms[n] = 0 + need(center is None, 'COPY closure') + peaks.append(peak) + f, b = peaks + payload = 64 * f ** 3 * b ** 2 + need(payload < 1 << 104, 'strict 104-bit precision') + return dict(forward=f, reverse=b, payload=str(payload), payload_bits=payload.bit_length()) + + +def formal_endpoint(raw, n): + """Set-valued symbolic replay, separate from search's integer matrices.""" + values = [{i} for i in range(n)] + [set()] + for op, a, b, coefficient in events(raw): + if op == 1: + if coefficient & 1: + values[a].symmetric_difference_update(values[b]) + elif op == 2: + values[n] = values[a].copy() + else: + values[n].clear() + want = [{r, r - 120} if 120 <= r < 240 else {r} for r in range(n)] + [set()] + need(values == want, 'complete arbitrary-dirt Boolean endpoint') + return sha(canonical([sorted(s) for s in values])) + + +def stage_replay(raw, pairs, skip=None): + """Literal bridged scalar schedule from DaysSky's PR363 rule, over F2.""" + v, helpers, local = 120, 480, 720 + total = 2 * pairs * v + helpers + values = [1 << i for i in range(total)] + [0] + schedule, after = [], [[] for _ in range(2 * pairs + 1)] + for stage in range(2 * pairs + 1): + pair = 1 if stage < 3 else (stage + 1) // 2 + reverse = stage % 2 == 1 + x, y = 2 * (pair - 1), 2 * (pair - 1) + 1 + schedule.append((y, x, reverse) if reverse else (x, y, reverse)) + for q in range(2, pairs + 1): + x0, y0, x1, y1 = 2 * (q - 2), 2 * (q - 2) + 1, 2 * (q - 1), 2 * (q - 1) + 1 + after[2 * q - 3].extend([(x0, x1), (y1, y0)]) + after[2 * q - 2].extend([(y1, y0), (x0, x1)]) + for q in range(pairs, 1, -1): + after[-1].extend([(2 * (q - 2) + 1, 2 * (q - 1) + 1), + (2 * (q - 1), 2 * (q - 2))]) + seq = events(raw) + bridge = 0 + for stage, (xb, yb, reverse) in enumerate(schedule): + def mapped(r): + if r < v: + return xb * v + r + if r < 2 * v: + return yb * v + r - v + return 2 * pairs * v + r - 2 * v if r < local else total + for op, a, b, coefficient in (reversed(seq) if reverse else seq): + if op == 1: + if coefficient & 1: + values[mapped(a)] ^= values[mapped(b)] + elif (op == 2) != reverse: + values[total] = values[mapped(a)] + else: + values[total] = 0 + if stage == 0: + expected = [(1 << i) ^ (1 << (i - v)) if v <= i < 2 * v else 1 << i + for i in range(total)] + [0] + need(values == expected, 'stage-zero full boundary') + for d, s in after[stage]: + if bridge != skip: + for i in range(v): + values[d * v + i] ^= values[s * v + i] + bridge += 1 + for bank in range(0, 2 * pairs, 2): + for i in range(v): + a, b = bank * v + i, (bank + 1) * v + i + values[a], values[b] = values[b], values[a] + need(values == [1 << i for i in range(total)] + [0], 'bridged full-column endpoint') + return dict(stages=2 * pairs + 1, columns=total, bridges=bridge) + + +def integer_inverse(gates): + values = [[int(i == j) for j in range(12)] for i in range(12)] + index = {r: i for i, r in enumerate(REGS)} + for reverse in (False, True): + for _, d, sources in (reversed(gates) if reverse else gates): + for s in sources: + sign = -1 if reverse else 1 + values[index[d]] = [a + sign * b for a, b in zip(values[index[d]], values[index[s]])] + need(values == [[int(i == j) for j in range(12)] for i in range(12)], 'signed integer inverse') + + +def reject(action, label): + try: + action() + except (Reject, IndexError, KeyError): + return label + raise Reject('negative control unexpectedly passed: ' + label) + + +def verify_pins(): + pins = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + for relative, digest in pins['files'].items(): + need(sha((ROOT / relative).read_bytes()) == digest, 'source pin: ' + relative) + return pins + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path) + parser.add_argument('--replay-search', action='store_true') + parser.add_argument('--write-certificate', action='store_true') + args = parser.parse_args() + pins = verify_pins() + base = json.loads(gzip.decompress((ROOT / SOURCE).read_bytes())) + candidate_bytes = (HERE / 'CANDIDATE.json').read_bytes() + need(sha(candidate_bytes) == pins['candidate_sha256'], 'candidate digest') + candidate = json.loads(candidate_bytes) + gates = candidate['best']['gates'] + need(candidate['frame'] == FRAME and candidate['start'] == START and candidate['stop'] == STOP + and candidate['registers'] == REGS and candidate['trials'] == 2000, 'search domain') + need(sum(candidate['histogram'].values()) == 2000, 'search coverage count') + original = base['A'][START:STOP] + need(len(original) == 51 and len(gates) == 41, 'expected saving') + for value in range(1 << 12): + need(block_map(original, value) == block_map(gates, value), 'exhaustive fixed-output Boolean transfer') + need(block_map(list(reversed(gates)), block_map(gates, value)) == value, 'Boolean block inverse') + integer_inverse(gates) + w = make_word(base, gates) + dimensions = [rank(w['lines'][i] for i in frame) for frame in w['frames']] + need(dimensions[FRAME] == 4 and dimensions[0] == 0 and dimensions[1] == 8, 'frame ranks') + base_raw, base_trails, base_paid, base_copies = records(base, dimensions) + raw, trails, paid, copies = records(w, dimensions) + need(base_trails == trails and base_paid == paid and base_copies == copies, 'all paid paths preserved') + need(paid == {1:1200, 2:1440, 4:180, 6:120, 8:9}, 'historical paid profile') + need(base['D'] == w['D'] and base['B'] == w['B'], 'D and B unchanged') + endpoints = [formal_endpoint(data, 720) for data in (base_raw, raw)] + need(endpoints[0] == endpoints[1], 'baseline/candidate boundary') + precision = [positive_bounds(data, 720) for data in (base_raw, raw)] + need((precision[1]['forward'], precision[1]['reverse'], int(precision[1]['payload'])) == + (candidate['best']['forward'], candidate['best']['reverse'], candidate['best']['payload']), + 'independent positive invoice vs search') + counts = [sum(r[0] == 1 for r in data) for data in (base_raw, raw)] + need(counts == [33958, 33938], 'full ADD invoice including literal cleanup') + stages = [[stage_replay(data, k) for k in (2, 4, 5)] for data in (base_raw, raw)] + controls = [] + for j in range(len(gates)): + omitted = gates[:j] + gates[j+1:] + controls.append(reject(lambda g=omitted: need(all(block_map(g, 1 << i) == + block_map(original, 1 << i) for i in range(12)), 'omitted gate transfer'), + 'omit gate %s' % j)) + wrong_frame = copy.deepcopy(w) + wrong_frame['A'][START][0] = 0 + controls.append(reject(lambda: records(wrong_frame, dimensions), 'bad frame')) + no_cleanup = copy.deepcopy(w) + no_cleanup['C'] = base['C'] + formal_endpoint(records(no_cleanup, dimensions, check_cleanup=False)[0], 720) + controls.append(reject(lambda: records(no_cleanup, dimensions), 'endpoint-valid stale cleanup contract')) + bad_dirt = copy.deepcopy(w) + bad_dirt['D'][0][2].pop() + controls.append(reject(lambda: formal_endpoint(records(bad_dirt, dimensions)[0], 720), 'missing dirt compensation')) + # Endpoint-valid neutral insertion still fails precision: pairs cancel only over F2. + inflated = copy.deepcopy(w) + neutral = [[FRAME, REGS[0], [REGS[1]]]] * 1000 + inflated['A'][START:START] = neutral + inflated['C'] = [[1, d, list(ss)] for _, d, ss in reversed(inflated['A'] + inflated['B']) + if d < 120 or d >= 240] + inflated_raw = records(inflated, dimensions)[0] + formal_endpoint(inflated_raw, 720) + controls.append(reject(lambda: positive_bounds(inflated_raw, 720), 'endpoint-valid precision overflow')) + for pairs in (2, 4, 5): + for skip in range(6 * (pairs - 1)): + controls.append(reject(lambda k=pairs, s=skip: stage_replay(raw, k, s), + 'omit bridge %s/%s' % (pairs, skip))) + out = args.output.resolve() if args.output else Path(tempfile.mkdtemp(prefix='qnode5-')) + need(out != HERE and HERE not in out.parents, 'output must be outside package') + out.mkdir(parents=True, exist_ok=True) + word_path = out / 'candidate-word.json.gz' + word_path.write_bytes(gzip.compress(canonical(w), mtime=0)) + # Pinned inherited checkers execute unchanged. Finite checks, not a full theorem proof. + commands = [ + [ROOT / 'research/e8-bit-p111-tuned/code/xcheck_p.py', word_path, '--json', out / 'interface.json'], + [ROOT / 'research/e8-bit-carrier-skeleton/code/bit/independent/interface.py', word_path], + [ROOT / 'research/e8-bit-carrier-skeleton/code/bit/export_records.py', word_path, out / 'export'], + ] + for j, command in enumerate(commands): + process = subprocess.run([sys.executable, '-I', '-B', *map(str, command)], capture_output=True, text=True) + (out / ('inherited-check-%s.log' % j)).write_text(process.stdout + process.stderr, encoding='utf-8') + need(process.returncode == 0, 'inherited checker %s: %s' % (j, process.stderr[-1000:])) + expected_binary = b''.join(struct.pack('<6i', *row) for row in raw) + need((out / 'export/249-records.bin').read_bytes() == expected_binary, 'unchanged exporter exact records') + iface = json.loads((out / 'interface.json').read_text()) + need(iface['status'] == 'PASS_EXACT_REPLAY_AND_INTERLEAVED_INTERFACE' and + all(iface['hypotheses'].values()) and all(iface['conclusion'].values()), 'inherited H1-H5') + if args.replay_search: + # A subprocess isolates the generator from this independent implementation. + with tempfile.TemporaryDirectory(prefix='qnode5-search-') as scratch: + search_result = Path(scratch) / 'CANDIDATE.json' + process = subprocess.run([sys.executable, '-I', '-B', HERE / 'search.py', '--output', search_result], + capture_output=True, text=True) + need(process.returncode == 0, 'bounded search replay') + need(search_result.read_bytes() == candidate_bytes, 'deterministic search replay') + report = dict(format='r480-qnode5-finite-certificate-v1', base=pins['base'], + assignment_seed=5, block_gates=[51, 41], complete_adds=counts, + word_content_sha256=sha(canonical(w)), endpoint_sha256=endpoints[1], + raw_records_sha256=sha(expected_binary), paid_profile={str(k): v for k, v in paid.items()}, + rank_mass=sum(k * v for k, v in paid.items()), copy_ranks=copies, + all_register_frame_paths_preserved=len(trails), Boolean_inputs=4096, + full_dirty_columns=720, precision=precision, stage_replays=stages, + rejected_controls=controls, no_new_kappa=True) + encoded = json.dumps(report, indent=2, sort_keys=True) + '\n' + if args.write_certificate: + (HERE / 'CERTIFICATE.json').write_text(encoded, encoding='utf-8', newline='\n') + else: + need(json.loads((HERE / 'CERTIFICATE.json').read_text(encoding='utf-8')) == report, 'certificate drift') + (out / 'REPORT.json').write_text(encoded, encoding='utf-8', newline='\n') + print('PASS_R480_QNODE5_SEED05 gates=51->41 ADDs=33958->33938 columns=720 ' + 'payload_bits=102 controls=%s rank_mass=5592 no_new_kappa' % len(controls)) + + +if __name__ == '__main__': + try: + main() + except Reject as error: + print('REJECT', error, file=sys.stderr) + raise SystemExit(1) From 9f33d4d10e59a7575d28378e63c033a4b0c13d3f Mon Sep 17 00:00:00 2001 From: martinxxx9 <341803289+martinxxx9@users.noreply.github.com> Date: Tue, 13 Oct 2026 19:56:00 +0200 Subject: [PATCH 2/2] Record Q-node5 sprint result and review link --- research/r480-qnode5-seed05/CLAIM.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/research/r480-qnode5-seed05/CLAIM.md b/research/r480-qnode5-seed05/CLAIM.md index 65646de5ee..4064292264 100644 --- a/research/r480-qnode5-seed05/CLAIM.md +++ b/research/r480-qnode5-seed05/CLAIM.md @@ -12,3 +12,7 @@ Three candidates considered: Q-node 5 resynthesis, six-wire quad 5 resynthesis, Open PR metadata through #1069 and all-state GitHub searches for `R480 Q-node5` and `R480 Qnode` were checked before this claim. The two open issues (#913 and #650) are not sprint coordination issues; no pinned sprint issue was visible, so this claim is local. The system Git credential manager subsequently authenticated as `martinxxx9`; GitHub CLI is unavailable. Prepared for `martinxxx9` by OpenAI Codex, with substantial AI assistance in research, implementation, verification and writing. No independent human review is implied. New material: Apache-2.0. + +## Result (single claim update) + +Submitted [PR1089](https://github.com/CrocSwap/integer-mult-bounds/pull/1089): 41 rather than 51 fixed-output Q-node XORs, full literal word 33,958 -> 33,938 ADDs, unchanged rank mass 5,592 and all 720 frame paths, complete 102-bit precision admission. The 2,000-trajectory search, independent 720-column replay, original H1-H5/interface checks, exact exporter equality, 5/9/11-stage Python replays and 93 controls pass. Five package tests (including relocated optimized verification), five selected-record tests and a replay from exact staged Git blobs pass. No new kappa, native C++ pass, repository-wide suite, hosted/outer adoption or full theorem proof is claimed. Finished within the planned 30-minute budget, with the final quarter spent verifying and handing off the result.