From 12470750d68b13b88e91277cacf95efddab95a59 Mon Sep 17 00:00:00 2001 From: woklerx <338878655+woklerx@users.noreply.github.com> Date: Tue, 13 Oct 2026 08:57:59 -0700 Subject: [PATCH] Research: certify frame281 12/13 boundary and shorter circuit --- .../r439-frame281-seed15/CERTIFICATE.json | 794 ++++++++++++++++++ research/r439-frame281-seed15/CLAIM.md | 56 ++ research/r439-frame281-seed15/NOTICE.md | 51 ++ research/r439-frame281-seed15/OVERLAP.json | 127 +++ research/r439-frame281-seed15/PROOF.md | 114 +++ research/r439-frame281-seed15/README.md | 124 +++ research/r439-frame281-seed15/SOURCES.json | 38 + research/r439-frame281-seed15/VALIDATION.md | 76 ++ research/r439-frame281-seed15/WITNESS.json | 525 ++++++++++++ research/r439-frame281-seed15/independent.py | 287 +++++++ research/r439-frame281-seed15/native.py | 189 +++++ research/r439-frame281-seed15/search.py | 202 +++++ research/r439-frame281-seed15/verify.py | 258 ++++++ 13 files changed, 2841 insertions(+) create mode 100644 research/r439-frame281-seed15/CERTIFICATE.json create mode 100644 research/r439-frame281-seed15/CLAIM.md create mode 100644 research/r439-frame281-seed15/NOTICE.md create mode 100644 research/r439-frame281-seed15/OVERLAP.json create mode 100644 research/r439-frame281-seed15/PROOF.md create mode 100644 research/r439-frame281-seed15/README.md create mode 100644 research/r439-frame281-seed15/SOURCES.json create mode 100644 research/r439-frame281-seed15/VALIDATION.md create mode 100644 research/r439-frame281-seed15/WITNESS.json create mode 100644 research/r439-frame281-seed15/independent.py create mode 100644 research/r439-frame281-seed15/native.py create mode 100644 research/r439-frame281-seed15/search.py create mode 100644 research/r439-frame281-seed15/verify.py diff --git a/research/r439-frame281-seed15/CERTIFICATE.json b/research/r439-frame281-seed15/CERTIFICATE.json new file mode 100644 index 0000000000..f4e99cd810 --- /dev/null +++ b/research/r439-frame281-seed15/CERTIFICATE.json @@ -0,0 +1,794 @@ +{ + "base_commit": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87", + "columns": 661, + "controls_rejected": [ + "drop circuit gate", + "reverse circuit operands", + "F2-neutral positive inflation", + "drop cleanup gate", + "stale nonliteral cleanup", + "illegal frame descent", + "missing dirty compensation" + ], + "exported_records": { + "original": { + "adds": 23673, + "copies": 9, + "erasures": 9, + "moves": 2911, + "paid_histogram": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "records": 26602, + "records_sha256": "50275275cdcdef8cd28edfda8f07bb02af6d113ff91bcba952f6650c90ccf564" + }, + "replacement": { + "adds": 23671, + "copies": 9, + "erasures": 9, + "moves": 2911, + "paid_histogram": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "records": 26600, + "records_sha256": "f5a04de71fd30c0aeee9637fe7c712abab8dbe0cb86e6559e9dd6502490a31b0" + } + }, + "frame": 281, + "independent": { + "F2_matrix": [ + [ + 1, + 0, + 1, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 0, + 1 + ], + [ + 1, + 1, + 1, + 1, + 0, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1 + ] + ], + "boolean_inputs": 64, + "class": "six labelled registers; elementary positive ADD only; exact integer target; no ancillas", + "controls_rejected": [ + "dropped circuit ADD", + "reversed ADD operands", + "F2-neutral positive-transfer inflation", + "minimum underclaim", + "minimum overclaim", + "budget exhaustion is not a proof", + "reverse-guard minimum underclaim", + "reverse-guard minimum overclaim", + "reverse-guard budget exhaustion is not a proof" + ], + "independent_minimum": { + "completed_expansion_depths": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "edges_from_completed_layers": 208824, + "layers": [ + 1, + 10, + 54, + 207, + 808, + 2258, + 4894, + 8249, + 10256, + 8635, + 4493, + 1214, + 124 + ], + "method": "first-ADD column-subtraction BFS", + "minimum": 12, + "visited_states": 41203 + }, + "independent_reverse_guard_minimum": { + "completed_expansion_depths": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12 + ], + "layers": [ + 1, + 6, + 18, + 40, + 70, + 99, + 120, + 122, + 106, + 77, + 46, + 22, + 7, + 1 + ], + "method": "first-ADD paired column-subtraction and column-addition BFS", + "minimum": 13, + "positive_residual_edges_from_completed_layers": 5005, + "reverse_guard_pruned_edges": 2943, + "visited_states": 735 + }, + "positive_matrices": { + "forward": { + "original": [ + [ + 3, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 0, + 1 + ], + [ + 3, + 3, + 1, + 1, + 2, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1 + ] + ], + "replacement": [ + [ + 3, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 0, + 1 + ], + [ + 3, + 3, + 1, + 1, + 2, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1 + ] + ] + }, + "reverse": { + "original": [ + [ + 1, + 0, + 1, + 1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 0, + 2, + 1, + 1, + 0 + ], + [ + 1, + 1, + 3, + 3, + 0, + 1 + ], + [ + 1, + 1, + 3, + 3, + 1, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 1 + ] + ], + "replacement": [ + [ + 1, + 0, + 1, + 1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 2, + 2, + 1, + 1, + 0 + ], + [ + 1, + 1, + 3, + 3, + 0, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 0, + 2, + 3, + 2, + 0, + 1 + ] + ] + } + }, + "precision_scope": "reverse increases require full-word prefix and native payload pricing", + "reverse_entrywise_dominated": false, + "reverse_increased_entries": [ + { + "column": 1, + "original": 0, + "replacement": 2, + "row": 2 + }, + { + "column": 1, + "original": 0, + "replacement": 2, + "row": 5 + }, + { + "column": 2, + "original": 1, + "replacement": 3, + "row": 5 + }, + { + "column": 3, + "original": 0, + "replacement": 2, + "row": 5 + } + ] + }, + "kappa_claim": "none; unchanged paid profile; full hosted adoption not performed", + "labels": { + "frames": 636, + "gram_det": 1, + "labels": 111, + "lattice_rank": 8, + "punctured": 9, + "root_lines": 120 + }, + "new_gates": 12, + "old_gates": 13, + "overlap": { + "additional_frame_saving_vs_pr952": 1, + "new_frame_gates": 12, + "pr952_frame_gates": 13, + "pr952_word_ADDs": 23673, + "same_positive_transfer_as_selected": false, + "selected_frame_gates": 21, + "selected_ops": [ + [ + 5, + 2 + ], + [ + 5, + 1 + ], + [ + 5, + 0 + ], + [ + 5, + 4 + ], + [ + 3, + 2 + ], + [ + 3, + 4 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 2, + 4 + ], + [ + 4, + 5 + ], + [ + 4, + 3 + ], + [ + 4, + 2 + ], + [ + 4, + 1 + ], + [ + 4, + 0 + ], + [ + 0, + 5 + ], + [ + 0, + 3 + ], + [ + 0, + 2 + ], + [ + 1, + 5 + ], + [ + 1, + 3 + ], + [ + 1, + 2 + ], + [ + 3, + 5 + ] + ], + "selected_slice": [ + 906, + 927 + ] + }, + "positive_matrices": { + "forward": { + "original": [ + [ + 3, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 0, + 1 + ], + [ + 3, + 3, + 1, + 1, + 2, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1 + ] + ], + "replacement": [ + [ + 3, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 0, + 1 + ], + [ + 3, + 3, + 1, + 1, + 2, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1 + ] + ] + }, + "reverse": { + "original": [ + [ + 1, + 0, + 1, + 1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 0, + 2, + 1, + 1, + 0 + ], + [ + 1, + 1, + 3, + 3, + 0, + 1 + ], + [ + 1, + 1, + 3, + 3, + 1, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 1 + ] + ], + "replacement": [ + [ + 1, + 0, + 1, + 1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 2, + 2, + 1, + 1, + 0 + ], + [ + 1, + 1, + 3, + 3, + 0, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 0, + 2, + 3, + 2, + 0, + 1 + ] + ] + } + }, + "prefix_source": { + "K": 4, + "bridges": 18, + "formula": "2^18 * F^5 * B^4", + "source": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py", + "stages": 9 + }, + "quad": 15, + "saved_with_cleanup": 2, + "scalar": { + "original": { + "ADDs": 23673, + "B": 833084, + "F": 41287, + "columns_each_order": 661, + "instructions_both_orders": 47382, + "local_payload_bits": 92, + "nine_stage_bound": "15148224495959132732497298498295876067945200524197888", + "nine_stage_prefix_bits": 174 + }, + "replacement": { + "ADDs": 23671, + "B": 832712, + "F": 41287, + "columns_each_order": 661, + "instructions_both_orders": 47378, + "local_payload_bits": 92, + "nine_stage_bound": "15121185848152904741114841695242575582734804360101888", + "nine_stage_prefix_bits": 174 + }, + "selected589": { + "ADDs": 24305, + "B": 1113070, + "F": 49347, + "columns_each_order": 661, + "instructions_both_orders": 48646, + "local_payload_bits": 93, + "nine_stage_bound": "117742596540718658156527847560864213734191286190080000", + "nine_stage_prefix_bits": 177 + } + }, + "source_slice": [ + 825, + 838 + ], + "status": "PASS_R439_FRAME281", + "wires": [ + 263, + 275, + 310, + 374, + 410, + 491 + ], + "word_sha256": "ab1c8266f17a1d61067bdd38d0ba74ba96a277cee1cc198a19510f3f453ce60a" +} diff --git a/research/r439-frame281-seed15/CLAIM.md b/research/r439-frame281-seed15/CLAIM.md new file mode 100644 index 0000000000..07a273181f --- /dev/null +++ b/research/r439-frame281-seed15/CLAIM.md @@ -0,0 +1,56 @@ +# Bit supplier sprint claim, seed 15 + +- Assignment: first operating-system cryptographic random draw, rejection sampled + uniformly from 0 through 99, was **15** (bit supplier). +- Exact base: `bbc600db2fc15007b7c914f4f2b2ed55fa909c87`. +- Claim recorded: 2026-10-13 15:34 UTC; target handoff: 16:18 UTC. +- Object: complete six-register phase-A frame **281** (quad 15) in the R439 + bit word; compare the selected PR589 word and the retained PR952 candidate. +- Method: bounded exact nonnegative row-subtraction synthesis for the fixed + positive transfer, with repeated destination writes, followed by independent + matrix replay, dirty-column and paid-frame checks. This differs from PR952's + bounded pivot-order Boolean elimination scan and PR925's frame-267 matrix. +- Expected deliverable: one source-pinned finite circuit improvement or scoped + exact class boundary, a reproducible checker, negative controls and attribution. +- Budget: one matrix, at most 1,000,000 discovery states initially; one + evidence-driven pivot allowed within this same frame. Final quarter reserved + for independent verification, overlap refresh and handoff. + +Three candidates considered: (1) frame281 fixed-transfer synthesis (chosen by +seed15 among the 60 complete six-register phase-A frames); (2) another phase-B +fixed-factor schedule (declined because the ten blocks have recent direct +contributions); (3) multi-helper D compensation (declined because PR965/967 +already investigate coupled helpers and restored stars). Existing PR933 closes +the selected word's relocation/Steinberg class; this claim changes the full +six-wire circuit instead. PR904/936/952 prefix results and PR925 are predecessor +work, not imported savings unless explicitly replayed and compared. + +The issues page at claim selection showed only issues #913 and #650 and no +pinned sprint coordination issue. No reservation issue was opened. Public +Curiosity Bot searches checked recent bit/frame PRs and frame281 references; +the local claim is used as requested. No selected frontier or upstream edit. + +Selected result at the base: PR942, conditional kappa 0.001661960547713947, +complex-bound, retaining PR589 on PR555. This task does not promise a new kappa. + +Prepared for contributor @woklerx with substantial OpenAI Codex assistance. + +## Result update (2026-10-13) + +Completed the single evidence-driven pivot to PR952's distinct frame281 +integer transfer after detecting that the initial selected-word matrix is +conjugate to PR925's prior result. The final 12-ADD circuit saves two complete +local ADDs, including cleanup: 23,673 -> 23,671. Two different exhaustive +implementations establish the fixed-transfer minimum12 and reverse-envelope +minimum13. Exact source/dirty-column/exported-record checks pass; native C++ +and full make verification remain unavailable in this environment. + +Final overlap refresh inspected concurrent PR980 at +`ba1cf68bef0c97dfb120add04304e2de0db6f29c`: its frame281 still has the same +13-ADD transfer. Its general admission method is credited separately and its +other block savings are not composed here. All workers stayed within this +frame's discovery, independent proof, replay or review scope. + +Reviewable result: +[frame281 package on the submission branch](https://github.com/woklerx/integer-mult-bounds/tree/research/seed15-bit-supplier/research/r439-frame281-seed15). +One focused upstream PR is the handoff; no merge or selected-frontier edit. diff --git a/research/r439-frame281-seed15/NOTICE.md b/research/r439-frame281-seed15/NOTICE.md new file mode 100644 index 0000000000..4f02baeeda --- /dev/null +++ b/research/r439-frame281-seed15/NOTICE.md @@ -0,0 +1,51 @@ +# Attribution and license + +Prepared for GitHub contributor **woklerx (@woklerx)** with substantial +**OpenAI Codex assistance** in task selection, research, implementation, +proof analysis, independent implementations, verification and documentation. +Several scoped AI workers collaborated; no independent human review is claimed. +New work is offered under the repository's **Apache-2.0 license**. + +This contribution depends on and credits: + +- **Gareth Davidson (@bitplane), PR952**: the complete six-wire Boolean-synthesis + candidate is the actual input, including its earlier PR904 contributions. + Its exact `candidate.json.gz` is consumed without modification; its `verify.py` + supplies credited whole-word scalar/prefix checks, and its `common.py` is + imported by that verifier. Earlier savings remain his and the named + predecessors' work. Source PR head: `11d24706f06e95271804c9438869546724c67aab`. +- **Ross Richardson (@RossRichardson), PR936 and PR925**: the five-wire parent + of PR952, the earlier exact positive-transfer frame267 result, and framing, + cleanup and exported-record verification routines. `search.py` adapts PR925's + row-subtraction recurrence with attribution. The selected PR589 frame281 + matrix is conjugate to PR925's target, so that initial lower bound is prior + work. The distinct PR952 transfer and the paired reverse-envelope boundary + are the new scoped objects. `verify.py` imports PR925 helper checks unchanged. +- **Jeffrey Cox, PR754**, and **mtpsl, PR691**: small-GL prefix synthesis and + the earlier fixed-integer-transfer/reverse-domination lineage, respectively, + as credited by the consumed PR904/925 packages. +- **Gareth Davidson, concurrent PR980**, and the **PR857/906** lineage credited + there: complete-prefix admission despite local entrywise growth. PR980's + broader construction is separately credited; this contribution establishes + an exact fixed-transfer/guard boundary at frame281, which PR980 leaves at + 13 ADDs. Its changes and claimed whole-word savings are not imported here. +- **eumemic, PR543/555**, **DreamingOfClouds, PR545/589/510**, **Dylan Crow**, + **Zhihao Chen**, **DaysSky**, and retained supplier contributors: R439 word, + frame geometry, original H1-H5 audit, exporter, stage/cohort checks, hosting + and pricing foundations. The selected PR589 head remains + `a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46`. +- **Ali Romman, PR688**, and Ross Richardson: the optional native harness is + adapted from their credited replay wrapper. The underlying C++ checkers and + all supplier files remain untouched. No new native execution is claimed. +- **Jonathan Capalbo, PR942**, with the U8/T21/T16 owner lineage credited in the + selected maintainer review: current conditional-frontier context only. + +`independent.py` was written separately from the discovery algorithm and +imports no discovery code. It uses first-gate column subtraction and a paired +column search, while discovery uses last-gate row subtraction and shortest-path +pruning. This is algorithmic independence inside an AI-assisted contribution, +not a claim of independent authorship from every predecessor or human review. + +Source file SHA-256 pins and the exact base are in `SOURCES.json`. Original +source notices and licenses remain in their existing package locations. The +selected certificate, upstream sources and predecessor packages are unchanged. diff --git a/research/r439-frame281-seed15/OVERLAP.json b/research/r439-frame281-seed15/OVERLAP.json new file mode 100644 index 0000000000..f55a5f9193 --- /dev/null +++ b/research/r439-frame281-seed15/OVERLAP.json @@ -0,0 +1,127 @@ +{ + "frame": 281, + "gates": 13, + "head": "ba1cf68bef0c97dfb120add04304e2de0db6f29c", + "ops": [ + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 1 + ], + [ + 4, + 1 + ], + [ + 2, + 4 + ], + [ + 3, + 5 + ], + [ + 1, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 0, + 2 + ], + [ + 1, + 3 + ], + [ + 4, + 3 + ], + [ + 0, + 3 + ] + ], + "own_gates": 12, + "path": "research/r439-global-prefix-admission/candidate.json.gz", + "positive_matrix": [ + [ + 3, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 0, + 1 + ], + [ + 3, + 3, + 1, + 1, + 2, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1 + ] + ], + "pr": 980, + "registers": [ + 263, + 275, + 310, + 374, + 410, + 491 + ], + "same_positive_matrix_as_pr952": true, + "scope": "Comparison only; PR980 candidate is not composed or executed here.", + "sha256": "fffc0484a3572c76bf3bb5284d4a40eeb723c4b3acf3da5e2d9e113ac1747ec6", + "slice": [ + 789, + 802 + ] +} diff --git a/research/r439-frame281-seed15/PROOF.md b/research/r439-frame281-seed15/PROOF.md new file mode 100644 index 0000000000..f2c8621860 --- /dev/null +++ b/research/r439-frame281-seed15/PROOF.md @@ -0,0 +1,114 @@ +# Fixed-transfer factorization and the reverse guard + +Use the ordered existing registers `[263,275,310,374,410,491]`. A gate `(d,s)` +means `register[d] += register[s]`; its Boolean action uses XOR, while its +positive integer action is used for the cancellation-free precision envelope. +The PR952 frame281 transfer is + +```text +3 2 1 1 1 1 +2 3 1 1 1 1 +1 1 1 0 1 0 +1 1 0 1 0 1 +3 3 1 1 2 1 +1 1 1 0 1 1 +``` + +The emitted 12-ADD circuit is + +```text +(5,1) (4,0) (3,5) (2,4) (5,2) (3,0) +(2,1) (1,3) (1,2) (4,1) (0,3) (0,2) +``` + +Its exact forward integer matrix equals the original 13-ADD circuit's matrix. +Independent column evaluation and all 64 Boolean inputs verify the identity. + +## Complete finite minimum recurrence + +Let `E_ds = I + e_ds` for `d != s`. Starting from identity, any positive +ADD-only program stays entrywise at least identity. Removing its last gate +subtracts row s from row d. Retain precisely those predecessor matrices P +still entrywise at least I. Every valid program has one such predecessor; +conversely each retained edge reverses to a legal positive ADD. The source +row has diagonal at least one, so every subtraction strictly lowers entry sum. +The graph is finite, and for this matrix the maximum path length is at most +`42 - 6 = 36`. + +Set `D(I)=0`; otherwise `D(M)=1+min D(P)` over retained predecessors, with +infinity when none reaches identity. The exhaustive row-subtraction recurrence +in `search.py` gives **D(M)=12**, with 41,235 vertices, 209,118 edges and 88 +dead ends. Its sentinel 999 exceeds every possible finite distance; a resource +cap is reported as incomplete, never as an impossibility result. + +`independent.py` instead removes the **first** ADD: right multiplication by +`E_ds^-1` subtracts column d from column s. A breadth-first traversal checks +every layer below 12 before accepting the first identity. It visits 41,203 +states and examines 208,824 edges from completed layers. It imports no discovery +code. Different closure counts are expected: one method finishes the entire +last-gate graph; the other stops at the first identity layer in the first-gate +graph. + +## An exact stricter-class minimum + +Let B be the positive matrix obtained by executing PR952's original 13 gates +in reverse order, without negating them. The new circuit exceeds B in four +entries: `(2,1):0->2`, `(5,1):0->2`, `(5,2):1->3`, `(5,3):0->2`. +Thus it fails an entrywise reverse-domination guard. + +Discovery traverses only shortest-distance edges `D(P)=D(M)-1`, accumulating +the positive reverse-prefix matrix of each peeled last gate. It prunes a branch +as soon as that matrix exceeds B; all entries can only increase. Exhausting +116 paired states and 283 surviving edges gives no guarded 12-gate witness. +All shorter words were already excluded by D(M)=12. The original 13-gate word +satisfies the guard with equality, proving guarded minimum **13**. + +The independent proof uses first-gate paired-column BFS and accumulates the +reverse product by column addition. It explores every retained paired state +through depth 12 and first reaches identity at 13, visiting 735 states. Positive +prefix monotonicity justifies its separate guard pruning. This independently +establishes the same minimum without using the discovery distances. Both +proofs concern a final **positive matrix** bound; no claim is made about every +possible arithmetic circuit or other norm-based guard. + +## Whole-word substitution and complete cost + +Only `A[825:838]` of the pinned PR952 candidate changes, at the same frame281. +All six registers occur in the replacement. Phase C is regenerated as the +literal reverse of the z-destination gates of A then B at the full frame, +exactly as required by the retained H4. D, scatter, B, frame geometry, retained +totals, start/final frames and other A gates are unchanged. Frame paths are +compared for all 661 registers, and all COPY/ERASE and MOVE costs are rechecked +in the actual emitted instructions. + +One forward ADD plus one mandatory cleanup ADD is saved. The complete count +is 23,673 -> 23,671; no new helper, copy, source access, frame conversion, +restoration call or recursive child is hidden. All 661 arbitrary-input columns +and original H1-H5 conditions hold. The paid rank histogram remains +`{1:1323,2:1342,3:79,4:44,5:102,6:11,7:19}`, with rank mass 5,129 and nine +rank-seven COPYs (decoder constant 63). + +The local reverse guard is sufficient but unnecessarily strong here. Direct +positive replay of the whole word gives F=41,287 before and after, and +B=833,084 -> 832,712. The exact local expression `64*F^3*B^2` remains below +`2^104` (92 bits). The inherited nine-stage expression `2^18*F^5*B^4` is +AST-bound to the pinned `global_k.py`; it changes from + +```text +15148224495959132732497298498295876067945200524197888 +``` + +to + +```text +15121185848152904741114841695242575582734804360101888 +``` + +and remains 174 bits under the 192-bit allowance. This exact expression check +does not constitute a native 5/9/11-stage replay or a hosted global invoice. +Those execution/adoption obligations remain open. The rank moment is unchanged +and the selected result is complex-bound, so no kappa improvement follows. + +These are finite algebraic arguments supported by exhaustive exact programs, +not a Lean proof of the multiplication theorem. Assumptions and attribution +remain as stated in README and NOTICE. diff --git a/research/r439-frame281-seed15/README.md b/research/r439-frame281-seed15/README.md new file mode 100644 index 0000000000..1f12306f44 --- /dev/null +++ b/research/r439-frame281-seed15/README.md @@ -0,0 +1,124 @@ +# Frame281: a 12-ADD circuit beyond PR952, and an exact 12/13 boundary + +**Finite bit-supplier construction and scoped class minimum; no new kappa.** +Replace one complete six-register phase-A block in Gareth Davidson's retained +PR952 word: frame281 (quad15), `A[825:838]`, drops from **13 to 12 ADDs**. +Rebuilding its required literal reverse cleanup saves one more ADD, so the +complete local word drops **23,673 -> 23,671 ADDs**. All other PR952 changes +are inherited and credited, not claimed as new savings. + +The exact minimum for this fixed positive integer transfer is **12**. If its +reverse positive matrix must also be entrywise no larger than PR952's matrix, +the exact minimum is **13**. Thus the stronger local guard excludes every +shortest circuit even though our 12-ADD witness *reduces* the complete word's +reverse bound. This is a concrete reason to price the full word after a local +guard rejects a candidate. + +| Complete local resource | PR952 parent | This candidate | +|---|---:|---:| +| ADDs, including cleanup and dirty compensation | 23,673 | **23,671** | +| Exported records | 26,602 | **26,600** | +| Forward positive bound F | 41,287 | 41,287 | +| Reverse positive bound B | 833,084 | **832,712** | +| Local payload bits, allowance 104 | 92 | 92 | +| Nine-stage expression bits, allowance 192 | 174 | 174 | +| Paid rank mass | 5,129 | 5,129 | +| MOVE / COPY / ERASE records | 2,911 / 9 / 9 | unchanged | + +All 661 symbolic dirty-input columns, original H1-H5 interface conditions, +per-register frame paths, and the actual exported record stream are checked. +No helper, frame, source-access operation, COPY, restoration call or recursive +child is added. The paid rank profile and decoder constant 63 are unchanged. +Neither the bit exponent nor the selected conditional kappa is improved. + +## Reproduce + +From the repository root, Python 3.11+ with the standard library only: + +```sh +python -I -B research/r439-frame281-seed15/verify.py +``` + +Expected final line: + +```text +PASS_R439_FRAME281 gates=13->12 local_ADDs=23673->23671 columns=661 rank_mass=5129 controls=7 +``` + +The command checks all source pins, reruns the bounded discovery and its +complete metadata, independently proves both class minima by column-based +breadth-first searches, checks 64 Boolean inputs and exact integer matrices, +prices the whole word in both directions, checks E8 geometry/H1-H5, regenerates +records and interprets their actual bytes. Nine independent mathematical +controls plus seven local/whole-word controls must reject. The certificate is +compared by canonical JSON, not regenerated gzip container bytes. Typical local +run is about 15 seconds; timing is not part of acceptance. + +Use `--output /absolute/fresh/directory` to retain both reconstructed words +(`original.json.gz` is PR952) and exported records. Outputs must be new. +`--write-certificate` explicitly regenerates only this package's certificate. +Discovery alone is `python -I -B research/r439-frame281-seed15/search.py`. + +An optional native harness is provided: + +```sh +BOOST_INCLUDE=/path/to/boost CXX=g++ python -I -B research/r439-frame281-seed15/native.py --write-certificate +``` + +**Native C++ legality and 5/9/11-stage execution were not run here.** No +`NATIVE-CERTIFICATE.json` is supplied. The environment lacks compatible +GCC/Clang and accessible Boost headers; `make verify` also stops because `make` +is unavailable. See [VALIDATION.md](VALIDATION.md). Exported-record interpretation +and scalar prefix expressions are not a substitute for that native replay. + +## Pins, novelty and overlap + +Exact base: **`bbc600db2fc15007b7c914f4f2b2ed55fa909c87`**. +At that base the selected record is PR942, conditional +**kappa 0.001661960547713947**, complex-bound, retaining PR589 on PR555. +The selected assembly gives bit c `0.001733427039589844234749`. +The actual candidate parent is **PR952**, head +`11d24706f06e95271804c9438869546724c67aab`, retained under +`research/r439-six-wire-boolean/`. [SOURCES.json](SOURCES.json) binds all +consumed sources; text hashes normalize CRLF to LF, immutable gzip inputs do not. + +Seed **15**, the first OS-random draw, selected quad15 within the bit-supplier +track. The initial selected-PR589 matrix proved permutation-conjugate to Ross +Richardson's PR925 frame267 matrix, so its minimum is credited to that prior +result rather than presented as a new discovery. The one evidence-driven pivot +kept frame281 but used PR952's distinct integer transfer: entry sum 42 rather +than 58 precludes permutation conjugacy. PR952's bounded pivot-order Boolean +scan did not certify an optimum for this transfer; this work exhausts the +positive-addition factorization class and a separate reverse-envelope class. + +Discovery exhausts **41,235 states / 209,118 edges**, including 88 dead ends, +for the PR952 fixed transfer. The independent first-ADD column search expands +all layers below 12, visiting **41,203 states**. Its separate paired-column +search establishes the guarded minimum 13 using **735 states**. These methods +are independent implementations, not independent human review. Domain, +one-million-state stopping caps, seed and the earlier conjugate exploration +are recorded in [CLAIM.md](CLAIM.md) and [WITNESS.json](WITNESS.json). + +The final overlap refresh found **Gareth Davidson's concurrent PR980**, head +`ba1cf68bef0c97dfb120add04304e2de0db6f29c`, which reports 240 further ADD savings +by full-prefix admission across 42 blocks. Its actual candidate still uses +the same **13-ADD frame281** program as PR952. [OVERLAP.json](OVERLAP.json) +records the extracted block and immutable artifact hash. Our 12-ADD factor +and exact 12/13 class boundary remain distinct evidence; no priority is claimed +for the general full-prefix admission idea, and no combined PR980 word or +additional whole-word saving on that candidate is claimed or tested. + +## Scope + +The minima apply only to positive elementary additions on these **six labelled +registers with the exact integer transfer fixed**; repeated destination writes +are allowed. Other Boolean lifts, subtraction, extra registers and free +permutations are outside the class. See [PROOF.md](PROOF.md) for the recurrence, +reverse guard and complete cost. The native multistage replay, hosted supplier +adoption, global invoice and outer assembly remain undone. Inherited all-size +compiler, mutable-source/common-label realization, whole-call hosting, +precision/tape and analytic transfer obligations remain. This is not a formal +proof of the full multiplication theorem or a new selected supplier. + +Prepared for **@woklerx with substantial OpenAI Codex assistance**. Predecessor +credit and Apache-2.0 licensing are detailed in [NOTICE.md](NOTICE.md). diff --git a/research/r439-frame281-seed15/SOURCES.json b/research/r439-frame281-seed15/SOURCES.json new file mode 100644 index 0000000000..66024342ba --- /dev/null +++ b/research/r439-frame281-seed15/SOURCES.json @@ -0,0 +1,38 @@ +{ + "base_commit": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87", + "candidate_parent_head": "11d24706f06e95271804c9438869546724c67aab", + "candidate_parent_pr": 952, + "files": { + "docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a", + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8", + "research/r439-frame267-seed01/WITNESS.json": "383b4dc38b5f38805319b7553f249efe2ae9898eb768fa2e0915a097fd692ba7", + "research/r439-frame267-seed01/search.py": "10eaa07ea45c791733e33bb04ee7c2587ae68c538db92ba22103879a5a7448c7", + "research/r439-frame267-seed01/verify.py": "cd0bdd6981e7698c2a248ff8774cba7a4c4cad7c0e7482a493b088c309a3f44a", + "research/r439-six-wire-boolean/CERTIFICATE.json": "aaa5f126fe0e4938df985c00bb47d1ce17da0eb8b20ae983813b66c02de07841", + "research/r439-six-wire-boolean/NOTICE.md": "997a26ce5831adfea30c964d7805a7794a50f4729649ce946067c4b6719db5d8", + "research/r439-six-wire-boolean/SOURCES.json": "aceb9bf4a8db79dde65d6bb915715f0657562956c4f66fff2a58eb207d93240d", + "research/r439-six-wire-boolean/candidate.json.gz": "5c67c7949c07a89ea8394a936a155585d22e6b258997df73e36e7be47fc84cb0", + "research/r439-six-wire-boolean/common.py": "4907fb14d0422216d549fc3a3fe5c354784ea3593370d54f3f939e8dd90d5de7", + "research/r439-six-wire-boolean/verify.py": "85afc79d0a0d6e64f632ecb2f69d1107ddd7a717ecf17665647d5e4caf907148" + }, + "format": "sha256-immutable-gzip-and-lf-normalized-text-v1", + "normalization": "Only CRLF is normalized to LF for text sources; gzip bytes are exact. No generated container hashes define mathematical equality.", + "selected_bit_source_head": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "selected_bit_source_pr": 589, + "selected_context_only": { + "note": "Observed at exact base; the mutable selected pointer is not a runtime dependency.", + "path": "certificates/selected-result.json", + "runtime_input": false, + "sha256": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3" + }, + "selected_kappa": "0.001661960547713947", + "selected_pr": 942 +} diff --git a/research/r439-frame281-seed15/VALIDATION.md b/research/r439-frame281-seed15/VALIDATION.md new file mode 100644 index 0000000000..043afa2c7c --- /dev/null +++ b/research/r439-frame281-seed15/VALIDATION.md @@ -0,0 +1,76 @@ +# Executed validation and limitations + +Environment: Windows, CPython 3.14. Exact research base +`bbc600db2fc15007b7c914f4f2b2ed55fa909c87`. No third-party Python dependency is +required by the new package or its exercised Python checker paths. + +## Completed + +- Complete bounded discovery replay: PR952 fixed-transfer minimum 12, + 41,235 states / 209,118 edges; reverse-guard shortest-path exhaustion, + 116 paired states / 283 edges. The earlier conjugate selected-word + exploration is retained and attributed, not claimed as a new minimum. +- Independent first-gate column BFS: minimum 12, 41,203 visited states, + 208,824 examined edges from completed layers 0..11. +- Independent paired-column BFS: reverse-guard minimum 13, 735 states, + completed layers 0..12. Nine independent controls reject mathematical + corruption, incorrect lower/upper claims and resource exhaustion. +- All 64 local Boolean inputs, exact forward integer matrix and reported + reverse matrix; four reverse entries grow, so local domination is explicitly + false. Complete F/B bounds are recomputed instead of assuming domination. +- Exact whole-word forward and reverse symbolic replay on all 661 arbitrary + source/target/helper input columns; original E8/frame checker and H1-H5. +- Fresh supplier export followed by a separate set-valued interpretation of + every actual binary MOVE, ADD, COPY and ERASE record. ADDs 23673->23671, + records 26602->26600; MOVE/COPY/ERASE costs, frame paths and paid histogram + unchanged. These are **exported-record checks**, not native C++ execution. +- Exact inherited local and nine-stage scalar prefix expressions: 92 and 174 + bits under 104 and 192. Their respective bounds do not increase. The nine-stage + expression and bridge count are checked against the pinned source AST. +- Seven additional local/whole-word negative controls: deleted ADD, swapped + operands, Boolean-neutral positive inflation, omitted cleanup, stale + nonliteral cleanup, invalid lower frame and missing dirty compensation. +- Source inventory coverage, normalized-text/immutable-gzip hashes, full + deterministic witness regeneration, and canonical certificate comparison. + +The reproducible command is +`python -I -B research/r439-frame281-seed15/verify.py`. Its final output is +recorded in README; `CERTIFICATE.json` contains the exact proof-relevant results. +The verifier uses temporary outputs by default and does not regenerate unrelated +repository artifacts. + +## Unavailable or not executed + +- `make verify` was attempted once and stopped immediately: **make is not + installed/on PATH**. The repository-wide suite did not execute. +- `python -I -B research/r439-frame281-seed15/native.py` was attempted and stopped + at preflight: **no GCC/Clang-compatible C++17 compiler was available**. Existing + MSVC was detected but the inherited harness uses GCC-style flags. Accessible + Boost headers were not found in checked common locations and WSL had no + registered distribution. No tools or system configuration were installed. +- The optional native harness was syntax checked and its prefix arithmetic + compared with a retained predecessor receipt. That is not a new native run; + no native certificate is included. Native legality, 883/1327/1549 formal-column + runs and 96 omitted-bridge controls remain for a suitably provisioned machine. +- Selected cold complex replay, full hosted emitter adoption, global invoices, + outer reassembly and formal proof of the multiplication theorem were not run. + The selected pointer and all predecessor sources remain unchanged. + +## Development failures retained as limitations of the process + +An initial canonical witness comparison failed because in-memory histogram +keys were integers while JSON-loaded keys were strings, leading to different +sort order. The keys are now strings at construction; strict canonical replay +passes without changing circuit results. No failed certificate was edited into +a passing receipt. Duplicate JSON keys and nonfinite values are rejected. + +The first selected-word search duplicated a predecessor matrix up to register +permutation. This was detected, credited, and caused the documented single +pivot to PR952's different matrix. The successful finite result does not imply +a new kappa or solve the remaining all-size/compiler and physical obligations. + +The sandbox's default Windows temporary directory later refused file writes. +Replays were rerun with the process-local `TMPDIR` pointing to a writable +workspace scratch directory; the default temporary-output path then passed. +This changed no mathematical code or system configuration. Scratch outputs +and failed runs are excluded from the patch. diff --git a/research/r439-frame281-seed15/WITNESS.json b/research/r439-frame281-seed15/WITNESS.json new file mode 100644 index 0000000000..1562120545 --- /dev/null +++ b/research/r439-frame281-seed15/WITNESS.json @@ -0,0 +1,525 @@ +{ + "assignment_seed": 15, + "completed_states": 41235, + "dead_end_distance": 999, + "distance_histogram": { + "0": 1, + "1": 10, + "2": 54, + "3": 207, + "4": 808, + "5": 2258, + "6": 4892, + "7": 8239, + "8": 10228, + "9": 8623, + "10": 4489, + "11": 1214, + "12": 124, + "999": 88 + }, + "edges": 209118, + "exhausted": true, + "frame": 281, + "minimum": 12, + "original": [ + [ + 3, + 0 + ], + [ + 4, + 0 + ], + [ + 3, + 1 + ], + [ + 4, + 1 + ], + [ + 2, + 4 + ], + [ + 3, + 5 + ], + [ + 1, + 2 + ], + [ + 4, + 2 + ], + [ + 5, + 2 + ], + [ + 0, + 2 + ], + [ + 1, + 3 + ], + [ + 4, + 3 + ], + [ + 0, + 3 + ] + ], + "phase": "A", + "quad": 15, + "registers": [ + 263, + 275, + 310, + 374, + 410, + 491 + ], + "replacement": [ + [ + 5, + 1 + ], + [ + 4, + 0 + ], + [ + 3, + 5 + ], + [ + 2, + 4 + ], + [ + 5, + 2 + ], + [ + 3, + 0 + ], + [ + 2, + 1 + ], + [ + 1, + 3 + ], + [ + 1, + 2 + ], + [ + 4, + 1 + ], + [ + 0, + 3 + ], + [ + 0, + 2 + ] + ], + "reverse_dominated_by_parent": false, + "reverse_guard": { + "edges": 283, + "exhausted_without_witness": true, + "shortest_feasible": false, + "states": 116 + }, + "reverse_original_matrix": [ + [ + 1, + 0, + 1, + 1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 0, + 2, + 1, + 1, + 0 + ], + [ + 1, + 1, + 3, + 3, + 0, + 1 + ], + [ + 1, + 1, + 3, + 3, + 1, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 1 + ] + ], + "reverse_replacement_matrix": [ + [ + 1, + 0, + 1, + 1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 2, + 2, + 1, + 1, + 0 + ], + [ + 1, + 1, + 3, + 3, + 0, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 0, + 2, + 3, + 2, + 0, + 1 + ] + ], + "selected_reference": { + "completed_states": 416508, + "dead_end_distance": 999, + "distance_histogram": { + "0": 1, + "1": 12, + "2": 92, + "3": 497, + "4": 1988, + "5": 6287, + "6": 16658, + "7": 38015, + "8": 69337, + "9": 94686, + "10": 90832, + "11": 56483, + "12": 19777, + "13": 3015, + "14": 159, + "15": 1, + "999": 18668 + }, + "edges": 2366680, + "exhausted": true, + "minimum": 12, + "original": [ + [ + 5, + 2 + ], + [ + 5, + 1 + ], + [ + 5, + 0 + ], + [ + 5, + 4 + ], + [ + 3, + 2 + ], + [ + 3, + 4 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 2, + 4 + ], + [ + 4, + 5 + ], + [ + 4, + 3 + ], + [ + 4, + 2 + ], + [ + 4, + 1 + ], + [ + 4, + 0 + ], + [ + 0, + 5 + ], + [ + 0, + 3 + ], + [ + 0, + 2 + ], + [ + 1, + 5 + ], + [ + 1, + 3 + ], + [ + 1, + 2 + ], + [ + 3, + 5 + ] + ], + "pr925_conjugacy": [ + 3, + 2, + 0, + 1, + 4, + 5 + ], + "replacement": [ + [ + 2, + 4 + ], + [ + 3, + 2 + ], + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 5, + 2 + ], + [ + 3, + 5 + ], + [ + 1, + 3 + ], + [ + 1, + 2 + ], + [ + 4, + 1 + ], + [ + 4, + 0 + ], + [ + 0, + 3 + ], + [ + 0, + 2 + ] + ], + "start": 906, + "state_cap": 1000000, + "states": 416508, + "stop": 927, + "target_matrix": [ + [ + 3, + 2, + 3, + 1, + 3, + 1 + ], + [ + 2, + 3, + 3, + 1, + 3, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 2, + 1, + 2, + 1 + ], + [ + 3, + 3, + 3, + 1, + 4, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1 + ] + ] + }, + "source_pr": 952, + "start": 825, + "state_cap": 1000000, + "states": 41235, + "stop": 838, + "target_matrix": [ + [ + 3, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 0, + 1 + ], + [ + 3, + 3, + 1, + 1, + 2, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1 + ] + ] +} diff --git a/research/r439-frame281-seed15/independent.py b/research/r439-frame281-seed15/independent.py new file mode 100644 index 0000000000..6f495b878c --- /dev/null +++ b/research/r439-frame281-seed15/independent.py @@ -0,0 +1,287 @@ +"""Independent exact checks for the fixed frame-281 six-wire transfer. + +Matrix replay evolves one input column at a time. Shortest-path checking peels +FIRST positive ADDs by column subtraction, independently of discovery's peeling +of LAST ADDs by row subtraction. No search.py imports; standard library only. + +The class is all finite straight-line circuits on these six labelled registers, +starting at identity, using only elementary ``x[d] += x[s]`` with d != s, and +having exactly the supplied nonnegative INTEGER transfer. Repeated writes and +arbitrary gate order are allowed. There are no additional registers, subtractions, +free permutations, or multi-source gates. This is not a minimum over all F2 +equivalent circuits, and it is not a lower bound on the multiplication exponent. + +Breadth-first proof idea follows PR925's frame-267 optimality.py by Ross +Richardson, with substantial OpenAI Codex assistance; this verifier uses the +opposite end of a circuit (column rather than row subtraction). +Prepared for @woklerx with substantial OpenAI Codex assistance; Apache-2.0. +""" + +from collections import deque + + +N = 6 + + +class Reject(ValueError): + """A finite check failed or its explicitly bounded resources were exhausted.""" + + +def _gates(ops): + if not isinstance(ops, (list, tuple)): + raise Reject("gate sequence must be a list or tuple") + for gate in ops: + if not isinstance(gate, (list, tuple)) or len(gate) != 2: + raise Reject("each elementary ADD requires [destination, source]") + d, s = gate + if type(d) is not int or type(s) is not int or not (0 <= d < N and 0 <= s < N) or d == s: + raise Reject("invalid elementary ADD operands") + return ops + + +def matrix(ops, positive=False): + """Return exact integer or F2 matrix using independent basis-column replay.""" + _gates(ops) + columns = [] + for col in range(N): + state = [int(row == col) for row in range(N)] + for d, s in ops: + state[d] = state[d] + state[s] if positive else state[d] ^ state[s] + columns.append(state) + return [[columns[col][row] for col in range(N)] for row in range(N)] + + +def check_truth_table(left, right): + """Exhaustively compare all 64 six-bit inputs, separately from matrix replay.""" + _gates(left) + _gates(right) + for input_word in range(1 << N): + outputs = [] + for circuit in (left, right): + values = [(input_word >> i) & 1 for i in range(N)] + for d, s in circuit: + values[d] = (values[d] + values[s]) % 2 + outputs.append(values) + if outputs[0] != outputs[1]: + raise Reject("Boolean transfer differs at input " + str(input_word)) + return {"boolean_inputs": 1 << N} + + +def circuit_check(original, replacement, exact_forward=True): + """Check Boolean transfer and monotone forward/reverse integer envelopes.""" + truth = check_truth_table(original, replacement) + if matrix(original) != matrix(replacement): + raise Reject("F2 matrix changed") + result = dict(truth) + for name, old, new in (("forward", original, replacement), + ("reverse", original[::-1], replacement[::-1])): + before, after = matrix(old, True), matrix(new, True) + if any(y > x for row_before, row_after in zip(before, after) + for x, y in zip(row_before, row_after)): + raise Reject(name + " positive transfer increased") + if name == "forward" and exact_forward and before != after: + raise Reject("fixed integer transfer changed") + result[name] = {"original": before, "replacement": after} + return result + + +def check_minimum(transfer, claimed, max_states=1_000_000): + """Prove exact minimum by complete BFS through depth ``claimed``. + + If M = E_last ... E_first, removing first ADD d += s right-multiplies + by I-e[d,s], thus subtracting column d from column s. Every remaining + positive circuit is >= I entrywise. Trying all 30 ordered pairs is + therefore exhaustive. Conversely, a path to I reverses to a circuit. + Each edge decreases the integer sum strictly, so the graph is finite. + + Resource exhaustion raises Reject and is NEVER reported as a lower bound. + """ + if type(claimed) is not int or not 0 <= claimed <= 21: + raise Reject("claimed distance must be an integer from 0 through 21") + if type(max_states) is not int or max_states < 1: + raise Reject("invalid state budget") + if not isinstance(transfer, (list, tuple)) or len(transfer) != N or any( + not isinstance(row, (list, tuple)) or len(row) != N for row in transfer): + raise Reject("transfer must be a 6 by 6 matrix") + if any(type(x) is not int or x < int(r == c) + for r, row in enumerate(transfer) for c, x in enumerate(row)): + raise Reject("positive transfer must be integral and entrywise >= identity") + + # Columns are contiguous here, unlike the row-major nomination matrix. + target = tuple(transfer[r][c] for c in range(N) for r in range(N)) + identity = tuple(int(r == c) for c in range(N) for r in range(N)) + queue = deque([target]) + seen = {target} + layers = [] + edges = 0 + for depth in range(claimed + 1): + width = len(queue) + layers.append(width) + # Check the entire layer before expanding it. A minimum claim at this + # depth needs all shallower layers, but no expansion of this layer. + if identity in queue: + if depth != claimed: + raise Reject("claimed minimum exceeds independent distance " + str(depth)) + return {"minimum": depth, "method": "first-ADD column-subtraction BFS", + "layers": layers, "visited_states": len(seen), + "edges_from_completed_layers": edges, + "completed_expansion_depths": list(range(depth))} + if depth == claimed: + raise Reject("identity absent through claimed distance " + str(claimed)) + for _ in range(width): + state = queue.popleft() + for d in range(N): + subtract = state[N*d:N*(d+1)] + for s in range(N): + if s == d: + continue + offset = N*s + reduced = tuple(state[offset+r] - subtract[r] for r in range(N)) + if any(value < int(r == s) for r, value in enumerate(reduced)): + continue + edges += 1 + previous = state[:offset] + reduced + state[offset+N:] + if previous not in seen: + if len(seen) >= max_states: + raise Reject("independent state budget exceeded; proof incomplete") + seen.add(previous) + queue.append(previous) + raise Reject("unreachable control flow") + + +def negative_controls(original, replacement, minimum): + """Small circuit controls; resource-heavy minimum mutations stay optional.""" + controls = [] + + def rejected(label, operation): + try: + operation() + except Reject: + controls.append(label) + return + raise Reject("negative control accepted: " + label) + + def fixed_check(candidate): + check_truth_table(original, candidate) + if matrix(original, True) != matrix(candidate, True): + raise Reject("fixed forward integer transfer changed") + + rejected("dropped circuit ADD", lambda: fixed_check(replacement[1:])) + flipped = [list(gate) for gate in replacement] + flipped[0].reverse() + rejected("reversed ADD operands", lambda: fixed_check(flipped)) + padded = list(replacement) + [[0, 1], [0, 1]] + check_truth_table(replacement, padded) + rejected("F2-neutral positive-transfer inflation", lambda: fixed_check(padded)) + # A small, fully exhausted graph checks both directions of the minimum + # comparison without repeating the frame-sized BFS several times. + unit = matrix([[0, 1]], True) + rejected("minimum underclaim", lambda: check_minimum(unit, 0)) + rejected("minimum overclaim", lambda: check_minimum(unit, 2)) + rejected("budget exhaustion is not a proof", lambda: check_minimum(unit, 1, 1)) + rejected("reverse-guard minimum underclaim", lambda: check_reverse_guard_minimum([[0, 1]], 0)) + rejected("reverse-guard minimum overclaim", lambda: check_reverse_guard_minimum([[0, 1]], 2)) + rejected("reverse-guard budget exhaustion is not a proof", + lambda: check_reverse_guard_minimum([[0, 1]], 1, 1)) + if type(minimum) is not int or minimum != len(replacement): + raise Reject("witness length does not match claimed minimum") + return controls + + +def check_reverse_guard_minimum(original, claimed, max_states=1_000_000): + """Independent shortest circuit proof with the original reverse envelope. + + Peel first gates with column subtraction. In parallel, their reverse-word + prefix is P = E_first E_second ... E_k, updated by right multiplication, + i.e. column ADD. Every entry of P is nondecreasing, so a prefix above the + original reverse matrix cannot complete to an admissible circuit. Enumerate + all surviving (residual transfer, reverse prefix) pairs breadth first. + Equal pairs reached later have identical possible continuations and may be + discarded. This proves a minimum in the narrower two-envelope class. + """ + if type(claimed) is not int or not 0 <= claimed <= 21: + raise Reject("invalid reverse-guard claimed distance") + if type(max_states) is not int or max_states < 1: + raise Reject("invalid reverse-guard state budget") + target_matrix = matrix(original, True) + bound_matrix = matrix(original[::-1], True) + target = tuple(target_matrix[r][c] for c in range(N) for r in range(N)) + bound = tuple(bound_matrix[r][c] for c in range(N) for r in range(N)) + identity = tuple(int(r == c) for c in range(N) for r in range(N)) + queue = deque([(target, identity)]) + seen = {(target, identity)} + layers, edges, pruned = [], 0, 0 + for depth in range(claimed + 1): + width = len(queue) + layers.append(width) + if any(residual == identity for residual, _ in queue): + if depth != claimed: + raise Reject("reverse-guard claim exceeds independent distance " + str(depth)) + return {"minimum": depth, "method": "first-ADD paired column-subtraction and column-addition BFS", + "layers": layers, "visited_states": len(seen), + "positive_residual_edges_from_completed_layers": edges, + "reverse_guard_pruned_edges": pruned, + "completed_expansion_depths": list(range(depth))} + if depth == claimed: + raise Reject("no reverse-guarded witness through claimed distance " + str(claimed)) + for _ in range(width): + residual, prefix = queue.popleft() + for d in range(N): + subtract = residual[N*d:N*(d+1)] + add = prefix[N*d:N*(d+1)] + for s in range(N): + if s == d: + continue + offset = N*s + reduced = tuple(residual[offset+r] - subtract[r] for r in range(N)) + if any(value < int(r == s) for r, value in enumerate(reduced)): + continue + edges += 1 + grown = tuple(prefix[offset+r] + add[r] for r in range(N)) + if any(value > bound[offset+r] for r, value in enumerate(grown)): + pruned += 1 + continue + previous = residual[:offset] + reduced + residual[offset+N:] + accumulated = prefix[:offset] + grown + prefix[offset+N:] + pair = (previous, accumulated) + if pair not in seen: + if len(seen) >= max_states: + raise Reject("reverse-guard state budget exceeded; proof incomplete") + seen.add(pair) + queue.append(pair) + raise Reject("unreachable reverse-guard control flow") + + +def verify(witness): + """Return a serializable finite proof; reverse growth is explicitly reported. + + Forward equality establishes the fixed-transfer synthesis claim. Reverse + domination is a sufficient precision condition, not an acceptance condition + here: any increases must be priced by the full-word auditor before deployment. + """ + original, replacement = witness["original"], witness["replacement"] + truth = check_truth_table(original, replacement) + before, after = matrix(original, True), matrix(replacement, True) + target = witness.get("integer_target", witness.get("target_matrix", before)) + if before != after or before != target: + raise Reject("claimed fixed forward integer transfer differs") + minimum = witness.get("minimum", len(replacement)) + if type(minimum) is not int or len(replacement) != minimum: + raise Reject("replacement length differs from claimed minimum") + optimum = check_minimum(target, minimum) + guarded_optimum = check_reverse_guard_minimum(original, len(original)) + reverse_before, reverse_after = matrix(original[::-1], True), matrix(replacement[::-1], True) + increases = [{"row": r, "column": c, "original": reverse_before[r][c], + "replacement": reverse_after[r][c]} + for r in range(N) for c in range(N) + if reverse_after[r][c] > reverse_before[r][c]] + return {**truth, "F2_matrix": matrix(replacement), + "positive_matrices": {"forward": {"original": before, "replacement": after}, + "reverse": {"original": reverse_before, "replacement": reverse_after}}, + "reverse_entrywise_dominated": not increases, + "reverse_increased_entries": increases, + "independent_minimum": optimum, + "independent_reverse_guard_minimum": guarded_optimum, + "controls_rejected": negative_controls(original, replacement, minimum), + "class": "six labelled registers; elementary positive ADD only; exact integer target; no ancillas", + "precision_scope": "reverse increases require full-word prefix and native payload pricing"} diff --git a/research/r439-frame281-seed15/native.py b/research/r439-frame281-seed15/native.py new file mode 100644 index 0000000000..f0be66ec3f --- /dev/null +++ b/research/r439-frame281-seed15/native.py @@ -0,0 +1,189 @@ +#!/usr/bin/env python3 +"""Replay frame281's two words with unchanged native legality/column checkers. + +Adapted from Ross Richardson's research/r439-frame267-seed01/native.py, +itself adapted from Ali Romman PR688, with substantial OpenAI Codex assistance. +The underlying exporter/cohort/checker authors retain their source attribution. +This frame281 adaptation was prepared with OpenAI Codex assistance. Apache-2.0. + +Requires a GCC/Clang-compatible C++17 compiler (CXX, default c++) and Boost +headers (BOOST_INCLUDE, default /usr/include). No dependency is installed. +""" +import argparse +import hashlib +import json +import os +from pathlib import Path +import platform +import shlex +import shutil +import struct +import subprocess +import sys +import tempfile + + +def compiler_command(): + value = os.environ.get("CXX", "c++") + # An unquoted Windows executable path may contain spaces. Shell-style + # commands such as "ccache c++" continue to work on other platforms. + return [value] if Path(value).is_file() else shlex.split(value) + + +def prefix_price(data): + """Price the pinned local and nine-stage expressions from native F/B bounds.""" + prefix = data["signed_lift_prefix"] + if len(prefix) != 2 or [row["reverse"] for row in prefix] != [False, True]: + raise ValueError("Signed prefix directions missing or reordered") + forward, backward = (int(row["cancellation_free_signed_row_l1_upper"]) for row in prefix) + if forward < 1 or backward < 1: + raise ValueError("Invalid signed prefix bound") + local = 64 * forward ** 3 * backward ** 2 + nine = (1 << 18) * forward ** 5 * backward ** 4 + if int(data["payload_prefix_upper"]) != local or data["payload_prefix_bits"] != local.bit_length(): + raise ValueError("Native payload receipt disagrees with its F/B bounds") + if local >= 1 << 104 or nine >= 1 << 192: + raise ValueError("Local 104-bit or nine-stage 192-bit precision charge exceeded") + return {"forward": str(forward), "backward": str(backward), + "local_payload_upper": str(local), "local_payload_bits": local.bit_length(), + "nine_stage_upper": str(nine), "nine_stage_bits": nine.bit_length()} + + +def run(root, out): + package = root / "research/e8-bit-carrier-skeleton" + bit = package / "code/bit" + checkers = bit / "checkers" + python = [sys.executable, "-I", "-B"] + compiler = compiler_command() + include = os.environ.get("BOOST_INCLUDE", "/usr/include") + flags = ["-O2", "-std=c++17", "-DHDIM=8", "-DNCOPY=9", "-DVPORTS=111", "-DRHELP=439", + "-I" + str(package / "portable-include"), "-I" + str(checkers), "-I" + include] + bindir = out / "bin" + bindir.mkdir() + suffix = ".exe" if os.name == "nt" else "" + commands = [] + + def binary(name): + return bindir / (name + suffix) + + def call(name, command): + command = list(map(str, command)) + commands.append(command) + (out / "commands.json").write_text(json.dumps(commands, indent=2) + "\n", encoding="utf-8") + with (out / (name + ".log")).open("x", encoding="utf-8") as log: + subprocess.run(command, check=True, stdout=log, stderr=subprocess.STDOUT) + + call("compile-legality", compiler + flags + ["-o", binary("legality"), checkers / "legality_h.cpp"]) + for pairs in (2, 4, 5): + call("compile-columns" + str(pairs), compiler + flags + ["-DKPAIRS=" + str(pairs), "-o", + binary("columns" + str(pairs)), checkers / "columns_k.cpp"]) + results, counts, nonadd = {}, {}, {} + for name in ("original", "replacement"): + base = out / name + records, cin, cout = (base / item for item in ("records", "cin", "cout")) + call(name + "-export", python + [bit / "export_records.py", out / (name + ".json.gz"), records]) + rows = list(struct.iter_unpack("<6i", (records / "249-records.bin").read_bytes())) + counts[name] = sum(row[0] == 1 for row in rows) + moves = {} + for row in rows: + if row[0] == 0: + moves.setdefault(row[1], []).append(row) + nonadd[name] = {"moves": moves, "copy_erase": [row for row in rows if row[0] in (2, 3)]} + call(name + "-cohort", python + [bit / "regression/stage_cohort.py", records, records, cin, cout]) + call(name + "-legality", [binary("legality"), cin, cout, cout / "legality.json"]) + legality = json.loads((cout / "legality.json").read_text()) + if legality["status"] != "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE": + raise ValueError("Legality did not pass") + if legality["common_frame_ADDs"] != counts[name] or legality["copies"] != 9 or legality["erasures"] != 9: + raise ValueError("Native legality ADD count or lifecycle differs") + results[name] = {"legality": legality, "stages": {}} + for pairs in (2, 4, 5): + receipt = cout / ("columns" + str(pairs) + ".json") + call(name + "-columns" + str(pairs), [binary("columns" + str(pairs)), + cout / "COHORT249-RECORDS.bin", receipt]) + data = json.loads(receipt.read_text()) + expected_status = ("PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" if pairs == 2 + else "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL") + if data["status"] != expected_status: + raise ValueError("Formal columns did not pass") + if (len(data["negative_controls"]) != 6 * (pairs - 1) + or not all(c["rejected"] is True for c in data["negative_controls"])): + raise ValueError("A bridge control failed") + if data["formal_columns_checked"] != 222 * pairs + 439 or len(data["stages"]) != 2 * pairs + 1: + raise ValueError("Wrong formal column or stage count") + if (data["local_scalar_additions"] != counts[name] + or data["bridge_additions"] != 6 * (pairs - 1) * 111 + or data["fresh_center_copies"] != 9 * (2 * pairs + 1)): + raise ValueError("Native stage cost differs from exported records") + price = prefix_price(data) + if "prefix_price" in results[name] and results[name]["prefix_price"] != price: + raise ValueError("Native local prefix bounds disagree across stage counts") + results[name]["prefix_price"] = price + data.pop("seconds", None) + data.pop("local_scalar_stream", None) + results[name]["stages"][str(2 * pairs + 1)] = data + if counts["original"] <= counts["replacement"]: + raise ValueError("Frame281 did not save exported ADDs") + if nonadd["original"] != nonadd["replacement"]: + raise ValueError("Per-register MOVE paths or COPY/ERASE events changed") + old_legal, new_legal = (results[name]["legality"] for name in ("original", "replacement")) + for key in ("rank_mass", "paid_histogram", "copies", "erasures"): + if old_legal[key] != new_legal[key]: + raise ValueError("Paid legality resource changed: " + key) + for stages in ("5", "9", "11"): + old, new = (results[name]["stages"][stages] for name in ("original", "replacement")) + if old["local_raw_H"] != new["local_raw_H"]: + raise ValueError("Paid profile differs") + return results + + +def main(): + here = Path(__file__).resolve().parent + root = here.parents[1] + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-certificate", action="store_true") + parser.add_argument("--output", type=Path, help="new output directory; preserve all native logs") + args = parser.parse_args() + compiler = compiler_command() + if not compiler or not shutil.which(compiler[0]): + raise ValueError("Set CXX to an available GCC/Clang-compatible C++17 compiler") + include = Path(os.environ.get("BOOST_INCLUDE", "/usr/include")) + if not (include / "boost/multiprecision/cpp_int.hpp").is_file(): + raise ValueError("Set BOOST_INCLUDE to the directory containing boost/multiprecision/cpp_int.hpp") + pins = json.loads((here / "SOURCES.json").read_text()) + for path, digest in pins["files"].items(): + content = (root / path).read_bytes() + if not path.endswith(".gz"): + content = content.replace(b"\r\n", b"\n") + if hashlib.sha256(content).hexdigest() != digest: + raise ValueError("source hash mismatch: " + path) + with tempfile.TemporaryDirectory(prefix="r439-frame281-native-") as temporary: + work = args.output.resolve() if args.output else Path(temporary) / "work" + # The verifier refuses an existing path and emits both bound words. + subprocess.run([sys.executable, "-I", "-B", str(here / "verify.py"), "--output", str(work)], check=True) + (work / "ENVIRONMENT.json").write_text(json.dumps({"python": sys.version, "platform": platform.platform(), + "compiler": subprocess.check_output(compiler + ["--version"], text=True), + "boost_include": str(include)}, indent=2) + "\n", encoding="utf-8") + result = run(root, work) + old_price, new_price = (result[name]["prefix_price"] for name in ("original", "replacement")) + growth = {key: int(new_price[key]) > int(old_price[key]) + for key in ("forward", "backward", "local_payload_upper", "nine_stage_upper")} + receipt = {"schema": "r439-frame281-native/1", "words": result, + "prefix_growth": growth, + "normalization": "Only seconds and local_scalar_stream removed; all other native fields retained. Derived prefix prices and growth flags are separate."} + path = here / "NATIVE-CERTIFICATE.json" + if args.write_certificate: + path.write_text(json.dumps(receipt, sort_keys=True, indent=2) + "\n", encoding="utf-8") + elif not path.is_file(): + raise ValueError("Native replay passed; use --write-certificate to record the first native receipt") + elif receipt != json.loads(path.read_text()): + raise ValueError("native certificate mismatch") + before, after = (result[name]["legality"]["common_frame_ADDs"] for name in ("original", "replacement")) + print(f"PASS_R439_FRAME281_NATIVE words=2 columns=883/1327/1549 bridge_controls=96 ADDs={before}->{after}") + print("prefix_growth=" + json.dumps(growth, sort_keys=True)) + print(f"prefix_bits local={old_price['local_payload_bits']}->{new_price['local_payload_bits']}/104 " + f"nine={old_price['nine_stage_bits']}->{new_price['nine_stage_bits']}/192") + + +if __name__ == "__main__": + main() diff --git a/research/r439-frame281-seed15/search.py b/research/r439-frame281-seed15/search.py new file mode 100644 index 0000000000..69d2f79e04 --- /dev/null +++ b/research/r439-frame281-seed15/search.py @@ -0,0 +1,202 @@ +"""Bounded exact synthesis for frame281's fixed positive six-wire transfer. + +Adapted from Ross Richardson's PR925 r439-frame267-seed01/search.py +(Apache-2.0), with flat immutable matrices and an explicit incomplete outcome. +Prepared for @woklerx with substantial OpenAI Codex assistance. +No search over other frames or general Boolean circuits. +""" +import argparse +from collections import Counter +from functools import cache +import gzip +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = ROOT / 'research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz' +PR952 = ROOT / 'research/r439-six-wire-boolean/candidate.json.gz' +REGS = [263, 275, 310, 374, 410, 491] +IDENTITY = bytes(int(i == j) for i in range(6) for j in range(6)) + + +def strict_json(raw): + def pairs(items): + result = {} + for key, value in items: + if key in result: + raise ValueError('duplicate JSON key: ' + key) + result[key] = value + return result + + def invalid_constant(value): + raise ValueError('invalid JSON constant: ' + value) + + return json.loads(raw, object_pairs_hook=pairs, parse_constant=invalid_constant) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False).encode() + + +def transfer(ops): + rows = [[int(i == j) for j in range(6)] for i in range(6)] + for dst, src in ops: + rows[dst] = [x + y for x, y in zip(rows[dst], rows[src])] + return rows + + +def source(path, start, stop): + word = strict_json(gzip.decompress(path.read_bytes())) + segment = word['A'][start:stop] + if len(segment) != stop-start or any(f != 281 or len(ss) != 1 for f, _, ss in segment): + raise ValueError('source slice changed') + if [i for i, gate in enumerate(word['A']) if gate[0] == 281] != list(range(start, stop)): + raise ValueError('slice is not the complete frame281 block') + return [[REGS.index(dst), REGS.index(ss[0])] for _, dst, ss in segment] + + +def nominate(original, state_cap=1_000_000, reverse_guard=False): + if type(state_cap) is not int or state_cap < 1: + raise ValueError('state cap must be a positive integer') + target = bytes(x for row in transfer(original) for x in row) + choices, histogram = {}, Counter() + edges = states = completed = 0 + infinity = 999 + + @cache + def distance(flat): + nonlocal edges, states, completed + if states >= state_cap: + raise OverflowError('state budget reached; no optimum established') + states += 1 + if flat == IDENTITY: + histogram[0] += 1 + completed += 1 + return 0 + best = infinity + for dst in range(6): + d = 6 * dst + row = flat[d:d+6] + for src in range(6): + if dst == src: + continue + s = 6 * src + other = flat[s:s+6] + if row[dst] <= other[dst] or any(x < y for x, y in zip(row, other)): + continue + previous = flat[:d] + bytes(x-y for x,y in zip(row,other)) + flat[d+6:] + edges += 1 + length = 1 + distance(previous) + if length < best: + best = length + choices[flat] = (dst, src, previous) + completed += 1 + histogram[best] += 1 + return best + + try: + minimum = distance(target) + except OverflowError: + return {'exhausted': False, 'minimum': None, 'replacement': original, + 'states': states, 'completed_states': completed, 'edges': edges, + 'state_cap': state_cap, 'distance_histogram': {str(k):v for k,v in sorted(histogram.items())}, + 'dead_end_distance': infinity} + if minimum >= infinity: + raise ValueError('no positive-addition factorization found') + backward, current = [], target + while current != IDENTITY: + dst, src, current = choices[current] + backward.append([dst, src]) + result = {'replacement': list(reversed(backward)), 'minimum': minimum, + 'exhausted': True, 'states': states, 'completed_states': completed, + 'edges': edges, 'state_cap': state_cap, + 'distance_histogram': {str(k):v for k,v in sorted(histogram.items())}, 'dead_end_distance': infinity} + if reverse_guard: + bound = bytes(x for row in transfer(original[::-1]) for x in row) + visited, guard_edges = 0, 0 + dead = set() + + def guarded(flat, reverse): + nonlocal visited, guard_edges + key = (flat, reverse) + if key in dead: + return None + if visited >= state_cap: + raise OverflowError('reverse guard state cap reached') + visited += 1 + if flat == IDENTITY: + return [] + remaining = distance(flat) + for dst in range(6): + d = 6*dst + row = flat[d:d+6] + for src in range(6): + if dst == src: + continue + s = 6*src + other = flat[s:s+6] + if row[dst] <= other[dst] or any(x < y for x,y in zip(row,other)): + continue + previous = flat[:d]+bytes(x-y for x,y in zip(row,other))+flat[d+6:] + if distance(previous) != remaining-1: + continue + summed = [x+y for x,y in zip(reverse[d:d+6],reverse[s:s+6])] + if any(x>y for x,y in zip(summed,bound[d:d+6])): + continue + next_reverse = reverse[:d]+bytes(summed)+reverse[d+6:] + guard_edges += 1 + tail = guarded(previous,next_reverse) + if tail is not None: + return [[dst,src]] + tail + dead.add(key) + return None + + try: + feasible = guarded(target, IDENTITY) + result['reverse_guard'] = {'states':visited,'edges':guard_edges, + 'shortest_feasible':feasible is not None, 'exhausted_without_witness':feasible is None} + if feasible is not None: + result['replacement'] = list(reversed(feasible)) + except OverflowError: + result['reverse_guard'] = {'states':visited,'edges':guard_edges, + 'shortest_feasible':None,'exhausted_without_witness':False} + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-witness', action='store_true') + args = parser.parse_args() + old = source(WORD, 906, 927) + retained = source(PR952, 825, 838) + prior = strict_json((ROOT / 'research/r439-frame267-seed01/WITNESS.json').read_bytes()) + permutation = [3, 2, 0, 1, 4, 5] + permuted_prior = [[permutation[d], permutation[s]] for d,s in prior['original']] + if transfer(permuted_prior) != transfer(old): + raise ValueError('selected-matrix PR925 conjugacy mismatch') + selected = {'start':906, 'stop':927, 'original':old, + 'target_matrix':transfer(old), 'pr925_conjugacy':permutation, **nominate(old)} + # Evidence-driven pivot within frame281: selected lift is conjugate to PR925. + # The retained PR952 lift is different and gives the genuinely new boundary. + result = {'phase': 'A', 'start': 825, 'stop': 838, 'frame': 281, 'quad': 15, + 'registers': REGS, 'assignment_seed': 15, 'source_pr':952, + 'original': retained, 'target_matrix': transfer(retained), + 'selected_reference':selected, **nominate(retained, reverse_guard=True)} + result['reverse_original_matrix'] = transfer(retained[::-1]) + result['reverse_replacement_matrix'] = transfer(result['replacement'][::-1]) + result['reverse_dominated_by_parent'] = all(y <= x + for a,b in zip(result['reverse_original_matrix'],result['reverse_replacement_matrix']) + for x,y in zip(a,b)) + path = HERE / 'WITNESS.json' + if args.write_witness: + path.write_text(json.dumps(result, indent=2, sort_keys=True, allow_nan=False) + '\n', encoding='utf-8') + elif canonical(result) != canonical(strict_json(path.read_bytes())): + raise ValueError('search witness mismatch') + print('PASS_FRAME281_SEARCH minimum={} states={} edges={} guarded_shortest={} selected_states={}'.format( + result['minimum'], result['states'], result['edges'], + result['reverse_guard']['shortest_feasible'], selected['states']), flush=True) + + +if __name__ == '__main__': + main() diff --git a/research/r439-frame281-seed15/verify.py b/research/r439-frame281-seed15/verify.py new file mode 100644 index 0000000000..7a4d9d7886 --- /dev/null +++ b/research/r439-frame281-seed15/verify.py @@ -0,0 +1,258 @@ +"""Source-bound finite frame281 circuit verification; no new kappa. + +Prepared for woklerx with substantial OpenAI Codex assistance, Apache-2.0. +Reuses credited, pinned PR925 framing/record checks and PR952 positive bounds. +The new local independent implementation does not import discovery code. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = 'research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz' +PR952 = 'research/r439-six-wire-boolean/candidate.json.gz' +AUDITOR = 'research/e8-bit-p111-tuned/code/xcheck_p.py' +EXPORTER = 'research/e8-bit-carrier-skeleton/code/bit/export_records.py' +REQUIRED_INPUTS = { + WORD, PR952, AUDITOR, EXPORTER, + 'research/r439-six-wire-boolean/verify.py', + 'research/r439-six-wire-boolean/common.py', + 'research/r439-six-wire-boolean/SOURCES.json', + 'research/r439-six-wire-boolean/CERTIFICATE.json', + 'research/r439-six-wire-boolean/NOTICE.md', + 'research/r439-frame267-seed01/verify.py', + 'research/r439-frame267-seed01/WITNESS.json', + 'research/r439-frame267-seed01/search.py', + 'research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py', + 'research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp', + 'research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp', + 'research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp', + 'research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h', + 'research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py', + 'docs/research/community-batch952-review.md', +} + + +def need(value, message): + if not value: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def load(path): + raw = Path(path).read_bytes() + if str(path).endswith('.gz'): + raw = gzip.decompress(raw) + def unique(items): + result = {} + for key, value in items: + need(key not in result, 'duplicate JSON key: ' + key) + result[key] = value + return result + + def invalid(value): + raise ValueError('non-finite JSON constant: ' + value) + + return json.loads(raw, object_pairs_hook=unique, parse_constant=invalid) + + +def module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + result = importlib.util.module_from_spec(spec) + spec.loader.exec_module(result) + return result + + +def source_pins(): + pins = load(HERE / 'SOURCES.json') + need(set(pins['files']) == REQUIRED_INPUTS, 'source inventory mismatch') + need(pins['base_commit'] == 'bbc600db2fc15007b7c914f4f2b2ed55fa909c87', 'base pin mismatch') + for name, expected in pins['files'].items(): + raw = (ROOT / name).read_bytes() + if not name.endswith('.gz'): + raw = raw.replace(b'\r\n', b'\n') + need(hashlib.sha256(raw).hexdigest() == expected, 'source pin mismatch: ' + name) + return pins + + +def extract(word): + indices = [i for i, g in enumerate(word['A']) if g[0] == 281] + need(indices and indices == list(range(indices[0], indices[-1] + 1)), 'frame281 not contiguous') + gates = word['A'][indices[0]:indices[-1] + 1] + need(all(len(s) == 1 for _, _, s in gates), 'non-elementary frame281 gate') + wires = sorted({r for _, d, ss in gates for r in [d] + ss}) + need(len(wires) == 6, 'frame281 wire count') + ops = [[wires.index(d), wires.index(ss[0])] for _, d, ss in gates] + return indices[0], indices[-1] + 1, wires, ops + + +def local_check(original, replacement, checks): + need(checks.matrix(original) == checks.matrix(replacement), 'local Boolean map changed') + need(checks.matrix(original, True) == checks.matrix(replacement, True), + 'fixed integer transfer changed') + return {direction: {'original': checks.matrix(a, True), + 'replacement': checks.matrix(b, True)} + for direction, a, b in (('forward', original, replacement), + ('reverse', original[::-1], replacement[::-1]))} + + +def splice(base, witness, checks): + start, stop, wires, original = extract(base) + need((start, stop) == (825, 838), 'PR952 frame281 slice changed') + need(witness['phase'] == 'A' and witness['frame'] == 281 and witness['quad'] == 15, + 'wrong witness object') + need(witness['assignment_seed'] == 15, 'assignment seed mismatch') + need((witness['start'], witness['stop']) == (start, stop), 'witness slice mismatch') + need(witness['registers'] == wires and witness['original'] == original, 'witness input mismatch') + need(witness['source_pr'] == 952, 'wrong source PR') + local_check(original, witness['replacement'], checks) + candidate = copy.deepcopy(base) + candidate['A'][start:stop] = [[281, wires[d], [wires[s]]] for d, s in witness['replacement']] + candidate['C'] = checks.cleanup(candidate) + need(checks.paths(base) == checks.paths(candidate), 'register frame paths changed') + return candidate + + +def run(output, write): + pins = source_pins() + discovery = subprocess.run([sys.executable, '-I', '-B', str(HERE / 'search.py')], + capture_output=True, text=True) + need(discovery.returncode == 0, 'discovery replay failed: ' + discovery.stderr) + selected, base = load(ROOT / WORD), load(ROOT / PR952) + witness = load(HERE / 'WITNESS.json') + checks = module('credited_pr925_checks', ROOT / 'research/r439-frame267-seed01/verify.py') + bounds = module('credited_pr952_checks', ROOT / 'research/r439-six-wire-boolean/verify.py') + independent = module('independent_frame281', HERE / 'independent.py') + # Discovery is run separately; this path never imports search.py. + candidate = splice(base, witness, checks) + old_ops = witness['original'] + new_ops = witness['replacement'] + old_start, old_stop, wires, _ = extract(base) + selected_start, selected_stop, selected_wires, selected_ops = extract(selected) + need(wires == selected_wires, 'selected frame281 wires changed') + need(checks.matrix(old_ops) == checks.matrix(selected_ops), 'selected comparison map differs') + independent_result = independent.verify(witness) + positive = local_check(old_ops, new_ops, checks) + scalar = {name: bounds.word_checks(word) for name, word in + (('original', base), ('replacement', candidate), ('selected589', selected))} + need(scalar['selected589']['ADDs'] == 24305 and scalar['original']['ADDs'] == 23673, + 'predecessor ADD bills') + saved = 2 * (len(old_ops) - len(new_ops)) + need(scalar['original']['ADDs'] - scalar['replacement']['ADDs'] == saved, + 'complete forward/cleanup ADD saving') + # Local reverse domination is sufficient, not necessary. word_checks prices + # both whole-word orientations and enforces 104/192-bit inherited caps. + prefix_source = bounds.prefix_binding(ROOT) + print('Local matrix, all-word dirty columns and positive bounds passed', flush=True) + + checker = module('pinned_interface_checker', ROOT / AUDITOR) + geometry, labels, original_full, h, conclusions, _ = checker.check(base) + need(all(h.values()) and all(conclusions.values()), 'original H1-H5 failed') + candidate_full = checks.audit(candidate, checker, geometry) + need(candidate_full['columns'] == 661, 'all-column coverage') + evidence = {} + for name, word in (('original', base), ('replacement', candidate)): + path = output / (name + '.json.gz') + path.write_bytes(gzip.compress(canonical(word), mtime=0)) + records = output / name / 'records' + completed = subprocess.run([sys.executable, '-I', '-B', str(ROOT / EXPORTER), + str(path), str(records)], capture_output=True, text=True) + need(completed.returncode == 0, 'export failed: ' + completed.stderr) + evidence[name] = checks.records_check(records, word) + for key in ('moves', 'copies', 'erasures', 'paid_histogram', 'rank_mass'): + need(evidence['original'][key] == evidence['replacement'][key], 'paid cost changed: ' + key) + need(evidence['replacement']['rank_mass'] == 5129 and evidence['replacement']['copies'] == 9, + 'rank mass or copy count') + need(evidence['original']['adds'] - evidence['replacement']['adds'] == saved, 'exported ADD saving') + + controls = [] + exceptions = (ValueError, checks.Reject, checker.Reject) + + def reject(name, action): + try: + action() + except exceptions: + controls.append(name) + return + raise ValueError('negative control accepted: ' + name) + + reject('drop circuit gate', lambda: local_check(old_ops, new_ops[1:], checks)) + bad_ops = copy.deepcopy(new_ops) + bad_ops[0].reverse() + reject('reverse circuit operands', lambda: local_check(old_ops, bad_ops, checks)) + inflated = new_ops + [[0, 1], [0, 1]] + need(checks.matrix(inflated) == checks.matrix(new_ops), 'inflation must be F2-neutral') + reject('F2-neutral positive inflation', lambda: local_check(old_ops, inflated, checks)) + bad = copy.deepcopy(candidate) + bad['C'].pop() + reject('drop cleanup gate', lambda: checks.audit(bad, checker, geometry)) + bad = copy.deepcopy(candidate) + bad['C'] = copy.deepcopy(base['C']) + # The stale cleanup has the right Boolean endpoint but fails literal H4. + obj = copy.copy(geometry) + obj.w = bad + obj.full() + reject('stale nonliteral cleanup', lambda: checks.audit(bad, checker, geometry)) + bad = copy.deepcopy(candidate) + bad['A'][old_start][0] = 0 + reject('illegal frame descent', lambda: checks.audit(bad, checker, geometry)) + bad = copy.deepcopy(candidate) + bad['D'][0][2].pop() + reject('missing dirty compensation', lambda: checks.audit(bad, checker, geometry)) + + # A source-bound comparison, not an assumed sum of other PRs' savings. + overlap = {'pr952_frame_gates': len(old_ops), 'selected_frame_gates': len(selected_ops), + 'new_frame_gates': len(new_ops), 'selected_slice': [selected_start, selected_stop], + 'same_positive_transfer_as_selected': checks.matrix(selected_ops, True) == checks.matrix(old_ops, True), + 'additional_frame_saving_vs_pr952': len(old_ops) - len(new_ops), + 'selected_ops': selected_ops, 'pr952_word_ADDs': scalar['original']['ADDs']} + certificate = {'status': 'PASS_R439_FRAME281', 'base_commit': pins['base_commit'], + 'frame': 281, 'quad': 15, 'source_slice': [old_start, old_stop], + 'wires': wires, 'old_gates': len(old_ops), 'new_gates': len(new_ops), + 'saved_with_cleanup': saved, 'independent': independent_result, + 'positive_matrices': positive, 'scalar': scalar, 'prefix_source': prefix_source, + 'labels': labels, 'columns': candidate_full['columns'], + 'exported_records': evidence, 'overlap': overlap, + 'controls_rejected': controls, 'word_sha256': digest(candidate), + 'kappa_claim': 'none; unchanged paid profile; full hosted adoption not performed'} + path = HERE / 'CERTIFICATE.json' + if write: + path.write_text(json.dumps(certificate, indent=2, sort_keys=True) + '\n', encoding='utf-8') + else: + need(canonical(certificate) == canonical(load(path)), 'certificate mismatch') + print('PASS_R439_FRAME281 gates={}->{} local_ADDs=23673->{} columns=661 rank_mass=5129 controls={}'.format( + len(old_ops), len(new_ops), evidence['replacement']['adds'], len(controls))) + return certificate + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path, help='fresh directory for both reconstructed words and records') + parser.add_argument('--write-certificate', action='store_true') + 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='r439-frame281-') as temporary: + run(Path(temporary), args.write_certificate) + + +if __name__ == '__main__': + main()