diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 6bd374e1ca..c846c8cdaa 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -16,7 +16,7 @@ jobs: fail-fast: false matrix: python-version: ['3.11', '3.13', '3.14'] - group: [community, producers, certificates, ternary, research, tests, strips, clones, positive, joint, pair] + group: [community, producers, certificates, ternary, research, tests, strips, clones, positive, joint, pair, rank-pair, reordered-rank-pair] steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 with: diff --git a/Makefile b/Makefile index 84fe8290f3..ad62295443 100644 --- a/Makefile +++ b/Makefile @@ -24,6 +24,8 @@ verify: $(MAKE) verify-joint $(MAKE) verify-pair $(MAKE) verify-tests + $(MAKE) verify-rank-pair + $(MAKE) verify-reordered-rank-pair verify-community: community-audit-check community-followup-check copied-reversed-producer copied-reversed-check copied-fixed-reversed-producer copied-fixed-reversed-check $(MAKE) copied-fixed-verify @@ -425,6 +427,23 @@ pair-assembly-check: pair-assembly-verify: pair-assembly-producer pair-assembly-check +.PHONY: verify-skip-strips verify-pair-assembly verify-rank-pair rank-pair-verify +verify-skip-strips: skip-strips-verify +verify-pair-assembly: pair-assembly-verify +verify-rank-pair: rank-pair-verify +rank-pair-verify: + python3 research/rank-pair/frame_compile.py + python3 research/rank-pair/screen.py + python3 -m unittest discover -s tests -p 'test_rank_pair.py' -v + +.PHONY: verify-reordered-rank-pair reordered-rank-pair-verify +verify-reordered-rank-pair: reordered-rank-pair-verify +reordered-rank-pair-verify: + python3 research/reordered-rank-pair/verify.py --rebuild + python3 research/reordered-rank-pair/test_negative.py + python3 research/reordered-rank-pair/arithmetic/refine.py + python3 research/reordered-rank-pair/arithmetic/audit.py + python3 -m unittest discover -s research/reordered-rank-pair/arithmetic -p 'test_arithmetic.py' -v .PHONY: verify-pair verify-pair: pair-assembly-verify python3 scripts/audit_pair_candidate.py --check docs/research/community-pair-arithmetic.json diff --git a/NOTICE b/NOTICE index b565637758..cfe333faf8 100644 --- a/NOTICE +++ b/NOTICE @@ -204,6 +204,19 @@ frame/movement/guard lemmas and independent paired-circuit checks (#26). Origina source notices and historical snapshots are preserved. Neither formal package claims a full formal proof of the multiplication algorithm or a new kappa. +Skip-prefix strip producer, 8 October 2026 +By Avi Eisenberg (ikeboy), with Anthropic Claude (Claude Opus 5.5) +assistance. The skip-prefix leave-one-out strip layout in +research/skip-strips/skip_graph.py is new. Everything else reuses Chafik +Boukhalfa's PR #43/#46/#48 research/copied-fixed pipeline, its verification +code, exact data recovery and support-order sorting, together with: +- Rohan Arun's PR #44 weighted carrier matching optimizer; +- RaD (hipotures) PR #41 alternating point order; +- every predecessor credited above. +Complete attribution and the conditional proof boundary are recorded in +research/skip-strips/PROOF.md. Original Apache-2.0 and CC0 notices remain +applicable. + Joint frame compilation of skip-prefix strips The local compiler and exact finite witnesses were prepared by eumemic with @@ -302,3 +315,14 @@ inherited PR #48 sources. The stacked witness in research/pair-assembly/frame uses eumemic's PR #57 joint frame compiler unchanged; its driver and verifier are adaptations of PR #57's skip_frame_compiler.py, skip_frame_compose.py and verify_skip_frame.py. Original notices are retained. + +Rank-first reclamation on interval-strip pair assembly, 8 October 2026 +Composition and exact profile witness: Dominik Scholz, with substantial OpenAI +GPT-6 Astra / Codex assistance. The PR #60 descending-frame-rank compiler by +Chafik Boukhalfa is reused unchanged on Avi Eisenberg's PR #62 scalar graph. +The joint frame compiler and paid reclamation are eumemic's PR #57, developed +with OpenAI Codex assistance. PR #62 records Anthropic Claude assistance. +This composition improves actual fixed-basis block profiles with unchanged +role counts; no new slot-priority rule or scalar graph is claimed. All prior +contributors, licenses, compiler arguments and conditional analytic/tape +interfaces remain credited. See research/rank-pair/PROOF.md. diff --git a/README.md b/README.md index 035c259b68..016491e638 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,34 @@ +# Reordered rank-first regions: conditional saving 5.1028985071975e-5 + +This branch proposes **κ = 2041159402879/(4×10^16) = 5.1028985071975×10^-5**, +about **0.00277% above [PR #63](https://github.com/CrocSwap/integer-mult-bounds/pull/63)**. +The bit saving is **5103158916233/10^17**. Within each frame rank, use +cover/core order at h=23 and decreasing minimum-node order at h=25. The scalar graph, rank-first +retired-slot policy, role counts and paid endpoints remain inherited from #63; +the changed schedule changes the physical frame transitions and their complete +fixed-basis child profile. W remains **137,151,806**. + +[Construction, proof and credits](research/reordered-rank-pair/README.md) · +[Exact arithmetic certificate](research/reordered-rank-pair/arithmetic/certificate.json) + +Run `make reordered-rank-pair-verify` to rebuild both physical words and profiles, +then check the exact moment and inherited assembly. `make verify` includes this +new target and all inherited verification groups. Full repository validation +passed on research commit `49e84f9`: 467 core tests, all 20 historical patch +checks, and complete physical/profile and exact arithmetic checks. The +[receipt](research/reordered-rank-pair/validation.json) distinguishes that run +from subsequent upstream integration, which leaves the witness unchanged. + +This is a finite conditional witness under the inherited analytic, all-size +compiler and fixed finite-alphabet multitape hypotheses. It is not a proof +of global optimality or a measured practical speedup. The schedule gain and +the finer arithmetic-grid gain are distinguished in the research note. + +Prepared by Rohan Arun with OpenAI Codex assistance. Credit Dominik Scholz +(#63), Avi Eisenberg (#62), Chafik Boukhalfa (#60), eumemic (#57), and the +Alejandro Zarzuelo Urdiales (#61, parameter-refinement precedent), together with all inherited contributors. +The reviewed main-branch result below remains separately identified. + # A sharper exponent for integer multiplication **Community research maintained by Douglas Colkitt — conditional on the original diff --git a/certificates/joint-dual-kappa.json b/certificates/joint-dual-kappa.json index d92f653fe4..67fdde0fce 100644 --- a/certificates/joint-dual-kappa.json +++ b/certificates/joint-dual-kappa.json @@ -842,7 +842,7 @@ "scripts/experiments/pin_joint_dual_sources.py": "4d31cc0e38b7902709ca5f8f714cba109760d2592346dd7f8dc0b900a2d9fe00", "scripts/experiments/verify_joint_dual.py": "7a31bba1e9c0ded32ae285df2ca9bc91ef20c330f6789fdba361876f3c7a1985" }, - "source_manifest_sha256": "fd1aab7d75753b4b55b2377f26119dae74f367b0b4fab66cba42d944b3042cc9", + "source_manifest_sha256": "b497d3127bd62ea97e2e022b4239ad9d4fbcc374c9b0b8b9d26a18195a2c6e7d", "sources": [ { "files": { diff --git a/certificates/joint-dual-validation.json b/certificates/joint-dual-validation.json index 99adb4cf74..2d13e4f513 100644 --- a/certificates/joint-dual-validation.json +++ b/certificates/joint-dual-validation.json @@ -226,7 +226,7 @@ } }, "bit_saving": "2382370177/50000000000000", - "certificate_sha256": "2ed658f05365b28825e24a6e7bac9fc9cc015d5a5d63d9579f4ac6e0640ae559", + "certificate_sha256": "aa44cb8cc3b071445f49d05e2e2c6c715fdca85294d01a71cd9eaed7bf569f44", "kappa": "4764513337/100000000000000", "margins": 7, "producer_words_regenerated_and_matched": true, diff --git a/research/joint-dual/SOURCE.json b/research/joint-dual/SOURCE.json index 80c0f29dc4..707187ca0f 100644 --- a/research/joint-dual/SOURCE.json +++ b/research/joint-dual/SOURCE.json @@ -3,9 +3,9 @@ "base_pr57_commit": "cd350f76c9bc01489ec83568bded532cb69be938", "base_pr58_commit": "bc2f7ed4c20dc18898305ab17165c0c995cbb804", "files": { - "Makefile": "97620e0205736d9c0fce736e8ac6ab67f8ed0e490c381f6cac152cc6a003dca7", - "NOTICE": "1c53970fb4face631a1b331ec66d33111eccd280a129f9b64c2da6df96861c3f", - "README.md": "fd92de31aece76b1f5ff897e6e0dbc38dd3bf67c140579bbcb03a1a11a792668", + "Makefile": "caae1250a07ceb5f91c1a20379854bdd5309792363e9635fa54318c663008a4d", + "NOTICE": "ca6db061015c85b57ce5d2a16667a4948010e655e70a1bf2e66e519d9180c343", + "README.md": "fc202819e373483c015b21e2e204317434ad697f04b09a1cc621f82a4d2d746c", "certificates/joint-dual-compiler.json": "516c4d85158553dabd0a98216a064b2a7397957a9d5dd0df1d6e5aec53a4e805", "certificates/joint-dual-profiles-23.json": "159fa8fee175fc1d24f63e72d3c2f1dc9f4fcd78b938c5e7d2f735fd0fd37209", "certificates/joint-dual-profiles-25.json": "8d190ce42d097e828c5756918c52f2963df576cf4c6600b0fc7f2b7fdb6ad223", diff --git a/research/rank-pair/.gitignore b/research/rank-pair/.gitignore new file mode 100644 index 0000000000..b32ee5c816 --- /dev/null +++ b/research/rank-pair/.gitignore @@ -0,0 +1,4 @@ +profiles +*.bin +*.bin.json +*.bin.profiles.json diff --git a/research/rank-pair/PROOF.md b/research/rank-pair/PROOF.md new file mode 100644 index 0000000000..ba95aa98bf --- /dev/null +++ b/research/rank-pair/PROOF.md @@ -0,0 +1,137 @@ +# Rank-first reclamation on interval strips and pair assembly + +This finite conditional witness gives + +\[ +\kappa=\frac{5102757}{10^{11}}=0.00005102757, +\qquad a_b=\frac{5103018}{10^{11}}. +\] + +It composes Avi Eisenberg's PR #62 interval-strip and core-aware pair graph +(`ad0f25ff7b23cff7f08ad237c2254e6ecf74257e`) with Chafik Boukhalfa's PR #60 +rank-first reclamation compiler (`e7a492dd8bee4e6f574ced784a62af2ce735edc4`), +which derives from eumemic's PR #57 joint frame compiler. The graph is +unchanged, and the candidate compiler is copied byte-for-byte from PR #60. +The composition experiment and exact validation driver were prepared by +Dominik Scholz with substantial OpenAI GPT-6 Astra assistance. + +The witness exceeds PR #62's stacked κ by exactly 1066/10^11. It exceeds +PR #61 at `afb7cb67d1858641315cfbf4ac768ee64a8eff3a`, whose stated κ is +25508460085039/500000000000000000, by exactly +5324914961/500000000000000000 (approximately 0.0208751% relative). +These comparisons are against pinned research claims, not independent +acceptance of any of the full multiplication theorems. + +## Mechanism and paid quantities + +PR #57 originally visits retired physical roles in increasing slot order. +PR #60 visits them by descending current frame rank, breaking ties by slot +order. In either policy a retired role is eligible only if its current frame +is contained in the requested frame. Linear dependence is witnessed by +literal XOR operations involving eligible retired roles and the current +anchors; those XORs clear the selected role. Every operand is raised to the +requested frame and every resulting transition is charged. Only then is the +cleared role reused. + +For the PR #62 graph, this changes the physical frame paths and their actual +fixed-basis profiles without changing the roles or the total rank. The +improvement is therefore established by the complete child moment, not by a +role-count heuristic or by treating clearing as free. + +| h | roles | reclaimed roles | clearing XORs | all elementary XORs | distinct profile matrices | CRT-checked matrices | +|---|---:|---:|---:|---:|---:|---:| +| 23 | 27918 | 801 | 1612 | 149172 | 36378 | 6049 | +| 25 | 36586 | 1090 | 2092 | 205915 | 50419 | 8127 | + +Both axes have zero CRT disagreements. PR #62's original clearing counts +were 1398 and 1827, respectively: the present witness explicitly pays the +additional clearing. The unchanged global quantities are m=575, +N=4073300, L=2226400, W=137151806, total rank=78860441550, and deficit=1846900. + +## Finite validation and inherited hypotheses + +`frame_compile.py` checks every input and dirty basis vector in both +orientations, then calls the independent serialized-word replay. `screen.py` +repeats that replay, reconstructs every transition from the actual word, +regenerates all fixed-basis profiles with the inherited bounded-minor and CRT +checks, and applies PR #62's unchanged complete paid-profile constructor. +The constructor verifies the total-rank identity and copied-center counts. + +Exact rational logarithm/exponential enclosures show the moment is below 1 +at a_b=5103018/10^11 and its lower bound is above 1 at 5103019/10^11. +PR #62's original complete child network also has lower moment above 1 at +the new a_b. The inherited balanced assembly passes all 47 strict constraints +and all seven margins at κ=5102757/10^11, and rejects the next grid point. +It uses the unchanged β=1/20, backoff h=10^-12, complex saving 717/10^7, +semantic C1=1, and product row stock p^2000. Smaller rational grids and +backoff were not needed for this witness and could refine its last digits. + +The graph supports, scalar producer, original-envelope interpretation, data +geometry, paid endpoint copy, exact corner recovery, and all-size proofs +remain inherited from PR #62 and its cited predecessors. The rank-first +compiler uses precisely PR #60's mechanism. This note does not independently +prove OpenAI's base theorem, the fixed-alphabet/multitape transfer, the +analytic, semantic, routing or recovery interfaces, or their eventual +thresholds. Finite success is not formal verification of the full theorem, +and neither global optimality nor a practical speedup is claimed. + +## Reproduction + +```sh +python3 research/rank-pair/frame_compile.py +python3 research/rank-pair/screen.py +python3 -m unittest discover -s tests -p test_rank_pair.py -v +``` + +On this development machine the default MacOSX27 SDK fails to link because +the selected linker does not recognize its arm64e.x1 TBD architecture. The +successful local process-scoped override was: + +```sh +CXX='c++ -isysroot /Library/Developer/CommandLineTools/SDKs/MacOSX15.2.sdk' python3 research/rank-pair/screen.py +``` + +The candidate compiler SHA256 is +`9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd`. +The graph SHA256 is +`3d47e89d2649c90800a276bdd0480131def50e0bdf92c122a19494b55bf17420`. +`frame-compiler.json` pins both sources and every serialized word; wall-clock +timing is excluded so recompilation reproduces the record deterministically. +`screen-certificate.json` records the exact moment, assembly, eventual +arithmetic cutoffs, complete child multiplicities, and pinned comparisons. +Six failure controls check omitted literal XORs, understated physical width, +omitted paid transitions, non-nested frames, exclusion of the old network, +and refusal to disable assertions with optimized Python. The independent experimental reproduction and a fresh parent reproduction +on the integrated main-based branch passed, including all six failure +controls. Repository-wide validation and PR review remain pending in CI. + +Integration preserves main d55bcd62 and its existing verification groups. +The imported pair/skip source manifests were updated for main's six added +standard-library includes in `binary_io.hpp`; its functions and binary format +are unchanged. Their arithmetic certificates were regenerated. The imported +stacked certificate's source paths use POSIX separators for Linux CI. +The new candidate and both imported producers have separate CI groups. + +## Bounded unsuccessful experiments + +At h=23, three further policies were tested: descending rank with decreasing +slot tie-break; decreasing slot without rank; and increasing rank with +increasing slot tie-break. All retained the same 27918 roles. Full independent +dirty-word replay, frame reconstruction and profile regeneration passed for +each, but disjoint exact enclosures prove each has a strictly worse internal +moment than the selected rank-first policy at a_b=5103018/10^11. No claim is +made about those policies at h=25, which was not tested in this bounded round. +The negative-result records and exploratory compiler variants remain local +research scratch; they are not used to generate this witness. + +## Attribution + +Retain PR #62's full attribution in `research/pair-assembly/PROOF.md`, PR #60's +Chafik Boukhalfa rank-first contribution, and PR #57's eumemic compiler. +The pipeline additionally depends on Avi Eisenberg, Rohan Arun, RaD / +hipotures, icekylinx, Zhihao Chen, Aurel Prosz / Paureel, Swapnil Jain, +James Chang, Douglas Colkitt, OpenAI and Harvey–van der Hoeven, with the +complete inherited notices retained in the repository. The PR #62 graph was +prepared with Claude (Anthropic) assistance; the PR #57/#60 compiler and this +composition use substantial OpenAI assistance. Apache-2.0 applies, subject +to the existing separately retained source notices and terms. diff --git a/research/rank-pair/frame-compiler.json b/research/rank-pair/frame-compiler.json new file mode 100644 index 0000000000..8c422bb9f1 --- /dev/null +++ b/research/rank-pair/frame-compiler.json @@ -0,0 +1,177 @@ +{ + "status": "Joint frame compilation of the pair-assembly graph; complete dirty basis both orientations", + "axes": { + "23": { + "compiled": { + "h": 23, + "mode": { + "matching": true, + "reclaim": true + }, + "roles": 27918, + "baseline_pr48_roles": 36432, + "histogram": { + "1": 42694, + "0": 302093, + "2": 82741, + "3": 11086, + "4": 10683, + "6": 2005, + "5": 7757, + "8": 1362, + "9": 525, + "10": 449, + "12": 464, + "14": 2005, + "16": 547, + "18": 4220, + "19": 7820, + "22": 23, + "15": 544, + "17": 368, + "7": 275, + "21": 165, + "13": 22 + }, + "rank_mass": 642620, + "elementary_xors": 149172, + "stats": { + "augmentations": 220, + "regions": 52473, + "matched": 37025, + "multi_node_regions": 10350, + "reclaimed": 801, + "clearing_xors": 1612 + }, + "dirty_basis_vectors": 31460, + "complete_dirty_basis_both_orientations": true, + "all_physical_frame_inclusions": true + }, + "replay": { + "status": "independent serialized word, exact frames, full input and dirty basis both orientations PASS", + "h": 23, + "roles": 27918, + "output_roles": 5336, + "elementary_xors": 149172, + "word_length": 621482, + "full_basis_vectors": 31460, + "rank_mass": 642620, + "histogram": { + "1": 42694, + "0": 162950, + "2": 82741, + "3": 11086, + "4": 10683, + "6": 2005, + "5": 7757, + "8": 1362, + "9": 525, + "10": 449, + "12": 464, + "14": 2005, + "16": 547, + "18": 4220, + "19": 7820, + "22": 23, + "15": 544, + "17": 368, + "7": 275, + "21": 165, + "13": 22 + } + }, + "gzip_sha256": "1a57c143380a063211653f1f35e7cc9710539523b0b34c90f354a0425c34bd59", + "word_sha256": "640696dd7cd893add9d6e12d0d587956fecf113b2eff8c29547b82e5a6f3c0ad" + }, + "25": { + "compiled": { + "h": 25, + "mode": { + "matching": true, + "reclaim": true + }, + "roles": 36586, + "baseline_pr48_roles": 48329, + "histogram": { + "1": 55478, + "0": 416643, + "2": 115797, + "3": 14362, + "4": 16835, + "5": 10237, + "6": 1767, + "8": 2116, + "9": 642, + "10": 529, + "12": 614, + "14": 529, + "16": 3146, + "18": 519, + "20": 5436, + "21": 10148, + "24": 25, + "17": 854, + "19": 396, + "13": 24, + "7": 525, + "23": 220 + }, + "rank_mass": 915250, + "elementary_xors": 205915, + "stats": { + "augmentations": 286, + "regions": 73695, + "matched": 53194, + "multi_node_regions": 13975, + "reclaimed": 1090, + "clearing_xors": 2092 + }, + "dirty_basis_vectors": 41186, + "complete_dirty_basis_both_orientations": true, + "all_physical_frame_inclusions": true + }, + "replay": { + "status": "independent serialized word, exact frames, full input and dirty basis both orientations PASS", + "h": 25, + "roles": 36586, + "output_roles": 6925, + "elementary_xors": 205915, + "word_length": 855860, + "full_basis_vectors": 41186, + "rank_mass": 915250, + "histogram": { + "1": 55478, + "0": 224367, + "2": 115797, + "3": 14362, + "4": 16835, + "5": 10237, + "6": 1767, + "8": 2116, + "9": 642, + "10": 529, + "12": 614, + "14": 529, + "16": 3146, + "18": 519, + "20": 5436, + "21": 10148, + "24": 25, + "17": 854, + "19": 396, + "13": 24, + "7": 525, + "23": 220 + } + }, + "gzip_sha256": "fff17e3f6742e0810247747c3bbf393eb6b1b2b5a6c9887c83adeecd298d1bfe", + "word_sha256": "7a827318eff45db1183d66e80d38ddbd4ce321bbc033d2effb7afa438d6b63a9" + } + }, + "source": { + "graph": "research/pair-assembly/pair_graph.py", + "graph_sha256": "3d47e89d2649c90800a276bdd0480131def50e0bdf92c122a19494b55bf17420", + "compiler": "scripts/experiments/rank_pair_compiler.py (PR #60 rank-first variant of PR #57)", + "compiler_sha256": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd" + } +} diff --git a/research/rank-pair/frame-profiles-23.json b/research/rank-pair/frame-profiles-23.json new file mode 100644 index 0000000000..1663c97520 --- /dev/null +++ b/research/rank-pair/frame-profiles-23.json @@ -0,0 +1,38 @@ +{ + "h": 23, + "v": 1771, + "R": 27918, + "loss": 506, + "rank_sum": 642620, + "field_prime": 2305843009213693951, + "frames": 52475, + "distinct_matrices": 36378, + "crt_matrices": 6049, + "crt_disagreements": 0, + "blocks": [ + 0, + 343922, + 16866, + 10526, + 5756, + 4155, + 3904, + 3650, + 2861, + 2284, + 1800, + 1716, + 1263, + 1077, + 710, + 590, + 352, + 193, + 114, + 0, + 45, + 23, + 0, + 0 + ] +} diff --git a/research/rank-pair/frame-profiles-25.json b/research/rank-pair/frame-profiles-25.json new file mode 100644 index 0000000000..e9f49b5c4d --- /dev/null +++ b/research/rank-pair/frame-profiles-25.json @@ -0,0 +1,40 @@ +{ + "h": 25, + "v": 2300, + "R": 36586, + "loss": 600, + "rank_sum": 915250, + "field_prime": 2305843009213693951, + "frames": 73697, + "distinct_matrices": 50419, + "crt_matrices": 8127, + "crt_disagreements": 0, + "blocks": [ + 0, + 474727, + 25146, + 12129, + 6776, + 5700, + 5502, + 4919, + 3780, + 3213, + 2699, + 2650, + 1907, + 1665, + 1346, + 1126, + 698, + 585, + 371, + 181, + 111, + 0, + 55, + 25, + 0, + 0 + ] +} diff --git a/research/rank-pair/frame-transitions-23.json b/research/rank-pair/frame-transitions-23.json new file mode 100644 index 0000000000..a186d47c0c --- /dev/null +++ b/research/rank-pair/frame-transitions-23.json @@ -0,0 +1,34 @@ +{ + "h": 23, + "v": 1771, + "R": 27918, + "frames": 52475, + "distinct_transitions": 138003, + "singles": 15939, + "rank_mass": 642620, + "rank_histogram_with_side_growth_split_into_singletons": { + "1": 53320, + "2": 77428, + "3": 11086, + "4": 10683, + "5": 7757, + "6": 2005, + "7": 275, + "8": 1362, + "9": 525, + "10": 449, + "12": 464, + "13": 22, + "14": 2005, + "15": 544, + "16": 547, + "17": 368, + "18": 4220, + "19": 7820, + "21": 165, + "22": 23 + }, + "word_sha256": "640696dd7cd893add9d6e12d0d587956fecf113b2eff8c29547b82e5a6f3c0ad", + "copied_centers": 23, + "transition_events_equal_independent_xor_word_reconstruction": true +} diff --git a/research/rank-pair/frame-transitions-25.json b/research/rank-pair/frame-transitions-25.json new file mode 100644 index 0000000000..9f7afe51b7 --- /dev/null +++ b/research/rank-pair/frame-transitions-25.json @@ -0,0 +1,35 @@ +{ + "h": 25, + "v": 2300, + "R": 36586, + "frames": 73697, + "distinct_transitions": 190879, + "singles": 20700, + "rank_mass": 915250, + "rank_histogram_with_side_growth_split_into_singletons": { + "1": 69278, + "2": 108897, + "3": 14362, + "4": 16835, + "5": 10237, + "6": 1767, + "7": 525, + "8": 2116, + "9": 642, + "10": 529, + "12": 614, + "13": 24, + "14": 529, + "16": 3146, + "17": 854, + "18": 519, + "19": 396, + "20": 5436, + "21": 10148, + "23": 220, + "24": 25 + }, + "word_sha256": "7a827318eff45db1183d66e80d38ddbd4ce321bbc033d2effb7afa438d6b63a9", + "copied_centers": 25, + "transition_events_equal_independent_xor_word_reconstruction": true +} diff --git a/research/rank-pair/frame-word-23.json.gz b/research/rank-pair/frame-word-23.json.gz new file mode 100644 index 0000000000..f1ab2ff5fb Binary files /dev/null and b/research/rank-pair/frame-word-23.json.gz differ diff --git a/research/rank-pair/frame-word-25.json.gz b/research/rank-pair/frame-word-25.json.gz new file mode 100644 index 0000000000..b94aa6aded Binary files /dev/null and b/research/rank-pair/frame-word-25.json.gz differ diff --git a/research/rank-pair/frame_compile.py b/research/rank-pair/frame_compile.py new file mode 100644 index 0000000000..52e79f0a00 --- /dev/null +++ b/research/rank-pair/frame_compile.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +"""Compile PR #62's pair graph with PR #60's rank-first joint compiler. + +PR #60's compiler (by Chafik Boukhalfa, derived from eumemic's PR #57, both +with OpenAI Codex assistance) is used unchanged; only its input graph changes. +The graph source is hash-pinned below. Every word is checked by the compiler on +the complete input and dirty basis in both orientations, and frame_verify.py +replays it independently. Adapted with assistance from Claude (Anthropic). +Rank-first composition experiment: Dominik Scholz with OpenAI GPT-6 Astra assistance. +Compiler copied unchanged from Chafik Boukhalfa PR #60 e7a492dd8bee4e6f574ced784a62af2ce735edc4. +Usage: python frame_compile.py (writes words and frame-compiler.json here) +""" +import sys +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') +sys.dont_write_bytecode = True +import gzip +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +from multiprocessing import Process + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(ROOT/'scripts/experiments')) +GRAPH = HERE.parent/'pair-assembly/pair_graph.py' +GRAPH_SHA256 = '3d47e89d2649c90800a276bdd0480131def50e0bdf92c122a19494b55bf17420' +COMPILER_SHA256 = '9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd' + + +def load_graph(): + assert sha256(GRAPH.read_bytes()).hexdigest() == GRAPH_SHA256, 'pair_graph.py changed' + spec = importlib.util.spec_from_file_location('pinned_pair_graph', GRAPH) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module.graph + + +def compile_axis(h): + assert sha256((ROOT/'scripts/experiments/rank_pair_compiler.py').read_bytes()).hexdigest() == COMPILER_SHA256, 'rank-first compiler changed' + import rank_pair_compiler as compiler + compiler.graph = load_graph() + result, word = compiler.compile_(h, matching=True, reclaim=True, dirty=True) + result.pop('seconds') # Elapsed time is not part of the deterministic witness. + raw = (json.dumps(word, separators=(',', ':'))+'\n').encode() + path = HERE/f'frame-word-{h}.json.gz' + with path.open('wb') as stream: + with gzip.GzipFile(fileobj=stream, mode='wb', mtime=0) as archive: + archive.write(raw) + from binary_frame_replay import replay + receipt = replay(path) + (HERE/f'frame-compiled-{h}.json').write_text(json.dumps(dict( + compiled=result, replay=receipt, gzip_sha256=sha256(path.read_bytes()).hexdigest(), + word_sha256=sha256(raw).hexdigest()), indent=2)+'\n') + print(f"h={h} roles={result['roles']} replay roles={receipt['roles']}", flush=True) + + +if __name__ == '__main__': + jobs = [Process(target=compile_axis, args=(h,)) for h in (23, 25)] + for job in jobs: + job.start() + for job in jobs: + job.join() + assert job.exitcode == 0 + axes = {str(h): json.loads((HERE/f'frame-compiled-{h}.json').read_text()) for h in (23, 25)} + record = dict(status='Joint frame compilation of the pair-assembly graph; complete dirty basis both orientations', + axes=axes, source=dict(graph='research/pair-assembly/pair_graph.py', graph_sha256=GRAPH_SHA256, + compiler='scripts/experiments/rank_pair_compiler.py (PR #60 rank-first variant of PR #57)', + compiler_sha256=sha256((ROOT/'scripts/experiments/rank_pair_compiler.py').read_bytes()).hexdigest())) + (HERE/'frame-compiler.json').write_text(json.dumps(record, indent=2)+'\n') + for h in (23, 25): + (HERE/f'frame-compiled-{h}.json').unlink() + print('PASS compiled and independently replayed both axes', flush=True) diff --git a/research/rank-pair/screen-certificate.json b/research/rank-pair/screen-certificate.json new file mode 100644 index 0000000000..72ed101789 --- /dev/null +++ b/research/rank-pair/screen-certificate.json @@ -0,0 +1,710 @@ +{ + "assembly": { + "absorption_gap": "151344121301697306654639/25001275754499997448491000000000000", + "constraints": { + "K_dominates_log": "1275754506246172736493752551509/25001275754499997448491000000000000", + "K_geometry": "18751275754506247448491/25001275754499997448491000000000000", + "a_below_b": "1033491/50000000000", + "a_positive": "2551509/50000000000", + "alpha_below_one": "49999999999975001275754499997448491/50002551508999994896982000000000000", + "alpha_below_one_fourth": "12498086368225005103017999997448491/50002551508999994896982000000000000", + "alpha_positive": "2551509024993621227500002551509/50002551508999994896982000000000000", + "artificial_boundary": "1400081648288274840530687499992345473/200010206035999979587928000000000000", + "b_below_one_over32": "311783/10000000", + "beta_below_one": "19/20", + "beta_positive": "1/20", + "c_below_one": "24998724245493752551509/25000000000000000000000", + "c_positive": "1275754506247448491/25000000000000000000000", + "cell_above_band": "49999999999924998724245500002551509/100005103017999989793964000000000000", + "compact_leaf": "427120500002551509/25000000000000000000000", + "compact_reservations": "1/4000000000000", + "delta_below_one_eighth": "999999999999/8000000000000", + "delta_positive": "1/8000000000000", + "epsilon_below_one": "1275754524997448491/25001275754499997448491", + "epsilon_positive": "24999999999975000000000/25001275754499997448491", + "g1_above_kappa": "17634539705619730410313/2500127575449999744849100000000000", + "g2_above_kappa": "261/100000000000", + "g3_above_kappa": "151344121301697306654639/25001275754499997448491000000000000", + "g4_above_kappa": "261/100000000000", + "g5_above_kappa": "257151359535415689116517/40002041207199995917585600000000000", + "g6_above_kappa": "1385761900695078435376549/200010206035999979587928000000000000", + "g7_above_kappa": "2499872424562634794856519730410313/2500127575449999744849100000000000", + "gamma_sublinear": "1/2000000000000", + "guard_width": "1275754524997448491/25001275754499997448491", + "lambda_above_internal": "2551509/50000000000000000000000", + "lambda_above_sigma": "1033491000002551509/50000000000000000000000", + "lambda_above_tau": "2551509/50000000000000000000000", + "lambda_prime_above_lambda": "2551509/50000000000000000000000", + "lambda_prime_below_one": "1275754499997448491/25000000000000000000000", + "literal_scalar_guard": "9693793493753822316795466474748", + "phase_boundary": "2041207214994641831100002551509/40002041207199995917585600000000000", + "phase_leaf_above_bit": "854241/50000000000", + "phase_local": "10206036174978312173500002551509/200010206035999979587928000000000000", + "prime_interval_packing": "1275754524997448491/25001275754499997448491", + "q_below_internal": "2551509/25000000000000000000000", + "q_below_leaf": "427120500002551509/25000000000000000000000", + "q_below_reservations": "1/4000000000000", + "q_positive": "1275754499997448491/25000000000000000000000", + "record_suffix": "1275754524997448491/25001275754499997448491", + "row_product_gap": "6548/25", + "short_record_fallback": "1249936209018650911466010198177081/1250063787724999872424550000000000", + "small_field_exposure": "1/1000000000000" + }, + "finite_bridge": { + "bit": { + "W": 137151806, + "halving_degree": 9, + "m": 575, + "maxchild": 529, + "wire_bits": 28 + }, + "complex": { + "W": 537696432, + "halving_degree": 20, + "m": 784, + "maxchild": 756, + "s": 421548223824, + "scalar_group_upper": 4793351472, + "wire_bits": 30 + }, + "rows": { + "coefficient": 852, + "degree": 2000, + "degree_gap": "6548/25", + "suffix_slope": 8000 + }, + "semantic": { + "B": 9696565176891520488614054257040, + "C0": 2358858462850846165593256368932965330169899180021667007021321420800, + "C1": 1, + "E": 9696565176891520488192506033216, + "induction_gap": 533311084729033626873772984137200, + "literal_charge": 2771683137698171397039558468, + "strict_literal_gap": 9693793493753822316795466474748 + } + }, + "margins": { + "g1": "1275754524997448491/25001275754499997448491", + "g2": "2551509/50000000000", + "g3": "1275754499996172736500002551509/25001275754499997448491000000000000", + "g4": "2551509/50000000000", + "g5": "2041207214994641831100002551509/40002041207199995917585600000000000", + "g6": "10206036174978312173500002551509/200010206035999979587928000000000000", + "g7": "24999999999975000000000/25001275754499997448491" + }, + "minimum_margin": "1275754499996172736500002551509/25001275754499997448491000000000000", + "parameters": { + "C0": 2358858462850846165593256368932965330169899180021667007021321420800, + "C1": "1", + "a_bit": "2551509/50000000000", + "a_complex": "717/10000000", + "alpha_squared_power": "2551509024993621227500002551509/50002551508999994896982000000000000", + "beta": "1/20", + "c": "1275754506247448491/25000000000000000000000", + "delta": "1/8000000000000", + "epsilon": "24999999999975000000000/25001275754499997448491", + "h": "1/1000000000000", + "kappa": "5102757/100000000000", + "lambda_": "49997448491000002551509/50000000000000000000000", + "lambda_prime": "24998724245500002551509/25000000000000000000000", + "q": "1275754499997448491/25000000000000000000000", + "sigma": "9999283/10000000", + "tau": "49997448491/50000000000" + }, + "recurrence": { + "internal": "49997448491/50000000000", + "leaf": "199986377/200000000", + "reservations": "24998724245493752551509/25000000000000000000000" + }, + "scoped_limit": "2551509/50002551509" + }, + "bit": { + "L": 2226400, + "N": 4073300, + "W": 137151806, + "axes": [ + { + "R": 27918, + "blocks": [ + 0, + 343922, + 16866, + 10526, + 5756, + 4155, + 3904, + 3650, + 2861, + 2284, + 1800, + 1716, + 1263, + 1077, + 710, + 590, + 352, + 193, + 114, + 0, + 45, + 23, + 0, + 0 + ], + "crt_disagreements": 0, + "crt_matrices": 6049, + "distinct_matrices": 36378, + "field_prime": 2305843009213693951, + "frames": 52475, + "h": 23, + "loss": 506, + "rank_sum": 642620, + "v": 1771 + }, + { + "R": 36586, + "blocks": [ + 0, + 474727, + 25146, + 12129, + 6776, + 5700, + 5502, + 4919, + 3780, + 3213, + 2699, + 2650, + 1907, + 1665, + 1346, + 1126, + 698, + 585, + 371, + 181, + 111, + 0, + 55, + 25, + 0, + 0 + ], + "crt_disagreements": 0, + "crt_matrices": 8127, + "distinct_matrices": 50419, + "field_prime": 2305843009213693951, + "frames": 73697, + "h": 25, + "loss": 600, + "rank_sum": 915250, + "v": 2300 + } + ], + "child_multiplicities": { + "1": 1725448017, + "10": 8919929, + "11": 8639950, + "12": 6282197, + "13": 5425815, + "14": 4016766, + "15": 3351146, + "16": 2045758, + "17": 9626535, + "18": 919241, + "19": 320551, + "2": 83325366, + "20": 300081, + "21": 16346100, + "22": 97405, + "23": 72402275, + "25": 64793806, + "3": 45690259, + "4": 25239096, + "481": 8146600, + "5": 19651200, + "525": 64793806, + "529": 64211400, + "6": 18723242, + "7": 17106549, + "8": 13274680, + "9": 10943423 + }, + "deficit": 1846900, + "excluded_above_lower": "8131530000007428916344426560363425376545435885706917766436209786193813885001996064633204627770717193381579821657410997368932854661/8131530000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "m": 575, + "maxchild": 529, + "moment": { + "exponent": "49997448491/50000000000", + "logarithms": { + "1": { + "lower": "3177185020398675220004135749131/500000000000000000000000000000", + "upper": "6354370040797350440008271498263/1000000000000000000000000000000" + }, + "10": { + "lower": "2025892473901652377995140021789/500000000000000000000000000000", + "upper": "4051784947803304755990280043579/1000000000000000000000000000000" + }, + "11": { + "lower": "3956474767998979895946327920297/1000000000000000000000000000000", + "upper": "1978237383999489947973163960149/500000000000000000000000000000" + }, + "12": { + "lower": "3869463391009350129778562018423/1000000000000000000000000000000", + "upper": "483682923876168766222320252303/125000000000000000000000000000" + }, + "13": { + "lower": "3789420683335813703954784056697/1000000000000000000000000000000", + "upper": "1894710341667906851977392028349/500000000000000000000000000000" + }, + "14": { + "lower": "3715312711182091825485686633361/1000000000000000000000000000000", + "upper": "1857656355591045912742843316681/500000000000000000000000000000" + }, + "15": { + "lower": "3646319839695140374012266928113/1000000000000000000000000000000", + "upper": "1823159919847570187006133464057/500000000000000000000000000000" + }, + "16": { + "lower": "3581781318557569202339343012429/1000000000000000000000000000000", + "upper": "358178131855756920233934301243/100000000000000000000000000000" + }, + "17": { + "lower": "3521156696741134359758736880389/1000000000000000000000000000000", + "upper": "352115669674113435975873688039/100000000000000000000000000000" + }, + "18": { + "lower": "3463998282901185747800548902959/1000000000000000000000000000000", + "upper": "43299978536264821847506861287/12500000000000000000000000000" + }, + "19": { + "lower": "1704965530815454989999622033187/500000000000000000000000000000", + "upper": "27279448493047279839993952531/8000000000000000000000000000" + }, + "2": { + "lower": "1415305715059351282647759844201/250000000000000000000000000000", + "upper": "1132244572047481026118207875361/200000000000000000000000000000" + }, + "20": { + "lower": "83965944181083986164326198053/25000000000000000000000000000", + "upper": "3358637767243359446573047922121/1000000000000000000000000000000" + }, + "21": { + "lower": "413730950384240930438459189737/125000000000000000000000000000", + "upper": "3309847603073927443507673517897/1000000000000000000000000000000" + }, + "22": { + "lower": "3263327587439034586529095798839/1000000000000000000000000000000", + "upper": "81583189685975864663227394971/25000000000000000000000000000" + }, + "23": { + "lower": "804718956217050187300379666613/250000000000000000000000000000", + "upper": "3218875824868200749201518666453/1000000000000000000000000000000" + }, + "25": { + "lower": "313549421592914969080675283181/100000000000000000000000000000", + "upper": "3135494215929149690806752831811/1000000000000000000000000000000" + }, + "3": { + "lower": "262787887606462037430651313067/50000000000000000000000000000", + "upper": "5255757752129240748613026261341/1000000000000000000000000000000" + }, + "4": { + "lower": "2484037839838729910586903627673/500000000000000000000000000000", + "upper": "4968075679677459821173807255347/1000000000000000000000000000000" + }, + "481": { + "lower": "35700554138317851917337677133/200000000000000000000000000000", + "upper": "89251385345794629793344192833/500000000000000000000000000000" + }, + "5": { + "lower": "1186233032090812516351878041259/250000000000000000000000000000", + "upper": "4744932128363250065407512165037/1000000000000000000000000000000" + }, + "525": { + "lower": "22742944551431673576538712861/250000000000000000000000000000", + "upper": "18194355641145338861230970289/200000000000000000000000000000" + }, + "529": { + "lower": "41690804469525529197382917321/500000000000000000000000000000", + "upper": "83381608939051058394765834643/1000000000000000000000000000000" + }, + "6": { + "lower": "4562610571569295439195794139881/1000000000000000000000000000000", + "upper": "2281305285784647719597897069941/500000000000000000000000000000" + }, + "7": { + "lower": "4408459891742037134902918754819/1000000000000000000000000000000", + "upper": "220422994587101856745145937741/50000000000000000000000000000" + }, + "8": { + "lower": "66795757798711164246196486467/15625000000000000000000000000", + "upper": "4274928499117514511756575133889/1000000000000000000000000000000" + }, + "9": { + "lower": "4157145463461131057217781024417/1000000000000000000000000000000", + "upper": "2078572731730565528608890512209/500000000000000000000000000000" + } + }, + "lower": "85719878749684880083239017888220893012178651419025873070498874826515938801606425483061791512049798538759854527501661466906780443141/85719878750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "saving": "2551509/50000000000", + "strict_gap": "1160285669228080804985696742762548864117748192029503902793446817455290237923009421731296883926293712906759747570773043023128743439780023464056477184375055071084267917722300010912264368328217675020096920394417178260460671772870600580110500858560267197697353603594763931543283156323639633672156790265885447551324898421310896830247265338272462374351509596938387909670067592270176811470604577231505879917483683000671091250013098089090852329406229278740972875468982096000153288448707646867236911230363608995750304150467247077902721093467703339409816278927142168293871385458622301430859261645304807392287790833037913095164905576935296914096180937468528030716877853593031781402413133053734165562530067293082534023869381854686817734022861691702574731869881820526546265149512568903881252684753739140988755225229557660592626069265001795066846815964874478822272279675674049309564331338710474989079155779453932990001292388784479881782701949208654880092958569615802082431363900229602753991900853201913911670246559698484755201974712628110823752694017662561262052474618618107758076844613823010409168166656980945127261559/315626025703523256436373828773119248868328570003601284401783327620485824290407942127803580393340812889698148758924133479025758364078093670255879309132950054104615765125691706041738830634604145909080130789538379493541094349130135010269852654813939583894293595610721836471960231778413843982961220577352867742682237294710328500919881069815254823466516726941215799481498258286464082481917435797759202968178203948647233925599152839019622348889931539918866575348104483522917642658072219294880111652763716469213034860437462476978595118121095767900659836027746813372903785902916560713854727223961240267958743873692493155202642125513083347474239635965998188204059078882140912548993959615358584252244602626383835895397135989159308501078347943460081273885770457814084814240605400291738759906839017728139657732973657273177614169893630466136399154192311276005157199960325317251651811708994090196174340101359915488961367796866267450125636185918627913310232479566672686868942152217035787340101388700150139476507369493294361364680633307501462853275125065501567215057815707453500598505995589250000000000000000000000000000000000000000", + "upper": "315626025702362970767145747968133552125566021139483536209753823717692377472952651889880570971609516005771855046017373731454985321054964926816099285668893576920240710054607438124016530623691881540751913114518282573146677170869674338496982054233829083035733328413024482868365467846870560826637580943680710952416351847159003602498570172985007558128244264566864289884559870376794014889647258986288598390946698068729750242598481747769609250800840687589460346069363510647448660562072066006431404005896479557982671251441712172828127871043193046807192132688336997093976643734622689328396104922530381006313439066300205364369604212417918441897304339051902007266590550851424034695400927833956171119190868460821305828104053455135439119223661125726058412194067883082214932420078854026589247337935136475454903993832668517952384612233037840067134152397244429189192325481503044971976137659684525864835629626370836333181913863876266157736851706036845211361023824686579728299326350134604423439871785946158238623305455581624114804982148552299488140647014241748873197395254445401025979887887831173155386176989590831833343019054872738441/315626025703523256436373828773119248868328570003601284401783327620485824290407942127803580393340812889698148758924133479025758364078093670255879309132950054104615765125691706041738830634604145909080130789538379493541094349130135010269852654813939583894293595610721836471960231778413843982961220577352867742682237294710328500919881069815254823466516726941215799481498258286464082481917435797759202968178203948647233925599152839019622348889931539918866575348104483522917642658072219294880111652763716469213034860437462476978595118121095767900659836027746813372903785902916560713854727223961240267958743873692493155202642125513083347474239635965998188204059078882140912548993959615358584252244602626383835895397135989159308501078347943460081273885770457814084814240605400291738759906839017728139657732973657273177614169893630466136399154192311276005157199960325317251651811708994090196174340101359915488961367796866267450125636185918627913310232479566672686868942152217035787340101388700150139476507369493294361364680633307501462853275125065501567215057815707453500598505995589250000000000000000000000000000000000000000" + }, + "parts": { + "data": { + "1": 73319400, + "17": 8146600, + "21": 8146600, + "481": 8146600 + }, + "data_growth_23": { + "1": 8146600, + "21": 8146600 + }, + "data_growth_25": { + "1": 8146600, + "23": 8146600 + }, + "exterior_23": { + "23": 64211400, + "529": 64211400 + }, + "exterior_25": { + "25": 64793806, + "525": 64793806 + }, + "internal_23": { + "1": 791020600, + "10": 4140000, + "11": 3946800, + "12": 2904900, + "13": 2477100, + "14": 1633000, + "15": 1357000, + "16": 809600, + "17": 443900, + "18": 262200, + "2": 38791800, + "20": 103500, + "21": 52900, + "3": 24209800, + "4": 13238800, + "5": 9556500, + "6": 8979200, + "7": 8395000, + "8": 6580300, + "9": 5253200 + }, + "internal_25": { + "1": 840741517, + "10": 4779929, + "11": 4693150, + "12": 3377297, + "13": 2948715, + "14": 2383766, + "15": 1994146, + "16": 1236158, + "17": 1036035, + "18": 657041, + "19": 320551, + "2": 44533566, + "20": 196581, + "22": 97405, + "23": 44275, + "3": 21480459, + "4": 12000296, + "5": 10094700, + "6": 9744042, + "7": 8711549, + "8": 6694380, + "9": 5690223 + }, + "paid_endpoint_copy": { + "1": 4073300 + } + }, + "total_rank": 78860441550 + }, + "bit_saving": "2551509/50000000000", + "comparison": { + "difference": "533/50000000000", + "difference_pr61": "5324914961/500000000000000000", + "pr61_head": "afb7cb67d1858641315cfbf4ac768ee64a8eff3a", + "pr61_kappa": "25508460085039/500000000000000000", + "pr62_kappa": "5101691/100000000000", + "pr62_network_at_new_bit_lower": "3428795166774725707029430980420227920340827739703568976514604805405819541248322714869086735630197255034188622548856339970727442809/3428795150000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "ratio": "5102757/5101691", + "ratio_pr61": "25513785000000/25508460085039" + }, + "eventual_bounds": { + "additional_eventual_conditions": [ + "BHP prime threshold and distinct-prime packing", + "Fixed rational basis, eligible common prime and native table setup", + "Catalogue/descriptor domination, logarithm absorption, exact recovery" + ], + "all_interval_argument": "For [Z,Z+k), bound RHS at Z+k and LHS at floor(Z/k). Successive intervals double LHS; the positive affine RHS grows at most linearly, so 2^j >= j+1 proves persistence.", + "common_cutoff": 14000000000000, + "cutoff_log2_input": { + "alpha": 6145305665, + "compact": 24581222657, + "geometry": 3999931964388, + "guard": 4350589, + "log_p": 25, + "normalization": 14000000000000, + "period": 49162445313, + "phase_cell": 19, + "reservoir": 14, + "stopped_leaf": 252 + }, + "power_checkpoints": [ + { + "log2_input": 14000000000000, + "powers": { + "alpha": { + "exponent": 714358608, + "rhs": 112000000156848, + "rhs_bits": 47 + }, + "compact": { + "exponent": 714358608, + "rhs": 448000000627328, + "rhs_bits": 49 + }, + "leaf": { + "exponent": 666666666666, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 714358608, + "rhs": 224000000313624, + "rhs_bits": 48 + }, + "rows": { + "exponent": 714358608, + "rhs": 112000000156848000, + "rhs_bits": 57 + } + } + }, + { + "log2_input": 28000000000000, + "powers": { + "alpha": { + "exponent": 1428717216, + "rhs": 224000000156848, + "rhs_bits": 48 + }, + "compact": { + "exponent": 1428717216, + "rhs": 896000000627328, + "rhs_bits": 50 + }, + "leaf": { + "exponent": 1333333333333, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 1428717216, + "rhs": 448000000313624, + "rhs_bits": 49 + }, + "rows": { + "exponent": 1428717216, + "rhs": 224000000156848000, + "rhs_bits": 58 + } + } + }, + { + "log2_input": 56000000000000, + "powers": { + "alpha": { + "exponent": 2857434432, + "rhs": 448000000156848, + "rhs_bits": 49 + }, + "compact": { + "exponent": 2857434432, + "rhs": 1792000000627328, + "rhs_bits": 51 + }, + "leaf": { + "exponent": 2666666666666, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 2857434432, + "rhs": 896000000313624, + "rhs_bits": 50 + }, + "rows": { + "exponent": 2857434432, + "rhs": 448000000156848000, + "rhs_bits": 59 + } + } + }, + { + "log2_input": 112000000000000, + "powers": { + "alpha": { + "exponent": 5714868864, + "rhs": 896000000156848, + "rhs_bits": 50 + }, + "compact": { + "exponent": 5714868864, + "rhs": 3584000000627328, + "rhs_bits": 52 + }, + "leaf": { + "exponent": 5333333333333, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 5714868864, + "rhs": 1792000000313624, + "rhs_bits": 51 + }, + "rows": { + "exponent": 5714868864, + "rhs": 896000000156848000, + "rhs_bits": 60 + } + } + }, + { + "log2_input": 224000000000000, + "powers": { + "alpha": { + "exponent": 11429737728, + "rhs": 1792000000156848, + "rhs_bits": 51 + }, + "compact": { + "exponent": 11429737728, + "rhs": 7168000000627328, + "rhs_bits": 53 + }, + "leaf": { + "exponent": 10666666666666, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 11429737728, + "rhs": 3584000000313624, + "rhs_bits": 52 + }, + "rows": { + "exponent": 11429737728, + "rhs": 1792000000156848000, + "rhs_bits": 61 + } + } + }, + { + "log2_input": 448000000000000, + "powers": { + "alpha": { + "exponent": 22859475456, + "rhs": 3584000000156848, + "rhs_bits": 52 + }, + "compact": { + "exponent": 22859475456, + "rhs": 14336000000627328, + "rhs_bits": 54 + }, + "leaf": { + "exponent": 21333333333333, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 22859475456, + "rhs": 7168000000313624, + "rhs_bits": 53 + }, + "rows": { + "exponent": 22859475456, + "rhs": 3584000000156848000, + "rhs_bits": 62 + } + } + } + ], + "practical_runtime_claim": false + }, + "finite_bridge": { + "bit": { + "W": 137151806, + "halving_degree": 9, + "m": 575, + "maxchild": 529, + "wire_bits": 28 + }, + "complex": { + "W": 537696432, + "halving_degree": 20, + "m": 784, + "maxchild": 756, + "s": 421548223824, + "scalar_group_upper": 4793351472, + "scalar_terms": [ + { + "c": 78437, + "copied_center_extra_groups": 56, + "h": 28, + "invocations": 3276, + "local_group_upper": 729892, + "v": 3276 + }, + { + "c": 78437, + "copied_center_extra_groups": 56, + "h": 28, + "invocations": 3276, + "local_group_upper": 729892, + "v": 3276 + } + ], + "wire_bits": 30 + }, + "rows": { + "coefficient": 852, + "contract": "W_complex^D_complex * W_bit^D_bit; one preceding prefix and padding; all temporary copies sequential", + "degree": 2000, + "degree_gap": "6548/25", + "suffix_slope": 8000 + }, + "semantic": { + "B": 9696565176891520488614054257040, + "C0": 2358858462850846165593256368932965330169899180021667007021321420800, + "C1": 1, + "E": 9696565176891520488192506033216, + "induction_gap": 533311084729033626873772984137200, + "literal_charge": 2771683137698171397039558468, + "strict_literal_gap": 9693793493753822316795466474748 + } + }, + "kappa": "5102757/100000000000", + "next_bit_saving": "5103019/100000000000", + "source": { + "compiler_sha256": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd", + "inherited_verifier_sha256": "fafe25d57166a747eeb847444a2e02dd7eed19038b93a2c495014d147d04a8fb", + "records": { + "compiler": "scripts/experiments/rank_pair_compiler.py (PR #60 rank-first variant of PR #57)", + "compiler_sha256": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd", + "graph": "research/pair-assembly/pair_graph.py", + "graph_sha256": "3d47e89d2649c90800a276bdd0480131def50e0bdf92c122a19494b55bf17420" + } + }, + "status": "Exact finite screen; retained analytic and fixed-tape hypotheses unchanged" +} diff --git a/research/rank-pair/screen.py b/research/rank-pair/screen.py new file mode 100644 index 0000000000..5d146f0edf --- /dev/null +++ b/research/rank-pair/screen.py @@ -0,0 +1,119 @@ +#!/usr/bin/env python3 +"""Regenerate paid profiles and exact screen for rank-first PR62 composition. + +Uses PR62's profile construction, eumemic's PR57 word/profile checkers and +Chafik Boukhalfa's PR60 rank-first compiler. Prepared by Dominik Scholz with +substantial OpenAI GPT-6 Astra assistance. Apache-2.0; inherited notices apply. +This is a research screen, not a claim of formal verification. +""" +import sys + +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') +sys.dont_write_bytecode = True + +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import json +import os +from pathlib import Path +import shlex +import subprocess + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +EXP = ROOT / 'scripts/experiments' +sys.path.insert(0, str(EXP)) +import binary_frame_math as arithmetic +from binary_frame_profile_prepare import prepare +from binary_frame_replay import replay +from frame_compile import COMPILER_SHA256, GRAPH_SHA256 + +spec = importlib.util.spec_from_file_location( + 'pair_frame_verifier', ROOT / 'research/pair-assembly/frame/frame_verify.py') +baseline = importlib.util.module_from_spec(spec) +spec.loader.exec_module(baseline) + + +def main(): + records = json.loads((HERE / 'frame-compiler.json').read_text()) + assert records['source']['compiler_sha256'] == COMPILER_SHA256 + assert records['source']['graph_sha256'] == GRAPH_SHA256 + assert sha256((EXP/'rank_pair_compiler.py').read_bytes()).hexdigest() == records['source']['compiler_sha256'] + assert sha256((ROOT/records['source']['graph']).read_bytes()).hexdigest() == records['source']['graph_sha256'] + baseline.check_sources() + profiles = [] + profiler = HERE / 'profiles' + subprocess.run([*shlex.split(os.environ.get('CXX', 'c++')), '-O3', '-std=c++17', '-I', + str(baseline.INHERITED / 'scripts/partial_swap'), + str(EXP / 'binary_frame_profiles.cpp'), '-o', str(profiler)], check=True) + for h in (23, 25): + path = HERE / f'frame-word-{h}.json.gz' + packed = path.read_bytes() + assert sha256(packed).hexdigest() == records['axes'][str(h)]['gzip_sha256'] + receipt = replay(path) + assert json.loads(json.dumps(receipt)) == records['axes'][str(h)]['replay'] + transitions = HERE / f'word{h}.bin' + prepared = prepare(path, transitions) + (HERE / f'frame-transitions-{h}.json').write_text(json.dumps(prepared, indent=2)+'\n') + subprocess.run([str(profiler), str(transitions)], check=True) + profile = json.loads(Path(str(transitions)+'.profiles.json').read_text()) + (HERE / f'frame-profiles-{h}.json').write_text(json.dumps(profile, indent=2)+'\n') + profiles.append(profile) + print(f'PASS physical replay and fixed profiles h={h}, roles={profile["R"]}', flush=True) + # The unchanged profile constructor validates the literal rank identity. + baseline.WIRES_S = 2*4073300 + sum(4073300//f['v']*f['R'] for f in profiles) + baseline.MASS_S = 575*baseline.WIRES_S - 1846900 + profile = baseline.profile(profiles, records) + rows = profile['child_multiplicities'] + low, high = 1, 7170000 + while low+1 < high: + mid = (low+high)//2 + test = arithmetic.moment(575, profile['W'], rows, Q(mid, 10**11)) + if test['strict_gap'] > 0: + low = mid + else: + high = mid + ab = Q(low, 10**11) + accepted = arithmetic.moment(575, profile['W'], rows, ab) + rejected = arithmetic.moment(575, profile['W'], rows, Q(high, 10**11)) + assert accepted['strict_gap'] > 0 and rejected['lower'] > 1 + bridge = json.loads((baseline.OLD/'certificate.json').read_text())['finite_bridge'] + bridge['bit']['W'] = profile['W'] + preliminary = baseline.balanced.assembly(bridge, ab, Q(1, 10**11)) + scaled = preliminary['minimum_margin'] * 10**11 + kappa = Q(-(-scaled.numerator//scaled.denominator)-1, 10**11) + assembled = baseline.balanced.assembly(bridge, ab, kappa) + try: + baseline.balanced.assembly(bridge, ab, kappa+Q(1, 10**11)) + except baseline.balanced.InvalidAssembly: + pass + else: + raise AssertionError('Next assembly grid point unexpectedly passed') + prior = json.loads((ROOT/'research/pair-assembly/frame/frame-certificate.json').read_text()) + old_rows = {int(t): n for t,n in prior['bit']['child_multiplicities'].items()} + old_at_new = arithmetic.moment(575, prior['bit']['W'], old_rows, ab) + result = dict( + status='Exact finite screen; retained analytic and fixed-tape hypotheses unchanged', + kappa=kappa, bit_saving=ab, next_bit_saving=Q(high, 10**11), + bit=dict(profile, moment=accepted, excluded_above_lower=rejected['lower']), + assembly=assembled, finite_bridge=bridge, + eventual_bounds=baseline.balanced.cutoffs(bridge, assembled), + comparison=dict(pr62_kappa=Q(5101691,10**11), + difference=kappa-Q(5101691,10**11), + ratio=kappa/Q(5101691,10**11), + pr61_head='afb7cb67d1858641315cfbf4ac768ee64a8eff3a', + pr61_kappa=Q(25508460085039,500000000000000000), + difference_pr61=kappa-Q(25508460085039,500000000000000000), + ratio_pr61=kappa/Q(25508460085039,500000000000000000), + pr62_network_at_new_bit_lower=old_at_new['lower']), + source=dict(records=records['source'], compiler_sha256=sha256((EXP/'rank_pair_compiler.py').read_bytes()).hexdigest(), + inherited_verifier_sha256=sha256((ROOT/'research/pair-assembly/frame/frame_verify.py').read_bytes()).hexdigest())) + (HERE/'screen-certificate.json').write_text(json.dumps(arithmetic.js(result), indent=2, sort_keys=True)+'\n') + print('EXACT SCREEN', json.dumps(arithmetic.js(dict(kappa=kappa, bit=ab, W=profile['W'], + comparison=result['comparison']))), flush=True) + + +if __name__ == '__main__': + main() diff --git a/research/reordered-rank-pair/README.md b/research/reordered-rank-pair/README.md new file mode 100644 index 0000000000..3ad7952ba9 --- /dev/null +++ b/research/reordered-rank-pair/README.md @@ -0,0 +1,85 @@ +# Reordering the rank-pair physical compilation + +This experiment changes the schedule of equal-rank regions in PR #63's +composition of the PR #62 scalar graph and PR #60 rank-first compiler. The +23-axis uses increasing `(rank, cover, core)`; the 25-axis uses increasing rank +and decreasing minimum node number. The scalar identities, matched carrier +candidates, synthesis, and descending-rank retirement policy are unchanged. + +Reordering changes which retired physical roles are available when a region +is compiled. The resulting words have the same 27,918 and 36,586 physical +roles, but different paid fixed-I+J profiles. The selected schedules came +from a bounded comparison of reverse-node, core-cover, cover-core, and +reverse-core-cover orders. Core-cover was screened only; the other three +23-axis words and the reverse-node 25-axis word were independently replayed +and physically profiled before selection. Reversing both axes was weaker +than the selected mixed schedule. These finite tests do not prove optimality. + +## Why the schedule remains valid + +Every region retains its exact original envelope and its original linear +map. The wrapper checks every incoming inter-region dependency and every +selected-candidate direction against the new order. Thus all required inputs +are available, and retained carriers still travel forward. The admissibility argument uses these explicit dependency inequalities; +rank ties alone do not certify topological order, especially for source +frames. The complete serialized physical word is replayed on every input +and dirty basis vector in both orientations, and all frame inclusions and +actual fixed-basis profiles are independently regenerated. + +The literal rank identity and all paid endpoint/data/exterior terms use the +unchanged inherited profile constructor. No histogram estimate substitutes +for the physical word. The general transfer, routing, analytic, recovery, +and fixed-tape hypotheses remain inherited conditions; this is a finite +conditional certificate rather than a new formal proof of those hypotheses. + +## Reproduce + +From the repository root, with assertions enabled: + +```sh +PYTHONDONTWRITEBYTECODE=1 python3 research/reordered-rank-pair/verify.py +PYTHONDONTWRITEBYTECODE=1 python3 research/reordered-rank-pair/verify.py --rebuild +PYTHONDONTWRITEBYTECODE=1 python3 research/reordered-rank-pair/test_negative.py +``` + +The first command checks source/artifact hashes, independently replays both +committed words, rebuilds their fixed-I+J profiles, and recomposes the paid +global profile. `--rebuild` also recompiles both words and requires exact +byte equality with the committed decompressed witnesses. Disposable output +goes under `build/reordered-rank-pair` (or `--work-dir`). The tests reject a +missing physical XOR, understated physical role count, changed word/profile +digests, a backward region dependency, and execution with Python assertions +disabled. Arithmetic witnesses and their +independent controls are in `arithmetic/`. + +## Attribution + +The graph is Avi Eisenberg's PR #62 interval-strip/core-aware pair assembly, +prepared with Claude assistance, with its retained credits to PR #53, #48, +#44, #46, #41, #43, and earlier icekylinx work. Chafik Boukhalfa's PR #60 +rank-first compiler derives from eumemic's PR #57 joint frame compiler, +both with OpenAI Codex assistance. Dominik Scholz's PR #63 combines those +sources, with OpenAI GPT-6 Astra assistance. Alejandro Zarzuelo Urdiales's +PR #61 supplies precedent for rational parameter refinement. This bounded +region-order experiment and its packaging are by Rohan Arun with OpenAI +Codex assistance. Original Apache-2.0 notices remain applicable. + +## Live comparison at publication + +PR #64 (`790a14e28e935398072b9a9a68694ce7fba8940f`, @rfu08) reports +`20411033624901463/400000000000000000000` for the unchanged #63 profiles, +with additional independent verification and scoped Lean formalization. +The present changed-schedule bound exceeds that reported value; exact +arithmetic and the source pin are in `current-comparison.json`. This is only +a bound comparison, not a comparison of formal proof coverage. + +## Repository validation + +Full `make verify` passed on research commit `49e84f939d15b618b50714eb039cabf97c74256a` +in 1409.512 seconds, including 467 core unit tests, 20 historical patch checks, +and the complete new physical rebuild, profiles, independent arithmetic and +negative controls. All 32 GitHub CI jobs on that head passed. The +[validation receipt](validation.json) records the log hash and subsequent +upstream integration. That integration preserves every consumed source and +witness byte; its newly imported upstream test groups are covered separately +by the expanded CI matrix, not retrospectively by the earlier local run. diff --git a/research/reordered-rank-pair/arithmetic/README.md b/research/reordered-rank-pair/arithmetic/README.md new file mode 100644 index 0000000000..fed8b1bc5d --- /dev/null +++ b/research/reordered-rank-pair/arithmetic/README.md @@ -0,0 +1,174 @@ +# Exact arithmetic for the reordered rank-pair witness + +The selected complete paid profile admits + +- bit saving `a = 5103158916233/100000000000000000`; +- backoff `h = 1/1000000000000`, unchanged from PR63; +- `kappa = 2041159402879/40000000000000000 = 0.000051028985071975`. + +All 47 strict assembly inequalities and all seven margins pass. The next bit +saving on the 1e-18 grid has moment strictly above one; the next kappa on that +grid fails the unchanged balanced assembly. The finite sufficient arithmetic +cutoff remains `log2(input) >= 14000000000000`. This is an eventual arithmetic +threshold, not a practical runtime claim or the complete all-size threshold. + +The exact gain above PR63's `5102757/10^11` is +`56602879/40000000000000000`, approximately 0.0027731518 percent relative. +The construction gain is separated from parameter precision: + +| Check | Bit saving | Kappa | Gain versus PR63 | +|---|---:|---:|---:| +| Same 1e-11 grid and same h as PR63 | 0.00005103158 | 0.00005102897 | 0.0000000014 | +| Refined 1e-18 grid; same h | 0.000051031589162330 | 0.000051028985071975 | 0.000000001415071975 | + +The first row passes even with PR63's original low-order exponential bounds, +and its next bit grid point fails with those bounds. Thus its 1.4e-9 gain does +not depend on tightening the numerical enclosure. Precision adds a further +`602879/40000000000000000 = 1.5071975e-11`. + +## Reproduction and source linkage + +Run from any checkout location using Python 3.11 or later: + +```sh +python3 -B research/reordered-rank-pair/arithmetic/refine.py +python3 -B research/reordered-rank-pair/arithmetic/audit.py +python3 -B -m unittest discover -s research/reordered-rank-pair/arithmetic -p test_arithmetic.py -v +``` + +The default commands recompute and compare without writing outputs. An +intentional certificate update uses `--record` on the first two commands. +`refine.py` accepts `--profile PATH` and `--certificate PATH`; `audit.py` +accepts `--certificate PATH` and `--receipt PATH`. + +`certificate.json` pins `../paired-candidate.json`, both arithmetic scripts, +the inherited logarithm implementation and the inherited balanced assembly +by SHA256. All paths are repository relative. It includes the complete exact +per-child logarithm and exponential intervals, weighted moment bounds, +assembly slacks, all seven margins, next-grid failures, comparisons and +sufficient arithmetic cutoffs. `audit-receipt.json` records an independently +computed enclosure and ten deliberate assembly failures. + +This package checks the supplied complete paid profile. The parent +`../verify.py` checks the words, physical replay, actual profile/CRT results, +paid profile assembly and its correspondence to `../paired-candidate.json`. +An arithmetic pass alone does not prove that physical linkage. + +## Rational logarithm enclosure + +For `y >= 1`, put `z = (y-1)/(y+1)`. With `0 <= z < 1`, + +`log(y) = 2 * sum(j>=0, z^(2j+1)/(2j+1))`. + +Every term is nonnegative. Truncation after indices `0,...,J-1` is therefore a +lower bound. For the tail, `2j+1 >= 2J+1` and the powers form a geometric series, +so the upper remainder is + +`2*z^(2J+1)/((2J+1)*(1-z^2))`. + +The inherited helper reduces by powers of 2 to `1 <= y <= 2`, uses `J=32`, +adds the corresponding multiple of `log(2)`, then rounds downward/upward to +the 1e-30 rational grid. These operations preserve the enclosure. + +The independent audit instead reduces by powers of 3/2 to +`1 <= y <= 3/2`, uses `J=60`, and adds the corresponding multiple of +`log(3/2)`. Its exact logarithm enclosure is checked to lie inside the recorded +inherited interval for every child. The two implementations share the +mathematical atanh-series identity but use different range reduction, term +counts and evaluation code; neither relies on machine floating-point logs. + +## Rational exponential and complete moment enclosure + +For a child of dimension `t`, multiplicity `n`, arity `m` and width `W`, the +weight is `w=t*n/(m*W) > 0`. With bit saving `a>0`, its contribution to the +characteristic moment is `w*exp(a*log(m/t))`. The complete histogram includes +all paid parts; neither rare children nor physical transitions are omitted. + +Write `u=a*log_lower` and `v=a*log_upper`. The checker verifies +`0 <= u <= v < 1`. For `S_d(x)=sum(j=0..d, x^j/j!)`, positivity gives + +`S_d(u) <= exp(a*log(m/t))`. + +At `v`, the first omitted term is `v^(d+1)/(d+1)!`; each later term divided by +its predecessor is at most `v/(d+2) < 1`. A geometric majorant therefore gives + +`exp(a*log(m/t)) <= S_d(v) + v^(d+1)/((d+1)!*(1-v/(d+2)))`. + +The primary checker uses `d=8`. It rounds the lower expression downward and +the upper expression upward to the 1e-40 rational grid, multiplies by each +positive exact weight, and sums. Directed rounding can only widen the +interval. Every arithmetic operation uses integers and exact Fractions. + +The independent audit evaluates the exponential by a recurrence through +degree 12. It checks `v<1/1000`, rounds input bounds outward, and bounds the +remaining tail by twice the first omitted term. This is valid because all +successive tail ratios are below 1/2. It independently confirms that the +accepted upper moment is below one and the successor lower moment is above +one. No empirical epsilon, decimal-log assumption or float tolerance enters +the acceptance decision. + +All weights and `log(m/t)` are strictly positive, since `0= 1 + k = 0 + while x > Q(3, 2): + x /= Q(3, 2) + k += 1 + def small(y): + z = (y-1)/(y+1) + power, total = z, Q() + for j in range(60): + total += power/Q(2*j+1) + power *= z*z + return 2*total, 2*total+2*power/(121*(1-z*z)) + lo, hi = small(x) + blo, bhi = small(Q(3, 2)) + return lo+k*blo, hi+k*bhi + + +def independent_moment(profile, saving, recorded_terms): + low, high = Q(), Q() + rows = {int(t): n for t, n in profile['child_multiplicities'].items()} + for t, n in sorted(rows.items()): + lo, hi = log_interval(Q(profile['m'], t)) + recorded = recorded_terms[str(t)] + assert Q(recorded['log_lower']) <= lo <= hi <= Q(recorded['log_upper']) + u, v = lo*saving, hi*saving + assert 0 < u <= v < Q(1, 1000) + # Directed rounding of input logs bounds rational denominator sizes. + u = Q(refine.floor_scaled(u, 10**40), 10**40) + v = Q(refine.ceiling_scaled(v, 10**40), 10**40) + tlo, thi = Q(1), Q(1) + elo, ehi = Q(1), Q(1) + for j in range(1, 13): + tlo, thi = tlo*u/j, thi*v/j + elo, ehi = elo+tlo, ehi+thi + # First omitted term is degree13; subsequent ratios <1/2. + ehi += 2*thi*v/13 + weight = Q(t*n, profile['m']*profile['W']) + low += weight*Q(refine.floor_scaled(elo, 10**40), 10**40) + high += weight*Q(refine.ceiling_scaled(ehi, 10**40), 10**40) + return low, high + + +def audit(certificate): + profile_path = ROOT/certificate['profile_path'] + assert sha256(profile_path.read_bytes()).hexdigest() == certificate['profile_sha256'] + for name, digest in certificate['source_sha256'].items(): + assert sha256((ROOT/name).read_bytes()).hexdigest() == digest, name + source = json.loads(profile_path.read_text()) + p = source['bit'] + assert sum(int(t)*n for t, n in p['child_multiplicities'].items()) == p['total_rank'] + accepted = independent_moment(p, Q(certificate['bit_saving']), certificate['accepted_moment']['terms']) + rejected = independent_moment(p, Q(certificate['next_bit_saving']), certificate['accepted_moment']['terms']) + assert accepted[1] < 1 < rejected[0] + controls = {} + for name, variant in [('preferred', certificate['preferred']), ('coarse_grid_control', certificate['coarse_grid_control'])]: + params = variant['assembly']['parameters'] + result = refine.balanced.assembly(source['finite_bridge'], Q(params['a_bit']), Q(params['kappa']), h=Q(params['h'])) + assert refine.arithmetic.js(result) == variant['assembly'] + assert len(result['constraints']) == 47 and len(result['margins']) == 7 + assert all(v > 0 for v in result['constraints'].values()) + for label, kwargs in [('next_grid', dict(kappa=Q(variant['next_kappa']))), + ('zero_backoff', dict(h=Q())), + ('original_prefix', dict(original_prefix=True)), + ('old_guard', dict(old_guard=True)), + ('old_exposures', dict(old_exposures=True))]: + call = dict(a_bit=Q(params['a_bit']), kappa=Q(params['kappa']), h=Q(params['h'])) + call.update(kwargs) + try: + refine.balanced.assembly(source['finite_bridge'], **call) + except refine.balanced.InvalidAssembly as error: + controls[name+'/'+label] = str(error) + else: + raise AssertionError('Negative control accepted: '+name+'/'+label) + next_a = Q(certificate['next_bit_saving']) + best = Q(certificate['preferred']['kappa']) + cap = next_a/(1+next_a) + assert cap > best + return dict(status='PASS', independent_log_base='3/2', independent_log_terms=60, + independent_exp_degree=12, independent_tail='twice first omitted term', + independent_accepted_gap=1-accepted[1], independent_rejected_gap=rejected[0]-1, + variants_reassembled=2, constraints_each=47, margins_each=7, controls=controls, + fixed_profile_balanced_family_kappa_strict_upper=cap, + remaining_possible_parameter_gain_upper=cap-best) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--certificate', type=Path, default=HERE/'certificate.json') + parser.add_argument('--receipt', type=Path, default=HERE/'audit-receipt.json') + parser.add_argument('--record', action='store_true') + args = parser.parse_args() + result = refine.arithmetic.js(audit(json.loads(args.certificate.read_text()))) + if args.record: + args.receipt.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + assert result == json.loads(args.receipt.read_text()), 'Independent receipt changed' + print('PASS independent logarithm/exponential enclosures; 47 strict constraints; seven margins; ten assembly negative controls') + + +if __name__ == '__main__': + main() diff --git a/research/reordered-rank-pair/arithmetic/certificate.json b/research/reordered-rank-pair/arithmetic/certificate.json new file mode 100644 index 0000000000..346cf87ea3 --- /dev/null +++ b/research/reordered-rank-pair/arithmetic/certificate.json @@ -0,0 +1,1087 @@ +{ + "accepted_moment": { + "degree": 8, + "lower": "34287951499999999998997315662315085394575263036671/34287951500000000000000000000000000000000000000000", + "rounding_denominator": 10000000000000000000000000000000000000000, + "saving": "5103158916233/100000000000000000", + "strict_gap": "2278828040192983762647964739/77927162500000000000000000000000000000000000000", + "terms": { + "1": { + "exp_lower": "5001621630918375893019301295747281962987/5000000000000000000000000000000000000000", + "exp_upper": "10003243261836751786038602591494564437549/10000000000000000000000000000000000000000", + "log_lower": "3177185020398675220004135749131/500000000000000000000000000000", + "log_upper": "6354370040797350440008271498263/1000000000000000000000000000000", + "weight": "61988/2833715" + }, + "10": { + "exp_lower": "1000206790403018649267184041288978248657/1000000000000000000000000000000000000000", + "exp_upper": "2500516976007546623167960103222445749253/2500000000000000000000000000000000000000", + "log_lower": "2025892473901652377995140021789/500000000000000000000000000000", + "log_upper": "4051784947803304755990280043579/1000000000000000000000000000000", + "weight": "7053/6234173" + }, + "11": { + "exp_lower": "10002019255791173815676540174477997136241/10000000000000000000000000000000000000000", + "exp_upper": "2500504813947793453919135043619499411669/2500000000000000000000000000000000000000", + "log_lower": "3956474767998979895946327920297/1000000000000000000000000000000", + "log_upper": "1978237383999489947973163960149/500000000000000000000000000000", + "weight": "34143/28337150" + }, + "12": { + "exp_lower": "244188838955937173152799000772966753/244140625000000000000000000000000000", + "exp_upper": "1000197484363518661233864707166071871331/1000000000000000000000000000000000000000", + "log_lower": "3869463391009350129778562018423/1000000000000000000000000000000", + "log_upper": "483682923876168766222320252303/125000000000000000000000000000", + "weight": "1637772/1714397575" + }, + "13": { + "exp_lower": "10001933988586235970593248414082864793191/10000000000000000000000000000000000000000", + "exp_upper": "10001933988586235970593248414082865303617/10000000000000000000000000000000000000000", + "log_lower": "3789420683335813703954784056697/1000000000000000000000000000000", + "log_upper": "1894710341667906851977392028349/500000000000000000000000000000", + "weight": "3064763/3428795150" + }, + "14": { + "exp_lower": "625118510179239092134146727144581987029/625000000000000000000000000000000000000", + "exp_upper": "5000948081433912737073173817156656151443/5000000000000000000000000000000000000000", + "log_lower": "3715312711182091825485686633361/1000000000000000000000000000000", + "log_upper": "1857656355591045912742843316681/500000000000000000000000000000", + "weight": "1222116/1714397575" + }, + "15": { + "exp_lower": "10001860948095049038065447122495285494181/10000000000000000000000000000000000000000", + "exp_upper": "50009304740475245190327235612476430023/50000000000000000000000000000000000000", + "log_lower": "3646319839695140374012266928113/1000000000000000000000000000000", + "log_upper": "1823159919847570187006133464057/500000000000000000000000000000", + "weight": "437037/685759030" + }, + "16": { + "exp_lower": "10001828006987297838063812648469929988329/10000000000000000000000000000000000000000", + "exp_upper": "2000365601397459567612762529693986099749/2000000000000000000000000000000000000000", + "log_lower": "3581781318557569202339343012429/1000000000000000000000000000000", + "log_upper": "358178131855756920233934301243/100000000000000000000000000000", + "weight": "65416/155854325" + }, + "17": { + "exp_lower": "2500449265917948104603244530335785484971/2500000000000000000000000000000000000000", + "exp_upper": "5000898531835896209206489060671571225149/5000000000000000000000000000000000000000", + "log_lower": "3521156696741134359758736880389/1000000000000000000000000000000", + "log_upper": "352115669674113435975873688039/100000000000000000000000000000", + "weight": "1423053/685759030" + }, + "18": { + "exp_lower": "5000883944812795540643983155649296384137/5000000000000000000000000000000000000000", + "exp_upper": "5000883944812795540643983155649296639343/5000000000000000000000000000000000000000", + "log_lower": "3463998282901185747800548902959/1000000000000000000000000000000", + "log_upper": "43299978536264821847506861287/12500000000000000000000000000", + "weight": "73188/342879515" + }, + "19": { + "exp_lower": "2500435073355895874949004807973392212539/2500000000000000000000000000000000000000", + "exp_upper": "2000348058684716699959203846378713872113/2000000000000000000000000000000000000000", + "log_lower": "1704965530815454989999622033187/500000000000000000000000000000", + "log_upper": "27279448493047279839993952531/8000000000000000000000000000", + "weight": "24073/311708650" + }, + "2": { + "exp_lower": "10002889429351305579391066844438599404943/10000000000000000000000000000000000000000", + "exp_upper": "10002889429351305579391066844438599915793/10000000000000000000000000000000000000000", + "log_lower": "1415305715059351282647759844201/250000000000000000000000000000", + "log_upper": "1132244572047481026118207875361/200000000000000000000000000000", + "weight": "3622866/1714397575" + }, + "20": { + "exp_lower": "5000857056559616993851882270551970640809/5000000000000000000000000000000000000000", + "exp_upper": "400068564524769359508150581644157671681/400000000000000000000000000000000000000", + "log_lower": "83965944181083986164326198053/25000000000000000000000000000", + "log_upper": "3358637767243359446573047922121/1000000000000000000000000000000", + "weight": "26402/342879515" + }, + "21": { + "exp_lower": "5000844605243119232606473780943636091543/5000000000000000000000000000000000000000", + "exp_upper": "2500422302621559616303236890471818173373/2500000000000000000000000000000000000000", + "log_lower": "413730950384240930438459189737/125000000000000000000000000000", + "log_upper": "3309847603073927443507673517897/1000000000000000000000000000000", + "weight": "12978/2981561" + }, + "22": { + "exp_lower": "10001665466600995950680178785864990598847/10000000000000000000000000000000000000000", + "exp_upper": "2500416366650248987670044696466247777313/2500000000000000000000000000000000000000", + "log_lower": "3263327587439034586529095798839/1000000000000000000000000000000", + "log_upper": "81583189685975864663227394971/25000000000000000000000000000", + "weight": "77/2833715" + }, + "23": { + "exp_lower": "10001642778407860986976249508714803404087/10000000000000000000000000000000000000000", + "exp_upper": "1000164277840786098697624950871480391449/1000000000000000000000000000000000000000", + "log_lower": "804718956217050187300379666613/250000000000000000000000000000", + "log_upper": "3218875824868200749201518666453/1000000000000000000000000000000", + "weight": "11447/542102" + }, + "25": { + "exp_lower": "5000800110274057186642873980504034355159/5000000000000000000000000000000000000000", + "exp_upper": "5000800110274057186642873980504034610359/5000000000000000000000000000000000000000", + "log_lower": "313549421592914969080675283181/100000000000000000000000000000", + "log_upper": "3135494215929149690806752831811/1000000000000000000000000000000", + "weight": "11641/566743" + }, + "3": { + "exp_lower": "5001341228208864565852456321215617302809/5000000000000000000000000000000000000000", + "exp_upper": "1000268245641772913170491264243123511627/1000000000000000000000000000000000000000", + "log_lower": "262787887606462037430651313067/50000000000000000000000000000", + "log_upper": "5255757752129240748613026261341/1000000000000000000000000000000", + "weight": "5956407/3428795150" + }, + "4": { + "exp_lower": "10002535609381542984545633250181207029999/10000000000000000000000000000000000000000", + "exp_upper": "2500633902345385746136408312545301885141/2500000000000000000000000000000000000000", + "log_lower": "2484037839838729910586903627673/500000000000000000000000000000", + "log_upper": "4968075679677459821173807255347/1000000000000000000000000000000", + "weight": "95648/74539025" + }, + "481": { + "exp_lower": "5000045546607739441768548232115119086657/5000000000000000000000000000000000000000", + "exp_upper": "2000018218643095776707419292846047736727/2000000000000000000000000000000000000000", + "log_lower": "35700554138317851917337677133/200000000000000000000000000000", + "log_upper": "89251385345794629793344192833/500000000000000000000000000000", + "weight": "13468/271051" + }, + "5": { + "exp_lower": "5001210853727897355673045114388323699841/5000000000000000000000000000000000000000", + "exp_upper": "5001210853727897355673045114388323955101/5000000000000000000000000000000000000000", + "log_lower": "1186233032090812516351878041259/250000000000000000000000000000", + "log_upper": "4744932128363250065407512165037/1000000000000000000000000000000", + "weight": "171439/137151806" + }, + "525": { + "exp_lower": "2500011606112967191389431902824088768163/2500000000000000000000000000000000000000", + "exp_upper": "10000046424451868765557727611296355582971/10000000000000000000000000000000000000000", + "log_lower": "22742944551431673576538712861/250000000000000000000000000000", + "log_upper": "18194355641145338861230970289/200000000000000000000000000000", + "weight": "244461/566743" + }, + "529": { + "exp_lower": "10000042551050640055883233578467532894109/10000000000000000000000000000000000000000", + "exp_upper": "2500010637762660013970808394616883351107/2500000000000000000000000000000000000000", + "log_lower": "41690804469525529197382917321/500000000000000000000000000000", + "log_upper": "83381608939051058394765834643/1000000000000000000000000000000", + "weight": "116748/271051" + }, + "6": { + "exp_lower": "10002328643768966895497189574260748515347/10000000000000000000000000000000000000000", + "exp_upper": "5001164321884483447748594787130374512919/5000000000000000000000000000000000000000", + "log_lower": "4562610571569295439195794139881/1000000000000000000000000000000", + "log_upper": "2281305285784647719597897069941/500000000000000000000000000000", + "weight": "97752/68575903" + }, + "7": { + "exp_lower": "5001124980109214394703176231536499760141/5000000000000000000000000000000000000000", + "exp_upper": "5001124980109214394703176231536500015377/5000000000000000000000000000000000000000", + "log_lower": "4408459891742037134902918754819/1000000000000000000000000000000", + "log_upper": "220422994587101856745145937741/50000000000000000000000000000", + "weight": "8995/5963122" + }, + "8": { + "exp_lower": "1250272725240877662442274762818427730447/1250000000000000000000000000000000000000", + "exp_upper": "2000436360385404259907639620509484470807/2000000000000000000000000000000000000000", + "log_lower": "66795757798711164246196486467/15625000000000000000000000000", + "log_upper": "4274928499117514511756575133889/1000000000000000000000000000000", + "weight": "2308672/1714397575" + }, + "9": { + "exp_lower": "10002121682438781438362153684387409255829/10000000000000000000000000000000000000000", + "exp_upper": "5001060841219390719181076842193704883139/5000000000000000000000000000000000000000", + "log_lower": "4157145463461131057217781024417/1000000000000000000000000000000", + "log_upper": "2078572731730565528608890512209/500000000000000000000000000000", + "weight": "4279437/3428795150" + } + }, + "upper": "77927162499999999997721171959807016237352035261/77927162500000000000000000000000000000000000000" + }, + "binary_search_steps": 46, + "bit_saving": "5103158916233/100000000000000000", + "coarse_grid_control": { + "assembly": { + "absorption_gap": "147772050946704450795209/25001275789499997448421000000000000", + "constraints": { + "K_dominates_log": "1275789506246172631493752551579/25001275789499997448421000000000000", + "K_geometry": "18751275789506247448421/25001275789499997448421000000000000", + "a_below_b": "1033421/50000000000", + "a_positive": "2551579/50000000000", + "alpha_below_one": "49999999999975001275789499997448421/50002551578999994896842000000000000", + "alpha_below_one_fourth": "12498086315725005103157999997448421/50002551578999994896842000000000000", + "alpha_positive": "2551579024993621052500002551579/50002551578999994896842000000000000", + "artificial_boundary": "1400081650528274840526312499992345263/200010206315999979587368000000000000", + "b_below_one_over32": "311783/10000000", + "beta_below_one": "19/20", + "beta_positive": "1/20", + "c_below_one": "24998724210493752551579/25000000000000000000000", + "c_positive": "1275789506247448421/25000000000000000000000", + "cell_above_band": "49999999999924998724210500002551579/100005103157999989793684000000000000", + "compact_leaf": "427085500002551579/25000000000000000000000", + "compact_reservations": "1/4000000000000", + "delta_below_one_eighth": "999999999999/8000000000000", + "delta_positive": "1/8000000000000", + "epsilon_below_one": "1275789524997448421/25001275789499997448421", + "epsilon_positive": "24999999999975000000000/25001275789499997448421", + "g1_above_kappa": "17277332673620444824363/2500127578949999744842100000000000", + "g2_above_kappa": "261/100000000000", + "g3_above_kappa": "147772050946704450795209/25001275789499997448421000000000000", + "g4_above_kappa": "261/100000000000", + "g5_above_kappa": "251436046988427119741387/40002041263199995917473600000000000", + "g6_above_kappa": "1357185338100135588500619/200010206315999979587368000000000000", + "g7_above_kappa": "2499872421062277587831520444824363/2500127578949999744842100000000000", + "gamma_sublinear": "1/2000000000000", + "guard_width": "1275789524997448421/25001275789499997448421", + "lambda_above_internal": "2551579/50000000000000000000000", + "lambda_above_sigma": "1033421000002551579/50000000000000000000000", + "lambda_above_tau": "2551579/50000000000000000000000", + "lambda_prime_above_lambda": "2551579/50000000000000000000000", + "lambda_prime_below_one": "1275789499997448421/25000000000000000000000", + "literal_scalar_guard": "9693793493753822316795466474748", + "phase_boundary": "2041263214994641684100002551579/40002041263199995917473600000000000", + "phase_leaf_above_bit": "854171/50000000000", + "phase_local": "10206316174978311578500002551579/200010206315999979587368000000000000", + "prime_interval_packing": "1275789524997448421/25001275789499997448421", + "q_below_internal": "2551579/25000000000000000000000", + "q_below_leaf": "427085500002551579/25000000000000000000000", + "q_below_reservations": "1/4000000000000", + "q_positive": "1275789499997448421/25000000000000000000000", + "record_suffix": "1275789524997448421/25001275789499997448421", + "row_product_gap": "6548/25", + "short_record_fallback": "1249936207268472303386010555393241/1250063789474999872421050000000000", + "small_field_exposure": "1/1000000000000" + }, + "finite_bridge": { + "bit": { + "W": 137151806, + "halving_degree": 9, + "m": 575, + "maxchild": 529, + "wire_bits": 28 + }, + "complex": { + "W": 537696432, + "halving_degree": 20, + "m": 784, + "maxchild": 756, + "s": 421548223824, + "scalar_group_upper": 4793351472, + "wire_bits": 30 + }, + "rows": { + "coefficient": 852, + "degree": 2000, + "degree_gap": "6548/25", + "suffix_slope": 8000 + }, + "semantic": { + "B": 9696565176891520488614054257040, + "C0": 2358858462850846165593256368932965330169899180021667007021321420800, + "C1": 1, + "E": 9696565176891520488192506033216, + "induction_gap": 533311084729033626873772984137200, + "literal_charge": 2771683137698171397039558468, + "strict_literal_gap": 9693793493753822316795466474748 + } + }, + "margins": { + "g1": "1275789524997448421/25001275789499997448421", + "g2": "2551579/50000000000", + "g3": "1275789499996172631500002551579/25001275789499997448421000000000000", + "g4": "2551579/50000000000", + "g5": "2041263214994641684100002551579/40002041263199995917473600000000000", + "g6": "10206316174978311578500002551579/200010206315999979587368000000000000", + "g7": "24999999999975000000000/25001275789499997448421" + }, + "minimum_margin": "1275789499996172631500002551579/25001275789499997448421000000000000", + "parameters": { + "C0": 2358858462850846165593256368932965330169899180021667007021321420800, + "C1": "1", + "a_bit": "2551579/50000000000", + "a_complex": "717/10000000", + "alpha_squared_power": "2551579024993621052500002551579/50002551578999994896842000000000000", + "beta": "1/20", + "c": "1275789506247448421/25000000000000000000000", + "delta": "1/8000000000000", + "epsilon": "24999999999975000000000/25001275789499997448421", + "h": "1/1000000000000", + "kappa": "5102897/100000000000", + "lambda_": "49997448421000002551579/50000000000000000000000", + "lambda_prime": "24998724210500002551579/25000000000000000000000", + "q": "1275789499997448421/25000000000000000000000", + "sigma": "9999283/10000000", + "tau": "49997448421/50000000000" + }, + "recurrence": { + "internal": "49997448421/50000000000", + "leaf": "199986377/200000000", + "reservations": "24998724210493752551579/25000000000000000000000" + }, + "scoped_limit": "2551579/50002551579" + }, + "bit_saving": "2551579/50000000000", + "eventual_bounds": { + "additional_eventual_conditions": [ + "BHP prime threshold and distinct-prime packing", + "Fixed rational basis, eligible common prime and native table setup", + "Catalogue/descriptor domination, logarithm absorption, exact recovery" + ], + "all_interval_argument": "For [Z,Z+k), bound RHS at Z+k and LHS at floor(Z/k). Successive intervals double LHS; the positive affine RHS grows at most linearly, so 2^j >= j+1 proves persistence.", + "common_cutoff": 14000000000000, + "cutoff_log2_input": { + "alpha": 6144678545, + "compact": 24578714177, + "geometry": 3999931962522, + "guard": 4350470, + "log_p": 25, + "normalization": 14000000000000, + "period": 49157428353, + "phase_cell": 19, + "reservoir": 14, + "stopped_leaf": 252 + }, + "power_checkpoints": [ + { + "log2_input": 14000000000000, + "powers": { + "alpha": { + "exponent": 714395060, + "rhs": 112000000156840, + "rhs_bits": 47 + }, + "compact": { + "exponent": 714395060, + "rhs": 448000000627296, + "rhs_bits": 49 + }, + "leaf": { + "exponent": 666666666666, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 714395060, + "rhs": 224000000313608, + "rhs_bits": 48 + }, + "rows": { + "exponent": 714395060, + "rhs": 112000000156840000, + "rhs_bits": 57 + } + } + }, + { + "log2_input": 28000000000000, + "powers": { + "alpha": { + "exponent": 1428790120, + "rhs": 224000000156840, + "rhs_bits": 48 + }, + "compact": { + "exponent": 1428790120, + "rhs": 896000000627296, + "rhs_bits": 50 + }, + "leaf": { + "exponent": 1333333333333, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 1428790120, + "rhs": 448000000313608, + "rhs_bits": 49 + }, + "rows": { + "exponent": 1428790120, + "rhs": 224000000156840000, + "rhs_bits": 58 + } + } + }, + { + "log2_input": 56000000000000, + "powers": { + "alpha": { + "exponent": 2857580241, + "rhs": 448000000156840, + "rhs_bits": 49 + }, + "compact": { + "exponent": 2857580241, + "rhs": 1792000000627296, + "rhs_bits": 51 + }, + "leaf": { + "exponent": 2666666666666, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 2857580241, + "rhs": 896000000313608, + "rhs_bits": 50 + }, + "rows": { + "exponent": 2857580241, + "rhs": 448000000156840000, + "rhs_bits": 59 + } + } + }, + { + "log2_input": 112000000000000, + "powers": { + "alpha": { + "exponent": 5715160483, + "rhs": 896000000156840, + "rhs_bits": 50 + }, + "compact": { + "exponent": 5715160483, + "rhs": 3584000000627296, + "rhs_bits": 52 + }, + "leaf": { + "exponent": 5333333333333, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 5715160483, + "rhs": 1792000000313608, + "rhs_bits": 51 + }, + "rows": { + "exponent": 5715160483, + "rhs": 896000000156840000, + "rhs_bits": 60 + } + } + }, + { + "log2_input": 224000000000000, + "powers": { + "alpha": { + "exponent": 11430320967, + "rhs": 1792000000156840, + "rhs_bits": 51 + }, + "compact": { + "exponent": 11430320967, + "rhs": 7168000000627296, + "rhs_bits": 53 + }, + "leaf": { + "exponent": 10666666666666, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 11430320967, + "rhs": 3584000000313608, + "rhs_bits": 52 + }, + "rows": { + "exponent": 11430320967, + "rhs": 1792000000156840000, + "rhs_bits": 61 + } + } + }, + { + "log2_input": 448000000000000, + "powers": { + "alpha": { + "exponent": 22860641934, + "rhs": 3584000000156840, + "rhs_bits": 52 + }, + "compact": { + "exponent": 22860641934, + "rhs": 14336000000627296, + "rhs_bits": 54 + }, + "leaf": { + "exponent": 21333333333333, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 22860641934, + "rhs": 7168000000313608, + "rhs_bits": 53 + }, + "rows": { + "exponent": 22860641934, + "rhs": 3584000000156840000, + "rhs_bits": 62 + } + } + } + ], + "practical_runtime_claim": false + }, + "kappa": "5102897/100000000000", + "next_kappa": "2551449/50000000000", + "next_kappa_rejection": "{'g1_above_kappa': '-3861971557939776312029/1250063789474999872421050000000000', 'g3_above_kappa': '-102240706948295523689001/25001275789499997448421000000000000', 'g5_above_kappa': '-148584365643572839433349/40002041263199995917473600000000000', 'g6_above_kappa': '-642916725059864207373061/200010206315999979587368000000000000'}", + "original_enclosure_control": { + "accepted_upper": "31414992474181823539041702638067726953223056746772774820280620883954624480305519031745809764132994753882959208071327673451891977500917359580739448204316627613266780596935363578879651608348551002554602192748716268528516725933970431888266732694392744516294938417364990394615459496174135452875261376547601026472470226550667164245213471672673356552873415990292886450680769855783208863391794669086641914987931788023468477730670510596084024075441538328713023339916398705498355221133970083432695259402733395827765524378869634877859432717500503762008141825929233798931167008254709475368374051508388865497584191790219342658185334902048023058803459831350043847989335813486544496037300755940307394107652855486456896566575748317602547494848406247443162533947105245390168398328016459797877468285152634495601980504971432647153838327703599916923129770537527763252079817632121422808367288976061726138191284657279243722541218532065785928083475110872929968618380998934997039362092148018713422246239745551881230117940054196601787013559986011292764417361901016082566421251251012796046354407091934611225772748232290671622065318731567021326655644433/31414992474313928708180677874523621352103556206396664915326573931249860477582831911222317820380827856642039713344072149134147290838751531190936044695701314916811987072594709057045214808187944535470830707987621606984629316990440314337928054373375239756786622747536638358910194874324537834871658829915196615134159915111843176058062858398672677319063507082132196557150809134463687646912815011944937916567827230684945134911902541741913908828373190059709863602873297351619699439315502609902441966270292307166646440080416271209577604712655987561111810454673336732766552145593680695393728809448293097946140834850551963984106408521113636519343699470563400737447659076590127108692675420700718486850662726460389191754854035249509438356371913439956070892922708754251914760229957817430459967799146328317903978512043261923216018417388785375175312052564481508758456363897794780826879543255296865094989354227737926374713389566671431655092360096234539036355176207671348640178309523607871939963595335502695552839476616785591517423577290524646680111733605065635354851433706404171727955918218555419921577500000000000000000000000000000000000000000", + "next_bit_lower": "83629150000032150841840339335260391704594576990920669747612543458292027591267047206938392674041113125970424391021640961919112939837/83629150000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + } + }, + "comparison": { + "additional_precision_gain": "602879/40000000000000000", + "difference": "56602879/40000000000000000", + "kappa": "2041159402879/40000000000000000", + "pr63_kappa": "5102757/100000000000", + "structural_gain_on_original_grid": "7/5000000000" + }, + "grid_denominator": 1000000000000000000, + "next_bit_saving": "51031589162331/1000000000000000000", + "preferred": { + "assembly": { + "absorption_gap": "693483857012977651709354807/2000102063178324455873643350680000000000000000", + "constraints": { + "K_dominates_log": "150092910035814427153715035479936249/2941326563497535964520063751000000000000", + "K_geometry": "37502551579470611396841083767/50002551579458111396841083767000000000000", + "a_below_b": "2066841083767/100000000000000000", + "a_positive": "5103158916233/100000000000000000", + "alpha_below_one": "99999999999950002551579458111396841083767/100005103158916222793682167534000000000000", + "alpha_below_one_fourth": "24996172630762835456317832460896841083767/100005103158916222793682167534000000000000", + "alpha_positive": "5103158966220242102709422603158916233/100005103158916222793682167534000000000000", + "artificial_boundary": "2800163301085869137052567735422190523251301/400020412635664891174728670136000000000000", + "b_below_one_over32": "311783/10000000", + "beta_below_one": "19/20", + "beta_positive": "1/20", + "c_below_one": "49997448420529388603158916233/50000000000000000000000000000", + "c_positive": "2551579470611396841083767/50000000000000000000000000000", + "cell_above_band": "99999999999849997448420541888603158916233/200010206317832445587364335068000000000000", + "compact_leaf": "854170541888603158916233/50000000000000000000000000000", + "compact_reservations": "1/4000000000000", + "delta_below_one_eighth": "999999999999/8000000000000", + "delta_positive": "1/8000000000000", + "epsilon_below_one": "2551579508111396841083767/50002551579458111396841083767", + "epsilon_positive": "49999999999950000000000000000/50002551579458111396841083767", + "g1_above_kappa": "2000102756662181468851295060034807/2000102063178324455873643350680000000000000000", + "g2_above_kappa": "520818071/200000000000000000", + "g3_above_kappa": "693483857012977651709354807/2000102063178324455873643350680000000000000000", + "g4_above_kappa": "520818071/200000000000000000", + "g5_above_kappa": "750038967175728683930267965859807/2000102063178324455873643350680000000000000000", + "g6_above_kappa": "1750089998764890911867089641199807/2000102063178324455873643350680000000000000000", + "g7_above_kappa": "1999897936819675646883018830788851295060034807/2000102063178324455873643350680000000000000000", + "gamma_sublinear": "1/2000000000000", + "guard_width": "2551579508111396841083767/50002551579458111396841083767", + "lambda_above_internal": "5103158916233/100000000000000000000000000000", + "lambda_above_sigma": "2066841083772103158916233/100000000000000000000000000000", + "lambda_above_tau": "5103158916233/100000000000000000000000000000", + "lambda_prime_above_lambda": "5103158916233/100000000000000000000000000000", + "lambda_prime_below_one": "2551579458111396841083767/50000000000000000000000000000", + "literal_scalar_guard": "9693793493753822316795466474748", + "phase_boundary": "4082527162975683366275915803158916233/80004082527132978234945734027200000000000", + "phase_leaf_above_bit": "1708341083767/100000000000000000", + "phase_local": "20412636014888623149212024603158916233/400020412635664891174728670136000000000000", + "prime_interval_packing": "2551579508111396841083767/50002551579458111396841083767", + "q_below_internal": "5103158916233/50000000000000000000000000000", + "q_below_leaf": "854170541888603158916233/50000000000000000000000000000", + "q_below_reservations": "1/4000000000000", + "q_positive": "2551579458111396841083767/50000000000000000000000000000", + "record_suffix": "2551579508111396841083767/50002551579458111396841083767", + "row_product_gap": "6548/25", + "short_record_fallback": "4999744829028072887861858675469183867110910289/5000255157945811139684108376700000000000000000", + "small_field_exposure": "1/1000000000000" + }, + "finite_bridge": { + "bit": { + "W": 137151806, + "halving_degree": 9, + "m": 575, + "maxchild": 529, + "wire_bits": 28 + }, + "complex": { + "W": 537696432, + "halving_degree": 20, + "m": 784, + "maxchild": 756, + "s": 421548223824, + "scalar_group_upper": 4793351472, + "wire_bits": 30 + }, + "rows": { + "coefficient": 852, + "degree": 2000, + "degree_gap": "6548/25", + "suffix_slope": 8000 + }, + "semantic": { + "B": 9696565176891520488614054257040, + "C0": 2358858462850846165593256368932965330169899180021667007021321420800, + "C1": 1, + "E": 9696565176891520488192506033216, + "induction_gap": 533311084729033626873772984137200, + "literal_charge": 2771683137698171397039558468, + "strict_literal_gap": 9693793493753822316795466474748 + } + }, + "margins": { + "g1": "2551579508111396841083767/50002551579458111396841083767", + "g2": "5103158916233/100000000000000000", + "g3": "2551579458108845261625655603158916233/50002551579458111396841083767000000000000", + "g4": "5103158916233/100000000000000000", + "g5": "4082527162975683366275915803158916233/80004082527132978234945734027200000000000", + "g6": "20412636014888623149212024603158916233/400020412635664891174728670136000000000000", + "g7": "49999999999950000000000000000/50002551579458111396841083767" + }, + "minimum_margin": "2551579458108845261625655603158916233/50002551579458111396841083767000000000000", + "parameters": { + "C0": 2358858462850846165593256368932965330169899180021667007021321420800, + "C1": "1", + "a_bit": "5103158916233/100000000000000000", + "a_complex": "717/10000000", + "alpha_squared_power": "5103158966220242102709422603158916233/100005103158916222793682167534000000000000", + "beta": "1/20", + "c": "2551579470611396841083767/50000000000000000000000000000", + "delta": "1/8000000000000", + "epsilon": "49999999999950000000000000000/50002551579458111396841083767", + "h": "1/1000000000000", + "kappa": "2041159402879/40000000000000000", + "lambda_": "99994896841083772103158916233/100000000000000000000000000000", + "lambda_prime": "49997448420541888603158916233/50000000000000000000000000000", + "q": "2551579458111396841083767/50000000000000000000000000000", + "sigma": "9999283/10000000", + "tau": "99994896841083767/100000000000000000" + }, + "recurrence": { + "internal": "99994896841083767/100000000000000000", + "leaf": "199986377/200000000", + "reservations": "49997448420529388603158916233/50000000000000000000000000000" + }, + "scoped_limit": "5103158916233/100005103158916233" + }, + "eventual_bounds": { + "additional_eventual_conditions": [ + "BHP prime threshold and distinct-prime packing", + "Fixed rational basis, eligible common prime and native table setup", + "Catalogue/descriptor domination, logarithm absorption, exact recovery" + ], + "all_interval_argument": "For [Z,Z+k), bound RHS at Z+k and LHS at floor(Z/k). Successive intervals double LHS; the positive affine RHS grows at most linearly, so 2^j >= j+1 proves persistence.", + "common_cutoff": 14000000000000, + "cutoff_log2_input": { + "alpha": 6144678545, + "compact": 24578714177, + "geometry": 3999931962510, + "guard": 4350469, + "log_p": 25, + "normalization": 14000000000000, + "period": 49157428353, + "phase_cell": 19, + "reservoir": 14, + "stopped_leaf": 252 + }, + "power_checkpoints": [ + { + "log2_input": 14000000000000, + "powers": { + "alpha": { + "exponent": 714395060, + "rhs": 112000000156840, + "rhs_bits": 47 + }, + "compact": { + "exponent": 714395060, + "rhs": 448000000627296, + "rhs_bits": 49 + }, + "leaf": { + "exponent": 666666666666, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 714395060, + "rhs": 224000000313608, + "rhs_bits": 48 + }, + "rows": { + "exponent": 714395060, + "rhs": 112000000156840000, + "rhs_bits": 57 + } + } + }, + { + "log2_input": 28000000000000, + "powers": { + "alpha": { + "exponent": 1428790120, + "rhs": 224000000156840, + "rhs_bits": 48 + }, + "compact": { + "exponent": 1428790120, + "rhs": 896000000627296, + "rhs_bits": 50 + }, + "leaf": { + "exponent": 1333333333333, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 1428790120, + "rhs": 448000000313608, + "rhs_bits": 49 + }, + "rows": { + "exponent": 1428790120, + "rhs": 224000000156840000, + "rhs_bits": 58 + } + } + }, + { + "log2_input": 56000000000000, + "powers": { + "alpha": { + "exponent": 2857580241, + "rhs": 448000000156840, + "rhs_bits": 49 + }, + "compact": { + "exponent": 2857580241, + "rhs": 1792000000627296, + "rhs_bits": 51 + }, + "leaf": { + "exponent": 2666666666666, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 2857580241, + "rhs": 896000000313608, + "rhs_bits": 50 + }, + "rows": { + "exponent": 2857580241, + "rhs": 448000000156840000, + "rhs_bits": 59 + } + } + }, + { + "log2_input": 112000000000000, + "powers": { + "alpha": { + "exponent": 5715160483, + "rhs": 896000000156840, + "rhs_bits": 50 + }, + "compact": { + "exponent": 5715160483, + "rhs": 3584000000627296, + "rhs_bits": 52 + }, + "leaf": { + "exponent": 5333333333333, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 5715160483, + "rhs": 1792000000313608, + "rhs_bits": 51 + }, + "rows": { + "exponent": 5715160483, + "rhs": 896000000156840000, + "rhs_bits": 60 + } + } + }, + { + "log2_input": 224000000000000, + "powers": { + "alpha": { + "exponent": 11430320967, + "rhs": 1792000000156840, + "rhs_bits": 51 + }, + "compact": { + "exponent": 11430320967, + "rhs": 7168000000627296, + "rhs_bits": 53 + }, + "leaf": { + "exponent": 10666666666666, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 11430320967, + "rhs": 3584000000313608, + "rhs_bits": 52 + }, + "rows": { + "exponent": 11430320967, + "rhs": 1792000000156840000, + "rhs_bits": 61 + } + } + }, + { + "log2_input": 448000000000000, + "powers": { + "alpha": { + "exponent": 22860641934, + "rhs": 3584000000156840, + "rhs_bits": 52 + }, + "compact": { + "exponent": 22860641934, + "rhs": 14336000000627296, + "rhs_bits": 54 + }, + "leaf": { + "exponent": 21333333333333, + "rhs": 3136, + "rhs_bits": 12 + }, + "period": { + "exponent": 22860641934, + "rhs": 7168000000313608, + "rhs_bits": 53 + }, + "rows": { + "exponent": 22860641934, + "rhs": 3584000000156840000, + "rhs_bits": 62 + } + } + } + ], + "practical_runtime_claim": false + }, + "kappa": "2041159402879/40000000000000000", + "next_kappa": "6378623133997/125000000000000000", + "next_kappa_rejection": "{'g3_above_kappa': '-4083181894266708763013401699/6250318947432263924605135470875000000000000000'}" + }, + "profile_path": "research/reordered-rank-pair/paired-candidate.json", + "profile_sha256": "34a500d739537235dfc5d24325c22856ca4567b9eac998a3bce9b13db5501940", + "proof_limits": [ + "The complete physical profile is supplied; independent word and CRT replay are parent-verifier responsibilities.", + "The rational logarithm and exponential enclosure derivations are documented in README.md, not formally mechanized.", + "All-size compiler, routing, recovery, prime-selection and fixed-tape transfer remain inherited.", + "Neither global optimality nor measured practical speedup is claimed." + ], + "rejected_moment": { + "degree": 8, + "lower": "8571987875000000003683551653063012975552828889113/8571987875000000000000000000000000000000000000000", + "rounding_denominator": 10000000000000000000000000000000000000000, + "saving": "51031589162331/1000000000000000000", + "strict_gap": "-920887913265753353254538048853/2142996968750000000000000000000000000000000000000", + "terms": { + "1": { + "exp_lower": "2000648652367350369920582377063597092877/2000000000000000000000000000000000000000", + "exp_upper": "250081081545918796240072797132949649399/250000000000000000000000000000000000000", + "log_lower": "3177185020398675220004135749131/500000000000000000000000000000", + "log_upper": "6354370040797350440008271498263/1000000000000000000000000000000", + "weight": "61988/2833715" + }, + "10": { + "exp_lower": "1250258488003773316649758574168230193791/1250000000000000000000000000000000000000", + "exp_upper": "10002067904030186533198068593345842060769/10000000000000000000000000000000000000000", + "log_lower": "2025892473901652377995140021789/500000000000000000000000000000", + "log_upper": "4051784947803304755990280043579/1000000000000000000000000000000", + "weight": "7053/6234173" + }, + "11": { + "exp_lower": "2500504813947793463812319247263927798241/2500000000000000000000000000000000000000", + "exp_upper": "10002019255791173855249276989055711703399/10000000000000000000000000000000000000000", + "log_lower": "3956474767998979895946327920297/1000000000000000000000000000000", + "log_upper": "1978237383999489947973163960149/500000000000000000000000000000", + "weight": "34143/28337150" + }, + "12": { + "exp_lower": "5000987421817593325520461283451770998243/5000000000000000000000000000000000000000", + "exp_upper": "2500493710908796662760230641725885626729/2500000000000000000000000000000000000000", + "log_lower": "3869463391009350129778562018423/1000000000000000000000000000000", + "log_upper": "483682923876168766222320252303/125000000000000000000000000000", + "weight": "1637772/1714397575" + }, + "13": { + "exp_lower": "10001933988586236008494783943791019880507/10000000000000000000000000000000000000000", + "exp_upper": "10001933988586236008494783943791020390933/10000000000000000000000000000000000000000", + "log_lower": "3789420683335813703954784056697/1000000000000000000000000000000", + "log_upper": "1894710341667906851977392028349/500000000000000000000000000000", + "weight": "3064763/3428795150" + }, + "14": { + "exp_lower": "2000379232573565102261303916827906717827/2000000000000000000000000000000000000000", + "exp_upper": "5000948081433912755653259792069767049779/5000000000000000000000000000000000000000", + "log_lower": "3715312711182091825485686633361/1000000000000000000000000000000", + "log_upper": "1857656355591045912742843316681/500000000000000000000000000000", + "weight": "1222116/1714397575" + }, + "15": { + "exp_lower": "80014887584760392596283449051250475889/80000000000000000000000000000000000000", + "exp_upper": "4883721166062035680925503482131987303/4882812500000000000000000000000000000", + "log_lower": "3646319839695140374012266928113/1000000000000000000000000000000", + "log_upper": "1823159919847570187006133464057/500000000000000000000000000000", + "weight": "437037/685759030" + }, + "16": { + "exp_lower": "2500457001746824468472043338830729543989/2500000000000000000000000000000000000000", + "exp_upper": "10001828006987297873888173355322918686373/10000000000000000000000000000000000000000", + "log_lower": "3581781318557569202339343012429/1000000000000000000000000000000", + "log_upper": "358178131855756920233934301243/100000000000000000000000000000", + "weight": "65416/155854325" + }, + "17": { + "exp_lower": "5000898531835896226815436415768443842763/5000000000000000000000000000000000000000", + "exp_upper": "500089853183589622681543641576844409797/500000000000000000000000000000000000000", + "log_lower": "3521156696741134359758736880389/1000000000000000000000000000000", + "log_upper": "352115669674113435975873688039/100000000000000000000000000000", + "weight": "1423053/685759030" + }, + "18": { + "exp_lower": "10001767889625591115934073106937856632037/10000000000000000000000000000000000000000", + "exp_upper": "10001767889625591115934073106937857142449/10000000000000000000000000000000000000000", + "log_lower": "3463998282901185747800548902959/1000000000000000000000000000000", + "log_upper": "43299978536264821847506861287/12500000000000000000000000000", + "weight": "73188/342879515" + }, + "19": { + "exp_lower": "10001740293423583533901264128804098082667/10000000000000000000000000000000000000000", + "exp_upper": "10001740293423583533901264128804098593077/10000000000000000000000000000000000000000", + "log_lower": "1704965530815454989999622033187/500000000000000000000000000000", + "log_upper": "27279448493047279839993952531/8000000000000000000000000000", + "weight": "24073/311708650" + }, + "2": { + "exp_lower": "10002889429351305636019653150309302953393/10000000000000000000000000000000000000000", + "exp_upper": "2500722357337826409004913287577325866061/2500000000000000000000000000000000000000", + "log_lower": "1415305715059351282647759844201/250000000000000000000000000000", + "log_upper": "1132244572047481026118207875361/200000000000000000000000000000", + "weight": "3622866/1714397575" + }, + "20": { + "exp_lower": "312553566034976063165496853081160074831/312500000000000000000000000000000000000", + "exp_upper": "2000342822623846804259179859719424581/2000000000000000000000000000000000000", + "log_lower": "83965944181083986164326198053/25000000000000000000000000000", + "log_upper": "3358637767243359446573047922121/1000000000000000000000000000000", + "weight": "26402/342879515" + }, + "21": { + "exp_lower": "2500422302621559624579253655476377600133/2500000000000000000000000000000000000000", + "exp_upper": "5000844605243119249158507310952755455469/5000000000000000000000000000000000000000", + "log_lower": "413730950384240930438459189737/125000000000000000000000000000", + "log_upper": "3309847603073927443507673517897/1000000000000000000000000000000", + "weight": "12978/2981561" + }, + "22": { + "exp_lower": "2500416366650248995829722405840081230591/2500000000000000000000000000000000000000", + "exp_upper": "10001665466600995983318889623360325432769/10000000000000000000000000000000000000000", + "log_lower": "3263327587439034586529095798839/1000000000000000000000000000000", + "log_upper": "81583189685975864663227394971/25000000000000000000000000000", + "weight": "77/2833715" + }, + "23": { + "exp_lower": "2500410694601965254792573914274872537973/2500000000000000000000000000000000000000", + "exp_upper": "2000328555681572203834059131419898132459/2000000000000000000000000000000000000000", + "log_lower": "804718956217050187300379666613/250000000000000000000000000000", + "log_upper": "3218875824868200749201518666453/1000000000000000000000000000000", + "weight": "11447/542102" + }, + "25": { + "exp_lower": "10001600220548114404645707602572389258573/10000000000000000000000000000000000000000", + "exp_upper": "10001600220548114404645707602572389768973/10000000000000000000000000000000000000000", + "log_lower": "313549421592914969080675283181/100000000000000000000000000000", + "log_upper": "3135494215929149690806752831811/1000000000000000000000000000000", + "weight": "11641/566743" + }, + "3": { + "exp_lower": "10002682456417729184276588504835870946771/10000000000000000000000000000000000000000", + "exp_upper": "5001341228208864592138294252417935728711/5000000000000000000000000000000000000000", + "log_lower": "262787887606462037430651313067/50000000000000000000000000000", + "log_upper": "5255757752129240748613026261341/1000000000000000000000000000000", + "weight": "5956407/3428795150" + }, + "4": { + "exp_lower": "10002535609381543034238987146257411071669/10000000000000000000000000000000000000000", + "exp_upper": "2000507121876308606847797429251482316447/2000000000000000000000000000000000000000", + "log_lower": "2484037839838729910586903627673/500000000000000000000000000000", + "log_upper": "4968075679677459821173807255347/1000000000000000000000000000000", + "weight": "95648/74539025" + }, + "481": { + "exp_lower": "10000091093215478885322140431537484956017/10000000000000000000000000000000000000000", + "exp_upper": "10000091093215478885322140431537485466339/10000000000000000000000000000000000000000", + "log_lower": "35700554138317851917337677133/200000000000000000000000000000", + "log_upper": "89251385345794629793344192833/500000000000000000000000000000", + "weight": "13468/271051" + }, + "5": { + "exp_lower": "10002421707455794758806902349921645317387/10000000000000000000000000000000000000000", + "exp_upper": "5001210853727897379403451174960822913953/5000000000000000000000000000000000000000", + "log_lower": "1186233032090812516351878041259/250000000000000000000000000000", + "log_upper": "4744932128363250065407512165037/1000000000000000000000000000000", + "weight": "171439/137151806" + }, + "525": { + "exp_lower": "10000046424451868766467449616668560743529/10000000000000000000000000000000000000000", + "exp_upper": "10000046424451868766467449616668561253849/10000000000000000000000000000000000000000", + "log_lower": "22742944551431673576538712861/250000000000000000000000000000", + "log_upper": "18194355641145338861230970289/200000000000000000000000000000", + "weight": "244461/566743" + }, + "529": { + "exp_lower": "10000042551050640056717053215833107892989/10000000000000000000000000000000000000000", + "exp_upper": "2500010637762660014179263303958277100827/2500000000000000000000000000000000000000", + "log_lower": "41690804469525529197382917321/500000000000000000000000000000", + "log_upper": "83381608939051058394765834643/1000000000000000000000000000000", + "weight": "116748/271051" + }, + "6": { + "exp_lower": "5001164321884483470566959992315705168419/5000000000000000000000000000000000000000", + "exp_upper": "10002328643768966941133919984631410847329/10000000000000000000000000000000000000000", + "log_lower": "4562610571569295439195794139881/1000000000000000000000000000000", + "log_upper": "2281305285784647719597897069941/500000000000000000000000000000", + "weight": "97752/68575903" + }, + "7": { + "exp_lower": "10002249960218428833500870239874329437677/10000000000000000000000000000000000000000", + "exp_upper": "200044999204368576670017404797486598963/200000000000000000000000000000000000000", + "log_lower": "4408459891742037134902918754819/1000000000000000000000000000000", + "log_upper": "220422994587101856745145937741/50000000000000000000000000000", + "weight": "8995/5963122" + }, + "8": { + "exp_lower": "4000872720770808536918724056383927967/4000000000000000000000000000000000000", + "exp_upper": "10002181801927021342296810140959820427959/10000000000000000000000000000000000000000", + "log_lower": "66795757798711164246196486467/15625000000000000000000000000", + "log_upper": "4274928499117514511756575133889/1000000000000000000000000000000", + "weight": "2308672/1714397575" + }, + "9": { + "exp_lower": "2500530420609695369985607115381001329959/2500000000000000000000000000000000000000", + "exp_upper": "5001060841219390739971214230762002915143/5000000000000000000000000000000000000000", + "log_lower": "4157145463461131057217781024417/1000000000000000000000000000000", + "log_upper": "2078572731730565528608890512209/500000000000000000000000000000", + "weight": "4279437/3428795150" + } + }, + "upper": "2142996968750000000920887913265753353254538048853/2142996968750000000000000000000000000000000000000" + }, + "source_sha256": { + "references/frame-compiler/pr48/research/copied-fixed/balanced_assembly.py": "4d27575dcad2b45a281a34054d311409ecd954f373c0c3a62c29bcc843f06a86", + "research/reordered-rank-pair/arithmetic/audit.py": "aa297fffcdaa133f5dee17d97fac72aa5ba2cf943da5a8a5e3f4d62f6f0a7f79", + "research/reordered-rank-pair/arithmetic/refine.py": "e0488c919e76850313ff93d7da704a7fcc14a316eee2cac81e2b8dff9c145b5d", + "scripts/experiments/binary_frame_math.py": "1f96e8aafc8ae89f8eeec5d03800131d93d58e01bf8a7fca8feb03702d1740d0" + }, + "status": "Exact finite conditional screen; physical linkage checked by parent verifier" +} diff --git a/research/reordered-rank-pair/arithmetic/refine.py b/research/reordered-rank-pair/arithmetic/refine.py new file mode 100644 index 0000000000..399299089e --- /dev/null +++ b/research/reordered-rank-pair/arithmetic/refine.py @@ -0,0 +1,162 @@ +#!/usr/bin/env python3 +"""Exact arithmetic screen of the reordered rank-pair complete physical profile. + +Uses PR63's paid profile, inherited PR48 logarithm enclosures and balanced +assembly (PR34 and successors). New directed Taylor bounds are documented in +this file. Prepared with OpenAI assistance. Inherited licenses apply. +Physical linkage is checked by the parent verifier; no full theorem or practical speedup claim is implied. +""" +import sys +sys.dont_write_bytecode = True +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') +import argparse +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import json +from math import factorial +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[3] +sys.path.insert(0, str(ROOT/'scripts/experiments')) +import binary_frame_math as arithmetic +spec = importlib.util.spec_from_file_location('inherited_assembly', ROOT/'references/frame-compiler/pr48/research/copied-fixed/balanced_assembly.py') +balanced = importlib.util.module_from_spec(spec) +spec.loader.exec_module(balanced) + + +def floor_scaled(x, denominator): + return (x * denominator).numerator // (x * denominator).denominator + + +def ceiling_scaled(x, denominator): + return -floor_scaled(-x, denominator) + + +def exact_moment(m, width, rows, saving, degree=8, rounding=10**40): + """Bound sum n*t/(mW)*exp(saving*log(m/t)) entirely in Q. + + At 0 <= u <= v < 1, S_d(u) is a lower bound for exp(u). + The tail at v has first term v^(d+1)/(d+1)!; successive ratios + are at most v/(d+2). Thus S_d(v)+first/(1-v/(d+2)) is upper. + Directed rounding per exp bound preserves both inequalities. + The inherited logarithm helper encloses log(m/t) rationally. + """ + assert type(saving) is Q and 0 < saving < 1 and degree >= 1 + lo, hi = Q(), Q() + terms = {} + for t, count in sorted(rows.items()): + assert type(t) is int and type(count) is int and 0 < t < m and count > 0 + loglo, loghi = arithmetic.logs(Q(m, t)) + u, v = saving*loglo, saving*loghi + assert 0 <= u <= v < 1 + lower = sum((u**j / factorial(j) for j in range(degree+1)), Q()) + upper = sum((v**j / factorial(j) for j in range(degree+1)), Q()) + upper += v**(degree+1)/factorial(degree+1)/(1-v/Q(degree+2)) + lower = Q(floor_scaled(lower, rounding), rounding) + upper = Q(ceiling_scaled(upper, rounding), rounding) + weight = Q(t*count, m*width) + lo += weight*lower + hi += weight*upper + terms[t] = dict(weight=weight, log_lower=loglo, log_upper=loghi, + exp_lower=lower, exp_upper=upper) + return dict(saving=saving, lower=lo, upper=hi, strict_gap=1-hi, + degree=degree, rounding_denominator=rounding, terms=terms) + + +def assemble(bridge, saving, h, denominator): + preliminary = balanced.assembly(bridge, saving, Q(1, denominator), h=h) + kappa = Q(ceiling_scaled(preliminary['minimum_margin'], denominator)-1, denominator) + accepted = balanced.assembly(bridge, saving, kappa, h=h) + assert len(accepted['constraints']) == 47 and len(accepted['margins']) == 7 + assert all(v > 0 for v in accepted['constraints'].values()) + assert all(v > kappa for v in accepted['margins'].values()) + try: + balanced.assembly(bridge, saving, kappa+Q(1, denominator), h=h) + except balanced.InvalidAssembly as error: + rejected = str(error) + else: + raise AssertionError('Next kappa grid unexpectedly passes') + return dict(kappa=kappa, assembly=accepted, + next_kappa=kappa+Q(1, denominator), next_kappa_rejection=rejected, + eventual_bounds=balanced.cutoffs(bridge, accepted)) + + +def build_certificate(profile_path, denominator=10**18, h=Q(1, 10**12)): + profile_path = profile_path.resolve() + source = json.loads(profile_path.read_text()) + profile = source['bit'] + bridge = source['finite_bridge'] + m, width = profile['m'], profile['W'] + rows = {int(t): n for t, n in profile['child_multiplicities'].items()} + assert sum(t*n for t, n in rows.items()) == profile['total_rank'] + assert bridge['bit']['W'] == width + low, high = 1, floor_scaled(Q(717, 10**7), denominator) + assert exact_moment(m, width, rows, Q(low, denominator))['upper'] < 1 + assert exact_moment(m, width, rows, Q(high, denominator))['lower'] > 1 + steps = 0 + while low+1 < high: + mid = (low+high)//2 + test = exact_moment(m, width, rows, Q(mid, denominator)) + if test['upper'] < 1: + low = mid + elif test['lower'] > 1: + high = mid + else: + raise ArithmeticError('Rational bounds inconclusive: increase enclosure precision') + steps += 1 + saving = Q(low, denominator) + accepted = exact_moment(m, width, rows, saving) + rejected = exact_moment(m, width, rows, Q(high, denominator)) + assert accepted['upper'] < 1 < rejected['lower'] + preferred = assemble(bridge, saving, h, denominator) + coarse_denom = 10**11 + coarse_bit = Q(floor_scaled(saving, coarse_denom), coarse_denom) + assert exact_moment(m, width, rows, coarse_bit)['upper'] < 1 + coarse = assemble(bridge, coarse_bit, h, coarse_denom) + inherited_coarse = arithmetic.moment(m, width, rows, coarse_bit) + inherited_next = arithmetic.moment(m, width, rows, coarse_bit+Q(1, coarse_denom)) + assert inherited_coarse['upper'] < 1 < inherited_next['lower'] + coarse['original_enclosure_control'] = dict(accepted_upper=inherited_coarse['upper'], + next_bit_lower=inherited_next['lower']) + # Same coarse grid/backoff as PR63 separates the structural gain from + # the additional precision refinement suggested by the PR61 precedent. + prior = Q(source['kappa']) + paths = (Path(__file__), Path(__file__).with_name('audit.py'), + ROOT/'scripts/experiments/binary_frame_math.py', Path(balanced.__file__)) + return dict(status='Exact finite conditional screen; physical linkage checked by parent verifier', + profile_path=str(profile_path.relative_to(ROOT)), + profile_sha256=sha256(profile_path.read_bytes()).hexdigest(), + source_sha256={str(path.relative_to(ROOT)):sha256(path.read_bytes()).hexdigest() for path in paths}, + grid_denominator=denominator, binary_search_steps=steps, bit_saving=saving, + next_bit_saving=Q(high, denominator), accepted_moment=accepted, rejected_moment=rejected, + preferred=preferred, coarse_grid_control=dict(bit_saving=coarse_bit, **coarse), + comparison=dict(pr63_kappa=prior, kappa=preferred['kappa'], + difference=preferred['kappa']-prior, + structural_gain_on_original_grid=coarse['kappa']-prior, + additional_precision_gain=preferred['kappa']-coarse['kappa']), + proof_limits=['The complete physical profile is supplied; independent word and CRT replay are parent-verifier responsibilities.', + 'The rational logarithm and exponential enclosure derivations are documented in README.md, not formally mechanized.', + 'All-size compiler, routing, recovery, prime-selection and fixed-tape transfer remain inherited.', + 'Neither global optimality nor measured practical speedup is claimed.']) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--profile', type=Path, default=Path(__file__).resolve().parent.parent/'paired-candidate.json') + parser.add_argument('--certificate', type=Path, default=Path(__file__).with_name('certificate.json')) + parser.add_argument('--record', action='store_true', help='Regenerate certificate instead of comparing with recorded result') + args = parser.parse_args() + result = arithmetic.js(build_certificate(args.profile)) + if args.record: + args.certificate.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + assert result == json.loads(args.certificate.read_text()), 'Arithmetic certificate changed' + print(json.dumps(dict(status='PASS exact arithmetic', bit_saving=result['bit_saving'], + kappa=result['preferred']['kappa'], constraints=47, margins=7, + next_grid_controls='PASS', comparison=result['comparison']), indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/reordered-rank-pair/arithmetic/test_arithmetic.py b/research/reordered-rank-pair/arithmetic/test_arithmetic.py new file mode 100644 index 0000000000..e23cba24ec --- /dev/null +++ b/research/reordered-rank-pair/arithmetic/test_arithmetic.py @@ -0,0 +1,68 @@ +"""Meaningful certificate verification and deliberate-failure controls.""" +import sys +sys.dont_write_bytecode = True +from copy import deepcopy +from fractions import Fraction as Q +import json +from pathlib import Path +import subprocess +import unittest + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import refine +import audit + + +class ExactArithmeticTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.certificate = json.loads((HERE/'certificate.json').read_text()) + cls.profile = json.loads((refine.ROOT/cls.certificate['profile_path']).read_text())['bit'] + + def test_complete_reproduction(self): + actual = refine.arithmetic.js(refine.build_certificate(refine.ROOT/self.certificate['profile_path'])) + self.assertEqual(actual, self.certificate) + + def test_independent_enclosures_and_controls(self): + actual = refine.arithmetic.js(audit.audit(self.certificate)) + self.assertEqual(actual, json.loads((HERE/'audit-receipt.json').read_text())) + self.assertEqual(len(actual['controls']), 10) + + def test_next_bit_grid_is_rejected(self): + p = self.profile + result = refine.exact_moment(p['m'], p['W'], {int(t):n for t,n in p['child_multiplicities'].items()}, Q(self.certificate['next_bit_saving'])) + self.assertGreater(result['lower'], 1) + + def test_forged_accepted_bit_is_rejected(self): + forged = deepcopy(self.certificate) + forged['bit_saving'] = forged['next_bit_saving'] + with self.assertRaises(AssertionError): + audit.audit(forged) + + def test_forged_source_digest_is_rejected(self): + forged = deepcopy(self.certificate) + forged['profile_sha256'] = '0'*64 + with self.assertRaises(AssertionError): + audit.audit(forged) + + def test_omitted_constraint_is_rejected(self): + forged = deepcopy(self.certificate) + del forged['preferred']['assembly']['constraints']['K_geometry'] + with self.assertRaises(AssertionError): + audit.audit(forged) + + def test_float_saving_refused(self): + with self.assertRaises(AssertionError): + refine.exact_moment(2, 1, {1:1}, 0.01) + + def test_python_optimization_is_rejected(self): + for script in ('refine.py', 'audit.py'): + result = subprocess.run([sys.executable, '-B', '-O', str(HERE/script)], + cwd=refine.ROOT, capture_output=True, text=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn('Assertions must remain enabled', result.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/reordered-rank-pair/current-comparison.json b/research/reordered-rank-pair/current-comparison.json new file mode 100644 index 0000000000..1d539de130 --- /dev/null +++ b/research/reordered-rank-pair/current-comparison.json @@ -0,0 +1,9 @@ +{ + "source_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/64", + "head": "790a14e28e935398072b9a9a68694ce7fba8940f", + "source": "PR body reported bound, checked 2026-10-08; not an independent audit of PR64", + "kappa": "2041159402879/40000000000000000", + "pr64_kappa": "20411033624901463/400000000000000000000", + "difference": "560403888537/400000000000000000000", + "relative_gain": "560403888537/20411033624901463" +} diff --git a/research/reordered-rank-pair/frame-compiler.json b/research/reordered-rank-pair/frame-compiler.json new file mode 100644 index 0000000000..f8fe913876 --- /dev/null +++ b/research/reordered-rank-pair/frame-compiler.json @@ -0,0 +1,200 @@ +{ + "artifact_sha256": { + "frame-profiles-23.json": "fec377bcf1512a427674983256b900229d4133026445b6e680c6e1e6dde5af7d", + "frame-profiles-25.json": "28b4b911e26fbc02dde0d2e1458ed16227f756126ab8144d6d45e164d1165262", + "frame-transitions-23.json": "86646f1110595294cccc15603c552f0a153574a690b69c3b144d84a449891103", + "frame-transitions-25.json": "c333c348665d12b95e168ca4fac48bfdca335104edd0f29c81fe94bec292e774", + "frame-word-23.json.gz": "a44e038e1c548ea8ac31dd04acc2bba7951b22e17df7b7ad3464ea2b504a8da4", + "frame-word-25.json.gz": "ad8b299697f90b185b6b791313b505586be97965519052100d097df6199e00c5", + "paired-candidate.json": "34a500d739537235dfc5d24325c22856ca4567b9eac998a3bce9b13db5501940" + }, + "axes": { + "23": { + "compiled": { + "all_physical_frame_inclusions": true, + "baseline_pr48_roles": 36432, + "complete_dirty_basis_both_orientations": true, + "dirty_basis_vectors": 31460, + "elementary_xors": 149137, + "h": 23, + "histogram": { + "0": 302057, + "1": 42694, + "10": 442, + "11": 11, + "12": 467, + "13": 22, + "14": 2005, + "15": 551, + "16": 547, + "17": 365, + "18": 4220, + "19": 7820, + "2": 82722, + "21": 165, + "22": 23, + "3": 11086, + "4": 10683, + "5": 7723, + "6": 1994, + "7": 294, + "8": 1362, + "9": 525 + }, + "mode": { + "matching": true, + "reclaim": true + }, + "rank_mass": 642620, + "roles": 27918, + "stats": { + "augmentations": 220, + "clearing_xors": 1577, + "matched": 37025, + "multi_node_regions": 10350, + "reclaimed": 801, + "regions": 52473 + } + }, + "gzip_sha256": "a44e038e1c548ea8ac31dd04acc2bba7951b22e17df7b7ad3464ea2b504a8da4", + "replay": { + "elementary_xors": 149137, + "full_basis_vectors": 31460, + "h": 23, + "histogram": { + "0": 162914, + "1": 42694, + "10": 442, + "11": 11, + "12": 467, + "13": 22, + "14": 2005, + "15": 551, + "16": 547, + "17": 365, + "18": 4220, + "19": 7820, + "2": 82722, + "21": 165, + "22": 23, + "3": 11086, + "4": 10683, + "5": 7723, + "6": 1994, + "7": 294, + "8": 1362, + "9": 525 + }, + "output_roles": 5336, + "rank_mass": 642620, + "roles": 27918, + "status": "independent serialized word, exact frames, full input and dirty basis both orientations PASS", + "word_length": 621342 + }, + "schedule": "cover-core", + "word_sha256": "09c20f4e46207b7c91092cefb2b851c88694b6c12d3bf5091333cd8a78a197a4" + }, + "25": { + "compiled": { + "all_physical_frame_inclusions": true, + "baseline_pr48_roles": 48329, + "complete_dirty_basis_both_orientations": true, + "dirty_basis_vectors": 41186, + "elementary_xors": 205977, + "h": 25, + "histogram": { + "0": 416741, + "1": 55478, + "10": 529, + "12": 599, + "13": 25, + "14": 530, + "16": 3130, + "17": 869, + "18": 519, + "19": 395, + "2": 115781, + "20": 5436, + "21": 10164, + "23": 220, + "24": 25, + "3": 14362, + "4": 16908, + "5": 10263, + "6": 1767, + "7": 541, + "8": 2115, + "9": 569 + }, + "mode": { + "matching": true, + "reclaim": true + }, + "rank_mass": 915250, + "roles": 36586, + "stats": { + "augmentations": 286, + "clearing_xors": 2154, + "matched": 53194, + "multi_node_regions": 13975, + "reclaimed": 1090, + "regions": 73695 + } + }, + "gzip_sha256": "ad8b299697f90b185b6b791313b505586be97965519052100d097df6199e00c5", + "replay": { + "elementary_xors": 205977, + "full_basis_vectors": 41186, + "h": 25, + "histogram": { + "0": 224465, + "1": 55478, + "10": 529, + "12": 599, + "13": 25, + "14": 530, + "16": 3130, + "17": 869, + "18": 519, + "19": 395, + "2": 115781, + "20": 5436, + "21": 10164, + "23": 220, + "24": 25, + "3": 14362, + "4": 16908, + "5": 10263, + "6": 1767, + "7": 541, + "8": 2115, + "9": 569 + }, + "output_roles": 6925, + "rank_mass": 915250, + "roles": 36586, + "status": "independent serialized word, exact frames, full input and dirty basis both orientations PASS", + "word_length": 856108 + }, + "schedule": "reverse-node", + "word_sha256": "a54443429f47c486016771ce0436effda098e142afc52861c20957e9ff8e086b" + } + }, + "source_sha256": { + "references/frame-compiler/pr48/SOURCE.json": "6ccc673f88d3650d75ed600b082fe2fc2866dd88a172d182a38c1d0cd27d24b3", + "references/frame-compiler/pr48/scripts/partial_swap/binary_io.hpp": "7e143eb75bb342ac8f0c82a60005e7c35c9ec827de479bf6fb773151f3af5fa1", + "research/pair-assembly/frame/frame_verify.py": "fafe25d57166a747eeb847444a2e02dd7eed19038b93a2c495014d147d04a8fb", + "research/pair-assembly/pair_graph.py": "3d47e89d2649c90800a276bdd0480131def50e0bdf92c122a19494b55bf17420", + "research/reordered-rank-pair/test_negative.py": "88832242e6f74e3fe08d109d4f21ff188a9ca0ae50c3e8f31da0243fe9501510", + "research/reordered-rank-pair/verify.py": "e84ed21dad24f9b8c429441caae49c13ccae883be2f04e696993cfe665b57352", + "scripts/experiments/binary_frame_math.py": "1f96e8aafc8ae89f8eeec5d03800131d93d58e01bf8a7fca8feb03702d1740d0", + "scripts/experiments/binary_frame_profile_prepare.py": "8a50381cab00b33e62b3a057d199ba5e19647929135c95b0fd63fc8a8ef7c9b3", + "scripts/experiments/binary_frame_profiles.cpp": "8e2e391d3ee57cbb1372c68e4aa031e1b861321536eabd642ada54e12e678669", + "scripts/experiments/binary_frame_replay.py": "392e78e62d7685c99a5888a7da743ea6c3dcad631af4a743c91e0c09348442bc", + "scripts/experiments/rank_pair_compiler.py": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd", + "scripts/partial_swap/__init__.py": "0438eaa34134600467a5864f93c3e15142eb025b35cef189c2e969cffea72a7f", + "scripts/partial_swap/paired.py": "ddcecace3a8e04d690914cbd64873ab8dde8c0c3477a255767b0ed6f639bb0c7", + "scripts/partial_swap/shared.py": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" + }, + "status": "Exact topological scheduling of unchanged PR63 graph/compiler; both physical orientations and fixed profiles checked" +} diff --git a/research/reordered-rank-pair/frame-profiles-23.json b/research/reordered-rank-pair/frame-profiles-23.json new file mode 100644 index 0000000000..3b648dbe21 --- /dev/null +++ b/research/reordered-rank-pair/frame-profiles-23.json @@ -0,0 +1,38 @@ +{ + "h": 23, + "v": 1771, + "R": 27918, + "loss": 506, + "rank_sum": 642620, + "field_prime": 2305843009213693951, + "frames": 52475, + "distinct_matrices": 36399, + "crt_matrices": 6049, + "crt_disagreements": 0, + "blocks": [ + 0, + 343849, + 16857, + 10540, + 5782, + 4156, + 3911, + 3635, + 2858, + 2284, + 1804, + 1716, + 1262, + 1077, + 711, + 589, + 352, + 193, + 114, + 0, + 45, + 23, + 0, + 0 + ] +} diff --git a/research/reordered-rank-pair/frame-profiles-25.json b/research/reordered-rank-pair/frame-profiles-25.json new file mode 100644 index 0000000000..19cc34b4ca --- /dev/null +++ b/research/reordered-rank-pair/frame-profiles-25.json @@ -0,0 +1,40 @@ +{ + "h": 25, + "v": 2300, + "R": 36586, + "loss": 600, + "rank_sum": 915250, + "field_prime": 2305843009213693951, + "frames": 73697, + "distinct_matrices": 50394, + "crt_matrices": 8127, + "crt_disagreements": 0, + "blocks": [ + 0, + 474640, + 25158, + 12097, + 6776, + 5735, + 5500, + 4875, + 3784, + 3209, + 2695, + 2649, + 1906, + 1663, + 1344, + 1127, + 711, + 585, + 380, + 181, + 113, + 0, + 55, + 25, + 0, + 0 + ] +} diff --git a/research/reordered-rank-pair/frame-transitions-23.json b/research/reordered-rank-pair/frame-transitions-23.json new file mode 100644 index 0000000000..2883a5f7c9 --- /dev/null +++ b/research/reordered-rank-pair/frame-transitions-23.json @@ -0,0 +1,35 @@ +{ + "h": 23, + "v": 1771, + "R": 27918, + "frames": 52475, + "distinct_transitions": 138016, + "singles": 15939, + "rank_mass": 642620, + "rank_histogram_with_side_growth_split_into_singletons": { + "1": 53320, + "2": 77409, + "3": 11086, + "4": 10683, + "5": 7723, + "6": 1994, + "7": 294, + "8": 1362, + "9": 525, + "10": 442, + "11": 11, + "12": 467, + "13": 22, + "14": 2005, + "15": 551, + "16": 547, + "17": 365, + "18": 4220, + "19": 7820, + "21": 165, + "22": 23 + }, + "word_sha256": "09c20f4e46207b7c91092cefb2b851c88694b6c12d3bf5091333cd8a78a197a4", + "copied_centers": 23, + "transition_events_equal_independent_xor_word_reconstruction": true +} diff --git a/research/reordered-rank-pair/frame-transitions-25.json b/research/reordered-rank-pair/frame-transitions-25.json new file mode 100644 index 0000000000..3b4bc33ff6 --- /dev/null +++ b/research/reordered-rank-pair/frame-transitions-25.json @@ -0,0 +1,35 @@ +{ + "h": 25, + "v": 2300, + "R": 36586, + "frames": 73697, + "distinct_transitions": 190838, + "singles": 20700, + "rank_mass": 915250, + "rank_histogram_with_side_growth_split_into_singletons": { + "1": 69278, + "2": 108881, + "3": 14362, + "4": 16908, + "5": 10263, + "6": 1767, + "7": 541, + "8": 2115, + "9": 569, + "10": 529, + "12": 599, + "13": 25, + "14": 530, + "16": 3130, + "17": 869, + "18": 519, + "19": 395, + "20": 5436, + "21": 10164, + "23": 220, + "24": 25 + }, + "word_sha256": "a54443429f47c486016771ce0436effda098e142afc52861c20957e9ff8e086b", + "copied_centers": 25, + "transition_events_equal_independent_xor_word_reconstruction": true +} diff --git a/research/reordered-rank-pair/frame-word-23.json.gz b/research/reordered-rank-pair/frame-word-23.json.gz new file mode 100644 index 0000000000..3a7c7c41c1 Binary files /dev/null and b/research/reordered-rank-pair/frame-word-23.json.gz differ diff --git a/research/reordered-rank-pair/frame-word-25.json.gz b/research/reordered-rank-pair/frame-word-25.json.gz new file mode 100644 index 0000000000..6a239a3e9f Binary files /dev/null and b/research/reordered-rank-pair/frame-word-25.json.gz differ diff --git a/research/reordered-rank-pair/paired-candidate.json b/research/reordered-rank-pair/paired-candidate.json new file mode 100644 index 0000000000..dbfad24526 --- /dev/null +++ b/research/reordered-rank-pair/paired-candidate.json @@ -0,0 +1,252 @@ +{ + "bit": { + "L": 2226400, + "N": 4073300, + "W": 137151806, + "axes": [ + { + "R": 27918, + "blocks": [ + 0, + 343849, + 16857, + 10540, + 5782, + 4156, + 3911, + 3635, + 2858, + 2284, + 1804, + 1716, + 1262, + 1077, + 711, + 589, + 352, + 193, + 114, + 0, + 45, + 23, + 0, + 0 + ], + "crt_disagreements": 0, + "crt_matrices": 6049, + "distinct_matrices": 36399, + "field_prime": 2305843009213693951, + "frames": 52475, + "h": 23, + "loss": 506, + "rank_sum": 642620, + "v": 1771 + }, + { + "R": 36586, + "blocks": [ + 0, + 474640, + 25158, + 12097, + 6776, + 5735, + 5500, + 4875, + 3784, + 3209, + 2695, + 2649, + 1906, + 1663, + 1344, + 1127, + 711, + 585, + 380, + 181, + 113, + 0, + 55, + 25, + 0, + 0 + ], + "crt_disagreements": 0, + "crt_matrices": 8127, + "distinct_matrices": 50394, + "field_prime": 2305843009213693951, + "frames": 73697, + "h": 25, + "loss": 600, + "rank_sum": 915250, + "v": 2300 + } + ], + "child_multiplicities": { + "1": 1725126040, + "10": 8922045, + "11": 8638179, + "12": 6278126, + "13": 5422273, + "14": 4015524, + "15": 3350617, + "16": 2068781, + "17": 9626535, + "18": 935180, + "19": 320551, + "2": 83325918, + "20": 303623, + "21": 16346100, + "22": 97405, + "23": 72402275, + "25": 64793806, + "3": 45665787, + "4": 25298896, + "481": 8146600, + "5": 19715485, + "525": 64793806, + "529": 64211400, + "6": 18735800, + "7": 16994125, + "8": 13274864, + "9": 10936339 + }, + "deficit": 1846900, + "m": 575, + "maxchild": 529, + "parts": { + "data": { + "1": 73319400, + "17": 8146600, + "21": 8146600, + "481": 8146600 + }, + "data_growth_23": { + "1": 8146600, + "21": 8146600 + }, + "data_growth_25": { + "1": 8146600, + "23": 8146600 + }, + "exterior_23": { + "23": 64211400, + "529": 64211400 + }, + "exterior_25": { + "25": 64793806, + "525": 64793806 + }, + "internal_23": { + "1": 790852700, + "10": 4149200, + "11": 3946800, + "12": 2902600, + "13": 2477100, + "14": 1635300, + "15": 1354700, + "16": 809600, + "17": 443900, + "18": 262200, + "2": 38771100, + "20": 103500, + "21": 52900, + "3": 24242000, + "4": 13298600, + "5": 9558800, + "6": 8995300, + "7": 8360500, + "8": 6573400, + "9": 5253200 + }, + "internal_25": { + "1": 840587440, + "10": 4772845, + "11": 4691379, + "12": 3375526, + "13": 2945173, + "14": 2380224, + "15": 1995917, + "16": 1259181, + "17": 1036035, + "18": 672980, + "19": 320551, + "2": 44554818, + "20": 200123, + "22": 97405, + "23": 44275, + "3": 21423787, + "4": 12000296, + "5": 10156685, + "6": 9740500, + "7": 8633625, + "8": 6701464, + "9": 5683139 + }, + "paid_endpoint_copy": { + "1": 4073300 + } + }, + "total_rank": 78860441550 + }, + "bit_saving": "2551509/50000000000", + "finite_bridge": { + "bit": { + "W": 137151806, + "halving_degree": 9, + "m": 575, + "maxchild": 529, + "wire_bits": 28 + }, + "complex": { + "W": 537696432, + "halving_degree": 20, + "m": 784, + "maxchild": 756, + "s": 421548223824, + "scalar_group_upper": 4793351472, + "scalar_terms": [ + { + "c": 78437, + "copied_center_extra_groups": 56, + "h": 28, + "invocations": 3276, + "local_group_upper": 729892, + "v": 3276 + }, + { + "c": 78437, + "copied_center_extra_groups": 56, + "h": 28, + "invocations": 3276, + "local_group_upper": 729892, + "v": 3276 + } + ], + "wire_bits": 30 + }, + "rows": { + "coefficient": 852, + "contract": "W_complex^D_complex * W_bit^D_bit; one preceding prefix and padding; all temporary copies sequential", + "degree": 2000, + "degree_gap": "6548/25", + "suffix_slope": 8000 + }, + "semantic": { + "B": 9696565176891520488614054257040, + "C0": 2358858462850846165593256368932965330169899180021667007021321420800, + "C1": 1, + "E": 9696565176891520488192506033216, + "induction_gap": 533311084729033626873772984137200, + "literal_charge": 2771683137698171397039558468, + "strict_literal_gap": 9693793493753822316795466474748 + } + }, + "kappa": "5102757/100000000000", + "source": { + "axis23": "research/reordered-rank-pair/frame-profiles-23.json", + "axis25": "research/reordered-rank-pair/frame-profiles-25.json", + "profile_constructor": "research/pair-assembly/frame/frame_verify.py" + } +} diff --git a/research/reordered-rank-pair/test_negative.py b/research/reordered-rank-pair/test_negative.py new file mode 100644 index 0000000000..a219a87719 --- /dev/null +++ b/research/reordered-rank-pair/test_negative.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +"""Adversarial controls for the reordered serialized words and scheduling.""" +import sys +sys.dont_write_bytecode=True +import gzip,json,tempfile,subprocess +from pathlib import Path +import verify + +def rejected(label,call): + try:call() + except (AssertionError,IndexError,ValueError): + print('PASS rejected '+label,flush=True) + else:raise AssertionError('Invalid control accepted: '+label) + +def main(): + optimized=subprocess.run([sys.executable,'-B','-O',str(verify.HERE/'verify.py')],capture_output=True,text=True) + assert optimized.returncode!=0 and 'Assertions must remain enabled' in optimized.stderr + print('PASS rejected optimized Python invocation',flush=True) + work=verify.ROOT/'build/reordered-rank-pair';work.mkdir(parents=True,exist_ok=True) + original=json.loads(gzip.decompress((verify.HERE/'frame-word-23.json.gz').read_bytes())) + with tempfile.TemporaryDirectory(prefix='negative-',dir=work) as temporary: + path=Path(temporary)/'mutated.json' + bad=dict(original);bad['ops']=original['ops'][1:] + path.write_text(json.dumps(bad,separators=(',',':'))) + rejected('omitted physical XOR',lambda:verify.replay(path)) + bad=dict(original);bad['R']=original['R']-1 + path.write_text(json.dumps(bad,separators=(',',':'))) + rejected('understated physical role count',lambda:verify.replay(path)) + records=json.loads((verify.HERE/'frame-compiler.json').read_text()) + for name in ('frame-word-23.json.gz','frame-profiles-23.json'): + path.write_bytes((verify.HERE/name).read_bytes()+b' ') + rejected('changed digest '+name,lambda name=name:require_digest(path,records['artifact_sha256'][name])) + # Two equal-rank regions with an actual dependency must not be reversed. + blocks=[{'rank':1,'nodes':[1],'inputs':[],'candidates':[]}, + {'rank':1,'nodes':[2],'inputs':[1],'candidates':[]}] + invalid=lambda h:(None,blocks,[],{}, {1:0,2:1},{},[0,1],None) + rejected('backward region dependency',lambda:verify.reordered_build(invalid,'reverse-node')(23)) + print('PASS all six reordered-word negative controls',flush=True) + +def require_digest(path,expected):assert verify.sha(path)==expected + +if __name__=='__main__':main() diff --git a/research/reordered-rank-pair/validation.json b/research/reordered-rank-pair/validation.json new file mode 100644 index 0000000000..af1990b6db --- /dev/null +++ b/research/reordered-rank-pair/validation.json @@ -0,0 +1,133 @@ +{ + "command": "make verify", + "completed_at": "2026-10-08T18:48:18.233362+00:00", + "core_unit_tests": 467, + "elapsed_seconds": 1409.5119581222534, + "focused_physical_negative_controls": 6, + "github_ci": { + "passed_jobs": 32, + "tested_head": "49e84f939d15b618b50714eb039cabf97c74256a", + "url": "https://github.com/CrocSwap/integer-mult-bounds/actions/runs/37824096643" + }, + "historical_patch_checks": 20, + "integration": { + "all_ci_and_formal_targets_parse": true, + "arithmetic_unit_tests": 8, + "baseline": "49e84f939d15b618b50714eb039cabf97c74256a", + "branch": "research/rank-pair-integration", + "ci_groups": [ + "certificates", + "clones", + "community", + "joint", + "pair", + "positive", + "producers", + "rank-pair", + "reordered-rank-pair", + "research", + "strips", + "ternary", + "tests" + ], + "formal_packages": [ + "gaussian", + "historical", + "matrix" + ], + "independent_arithmetic": true, + "inherited_sources": 9, + "merge_commit": "f03c172fdb1f193555a4ee955cebd1d33fe37fd7", + "pair-assembly_local_files": 32, + "pair-assembly_source_files": 70, + "pair_and_skip_certificates_regenerated_byte_identically": true, + "pr67_existing_prerequisites_verified": [ + "research/pair-assembly/frame/frame_verify.py", + "research/pair-assembly/pair_graph.py", + "scripts/experiments/binary_frame_math.py", + "scripts/experiments/binary_frame_profile_prepare.py", + "scripts/experiments/binary_frame_profiles.cpp", + "scripts/experiments/binary_frame_replay.py", + "scripts/experiments/rank_pair_compiler.py" + ], + "pr67_package_not_copied": [ + "research/slot-cost-rank-pair/compiler.py", + "research/slot-cost-rank-pair/profile_oracle.cpp", + "research/slot-cost-rank-pair/test_negative.py", + "research/slot-cost-rank-pair/verify.py" + ], + "published_witness_directories_unchanged": true, + "push_performed": false, + "rank-pair_complete_profile_unchanged": true, + "reordered-rank-pair_complete_profile_unchanged": true, + "reordered_artifacts": 7, + "reordered_sources": 9, + "skip-strips_local_files": 29, + "skip-strips_source_files": 70, + "status": "PASS focused integration: source hashes, unchanged witnesses, stored paid profiles, metadata, CI coverage", + "upstream": "230b5ea8eb9344fd36f13daa2933ab7b027ce046", + "validation_scope": "Focused integration only. Physical witness and all consumed source bytes unchanged. The baseline full make verify is being run separately by the parent; newly imported upstream CI/formal groups were preserved but not rerun here.", + "whitespace_scope": "Only pre-existing CRLF/trailing whitespace in upstream matrix package; our integration and witness paths pass diff checks." + }, + "joint_integration_recheck": { + "base_commit": "90a379681252c45c3f13134adf9a478e17f22b14", + "cause": "Upstream integration changed Makefile, README.md and NOTICE without refreshing joint-dual source hashes.", + "changed_source_pins": [ + "Makefile", + "README.md", + "NOTICE" + ], + "command": "make verify-joint", + "completed_at": "2026-10-08T18:59:00.727558+00:00", + "controls": 10, + "log_sha256": "d223cd2b7c97e491f77733a41af3be5bbcc8b3b25475c7f7570836d378defc55", + "numerical_and_physical_certificate_fields_unchanged": true, + "state": "passed" + }, + "log_sha256": "accde9848e886d6c7802a14d4ac415c1b0c2e5ce049868d5b8c2c150c1e74f76", + "pid": 30164, + "post_test_changes": "Upstream merge with unchanged consumed sources/witnesses, provenance-only source pins, validation receipt and README status.", + "returncode": 0, + "scope": "Full make verify passed on the tested research commit. Subsequent upstream integration preserves all witness and consumed source bytes; newly imported upstream groups were not included in this earlier full run.", + "started_at": "2026-10-08T18:24:48.721399+00:00", + "state": "passed", + "test_suites": [ + { + "seconds": 0.108, + "tests": 12 + }, + { + "seconds": 0.027, + "tests": 10 + }, + { + "seconds": 0.879, + "tests": 17 + }, + { + "seconds": 0.158, + "tests": 5 + }, + { + "seconds": 136.686, + "tests": 467 + }, + { + "seconds": 0.888, + "tests": 20 + }, + { + "seconds": 0.923, + "tests": 22 + }, + { + "seconds": 4.745, + "tests": 6 + }, + { + "seconds": 0.427, + "tests": 8 + } + ], + "tested_commit": "49e84f939d15b618b50714eb039cabf97c74256a" +} diff --git a/research/reordered-rank-pair/verify.py b/research/reordered-rank-pair/verify.py new file mode 100644 index 0000000000..5ac300ecd0 --- /dev/null +++ b/research/reordered-rank-pair/verify.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +"""Replay, profile, or deterministically rebuild a reordered PR63 circuit. + +PR62 graph: Avi Eisenberg, assisted by Claude; PR60 compiler: Chafik +Boukhalfa, derived from eumemic PR57, with OpenAI Codex assistance. +Region scheduling experiment: Rohan Arun with OpenAI Codex assistance. +Apache-2.0; inherited notices and mathematical dependencies remain applicable. +""" +import sys +sys.dont_write_bytecode = True +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') +import argparse, gzip, importlib.util, json, os, shlex, subprocess, tempfile +from hashlib import sha256 +from pathlib import Path + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +EXP=ROOT/'scripts/experiments' +sys.path[:0]=[str(EXP),str(ROOT/'scripts')] +from binary_frame_replay import replay +from binary_frame_profile_prepare import prepare +import binary_frame_math as arithmetic + +def load(path,name): + spec=importlib.util.spec_from_file_location(name,path) + module=importlib.util.module_from_spec(spec);spec.loader.exec_module(module) + return module + +def sha(path):return sha256(path.read_bytes()).hexdigest() + +def reordered_build(original,mode): + def build(h): + parts=list(original(h)) + c,blocks,uses,value_uses,owner,signal,order,contains=parts + if mode=='reverse-node': + key=lambda g:(blocks[g]['rank'],-min(blocks[g]['nodes'])) + elif mode=='cover-core': + key=lambda g:(blocks[g]['rank'],blocks[g]['frame'][1],blocks[g]['frame'][0]) + else:raise ValueError(mode) + parts[6]=sorted(range(len(blocks)),key=key) + position={g:i for i,g in enumerate(parts[6])} + for g,b in enumerate(blocks): + for x in b['inputs']: + assert position[owner[x]]1 for b in blocks) + def new(g): + s=len(slots);slots.append(0);frames.append(g);hist[blocks[g]['rank']]+=1;events.append((s,-1,g));return s + def raise_(s,g): + old=frames[s];assert contains(blocks[old]['frame'],blocks[g]['frame']);hist[blocks[g]['rank']-blocks[old]['rank']]+=1;frames[s]=g;events.append((s,old,g)) + def xor(a,b,g): + assert a!=b;raise_(a,g);raise_(b,g);slots[a]^=slots[b];ops.append((a,b,g)) + def acquire(g,anchors): + if reclaim: + bb={} + def ins(s): + row=slots[s];expr=1<>s&1;e^=1<>i&1) + if j!=i: + # Synthesize swap as three XORs at the single common frame. + for a,z in ((i,j),(j,i),(i,j)):rr[a]^=rr[z];elim.append((a,z)) + for j in range(len(ins)): + if j!=i and rr[j]>>i&1:rr[j]^=rr[i];elim.append((j,i)) + assert rr==[1<>i&1:xor(s,value_slots[y],g) + assert slots[s]==signal[x];value_slots[x]=s + used=set() + for u in outuses: + x=uses[u][0];s=value_slots[x] + if x in used: + ss=acquire(g,list(value_slots.values()));xor(ss,s,g);s=ss + used.add(x);assert u not in assign;assign[u]=s + if step%5000==0:print('compile',h,step,len(slots),'reclaimed',stats['reclaimed'],'seconds',time.time()-t0,flush=True,file=sys.stderr) + output_slots=[];output_records=[];scatter=[0]*v;J=[] + for u,(x,g,target)in enumerate(uses): + if target is None:continue + s=assign[u];assert slots[s]==signal[x];raise_(s,g);output_slots.append(s) + common,triple=target;output_records.append((s,g,common,triple)) + targets=[i for i,t in enumerate(c.inputs)if common in t]if len(triple)==1 else[c.inputs.index(triple)] + for i in targets:scatter[i]^=slots[s];J.append((v+i,2*v+s)) + rank=blocks[g]['rank'] + if len(triple)==1:hist[rank]+=1;hist[h-rank]+=1 + else:hist[h-1-rank]+=1;hist[1]+=1 + assert len(set(output_slots))==len(output_slots) + for s in retired:hist[h-blocks[frames[s]]['rank']]+=1 + assert len(retired)+len(output_slots)==len(slots) + assert scatter==[1<