diff --git a/research/r439-five-cycle-seed9f01/CANDIDATE.json.gz b/research/r439-five-cycle-seed9f01/CANDIDATE.json.gz new file mode 100644 index 0000000000..9e4ca90ee9 Binary files /dev/null and b/research/r439-five-cycle-seed9f01/CANDIDATE.json.gz differ diff --git a/research/r439-five-cycle-seed9f01/CERTIFICATE.json b/research/r439-five-cycle-seed9f01/CERTIFICATE.json new file mode 100644 index 0000000000..8f136b93c6 --- /dev/null +++ b/research/r439-five-cycle-seed9f01/CERTIFICATE.json @@ -0,0 +1,120 @@ +{ + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "controls": [ + "missing helper preparation edge rejected by D boundary", + "missing inverse restoration edge rejected by D boundary", + "stale injection rejected by D boundary", + "wrong inverse order rejected by D boundary", + "mutated injection coefficient rejected by D boundary" + ], + "exact_precision": { + "local": { + "lhs": "44468459235010318794652647424", + "rhs": "20282409603651670423947251286016" + }, + "nine_stage": { + "lhs": "4676708453903757010070537011688772133559165966010548224", + "rhs": "6277101735386680763835789423207666416102355444464034512896" + } + }, + "new_kappa": false, + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "paid_rank_mass": 5129, + "search": { + "candidates": 1860480, + "optimistic_max_net_ADD_saving": 109, + "positive_saving_candidates": 56, + "selected": { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 129, + 25 + ], + "saving": 12, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + "supports": 15504, + "sweeps_per_support": 120 + }, + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "status": "PASS_R439_FIVE_CYCLE", + "unrun": [ + "native C++ replay", + "supplier adoption", + "outer assembly replay", + "all-size/compiler and analytic proof obligations" + ], + "word": { + "columns": 661, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "directions": 2, + "exporter": { + "adds": 11488, + "copies": 9, + "erasures": 9, + "forward": 27061, + "payload_bits": 96, + "record_sha256": "10de6f93ba0dcf14aaeb0bfeaea0e35f65ad5ba22de6284fe2828a7ee0504930", + "reverse": 5921344 + }, + "literal": { + "B": 5921344, + "D_adds": 5536, + "F": 27061, + "local_bits": 96, + "native_ADDs": 11488, + "nine_stage_bits": 182 + } + } +} diff --git a/research/r439-five-cycle-seed9f01/README.md b/research/r439-five-cycle-seed9f01/README.md new file mode 100644 index 0000000000..3c699c1b1a --- /dev/null +++ b/research/r439-five-cycle-seed9f01/README.md @@ -0,0 +1,134 @@ +# Five-helper cyclic basis change on the R439 D map + +**Finite local circuit construction; no new κ.** A five-edge directed cycle on +five helpers reduces the pinned R439 D-stage cost by 12 ADDs after paying for +both preparation and restoration. The selected result, accepted bit supplier, +paid rank profile and `upstream/` are unchanged. The selected complex side still +binds. + +## Exact construction + +The source is the source-pinned 11,500-ADD word in +[`research/r439-bsection-stars-seed01/`](../r439-bsection-stars-seed01/README.md), +which combines the R439 helper-star D word with its ten phase-B block programs. +The cycle is applied **after** the old helper preparation. Using local helper +indices, its chronological word is: + +```text +helper[59] ^= helper[148] +helper[148] ^= helper[21] +helper[21] ^= helper[129] +helper[129] ^= helper[25] +helper[25] ^= helper[59] +``` + +The corresponding absolute wire IDs are 281, 370, 243, 351 and 247. Write +`H0` for the original helper basis change, `H1` for this five-operation cycle, +and `J0` for the original 111-by-439 injection. The old helper state at +injection is `H0 s`. The new state is `H1 H0 s`; use the injection +`J0 H1^-1`, then restore `H1^-1` in reverse operation order before the old +`H0^-1`. Thus + +```text +J0 H1^-1 H1 H0 s = J0 H0 s +``` + +for every helper vector `s`, including arbitrary dirty values. The target and +helper D boundary is identical. The existing target preparation/restoration, +other stages, COPY/ERASE records and frame schedule remain in place. + +The five selected injection columns have total weight 92 before the cycle and +70 after it. Their 111-row injection therefore drops from 4,464 to 4,442 ADDs. +The cycle adds five preparation and five restoration ADDs, giving: + +| Quantity | Pinned word | Cyclic word | +|---|---:|---:| +| Injection ADDs | 4,464 | 4,442 | +| Helper cycle preparation and restoration | 0 | 10 | +| Complete D-stage ADDs | 5,548 | 5,536 | +| Complete R439 word ADDs | 11,500 | **11,488** | +| Paid rank mass | 5,129 | 5,129 | + +The complete-word bounds are `F=27,061` and `B=5,921,344`. Exact integer +arithmetic gives + +```text +64 F^3 B^2 = 44468459235010318794652647424 + < 20282409603651670423947251286016 = 2^104 + +2^18 F^5 B^4 = 4676708453903757010070537011688772133559165966010548224 + < 6277101735386680763835789423207666416102355444464034512896 = 2^192 +``` + +## Bounded search and optimistic price + +Rank all 439 injection columns by their total pairwise support overlap, breaking +ties by column weight (larger first) and local helper index (smaller first). +Take the top 20 helpers. For every one of the 15,504 five-element supports, +test all 120 permutations, where each permutation gives the five chronological +cyclic edges `p[i] ^= p[i+1]` with indices modulo five. The search tests exactly +**1,860,480** words and stops there. It finds 56 words with positive complete +ADD savings; four tie at the maximum of 12. The candidate above is the +lexicographically first maximum. + +Before enumeration, a favorable basis bound gave at most 109 net ADDs of +savings in this domain: the highest-ranked five columns have weight 124 and +rank five, while preparation and restoration cost ten. For any invertible +change on five columns, the new injection has at least that rank in nonzero +columns. The cycle search attains 12 of the 109-ADD ceiling. + +The paid profile is unchanged, so the recursive moment and κ gain are exactly +zero. This construction does not enter the selected assembly or establish a +smaller integer-multiplication exponent. It is scoped to the frozen R439 word +and the stated top-20 cyclic-sweep domain; it is not a minimum over other helper +supports, longer cycles, target bases or complete circuits. + +## Verification + +The source-pinned replay uses the standard library and the retained R439 +boundary, owner and exporter checks: + +```sh +python3 -B research/r439-five-cycle-seed9f01/verify.py +python3 scripts/research_package.py --package research/r439-five-cycle-seed9f01 --check-only +python3.12 scripts/research_package.py --package research/r439-five-cycle-seed9f01 +``` + +The first command repeats the full finite search, checks all 661 formal columns +in both directions, verifies the dirty D boundary, replays H1–H5 and the paid +profile, and checks the complete exporter invoice and precision expressions. +It also rejects five controls: a missing preparation edge, a missing inverse +edge, the stale injection, a wrong inverse order, and a changed injection +coefficient. The expected final line is: + +```text +PASS_R439_FIVE_CYCLE candidates=1860480 best_saving=12 ADDs=11500->11488 columns=661 controls=5 no_new_kappa +``` + +The exact candidate, search receipt and replay receipt are +[`CANDIDATE.json.gz`](CANDIDATE.json.gz), +[`SEARCH-RESULT.json`](SEARCH-RESULT.json) and +[`CERTIFICATE.json`](CERTIFICATE.json). `SOURCES.json` pins the task catalogue, +selected result, review, source manifest, assembly certificate and every live +input used by the predecessor replay. The conditional result remains subject +to the inherited all-size/compiler, common-label/mutable-source realization, +whole-call hosting, precision/tape and analytic-transfer assumptions. Native +C++ replay, supplier adoption and outer assembly replay were not run here. + +## Open next questions + +- **Can a six-helper cyclic change save more on the same D map?** A longer cycle + could realize multi-column cancellations unavailable to a five-cycle. First + compute its exact rank-based optimistic ceiling and full six-edge + preparation/restoration bill on a bounded overlap-ranked support family. + Continue only if that ceiling is positive and the precision budget is + favorable. + +## Credit + +The R439 word, helper-star basis, phase-B programs and retained checkers come +from the predecessor packages and PR lineage named in `SOURCES.json` and the +linked README. Those inputs are reused unchanged. Prepared by Cinna Davis +(@1337isnot1337) with substantial OpenAI Codex assistance in the derivation, +search, implementation, checking and writing. No independent human review is +claimed. This package is Apache-2.0. diff --git a/research/r439-five-cycle-seed9f01/SEARCH-RESULT.json b/research/r439-five-cycle-seed9f01/SEARCH-RESULT.json new file mode 100644 index 0000000000..b0cbae6db2 --- /dev/null +++ b/research/r439-five-cycle-seed9f01/SEARCH-RESULT.json @@ -0,0 +1,2463 @@ +{ + "base_injection_adds": 4464, + "best_64": [ + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 129, + 25 + ], + "saving": 12, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 148 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 129, + 25 + ], + "saving": 12, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 129, + 131 + ], + "saving": 12, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 129, + 131 + ], + "saving": 12, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 59 + ] + ], + "injection_weight": 4447, + "new_support_weight": 75, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 131, + 129 + ], + "saving": 7, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 21 + ], + [ + 21, + 59 + ] + ], + "injection_weight": 4447, + "new_support_weight": 75, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 129, + 131, + 21 + ], + "saving": 7, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 148 + ] + ], + "injection_weight": 4447, + "new_support_weight": 75, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 131, + 129 + ], + "saving": 7, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 21 + ], + [ + 21, + 148 + ] + ], + "injection_weight": 4447, + "new_support_weight": 75, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 129, + 131, + 21 + ], + "saving": 7, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 59 + ] + ], + "injection_weight": 4448, + "new_support_weight": 76, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 131, + 129, + 21 + ], + "saving": 6, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 148 + ] + ], + "injection_weight": 4448, + "new_support_weight": 76, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 131, + 129, + 21 + ], + "saving": 6, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 199 + ], + [ + 199, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4448, + "new_support_weight": 73, + "old_support_weight": 89, + "permutation": [ + 59, + 148, + 21, + 199, + 131 + ], + "saving": 6, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 199 + ], + [ + 199, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4448, + "new_support_weight": 73, + "old_support_weight": 89, + "permutation": [ + 148, + 59, + 21, + 199, + 131 + ], + "saving": 6, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 139 + ], + [ + 139, + 25 + ], + [ + 25, + 119 + ], + [ + 119, + 59 + ] + ], + "injection_weight": 4448, + "new_support_weight": 83, + "old_support_weight": 99, + "permutation": [ + 59, + 148, + 139, + 25, + 119 + ], + "saving": 6, + "support": [ + 25, + 59, + 119, + 139, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 139 + ], + [ + 139, + 25 + ], + [ + 25, + 119 + ], + [ + 119, + 148 + ] + ], + "injection_weight": 4448, + "new_support_weight": 83, + "old_support_weight": 99, + "permutation": [ + 148, + 59, + 139, + 25, + 119 + ], + "saving": 6, + "support": [ + 25, + 59, + 119, + 139, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 25 + ], + [ + 25, + 129 + ], + [ + 129, + 59 + ] + ], + "injection_weight": 4449, + "new_support_weight": 77, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 25, + 129 + ], + "saving": 5, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 25 + ], + [ + 25, + 129 + ], + [ + 129, + 148 + ] + ], + "injection_weight": 4449, + "new_support_weight": 77, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 25, + 129 + ], + "saving": 5, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 25 + ], + [ + 25, + 139 + ], + [ + 139, + 119 + ], + [ + 119, + 59 + ] + ], + "injection_weight": 4449, + "new_support_weight": 84, + "old_support_weight": 99, + "permutation": [ + 59, + 148, + 25, + 139, + 119 + ], + "saving": 5, + "support": [ + 25, + 59, + 119, + 139, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 25 + ], + [ + 25, + 139 + ], + [ + 139, + 119 + ], + [ + 119, + 148 + ] + ], + "injection_weight": 4449, + "new_support_weight": 84, + "old_support_weight": 99, + "permutation": [ + 148, + 59, + 25, + 139, + 119 + ], + "saving": 5, + "support": [ + 25, + 59, + 119, + 139, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 78, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 129, + 21, + 25 + ], + "saving": 4, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 25 + ], + [ + 25, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 78, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 129, + 21, + 25 + ], + "saving": 4, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 112 + ], + [ + 112, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 74, + "old_support_weight": 88, + "permutation": [ + 59, + 148, + 21, + 129, + 112 + ], + "saving": 4, + "support": [ + 21, + 59, + 112, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 112 + ], + [ + 112, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 74, + "old_support_weight": 88, + "permutation": [ + 148, + 59, + 21, + 129, + 112 + ], + "saving": 4, + "support": [ + 21, + 59, + 112, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 78, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 129, + 21, + 131 + ], + "saving": 4, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 78, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 129, + 21, + 131 + ], + "saving": 4, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 199 + ], + [ + 199, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 75, + "old_support_weight": 89, + "permutation": [ + 59, + 148, + 21, + 131, + 199 + ], + "saving": 4, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 199 + ], + [ + 199, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 75, + "old_support_weight": 89, + "permutation": [ + 148, + 59, + 21, + 131, + 199 + ], + "saving": 4, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 125 + ], + [ + 125, + 112 + ], + [ + 112, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 79, + "old_support_weight": 93, + "permutation": [ + 59, + 148, + 125, + 112, + 131 + ], + "saving": 4, + "support": [ + 59, + 112, + 125, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 125 + ], + [ + 125, + 112 + ], + [ + 112, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 79, + "old_support_weight": 93, + "permutation": [ + 148, + 59, + 125, + 112, + 131 + ], + "saving": 4, + "support": [ + 59, + 112, + 125, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 52 + ], + [ + 52, + 58 + ], + [ + 58, + 59 + ] + ], + "injection_weight": 4451, + "new_support_weight": 80, + "old_support_weight": 93, + "permutation": [ + 59, + 148, + 21, + 52, + 58 + ], + "saving": 3, + "support": [ + 21, + 52, + 58, + 59, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 52 + ], + [ + 52, + 58 + ], + [ + 58, + 148 + ] + ], + "injection_weight": 4451, + "new_support_weight": 80, + "old_support_weight": 93, + "permutation": [ + 148, + 59, + 21, + 52, + 58 + ], + "saving": 3, + "support": [ + 21, + 52, + 58, + 59, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 91 + ], + [ + 91, + 113 + ], + [ + 113, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4451, + "new_support_weight": 85, + "old_support_weight": 98, + "permutation": [ + 59, + 148, + 91, + 113, + 131 + ], + "saving": 3, + "support": [ + 59, + 91, + 113, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 91 + ], + [ + 91, + 113 + ], + [ + 113, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4451, + "new_support_weight": 85, + "old_support_weight": 98, + "permutation": [ + 148, + 59, + 91, + 113, + 131 + ], + "saving": 3, + "support": [ + 59, + 91, + 113, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 112 + ], + [ + 112, + 125 + ], + [ + 125, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4451, + "new_support_weight": 80, + "old_support_weight": 93, + "permutation": [ + 59, + 148, + 112, + 125, + 131 + ], + "saving": 3, + "support": [ + 59, + 112, + 125, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 112 + ], + [ + 112, + 125 + ], + [ + 125, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4451, + "new_support_weight": 80, + "old_support_weight": 93, + "permutation": [ + 148, + 59, + 112, + 125, + 131 + ], + "saving": 3, + "support": [ + 59, + 112, + 125, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 21 + ], + [ + 21, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 59, + 21, + 148, + 129, + 25 + ], + "saving": 2, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 21 + ], + [ + 21, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 148 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 148, + 21, + 59, + 129, + 25 + ], + "saving": 2, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4452, + "new_support_weight": 77, + "old_support_weight": 89, + "permutation": [ + 59, + 148, + 21, + 112, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 112, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4452, + "new_support_weight": 77, + "old_support_weight": 89, + "permutation": [ + 148, + 59, + 21, + 112, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 112, + 131, + 148 + ] + }, + { + "edges": [ + [ + 21, + 59 + ], + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 21 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 21, + 59, + 148, + 129, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 21, + 148 + ], + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 21 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 21, + 148, + 59, + 129, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 21 + ], + [ + 21, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 59, + 21, + 148, + 129, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 21 + ], + [ + 21, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 148, + 21, + 59, + 129, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 119 + ], + [ + 119, + 59 + ] + ], + "injection_weight": 4452, + "new_support_weight": 87, + "old_support_weight": 99, + "permutation": [ + 59, + 148, + 129, + 131, + 119 + ], + "saving": 2, + "support": [ + 59, + 119, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 119 + ], + [ + 119, + 148 + ] + ], + "injection_weight": 4452, + "new_support_weight": 87, + "old_support_weight": 99, + "permutation": [ + 148, + 59, + 129, + 131, + 119 + ], + "saving": 2, + "support": [ + 59, + 119, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 58 + ], + [ + 58, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 81, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 112, + 58 + ], + "saving": 1, + "support": [ + 21, + 58, + 59, + 112, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 58 + ], + [ + 58, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 81, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 112, + 58 + ], + "saving": 1, + "support": [ + 21, + 58, + 59, + 112, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 129 + ], + [ + 129, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 77, + "old_support_weight": 88, + "permutation": [ + 59, + 148, + 21, + 112, + 129 + ], + "saving": 1, + "support": [ + 21, + 59, + 112, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 129 + ], + [ + 129, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 77, + "old_support_weight": 88, + "permutation": [ + 148, + 59, + 21, + 112, + 129 + ], + "saving": 1, + "support": [ + 21, + 59, + 112, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 199 + ], + [ + 199, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 78, + "old_support_weight": 89, + "permutation": [ + 59, + 148, + 199, + 21, + 131 + ], + "saving": 1, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 199 + ], + [ + 199, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 78, + "old_support_weight": 89, + "permutation": [ + 148, + 59, + 199, + 21, + 131 + ], + "saving": 1, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 91 + ], + [ + 91, + 131 + ], + [ + 131, + 113 + ], + [ + 113, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 87, + "old_support_weight": 98, + "permutation": [ + 59, + 148, + 91, + 131, + 113 + ], + "saving": 1, + "support": [ + 59, + 91, + 113, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 91 + ], + [ + 91, + 131 + ], + [ + 131, + 113 + ], + [ + 113, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 87, + "old_support_weight": 98, + "permutation": [ + 148, + 59, + 91, + 131, + 113 + ], + "saving": 1, + "support": [ + 59, + 91, + 113, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 119 + ], + [ + 119, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 88, + "old_support_weight": 99, + "permutation": [ + 59, + 148, + 131, + 129, + 119 + ], + "saving": 1, + "support": [ + 59, + 119, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 119 + ], + [ + 119, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 88, + "old_support_weight": 99, + "permutation": [ + 148, + 59, + 131, + 129, + 119 + ], + "saving": 1, + "support": [ + 59, + 119, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 122 + ], + [ + 122, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 87, + "old_support_weight": 98, + "permutation": [ + 59, + 148, + 129, + 131, + 122 + ], + "saving": 1, + "support": [ + 59, + 122, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 122 + ], + [ + 122, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 87, + "old_support_weight": 98, + "permutation": [ + 148, + 59, + 129, + 131, + 122 + ], + "saving": 1, + "support": [ + 59, + 122, + 129, + 131, + 148 + ] + } + ], + "candidate_gzip_sha256": "286fb2e8b397909bd74257ef911b4a76a633e169493d481a9ca40379ae9072b9", + "candidate_sha256": "b19f7c71997e5d402003b62c7083fc115fec931344ead2667d4e736e0008be2b", + "candidates": 1860480, + "optimistic_max_net_ADD_saving": { + "net": 109, + "old_weight": 124, + "preparation_and_restoration_ADDs": 10, + "rank": 5, + "support": [ + 58, + 113, + 131, + 25, + 139 + ] + }, + "positive_saving_candidates": 56, + "selected_candidate": { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 129, + 25 + ], + "saving": 12, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + "stopping_rule": "complete all 15,504 five-subsets of the top 20 helpers and all 120 directed cyclic sweeps per subset", + "supports": 15504, + "sweeps_per_support": 120, + "top_helpers": [ + 58, + 113, + 131, + 25, + 139, + 129, + 52, + 239, + 122, + 199, + 119, + 125, + 274, + 100, + 21, + 59, + 148, + 91, + 43, + 112 + ], + "top_scores": [ + 1849, + 1810, + 1657, + 1577, + 1535, + 1511, + 1408, + 1401, + 1400, + 1385, + 1374, + 1372, + 1370, + 1346, + 1318, + 1304, + 1304, + 1277, + 1270, + 1256 + ] +} diff --git a/research/r439-five-cycle-seed9f01/SOURCES.json b/research/r439-five-cycle-seed9f01/SOURCES.json new file mode 100644 index 0000000000..1bc4bcfacb --- /dev/null +++ b/research/r439-five-cycle-seed9f01/SOURCES.json @@ -0,0 +1,145 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "usage": "input", + "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/r439-bsection-stars-seed01/CERTIFICATE.json", + "usage": "input", + "git_blob": "2cff2738f7869abb58b95cc7eec533c46c4a591a", + "sha256": "252cf7c4981be1c9dcfb7654d917d51a0303a21eee036988b74f9ef436f9c287" + }, + { + "path": "research/r439-bsection-stars-seed01/README.md", + "usage": "input", + "git_blob": "188175a52bb2a3ad65c701b3bd218ae3fc0bdfde", + "sha256": "3a32ecbf886d6605eb7441c63ca934c6aab0942d0e7e570c3dd0795d1cf00336" + }, + { + "path": "research/r439-bsection-stars-seed01/SOURCES.json", + "usage": "input", + "git_blob": "8c02baa7fcc9e04abb8f7fc81299c708b3dfeb42", + "sha256": "779a4d0d1ca0d578026d0f4ce0f8f16466cc6e866b7d80193ef9e7eb2a2d6cfe" + }, + { + "path": "research/r439-bsection-stars-seed01/build.py", + "usage": "input", + "git_blob": "0c9e3253e527f3a409406797914a3aaa8cb36814", + "sha256": "15ceb1d806fcd4f903324d3c2aaf7655c08073f2bfa56bd39cbcfd49a0757fa6" + }, + { + "path": "research/r439-bsection-stars-seed01/candidate.json.gz", + "usage": "input", + "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c", + "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee" + }, + { + "path": "research/r439-bsection-stars-seed01/candidate_search.json", + "usage": "input", + "git_blob": "97f5d9f0d3a153feb2b38a39daf826d959364e8f", + "sha256": "488741d5ad803372b622495972d754ab2998a8afb0b84ef755edc337b20d0af0" + }, + { + "path": "research/r439-bsection-stars-seed01/inputs/PR1015-CANDIDATE.json", + "usage": "input", + "git_blob": "16532f2d8d4fb16fde803cecf32e3ce11369ea56", + "sha256": "388c2a0db00dbe77b67649af7293e577cf3869da7ae0d0341e17ecff2b16c84c" + }, + { + "path": "research/r439-bsection-stars-seed01/verify.py", + "usage": "input", + "git_blob": "be296a579cef6722786d589652f73662a92252fb", + "sha256": "eb387243b9071a0309e04248bc088fe6f33067e39f87d9fcd1785866020b97ee" + }, + { + "path": "research/r439-frame520/RECEIPT.json", + "usage": "input", + "git_blob": "f9feff1bf28ea44ff3d63e4b1527a0137972606c", + "sha256": "449b4c698edf4ba377bf41582c4cb8245aee6888b45e48c823270fbe9392bcfb" + }, + { + "path": "research/r439-frame520/candidate.json", + "usage": "input", + "git_blob": "f26a59896f5da6043e759f072232fb8a66c17f41", + "sha256": "18cb7f41f6451f3af3559e8c09fb323ec6d1003de82ab4f0cff5d59c070ed208" + }, + { + "path": "research/r439-helper-stars-seed19/CERTIFICATE.json", + "usage": "input", + "git_blob": "8eba4f44a484b047b82d48d4d87a356b67315555", + "sha256": "35bdbd763e29791e4fa43d99d764d536fa284e89023bb9da482d2f3ba80ce333" + }, + { + "path": "research/r439-helper-stars-seed19/build.py", + "usage": "input", + "git_blob": "c7a3a8355fa9362499ad52e2572d747ca912f0c6", + "sha256": "c14c75c73fab605ab9fc133d6c146bd3d14a5e8a0ed85db1247981c4959f9ac7" + }, + { + "path": "research/r439-helper-stars-seed19/candidate.json.gz", + "usage": "input", + "git_blob": "8b0210d8b8e9524182e5f54f9bf93c28f4719735", + "sha256": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8" + }, + { + "path": "research/r439-helper-stars-seed19/common.py", + "usage": "input", + "git_blob": "bced44f0b254eac7b3f832648ce0f0090f07930b", + "sha256": "a596d898017d8832e7bcb987fc12cccbd2c88a7ad760c10a1329b0a8ea21edec" + }, + { + "path": "research/r439-target-compensation/candidate.json.gz", + "usage": "input", + "git_blob": "7f1f188f516ca4661f419dc72114751abf3cc920", + "sha256": "ac30266144f8772ec8cd629153993aa9eb692fe745a9f95015a1b7fa88977a2e" + } + ] +} diff --git a/research/r439-five-cycle-seed9f01/TASK.json b/research/r439-five-cycle-seed9f01/TASK.json new file mode 100644 index 0000000000..0a7eac1614 --- /dev/null +++ b/research/r439-five-cycle-seed9f01/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Five-step directed cyclic helper basis changes applied after the pinned R439 helper preparation, with injection J0 H1^-1 and reverse restoration, exhaustively priced on all five-subsets of the top 20 overlap-ranked helper coordinates.", + "scope_change_reason": "The originally suggested helper-star/quartet instances already have source-pinned constructions and searches in main; a fresh overlap scan found no current claim for a five-helper cyclic sweep. The second eligible bit task is covered broadly by fresh PRs #1333 and #1662. This changes the mixing topology and checks the exact dirty-boundary identity for the new word rather than auditing the predecessor.", + "bottleneck_link": "The resulting word retains the same rank/copy/frame profile, so it changes no recursive moment or kappa and cannot unbind the selected complex side. It is a fully charged local bit-circuit reduction that may provide a lower-cost R439 implementation if the inherited supplier and hosting obligations are later accepted.", + "budget_minutes": 60, + "stop_rule": "Exhaust exactly 15,504 five-helper supports among the overlap-ranked top 20 and all 120 directed cyclic sweeps per support; certify the selected maximum-saving candidate under the exact D/full-word, paid-profile, exporter and precision checks. Stop without searching other support cutoffs, cycle lengths, target bases or supplier assembly.", + "outcome": "completed", + "evidence": "SEARCH-RESULT.json records all 1,860,480 candidates and the 109-ADD optimistic ceiling. CANDIDATE.json.gz is the deterministic 12-ADD winner. verify.py checks source pins, the 661-coordinate dirty endpoint, the complete R439 word in both directions, paid profile, exporter and five boundary failure controls.", + "author": "Cinna Davis (@1337isnot1337)", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical scoping, derivation, search implementation, exact checking and package writing. No independent human review is claimed.", + "assignment": { + "seed": "9f01e96180d88ff08d00037f7d9b9abc", + "track": "bit-mechanisms", + "scope_key": "3475f46c8358c6a9211b/five-helper-cycle/r439-dirty-boundary", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1695", + "claim_expires_utc": "2026-10-14T09:20:00Z", + "selected_record_kappa": "836330098538459/500000000000000000", + "selected_record_binding": "complex" + }, + "open_questions": [ + { + "question": "Can a six-helper cyclic basis change lower the same R439 injection cost beyond the five-helper result?", + "why_it_matters": "A longer cycle could expose multi-column cancellations that a single five-cycle cannot realize.", + "first_step": "Compute the exact six-column rank lower bound and full six-edge preparation/restoration charge on a seed-selected overlap-ranked support family before enumerating cyclic words.", + "blocked_by": "A positive fully charged ceiling and a bounded support family whose exact endpoint and precision can be replayed." + } + ] +} diff --git a/research/r439-five-cycle-seed9f01/VERIFY.json b/research/r439-five-cycle-seed9f01/VERIFY.json new file mode 100644 index 0000000000..a52063c7fe --- /dev/null +++ b/research/r439-five-cycle-seed9f01/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/r439-bsection-stars-seed01/CERTIFICATE.json", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-bsection-stars-seed01/SOURCES.json", + "research/r439-bsection-stars-seed01/build.py", + "research/r439-bsection-stars-seed01/candidate.json.gz", + "research/r439-bsection-stars-seed01/candidate_search.json", + "research/r439-bsection-stars-seed01/inputs/PR1015-CANDIDATE.json", + "research/r439-bsection-stars-seed01/verify.py", + "research/r439-frame520/RECEIPT.json", + "research/r439-frame520/candidate.json", + "research/r439-helper-stars-seed19/CERTIFICATE.json", + "research/r439-helper-stars-seed19/build.py", + "research/r439-helper-stars-seed19/candidate.json.gz", + "research/r439-helper-stars-seed19/common.py", + "research/r439-target-compensation/candidate.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Replays all 1,860,480 cyclic candidates; verifies the exact dirty D map, full 661-column word, paid profile, exporter invoice, precision guards and five negative controls." + } + ] +} diff --git a/research/r439-five-cycle-seed9f01/search.py b/research/r439-five-cycle-seed9f01/search.py new file mode 100644 index 0000000000..7af80a778b --- /dev/null +++ b/research/r439-five-cycle-seed9f01/search.py @@ -0,0 +1,231 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exhaust the declared five-helper cyclic-sweep domain on the pinned R439 word.""" +import gzip +import hashlib +import itertools +import json +import gzip +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE_WORD = ROOT / "research/r439-bsection-stars-seed01/candidate.json.gz" +TOP = 20 +WIDTH = 5 + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def load_word(path=BASE_WORD): + return json.loads(gzip.decompress(path.read_bytes())) + + +def split_d(word): + """Identify helper prep, target prep, injection, target restore, helper restore.""" + v, base = word["v"], 2 * word["v"] + parts = {"helper_prep": [], "target_prep": [], "injection": [], + "target_restore": [], "helper_restore": []} + stage = "helper_prep" + for gate in word["D"]: + frame, dest, srcs = gate + if frame != 0: + raise ValueError("D gate left frame zero") + dest_target = v <= dest < 2 * v + dest_helper = dest >= base + src_targets = bool(srcs) and all(v <= s < 2 * v for s in srcs) + src_helpers = bool(srcs) and all(s >= base for s in srcs) + if stage == "helper_prep" and dest_target: + stage = "target_prep" + if stage == "target_prep" and dest_target and src_helpers: + stage = "injection" + if stage == "injection" and dest_target and src_targets: + stage = "target_restore" + if stage == "target_restore" and dest_helper: + stage = "helper_restore" + if stage == "helper_prep": + if not (dest_helper and src_helpers and len(srcs) == 1): + raise ValueError("malformed helper preparation") + parts[stage].append(gate) + elif stage in ("target_prep", "target_restore"): + if not (dest_target and src_targets and len(srcs) == 1): + raise ValueError("malformed target basis change") + parts[stage].append(gate) + elif stage == "injection": + if not (dest_target and src_helpers): + raise ValueError("malformed D injection") + parts[stage].append(gate) + else: + if not (dest_helper and src_helpers and len(srcs) == 1): + raise ValueError("malformed helper restoration") + parts[stage].append(gate) + expected = {"helper_prep": 236, "target_prep": 306, "injection": 111, + "target_restore": 306, "helper_restore": 236} + if {k: len(vv) for k, vv in parts.items()} != expected: + raise ValueError("unexpected D block lengths") + return parts + + +def injection_columns(word, injection): + v, R, base = word["v"], word["R"], 2 * word["v"] + columns = [0] * R + seen_targets = set() + for _, dest, srcs in injection: + row = dest - v + if row in seen_targets or not 0 <= row < v: + raise ValueError("duplicate or invalid injection target") + seen_targets.add(row) + if len(set(srcs)) != len(srcs): + raise ValueError("duplicate injection source") + for src in srcs: + columns[src - base] |= 1 << row + if seen_targets != set(range(v)): + raise ValueError("injection does not cover all target rows") + return columns + + +def ranking(columns): + scores = [sum((columns[i] & columns[j]).bit_count() + for j in range(len(columns)) if j != i) + for i in range(len(columns))] + return sorted(range(len(columns)), + key=lambda i: (-scores[i], -columns[i].bit_count(), i)) + + +def rank_bits(vectors): + pivots = {} + for x in vectors: + while x: + bit = x.bit_length() - 1 + if bit in pivots: + x ^= pivots[bit] + else: + pivots[bit] = x + break + return len(pivots) + + +def apply_cycle(columns, permutation): + """Return J H^{-1}; H is the chronological five-edge helper sweep.""" + out = columns.copy() + edges = [(permutation[k], permutation[(k + 1) % WIDTH]) + for k in range(WIDTH)] + # A prep edge h_dest ^= h_src left-multiplies H by T. Right multiplication + # of J by H^{-1} updates its source column by its destination column. + for dest, src in edges: + out[src] ^= out[dest] + return out, edges + + +def optimistic_ceiling(columns, top): + best = None + for support in itertools.combinations(top, WIDTH): + old = sum(columns[i].bit_count() for i in support) + rank = rank_bits([columns[i] for i in support]) + # Any invertible basis has at least rank(J|support) nonzero output columns. + # Pay ten ADDs for the five-edge preparation and inverse restoration. + ceiling = old - rank - 2 * WIDTH + item = (ceiling, support, old, rank) + if best is None or item > best: + best = item + return best + + +def search(): + word = load_word() + parts = split_d(word) + columns = injection_columns(word, parts["injection"]) + total = sum(col.bit_count() for col in columns) + top = ranking(columns)[:TOP] + ceiling = optimistic_ceiling(columns, top) + + best_key = None + best = [] + candidates = 0 + positive = 0 + for support in itertools.combinations(top, WIDTH): + support_weight = sum(columns[i].bit_count() for i in support) + for permutation in itertools.permutations(support): + candidates += 1 + changed, edges = apply_cycle(columns, permutation) + new_weight = total - support_weight + sum(changed[i].bit_count() for i in support) + saving = total - new_weight - 2 * WIDTH + if saving <= 0: + continue + positive += 1 + # Retain the best 64 by exact completed D ADD saving, then stable IDs. + key = (-saving, tuple(sorted(support)), permutation) + if best_key is None or key < best_key: + best_key = key + item = {"saving": saving, "support": list(sorted(support)), + "permutation": list(permutation), "edges": [list(e) for e in edges], + "old_support_weight": support_weight, + "new_support_weight": sum(changed[i].bit_count() for i in support), + "injection_weight": new_weight} + best.append((key, item)) + if len(best) > 64: + best.sort(key=lambda x: x[0]) + best.pop() + best.sort(key=lambda x: x[0]) + return word, parts, columns, { + "top_helpers": top, + "top_scores": [sum((columns[i] & columns[j]).bit_count() + for j in range(len(columns)) if j != i) for i in top], + "supports": 15504, + "sweeps_per_support": 120, + "candidates": candidates, + "positive_saving_candidates": positive, + "base_injection_adds": total, + "optimistic_max_net_ADD_saving": { + "net": ceiling[0], "support": list(ceiling[1]), + "old_weight": ceiling[2], "rank": ceiling[3], + "preparation_and_restoration_ADDs": 10}, + "best_64": [x[1] for x in best], + "stopping_rule": "complete all 15,504 five-subsets of the top 20 helpers and all 120 directed cyclic sweeps per subset", + } + + +def candidate_for(word, parts, columns, item): + out = json.loads(json.dumps(word)) + v, base = out["v"], 2 * out["v"] + permutation = item["permutation"] + changed, edges = apply_cycle(columns, permutation) + prep = [[0, base + dest, [base + src]] for dest, src in edges] + restore = [[0, base + dest, [base + src]] for dest, src in reversed(edges)] + target_order = [gate[1] for gate in parts["injection"]] + injection = [] + for dest in target_order: + srcs = [base + i for i, col in enumerate(changed) if (col >> (dest - v)) & 1] + injection.append([0, dest, srcs]) + out["D"] = (parts["helper_prep"] + prep + parts["target_prep"] + injection + + parts["target_restore"] + restore + parts["helper_restore"]) + return out + + +def main(): + word, parts, columns, result = search() + best = result["best_64"] + if best: + candidate = candidate_for(word, parts, columns, best[0]) + payload = canonical(candidate) + (HERE / "CANDIDATE.json.gz").write_bytes(gzip.compress(payload, mtime=0)) + result["candidate_sha256"] = hashlib.sha256(payload).hexdigest() + result["candidate_gzip_sha256"] = hashlib.sha256((HERE / "CANDIDATE.json.gz").read_bytes()).hexdigest() + result["selected_candidate"] = best[0] + else: + result["candidate_sha256"] = None + result["candidate_gzip_sha256"] = None + result["selected_candidate"] = None + (HERE / "CANDIDATE.json.gz").unlink(missing_ok=True) + (HERE / "SEARCH-RESULT.json").write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print("PASS_R439_FIVE_CYCLE_SEARCH candidates=%d positive=%d best_ADD_saving=%d ceiling=%d" % ( + result["candidates"], result["positive_saving_candidates"], + best[0]["saving"] if best else 0, + result["optimistic_max_net_ADD_saving"]["net"])) + + +if __name__ == "__main__": + main() diff --git a/research/r439-five-cycle-seed9f01/verify.py b/research/r439-five-cycle-seed9f01/verify.py new file mode 100644 index 0000000000..0c907fb332 --- /dev/null +++ b/research/r439-five-cycle-seed9f01/verify.py @@ -0,0 +1,193 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Replay the exact five-helper cyclic search, endpoint and priced word.""" +import gzip +import hashlib +import json +import argparse +import runpy +import subprocess +import tempfile +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "research/r439-bsection-stars-seed01/" +BASE_WORD = ROOT / (BASE + "candidate.json.gz") +BASE_PACKAGE_VERIFY = ROOT / (BASE + "verify.py") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def verify_source_rows(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + base = manifest["base_commit"] + for row in manifest["files"]: + path = row["path"] + pinned = subprocess.check_output(["git", "show", base + ":" + path], cwd=ROOT) + blob = subprocess.check_output(["git", "rev-parse", base + ":" + path], cwd=ROOT).decode().strip() + need(blob == row["git_blob"], "source Git blob changed: " + path) + need(hashlib.sha256(pinned).hexdigest() == row["sha256"], "source provenance digest changed: " + path) + if row["usage"] == "input": + live = (ROOT / path).read_bytes() + need(live == pinned, "live input differs from pinned base: " + path) + old = runpy.run_path(str(BASE_PACKAGE_VERIFY)) + builder = old["Bd"] + builder["pins"](ROOT) + return manifest, old + + +def d_boundary(old, word): + return old["d_rows"](word) + + +def require_bad_control(label, candidate, old_rows, old): + need(d_boundary(old, candidate) != old_rows, "negative control accepted: " + label) + + +def controls(base_word, candidate, parts, old): + expected = d_boundary(old, base_word) + n0 = len(parts["helper_prep"]) + n1 = len(parts["target_prep"]) + n2 = len(parts["injection"]) + n3 = len(parts["target_restore"]) + prep_start = n0 + injection_start = n0 + 5 + n1 + restore_start = injection_start + n2 + n3 + report = [] + + bad = json.loads(json.dumps(candidate)) + del bad["D"][prep_start] + require_bad_control("missing helper preparation edge", bad, expected, old) + report.append("missing helper preparation edge rejected by D boundary") + + bad = json.loads(json.dumps(candidate)) + del bad["D"][restore_start] + require_bad_control("missing inverse restoration edge", bad, expected, old) + report.append("missing inverse restoration edge rejected by D boundary") + + bad = json.loads(json.dumps(candidate)) + bad["D"][injection_start:injection_start + n2] = parts["injection"] + require_bad_control("stale injection J0", bad, expected, old) + report.append("stale injection rejected by D boundary") + + bad = json.loads(json.dumps(candidate)) + edges = candidate["D"][prep_start:prep_start + 5] + bad["D"][restore_start:restore_start + 5] = edges + require_bad_control("wrong inverse order", bad, expected, old) + report.append("wrong inverse order rejected by D boundary") + + bad = json.loads(json.dumps(candidate)) + gate = bad["D"][injection_start] + source = gate[2][0] + if source in gate[2]: + gate[2].remove(source) + else: + gate[2].append(source) + require_bad_control("mutated injection coefficient", bad, expected, old) + report.append("mutated injection coefficient rejected by D boundary") + return report + + +def verify(write_certificate=False): + manifest, old = verify_source_rows() + search = runpy.run_path(str(HERE / "search.py")) + base_word = search["load_word"]() + parts = search["split_d"](base_word) + columns = search["injection_columns"](base_word, parts["injection"]) + word, got_parts, got_columns, replay = search["search"]() + need(canonical(word) == canonical(base_word), "search loaded a different source word") + need(got_parts == parts and got_columns == columns, "D source decomposition changed") + + candidate_path = HERE / "CANDIDATE.json.gz" + candidate_bytes = candidate_path.read_bytes() + candidate = json.loads(gzip.decompress(candidate_bytes)) + selected = replay["best_64"][0] + expected_candidate = search["candidate_for"](base_word, parts, columns, selected) + need(canonical(candidate) == canonical(expected_candidate), "candidate is not the exact search winner") + need(selected["saving"] == 12 and selected["injection_weight"] == 4442, + "selected five-cycle cost changed") + + expected_search = dict(replay) + expected_search["candidate_sha256"] = hashlib.sha256(canonical(candidate)).hexdigest() + expected_search["candidate_gzip_sha256"] = hashlib.sha256(candidate_bytes).hexdigest() + expected_search["selected_candidate"] = selected + stored_search = json.loads((HERE / "SEARCH-RESULT.json").read_text()) + need(stored_search == expected_search, "bounded search receipt differs") + need(replay["candidates"] == 1_860_480 and replay["positive_saving_candidates"] == 56, + "bounded search coverage changed") + need(replay["optimistic_max_net_ADD_saving"]["net"] == 109, + "optimistic fully charged ceiling changed") + + need(d_boundary(old, candidate) == d_boundary(old, base_word), "D arbitrary-input endpoint changed") + controls_found = controls(base_word, candidate, parts, old) + + original = old["load"](old["ROOT"] / old["WORD"]) + helper_star = old["load"](old["ROOT"] / "research/r439-helper-stars-seed19/candidate.json.gz") + reference_owner_all = old["owner"](helper_star) + reference_owner = {k: reference_owner_all[k] for k in ("hypotheses", "conclusions")} + with tempfile.TemporaryDirectory(prefix="r439-five-cycle-") as temp: + checks = old["word_checks"]("five_cycle", candidate, original, reference_owner, Path(temp)) + + baseline_owner = old["owner"](base_word) + candidate_owner = old["owner"](candidate) + need(candidate_owner["profile"] == baseline_owner["profile"], "paid profile changed") + need(sum(r * c for r, c in candidate_owner["profile"].items()) == 5129, + "paid rank mass changed") + need(checks["literal"]["D_adds"] == 5536, "complete D ADD invoice changed") + need(checks["literal"]["native_ADDs"] == 11488, "complete word ADD invoice changed") + need(checks["literal"]["F"] == 27061 and checks["literal"]["B"] == 5921344, + "F/B evidence changed") + need(checks["literal"]["local_bits"] <= 104 and checks["literal"]["nine_stage_bits"] <= 192, + "precision guard failed") + local_bound = 64 * checks["literal"]["F"]**3 * checks["literal"]["B"]**2 + nine_stage_bound = (1 << 18) * checks["literal"]["F"]**5 * checks["literal"]["B"]**4 + need(local_bound < (1 << 104) and nine_stage_bound < (1 << 192), + "exact precision inequality failed") + + report = { + "status": "PASS_R439_FIVE_CYCLE", + "base_commit": manifest["base_commit"], + "selected_record_sha256": manifest["selected_record_sha256"], + "search": { + "supports": replay["supports"], "sweeps_per_support": replay["sweeps_per_support"], + "candidates": replay["candidates"], "positive_saving_candidates": replay["positive_saving_candidates"], + "optimistic_max_net_ADD_saving": replay["optimistic_max_net_ADD_saving"]["net"], + "selected": selected, + }, + "word": checks, + "exact_precision": { + "local": {"lhs": str(local_bound), "rhs": str(1 << 104)}, + "nine_stage": {"lhs": str(nine_stage_bound), "rhs": str(1 << 192)}, + }, + "paid_profile": candidate_owner["profile"], + "paid_rank_mass": 5129, + "controls": controls_found, + "new_kappa": False, + "unrun": ["native C++ replay", "supplier adoption", "outer assembly replay", "all-size/compiler and analytic proof obligations"], + } + # JSON object keys (including paid-profile ranks) are strings in the receipt. + report = json.loads(json.dumps(report)) + certificate_path = HERE / "CERTIFICATE.json" + if write_certificate: + certificate_path.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n") + else: + stored = json.loads(certificate_path.read_text()) + need(stored == report, "certificate differs from replay") + print(json.dumps(report, sort_keys=True)) + print("PASS_R439_FIVE_CYCLE candidates=1860480 best_saving=12 ADDs=11500->11488 columns=661 controls=5 no_new_kappa") + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-certificate", action="store_true") + args = parser.parse_args() + verify(write_certificate=args.write_certificate)