From 0d9707207a44c6d2925b81f92052f067f720ef37 Mon Sep 17 00:00:00 2001 From: Matarener Date: Sat, 24 Oct 2026 04:18:01 +0300 Subject: [PATCH 1/2] Certify no H1+H1->H2 fusion pair in the #4610 word by free scalar rewiring (negative result, no new kappa) Co-Authored-By: Claude Fable 5.1 --- research/fusion-pair-scalar-rewiring/PROOF.md | 54 +++ .../fusion-pair-scalar-rewiring/README.md | 78 ++++ .../fusion-pair-scalar-rewiring/RESULT.json | 432 ++++++++++++++++++ .../fusion-pair-scalar-rewiring/SOURCES.json | 36 ++ .../fusion-pair-scalar-rewiring/TASK.json | 112 +++++ .../fusion-pair-scalar-rewiring/VERIFY.json | 37 ++ .../tools/cascade.py | 195 ++++++++ .../tools/compsearch.py | 205 +++++++++ .../fusion-pair-scalar-rewiring/verify.py | 288 ++++++++++++ 9 files changed, 1437 insertions(+) create mode 100644 research/fusion-pair-scalar-rewiring/PROOF.md create mode 100644 research/fusion-pair-scalar-rewiring/README.md create mode 100644 research/fusion-pair-scalar-rewiring/RESULT.json create mode 100644 research/fusion-pair-scalar-rewiring/SOURCES.json create mode 100644 research/fusion-pair-scalar-rewiring/TASK.json create mode 100644 research/fusion-pair-scalar-rewiring/VERIFY.json create mode 100644 research/fusion-pair-scalar-rewiring/tools/cascade.py create mode 100644 research/fusion-pair-scalar-rewiring/tools/compsearch.py create mode 100644 research/fusion-pair-scalar-rewiring/verify.py diff --git a/research/fusion-pair-scalar-rewiring/PROOF.md b/research/fusion-pair-scalar-rewiring/PROOF.md new file mode 100644 index 0000000000..f3ff34cb0b --- /dev/null +++ b/research/fusion-pair-scalar-rewiring/PROOF.md @@ -0,0 +1,54 @@ +# Why no pair fuses: statements and their status + +Notation follows `research/fragmentation-ceiling/PROOF.md` (#5226): a field holds one +logical value in a current frame; paid transports (climbs) change the frame and cost +its dimension gap; warps and scalar operations are free; a scalar ADD needs source and +destination in the same frame (contract H1, checked by every replay of the word). +A *fusion* replaces two consecutive rank-1 climbs `E ⊂ F ⊂ G` of one field f by the +single rank-2 climb `E ⊂ G`, lowering Λ_f by 2 − 2^t. + +## Lemma 1 (CHECKED-EXACT, verify.py S1) + +Every one of the 1,363 consecutive rank-1 pairs (per orientation) has at least one +event touching f while f stands in F. So a fusion must move or replace that event. + +## Lemma 2 (CHECKED-EXACT, verify.py S2) + +For each of the 1,261 pairs whose intermediate events are plain ADDs, some partner +field P of an intermediate ADD never occupies G at any time of the program. Since an +ADD needs P and f in one frame and f occupies only E (before) or G (after) the merged +climb, that ADD cannot be executed after the merged climb with P's own content. + +## Lemma 3 (CHECKED-EXACT, verify.py S3 and the relocation test) + +Exactly 12 pairs have all partners in E at some time (E = frame 0, cold helpers +241, 243, 257, 259, 273, 275, 289, 291, 305, 307, 401, 417 with partners 240, …, 416). +In each, between the partner's own climb into F and the intermediate ADD there is +exactly one event on the partner by a main field M at frame F (backward: `M += q·P`; +forward: `P += q·M`), so the value the ADD transfers at F exists only at F. M never +occupies E or G later, so no compensating ADD between f and M exists. The +frame-level relocation test, which allows the partner to receive commuting ADDs +or to be read while waiting, finds 0 relocatable pairs; deleting that one main +event makes pair 241/240 relocatable (control). + +## Lemma 4 (PROVED-PAPER) + +Any repair that introduces a paid job pays at least 1^t = 1 > 2 − 2^t for every +t ∈ (0, 1); a descent pays ≥ r^t + (9+r)^t − 9^t ≥ 1.99022 at t\* (#5226 Theorem D). +Hence a fusion can only be funded by free operations, which Lemmas 1–3 exclude for +operations that keep the partners' own contents, and the row-level searches +(RESULT.json, tools/) exclude for arbitrary same-frame linear recombination of the +contents present in a frame (pre- or post-payment in the exact window; greedy +propagation downstream), on the backward word. + +## Scope and status + +| claim | status | +|---|---| +| S1, S2, S3, relocation count, controls | CHECKED-EXACT (verify.py, both orientations) | +| price order (Lemma 4) | PROVED-PAPER; constants CHECKED-EXACT | +| row-level pre/post-payment: 0 pairs (backward) | CHECKED-EXACT by tools/compsearch.py, recorded | +| row-level propagated repayment: 0 pairs (backward) | computational, greedy, sampled in frames with > 80 members; recorded | +| forward row-level searches | not run to completion (transpose of backward) | +| 102 pairs with a warp or scale between the climbs | outside the claim | +| helper-input relations (#5377, #5383) | outside the claim | diff --git a/research/fusion-pair-scalar-rewiring/README.md b/research/fusion-pair-scalar-rewiring/README.md new file mode 100644 index 0000000000..c4f5e452dd --- /dev/null +++ b/research/fusion-pair-scalar-rewiring/README.md @@ -0,0 +1,78 @@ +# No H1+H1 → H2 fusion pair in the #4610 word by free scalar rewiring + +**Negative result, no new κ.** #5226 (DreamingOfClouds) prices the whole gap between +Cao Yifan's #4610 word and the bar 0.0030233 as fragmentation loss, and #5243 +(Clear1nsight) verifies the compiler target κ = 0.0030220 for one hypothetical +`H1+H1→H2` fusion per native call, asking for a physical pair. This package shows +that **no pair of consecutive rank-1 climbs on one field of the #4610 word can be +fused into one rank-2 climb by free scalar rewiring** (same-frame dyadic ADDs, +COPY/CLEAR of owned storage, any time, any field), in either orientation. + +## What is checked (`verify.py`, 2 s, standard library) + +Per orientation the word has 3,290 climbs, 2,201 of rank 1, and 1,363 pairs of +consecutive rank-1 climbs `E → F → G` on one field (509 fields). + +| step | exact statement on the word | count | +|---|---|---| +| S1 | no pair is idle: some event touches the field while it stands in the intermediate frame F | 0 idle of 1,363 | +| S2 | pairs whose intermediate events are plain ADDs; in **every** one some partner field never occupies G at any time of the program, so the interaction cannot follow a merged climb | 1,261 of 1,261 | +| S3 | pairs whose partners all visit the start frame E (cold helpers at frame 0, helpers 241/240 … 417/416): each is blocked before the merged climb by exactly one main-field event on the partner at F, and that main never shares a frame with the helper later | 12, all blocked | +| relocation | frame-level relocation test (move every intermediate event to a time when field and partner share E or G, partner unchanged or only receiving commuting ADDs) | 0 relocatable | +| P | price order at t\* = 1 − 0.0030233: one fusion gains 2 − 2^t\* = 0.0041868 Λ per call; any repair that adds one paid rank-1 job costs 1; a descent costs ≥ 1.99022 (#5226 Theorem D); the bar needs 0.0209332 per call | always negative | + +The remaining 102 pairs warp or scale the field between the climbs; warps are +bound to fixed frame pairs, so they are counted and left outside the claim. + +Controls: deleting the single blocking main event of helper pair 241/240 makes +exactly that pair relocatable in both orientations (the test is not vacuous); a +corrupted climb rank is rejected by the nested-climb replay. + +## Row-level searches (evidence, not replayed by CI) + +`tools/compsearch.py` and `tools/cascade.py` run an exact rational row engine (the +convention of #5377's `native.py`) over the backward word and ask whether the +contribution lost by deleting the intermediate events can be repaid by free +same-frame ADDs whose exact rows span it: before or after the merged climb inside +the exact legal window (compsearch, 6 min), or anywhere downstream after +propagating through reads, warps and scalings (cascade, 50 min, greedy). +Results recorded in `RESULT.json`: 1,261 pairs, 2,111 deficits, 12 repayable +deficits (the partner-helper deficits of the 12 cold pairs, repaid at frame 0), +**0 fully repayable pairs**; cascade: 2,522 pair-variants, **0 successes**, 0 +repayments. The forward word is the transpose of the backward word and shows +the same structural obstruction (S1–S3 are checked in both orientations). + +## Reproduce + +```sh +python3 -I -W error -B research/fusion-pair-scalar-rewiring/verify.py +python3 -B scripts/research_package.py --package research/fusion-pair-scalar-rewiring +# optional, minutes: exact row-level searches on the backward word +python3 -B research/fusion-pair-scalar-rewiring/tools/compsearch.py backward +python3 -B research/fusion-pair-scalar-rewiring/tools/cascade.py backward +``` + +Expected marker: `PASS_NO_FUSION_PAIR_SCALAR_REWIRING`. + +## Scope + +The claim is about the frozen #4610 word with its frames and native maps: a +fusion needs new frames or native maps (a changed mechanism), or an extra paid +transport for a partner, which never pays. Not covered: the 102 warp/scale pairs, +non-greedy repayment choices, owned-storage copies used as time shifters (they +cannot move content across frames), and relations among helper inputs (#5377, +#5383 and their audits). The forward row-level searches were not run to +completion. + +## Open next questions + +See `TASK.json`. The only way left to lower Λ by fusions is a changed native +word whose intermediate meeting frames are shared with G; pricing such a change +needs #5226's exchange table on the new word, not this one. + +## Credit + +Cao Yifan (intqwq, #4610) supplies the word; DreamingOfClouds (#5226) the +fragmentation framework and prices; Clear1nsight (#5243) the one-fusion target; +Ali Romman (#5377) the row convention. Mark (Matarener) with substantial Claude +Code (Claude) assistance. Apache-2.0; author-checked, not independent acceptance. diff --git a/research/fusion-pair-scalar-rewiring/RESULT.json b/research/fusion-pair-scalar-rewiring/RESULT.json new file mode 100644 index 0000000000..cede4a6a02 --- /dev/null +++ b/research/fusion-pair-scalar-rewiring/RESULT.json @@ -0,0 +1,432 @@ +{ + "bar": "0.0030233", + "orientations": { + "backward": { + "census": { + "climbs": 3290, + "idle_pairs": 0, + "pairs": 1363, + "pairs_with_warp_or_nonadd": 102, + "pure_add_pairs": 1261, + "pure_add_pairs_all_partners_ever_in_E": 12, + "pure_add_pairs_partner_never_in_G": 1261, + "rank1_climbs": 2201, + "relocatable_pairs": 0 + }, + "cold_pairs": [ + { + "E": 0, + "F": 72, + "G": 363, + "blocking_events": [ + [ + 8367, + 70 + ] + ], + "field": 241, + "main_readers": 1, + "partner": 240, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 73, + "G": 366, + "blocking_events": [ + [ + 8371, + 71 + ] + ], + "field": 243, + "main_readers": 1, + "partner": 242, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 74, + "G": 383, + "blocking_events": [ + [ + 8585, + 72 + ] + ], + "field": 257, + "main_readers": 1, + "partner": 256, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 4, + "G": 386, + "blocking_events": [ + [ + 8589, + 2 + ] + ], + "field": 259, + "main_readers": 1, + "partner": 258, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 14, + "G": 403, + "blocking_events": [ + [ + 8803, + 12 + ] + ], + "field": 273, + "main_readers": 1, + "partner": 272, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 102, + "G": 406, + "blocking_events": [ + [ + 8807, + 100 + ] + ], + "field": 275, + "main_readers": 1, + "partner": 274, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 103, + "G": 423, + "blocking_events": [ + [ + 9021, + 101 + ] + ], + "field": 289, + "main_readers": 1, + "partner": 288, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 56, + "G": 426, + "blocking_events": [ + [ + 9025, + 54 + ] + ], + "field": 291, + "main_readers": 1, + "partner": 290, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 100, + "G": 443, + "blocking_events": [ + [ + 9239, + 98 + ] + ], + "field": 305, + "main_readers": 1, + "partner": 304, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 50, + "G": 446, + "blocking_events": [ + [ + 9243, + 48 + ] + ], + "field": 307, + "main_readers": 1, + "partner": 306, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 17, + "G": 563, + "blocking_events": [ + [ + 10551, + 15 + ] + ], + "field": 401, + "main_readers": 1, + "partner": 400, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 15, + "G": 583, + "blocking_events": [ + [ + 10769, + 13 + ] + ], + "field": 417, + "main_readers": 1, + "partner": 416, + "reader_later_in_E_or_G": [] + } + ] + }, + "forward": { + "census": { + "climbs": 3290, + "idle_pairs": 0, + "pairs": 1363, + "pairs_with_warp_or_nonadd": 102, + "pure_add_pairs": 1261, + "pure_add_pairs_all_partners_ever_in_E": 12, + "pure_add_pairs_partner_never_in_G": 1261, + "rank1_climbs": 2201, + "relocatable_pairs": 0 + }, + "cold_pairs": [ + { + "E": 0, + "F": 72, + "G": 363, + "blocking_events": [ + [ + 8367, + 70 + ] + ], + "field": 241, + "main_readers": 1, + "partner": 240, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 73, + "G": 366, + "blocking_events": [ + [ + 8371, + 71 + ] + ], + "field": 243, + "main_readers": 1, + "partner": 242, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 74, + "G": 383, + "blocking_events": [ + [ + 8585, + 72 + ] + ], + "field": 257, + "main_readers": 1, + "partner": 256, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 4, + "G": 386, + "blocking_events": [ + [ + 8589, + 2 + ] + ], + "field": 259, + "main_readers": 1, + "partner": 258, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 14, + "G": 403, + "blocking_events": [ + [ + 8803, + 12 + ] + ], + "field": 273, + "main_readers": 1, + "partner": 272, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 102, + "G": 406, + "blocking_events": [ + [ + 8807, + 100 + ] + ], + "field": 275, + "main_readers": 1, + "partner": 274, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 103, + "G": 423, + "blocking_events": [ + [ + 9021, + 101 + ] + ], + "field": 289, + "main_readers": 1, + "partner": 288, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 56, + "G": 426, + "blocking_events": [ + [ + 9025, + 54 + ] + ], + "field": 291, + "main_readers": 1, + "partner": 290, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 100, + "G": 443, + "blocking_events": [ + [ + 9239, + 98 + ] + ], + "field": 305, + "main_readers": 1, + "partner": 304, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 50, + "G": 446, + "blocking_events": [ + [ + 9243, + 48 + ] + ], + "field": 307, + "main_readers": 1, + "partner": 306, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 17, + "G": 563, + "blocking_events": [ + [ + 10551, + 15 + ] + ], + "field": 401, + "main_readers": 1, + "partner": 400, + "reader_later_in_E_or_G": [] + }, + { + "E": 0, + "F": 15, + "G": 583, + "blocking_events": [ + [ + 10769, + 13 + ] + ], + "field": 417, + "main_readers": 1, + "partner": 416, + "reader_later_in_E_or_G": [] + } + ] + } + }, + "prices": { + "bar_0.0030233": { + "descent_price_thmD": "1.9902153752933601170824590496722686318103483680934", + "extra_rank1_job": "1", + "merge_gain_1plus1_to_2": "0.0041867953026785113088502757510664066261423899948", + "needed_per_call_for_bar": "0.0209331969", + "t": "0.9969767" + }, + "root_4610": { + "descent_price_thmD": "1.9902202863097255999173033676763276224598350395168", + "extra_rank1_job": "1", + "merge_gain_1plus1_to_2": "0.0041846867350274682014757574831632982687581506584", + "needed_per_call_for_bar": "0.0209331969", + "t": "0.9969782242" + } + }, + "row_level_searches": { + "cascade_backward": { + "dead_over_24_deficient_fields": 1446, + "pair_variants": 2522, + "repayments": 0, + "sampling": "frames with more than 80 members tested every 100th version", + "successes": 0, + "unfinished_with_deficits": 1076 + }, + "compsearch_backward": { + "deficits": 2111, + "fully_repayable_pairs": 0, + "pairs": 1261, + "repayable_deficits": 12, + "repayable_deficits_description": "the 12 partner-helper deficits of the cold pairs, repaid at frame 0 before the climbs; the main-read deficit of each of these pairs is never repayable" + }, + "forward": "not run to completion; the forward program is the transpose of the backward program and shows the same obstruction (S1-S3 above)", + "note": "exact rational row engine (same convention as PR #5377 native.py); run by tools/compsearch.py and tools/cascade.py on the backward word; 6 and 50 minutes; not part of the registered replay" + }, + "schema": "fusion-pair-scalar-rewiring/1", + "word_sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" +} diff --git a/research/fusion-pair-scalar-rewiring/SOURCES.json b/research/fusion-pair-scalar-rewiring/SOURCES.json new file mode 100644 index 0000000000..1d1f16a010 --- /dev/null +++ b/research/fusion-pair-scalar-rewiring/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e", + "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/kappa-round3-warp-20261022/ARITHMETIC.json", + "usage": "input", + "git_blob": "c89e009ca4a5ad316c69f0371d885d72045ba415", + "sha256": "ab10f6a4a8a4f589d4b094aac663e002c43ec44774e6bd181c51915c7fa7e521" + }, + { + "path": "research/fragmentation-ceiling/PROOF.md", + "usage": "provenance", + "git_blob": "c4033090d7cd35d9c80744922c587ae115b1de8a", + "sha256": "28be45a551ed8491be1ebb8c64acba2834aaa402452cb02e3c71c83e49232264" + } + ] +} diff --git a/research/fusion-pair-scalar-rewiring/TASK.json b/research/fusion-pair-scalar-rewiring/TASK.json new file mode 100644 index 0000000000..205fd5b4b6 --- /dev/null +++ b/research/fusion-pair-scalar-rewiring/TASK.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 7, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a changed frame itinerary remove a paid transition beyond the already covered scalar A2 contractions?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-a2-graph-rewrite/README.md", + "research/staged544-separated-a2/README.md", + "research/staged544-a2-composition-audit/README.md", + "research/staged544-a1858-contraction-audit/README.md" + ], + "methods": [ + "Derive the changed legal frame itinerary and exact child histogram.", + "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract." + ], + "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the A2 and separated-A2 constructions and their composition/contraction audits. Scalar contractions can preserve the complete recursive histogram; fewer ADDs alone do not justify further scans.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Identify an actual paid transition to remove and construct a legal replacement frame itinerary, charging restoration, source windows and changed helpers. Compare complete before/after histograms. Stop if only scalar count changes; report that benefit honestly, without expanding the same scalar-only census.", + "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.", + "allowed_variations": [ + "One existing scalar simplification and one proposed frame-path change." + ], + "scope_change_triggers": [ + "Submitting only another scalar count as completion of a paid-profile task." + ], + "overlap_terms": [ + "scalar simplification", + "paid profile", + "R439", + "3998", + "4019", + "4112", + "4152", + "staged544-a2-graph-rewrite", + "staged544-separated-a2", + "staged544-a2-composition-audit", + "staged544-a1858-contraction-audit" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Can the frame itinerary of one field of the #4610 word (research/kappa-round3-warp-20261022) be changed by free scalar rewiring so that two consecutive rank-1 climbs become one rank-2 climb (the H1+H1->H2 fusion priced by #5226 and targeted by #5243), in either orientation?", + "scope_change_reason": "The card asks for a changed frame itinerary that removes a paid transition; #5226/#5243 made the concrete instance on the current word explicit (one fusion per native call would reach 0.0030220, five per call 0.0030233) and asked for a physical pair. This package answers that instance negatively for all free scalar rewirings of the frozen word.", + "bottleneck_link": "Negative result: fragmentation Lambda of #4610 cannot be lowered by fusing rank-1 climbs without new frames or native maps; the staircase structure (each intermediate frame is the only meeting frame with a partner) is the obstruction, and any paid repair costs >= 1 against a gain of 0.0042.", + "budget_minutes": 240, + "stop_rule": "Stop after the structural certificate (S1-S3, relocation test, controls) passes in both orientations and the exact row-level searches on the backward word finish; do not start a new native word or a helper-relation search.", + "outcome": "negative-result", + "evidence": "verify.py binds the #4610 word by SHA256, replays the nested-climb contract, counts the 1363 pairs per orientation, certifies S1-S3 and 0 relocatable pairs, runs a positive control (deleting one main event makes one pair relocatable) and a negative control, and checks the price order; RESULT.json records the row-level searches (tools/compsearch.py: 0 of 1261 pairs; tools/cascade.py: 0 of 2522 pair-variants).", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Is there a native word in the (112, 8) family whose intermediate meeting frames are shared with the next climb target, so that fusions become legal?", + "why_it_matters": "Five fusions per call close the 0.0209 Lambda gap to 0.0030233 (#5226); on the frozen word none is legal, so only a changed word can use this lever.", + "first_step": "Take the per-field climb paths and partner frames exported by verify.py, and ask the MILP of research/kappa-round3-warp-20261022/helper_line_milp.py for a frame assignment in which a partner's frame at the intermediate interaction is nested in the field's next target.", + "blocked_by": "A changed word must be re-admitted (native maps, phases, 632 endpoints); not attempted here." + }, + { + "question": "Do the 102 pairs with a warp between the two climbs admit a fusion if the warp is re-bound to the merged target frame?", + "why_it_matters": "They are the only pairs outside this certificate.", + "first_step": "List the 102 pairs with their warp operators and check whether the warp's from/to frames can be replaced by the merged frames while preserving the 72 native maps.", + "blocked_by": "Warps are bound to fixed frame pairs in canonical.warps; changing them changes the native maps." + } + ] +} diff --git a/research/fusion-pair-scalar-rewiring/VERIFY.json b/research/fusion-pair-scalar-rewiring/VERIFY.json new file mode 100644 index 0000000000..a09b1e4aca --- /dev/null +++ b/research/fusion-pair-scalar-rewiring/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/kappa-round3-warp-20261022/ARITHMETIC.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Bind the #4610 word by SHA256; nested-climb replay; 1363 consecutive rank-1 pairs per orientation; S1 no idle pair, S2 partner never in the target frame for all 1261 pure-add pairs, S3 the 12 cold-helper pairs blocked by one main event; frame-level relocation test finds 0 pairs; positive and negative controls; price order at the bar and at the #4610 root; RESULT.json byte comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks with assertions optimised away; every check uses explicit raises." + } + ] +} diff --git a/research/fusion-pair-scalar-rewiring/tools/cascade.py b/research/fusion-pair-scalar-rewiring/tools/cascade.py new file mode 100644 index 0000000000..b5d852c230 --- /dev/null +++ b/research/fusion-pair-scalar-rewiring/tools/cascade.py @@ -0,0 +1,195 @@ +"""Cascade compensation search for H1+H1->H2 fusions on the #4610 word. + +Generalises compsearch.py: a deficit (missing contribution) is allowed to propagate downstream through +reads, warps and scalings, and may be repaid on ANY deficient field at ANY time by free same-frame adds +whose exact rows span the deficit. Greedy: repay as soon as the span test passes. A pair succeeds if +every deficit is repaid before the end of the program (then final rows are the original ones). + +One sweep of the original program serves all pairs: the original rows are shared; each pair keeps a +small dict {field: deficit}. Usage: py -3.12 cascade.py backward|forward [MAXDEF] +""" +import gzip, json, collections, sys, time +from fractions import Fraction as Q +ORIENT = sys.argv[1] if len(sys.argv) > 1 else 'backward' +MAXDEF = int(sys.argv[2]) if len(sys.argv) > 2 else 24 # give up on a pair with more deficient fields +import os +W = os.path.join(os.path.dirname(os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))), 'research', 'kappa-round3-warp-20261022', 'ACTUAL-WORD.json.gz') +LOG = open(f'cascade_{ORIENT}.log', 'a', buffering=1) +def log(*a): + s = time.strftime('%H:%M:%S ') + ' '.join(str(x) for x in a); print(s, flush=True); LOG.write(s + '\n') + +w = json.load(gzip.open(W, 'rt', encoding='utf-8')); c = w['canonical']; fr = c['frames'] +prog = w['programs'][ORIENT]; n = len(prog); backward = (ORIENT == 'backward'); NL = 632 + +touch = collections.defaultdict(list) +for i, e in enumerate(prog): + k = e[0] + if k == 'climb': touch[('L', e[2])].append((i, 'climb', None)) + elif k == 'warp': touch[tuple(e[1])].append((i, 'warp', None)) + elif k == 'center': touch[('C', e[1])].append((i, 'center', None)) + elif k == 'scalar': + g = e[1]; d = tuple(g[1]) + if g[0] in ('add', 'copy'): + s = tuple(g[2]); touch[d].append((i, 'dst:' + g[0], s)); touch[s].append((i, 'src:' + g[0], d)) + else: touch[d].append((i, 'dst:' + g[0], None)) +climbs = collections.defaultdict(list) +for i, e in enumerate(prog): + if e[0] == 'climb': climbs[e[2]].append((i, e[3], e[4], e[5])) +pairs = [] +for f, cl in climbs.items(): + for (i1, E, F, r1), (i2, F2, G, r2) in zip(cl, cl[1:]): + if r1 != 1 or r2 != 1: continue + between = [t for t in touch[('L', f)] if i1 < t[0] < i2] + if any(t[1] not in ('src:add', 'dst:add') for t in between): continue + for variant in ('late', 'early'): + pairs.append(dict(f=('L', f), i1=i1, i2=i2, E=E, F=F, G=G, variant=variant, deleted={j for j, k, P in between}, + D={}, dead=None, fixes=[], last={})) +log(ORIENT, 'pair-variants', len(pairs)) +by_start = collections.defaultdict(list) +for p in pairs: by_start[p['i1']].append(p) + +def add_into(dst, src, q): + for k, v in src.items(): + nv = dst.get(k, 0) + q * v + if nv: dst[k] = nv + else: dst.pop(k, None) +def warp_row(row, op): + sym = (1 if op > 0 else -1) * (abs(op) + (10**6 if backward else 0)) + return {(r, wd[1:] if wd and wd[0] == -sym else (sym,) + wd): q for (r, wd), q in row.items()} +def reduce_basis(vecs): + basis = [] + for role, row in vecs: + r = dict(row); combo = {role: Q(1)} + for pk, brow, bcombo in basis: + if pk in r: + coef = r[pk] / brow[pk]; add_into(r, brow, -coef); add_into(combo, bcombo, -coef) + if r: basis.append((min(r, key=repr), r, combo)) + return basis +def solve(basis, v): + r = dict(v); combo = {} + for pk, brow, bcombo in basis: + if pk in r: + coef = r[pk] / brow[pk]; add_into(r, brow, -coef); add_into(combo, bcombo, coef) + return None if r else combo +def dyadic(q): return (q.denominator & (q.denominator - 1)) == 0 + +rows = {('L', i): {(('L', i), ()): Q(1)} for i in range(NL)}; rows[('C', 0)] = {(('C', 0), ()): Q(1)} +frames = {('L', i): c['start'][i] for i in range(NL)}; frames[('C', 0)] = None +members = collections.defaultdict(set); version = collections.Counter() +for r, fr_ in frames.items(): + if fr_ is not None: members[fr_].add(r) +active = []; cache = {}; BIG = 80; t0 = time.time() + +def f_frame(p, t): + if t < p['i1']: return frames[p['f']] + if t < p['i2']: return p['G'] if p['variant'] == 'early' else p['E'] + return p['G'] +def frame_of(p, X, t): return f_frame(p, t) if X == p['f'] else frames[X] +def mod_row(p, X): return rows[X] if X not in p['D'] else {k: v for k, v in ((k, rows[X].get(k, 0) - p['D'][X].get(k, 0)) for k in set(rows[X]) | set(p['D'][X])) if v} + +def try_fix(p, t): + """repay any deficient field whose frame members span the deficit (shared basis per frame version)""" + ff = p['f'] + for X in list(p['D']): + v = p['D'][X] + if not v: p['D'].pop(X); continue + Phi = frame_of(p, X, t) + if Phi is None: continue + key = (Phi, version[Phi], len(p['D'])) + if p['last'].get(X) == key: continue + nmem = len(members[Phi]) + if nmem > BIG and version[Phi] % 100: continue + p['last'][X] = key + ukey = ('U', Phi, version[Phi]) + if ukey not in cache: + if len(cache) > 48: cache.clear() + u = set() + for r in members[Phi]: u.update(rows[r].keys()) + if f_frame(p, t) == Phi: u.update(rows[ff].keys()) + cache[ukey] = u + if not set(v.keys()) <= cache[ukey]: continue + bkey = ('B', Phi, version[Phi]) + if bkey not in cache: + if len(cache) > 48: cache.clear() + cache[bkey] = reduce_basis([(r, rows[r]) for r in sorted(members[Phi]) if rows[r]]) + combo = solve(cache[bkey], v) + if combo is None and f_frame(p, t) == Phi and ff not in members[Phi]: + # f is present in this frame only in the modified program: extend basis by f + combo = solve(reduce_basis([(r, rows[r]) for r in sorted(members[Phi]) if rows[r]] + [(ff, rows[ff])]), v) + if combo is None: continue + bad = any(r in p['D'] or r == X or (r == ff and f_frame(p, t) != Phi) for r in combo) + if bad: continue + p['fixes'].append(dict(t=t, X=X, frame=Phi, combo={str(k): str(q) for k, q in combo.items()}, dyadic=all(dyadic(q) for q in combo.values()))) + p['D'].pop(X); p['last'].pop(X, None) + +for t, e in enumerate(prog): + for p in by_start.get(t, ()): active.append(p) + k = e[0] + if active: + keep = [] + for p in active: + if p['dead']: continue + # 1. propagate / create deficits through this event (modified program semantics) + if t in p['deleted']: + g = e[1]; d = tuple(g[1]); s = tuple(g[2]); q = Q(g[3], g[4]) + # deleted d += q s -> d lacks q * (modified row of s) + add_into(p['D'].setdefault(d, {}), mod_row(p, s), q) + if not p['D'][d]: p['D'].pop(d) + elif k == 'scalar': + g = e[1]; d = tuple(g[1]) + if g[0] == 'clear': p['D'].pop(d, None) + elif g[0] == 'copy': + s = tuple(g[2]); p['D'].pop(d, None) + if s in p['D']: p['D'][d] = dict(p['D'][s]) + elif g[0] == 'add': + s = tuple(g[2]) + if s in p['D']: + add_into(p['D'].setdefault(d, {}), p['D'][s], Q(g[3], g[4])) + if not p['D'][d]: p['D'].pop(d) + elif g[0] == 'scale': + if d in p['D']: p['D'][d] = {kk: Q(g[2], g[3]) * v for kk, v in p['D'][d].items()} + elif k == 'warp': + d = tuple(e[1]) + if d in p['D']: p['D'][d] = warp_row(p['D'][d], e[2]) + # 2. try to repay (after the event's effect on rows below, so test before applying rows? rows change + # only for the touched field; we test with the state BEFORE applying, which is also a legal time) + if len(p['D']) > MAXDEF: p['dead'] = ('too many deficient fields', t); continue + if p['D']: try_fix(p, t) + if p['D'] or t < p['i2']: keep.append(p) + else: p['dead'] = None # finished clean: no deficits and past i2 -> success (stays success) + if not p['D'] and t >= p['i2']: p['done'] = t + active = keep + # apply event to the shared original state + oldf = None + if k == 'scalar': + g, frame = e[1], e[2]; d = tuple(g[1]); oldf = frames[d] + if g[0] == 'clear': rows[d] = {}; frames[d] = frame + elif g[0] == 'copy': rows[d] = dict(rows[tuple(g[2])]) + elif g[0] == 'add': add_into(rows[d], rows[tuple(g[2])], Q(g[3], g[4])) + elif g[0] == 'scale': rows[d] = {kk: Q(g[2], g[3]) * v for kk, v in rows[d].items()} + elif k == 'warp': + d = tuple(e[1]); oldf = e[3]; rows[d] = warp_row(rows[d], e[2]); frames[d] = e[4] + elif k == 'climb': d = ('L', e[2]); oldf = e[3]; frames[d] = e[4] + elif k == 'center': d = ('C', e[1]); oldf = e[2]; frames[d] = e[3] + else: d = None + if d is not None: + newf = frames[d] + if oldf != newf: + if oldf is not None: members[oldf].discard(d); version[oldf] += 1 + if newf is not None: members[newf].add(d) + if newf is not None: version[newf] += 1 + if t % 500 == 0: + log(' t=%d/%d active=%d dead=%d elapsed=%.0fs' % (t, n, len(active), sum(1 for p in pairs if p['dead']), time.time() - t0)) + +ok = [p for p in pairs if not p['dead'] and not p['D'] and p.get('done') is not None] +unfinished = [p for p in pairs if not p['dead'] and p['D']] +log('DONE %s: pair-variants %d, SUCCESS %d, dead %d, deficits left at end %d' % (ORIENT, len(pairs), len(ok), sum(1 for p in pairs if p['dead']), len(unfinished))) +deadreasons = collections.Counter(p['dead'][0] for p in pairs if p['dead']) +log('dead reasons', dict(deadreasons)) +out = [dict(f=p['f'], i1=p['i1'], i2=p['i2'], E=p['E'], F=p['F'], G=p['G'], variant=p['variant'], deleted=sorted(p['deleted']), + fixes=p['fixes'], dead=p['dead'], left={str(k): len(v) for k, v in p['D'].items()}) for p in pairs] +json.dump(out, open(f'cascade_{ORIENT}.json', 'w'), indent=1, default=str) +for p in ok: log(' SUCCESS', p['f'], p['i1'], p['i2'], p['variant'], 'fixes', json.dumps(p['fixes'])[:500]) +# statistics on how far pairs got +left = collections.Counter(len(p['D']) for p in unfinished) +log('deficient-field count at end among unfinished:', dict(sorted(left.items()))) diff --git a/research/fusion-pair-scalar-rewiring/tools/compsearch.py b/research/fusion-pair-scalar-rewiring/tools/compsearch.py new file mode 100644 index 0000000000..e4ee361c82 --- /dev/null +++ b/research/fusion-pair-scalar-rewiring/tools/compsearch.py @@ -0,0 +1,205 @@ +"""Compensation search for H1+H1->H2 fusions on the #4610 word. + +For each consecutive rank-1,rank-1 climb pair (f: E->F->G) whose intervening events are plain adds, +delete the first climb and the intervening events, climb E->G in one job, and ask whether every +"deficit" (the missing add contribution) can be delivered by free same-frame adds somewhere inside +the legal time window, using the exact rows of the fields that stand in that frame at that time. +Rows follow the convention of PR #5377's native.py (origin symbol x free warp word, rational coefficients). + +Usage: py -3.12 compsearch.py backward|forward +Writes progress_.log and result_.json. +""" +import gzip, json, collections, sys, time +from fractions import Fraction as Q +ORIENT = sys.argv[1] if len(sys.argv) > 1 else 'backward' +import os +W = os.path.join(os.path.dirname(os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))), 'research', 'kappa-round3-warp-20261022', 'ACTUAL-WORD.json.gz') +LOG = open(f'progress_{ORIENT}.log', 'a', buffering=1) +def log(*a): + s = time.strftime('%H:%M:%S ') + ' '.join(str(x) for x in a); print(s, flush=True); LOG.write(s + '\n') + +w = json.load(gzip.open(W, 'rt', encoding='utf-8')); c = w['canonical']; fr = c['frames'] +prog = w['programs'][ORIENT]; n = len(prog); backward = (ORIENT == 'backward') +NL = 632 + +# ---------- index events per role ---------- +touch = collections.defaultdict(list) # role -> [(idx, kind, partner)] +for i, e in enumerate(prog): + k = e[0] + if k == 'climb': touch[('L', e[2])].append((i, 'climb', None)) + elif k == 'warp': touch[tuple(e[1])].append((i, 'warp', None)) + elif k == 'center': touch[('C', e[1])].append((i, 'center', None)) + elif k == 'scalar': + g = e[1]; d = tuple(g[1]) + if g[0] in ('add', 'copy'): + s = tuple(g[2]); touch[d].append((i, 'dst:' + g[0], s)); touch[s].append((i, 'src:' + g[0], d)) + else: touch[d].append((i, 'dst:' + g[0], None)) +def consuming(k): # event kinds after which a pending deficit on the role can no longer be fixed locally + return k in ('warp', 'center') or k.startswith('src') or k in ('dst:scale', 'dst:clear', 'dst:copy') + +# ---------- candidate pairs and their deficits ---------- +climbs = collections.defaultdict(list) +for i, e in enumerate(prog): + if e[0] == 'climb': climbs[e[2]].append((i, e[3], e[4], e[5])) +cands = [] +for f, cl in climbs.items(): + for (i1, E, F, r1), (i2, F2, G, r2) in zip(cl, cl[1:]): + if r1 != 1 or r2 != 1: continue + between = [t for t in touch[('L', f)] if i1 < t[0] < i2] + if any(t[1] not in ('src:add', 'dst:add') for t in between): continue + prv = max([t[0] for t in touch[('L', f)] if t[0] < i1], default=-1) + nxt = min([t[0] for t in touch[('L', f)] if t[0] > i2 and consuming(t[1])], default=n) + defs = [] + for j, k, P in between: + q = Q(prog[j][1][3], prog[j][1][4]) + if k == 'src:add': # P += q f deleted -> P lacks q*row_f(j); fix on P in [j, consume_P) + cP = min([t[0] for t in touch[P] if t[0] > j and consuming(t[1])], default=n) + defs.append(dict(X=P, Y=('L', f), q=q, j=j, windows=[(j, cP)])) + else: # f += q P deleted -> f lacks q*row_P(j); fix on f in (prv,i1) at E or (i2,nxt) at G + defs.append(dict(X=('L', f), Y=P, q=q, j=j, windows=[(prv + 1, i1), (i1 + 1, nxt)])) + for d in defs: d.update(f=('L', f), i1=i1, i2=i2, E=E, G=G) + cands.append(dict(f=f, i1=i1, i2=i2, E=E, F=F, G=G, defs=defs)) +log(ORIENT, 'candidate pairs', len(cands), 'deficits', sum(len(x['defs']) for x in cands)) + +# ---------- exact row engine ---------- +def add_into(dst, src, q): + for k, v in src.items(): + nv = dst.get(k, 0) + q * v + if nv: dst[k] = nv + else: dst.pop(k, None) +def apply(e, rows, frames): + """apply one event; return the role touched""" + k = e[0] + if k == 'scalar': + g, frame = e[1], e[2]; d = tuple(g[1]) + if g[0] == 'clear': rows[d] = {}; frames[d] = frame + elif g[0] == 'copy': rows[d] = dict(rows[tuple(g[2])]) + elif g[0] == 'add': add_into(rows[d], rows[tuple(g[2])], Q(g[3], g[4])) + elif g[0] == 'scale': rows[d] = {kk: Q(g[2], g[3]) * v for kk, v in rows[d].items()} + return d + if k == 'warp': + d = tuple(e[1]); op = e[2] + sym = (1 if op > 0 else -1) * (abs(op) + (10**6 if backward else 0)) + rows[d] = {(r, wd[1:] if wd and wd[0] == -sym else (sym,) + wd): q for (r, wd), q in rows[d].items()} + frames[d] = e[4]; return d + if k == 'climb': d = ('L', e[2]); frames[d] = e[4]; return d + if k == 'center': d = ('C', e[1]); frames[d] = e[3]; return d + return None +def fresh_state(): + rows = {('L', i): {(('L', i), ()): Q(1)} for i in range(NL)}; rows[('C', 0)] = {(('C', 0), ()): Q(1)} + frames = {('L', i): c['start'][i] for i in range(NL)}; frames[('C', 0)] = None + return rows, frames + +# ---------- pass 1: deficit vectors v = q*row_Y(j) ---------- +need = collections.defaultdict(list) +for ci, cd in enumerate(cands): + for di, d in enumerate(cd['defs']): need[d['j']].append((ci, di)) +rows, frames = fresh_state() +for i, e in enumerate(prog): + for ci, di in need.get(i, ()): + d = cands[ci]['defs'][di]; d['v'] = {k: d['q'] * v for k, v in rows[d['Y']].items()} + apply(e, rows, frames) +log('pass 1 done: deficit vectors stored') + +# ---------- span test with memoised elimination per (frame, version) ---------- +def reduce_basis(vecs): + basis = [] + for role, row in vecs: + r = dict(row); combo = {role: Q(1)} + for pk, brow, bcombo in basis: + if pk in r: + coef = r[pk] / brow[pk] + add_into(r, brow, -coef); add_into(combo, bcombo, -coef) + if r: + pk = min(r, key=repr); basis.append((pk, r, combo)) + return basis +def solve(basis, v): + r = dict(v); combo = {} + for pk, brow, bcombo in basis: + if pk in r: + coef = r[pk] / brow[pk] + add_into(r, brow, -coef); add_into(combo, bcombo, coef) + return (None if r else combo) +def dyadic(q): return (q.denominator & (q.denominator - 1)) == 0 + +# ---------- pass 2: sweep, test active deficits ---------- +members = collections.defaultdict(set); version = collections.Counter() +rows, frames = fresh_state() +for r, fr_ in frames.items(): + if fr_ is not None: members[fr_].add(r) +active_by_start = collections.defaultdict(list) +for ci, cd in enumerate(cands): + for di, d in enumerate(cd['defs']): + d['found'] = {'early': None, 'late': None}; d['tests'] = 0 + for wi, (lo, hi) in enumerate(d['windows']): + if lo < hi: active_by_start[lo].append((ci, di, wi)) +active = [] +cache = {} +t0 = time.time(); BIG = 80 +for t, e in enumerate(prog): + for (ci, di, wi) in active_by_start.get(t, ()): + active.append([ci, di, wi, cands[ci]['defs'][di]['windows'][wi][1], None]) + if active: + keep = [] + for it in active: + ci, di, wi, hi, last = it + d = cands[ci]['defs'][di] + if t >= hi or all(d['found'].values()): continue + ff, i1_, i2_, E_, G_ = d['f'], d['i1'], d['i2'], d['E'], d['G'] + for variant in ('early', 'late'): + if d['found'][variant] is not None: continue + X = d['X'] + # frame of f in the modified program at time t (before applying event t) + if t < i1_: f_frame = frames[ff] + elif t < i2_: f_frame = G_ if variant == 'early' else E_ + else: f_frame = G_ + Phi = f_frame if X == ff else frames[X] + if Phi is None: continue + mem = set(members[Phi]) - {X} + if X != ff: + mem.discard(ff) + if Phi == f_frame: mem.add(ff) + mkey = (Phi, version[Phi], ff in mem, X) + lastkey = last if isinstance(last, dict) else {} + big = len(mem) > BIG + if mkey != lastkey.get(variant) and (not big or t == hi - 1 or version[Phi] % 40 == 0): + lastkey[variant] = mkey; it[4] = lastkey + bkey = (Phi, version[Phi], tuple(sorted(mem))) + if bkey not in cache: + if len(cache) > 64: cache.clear() + cache[bkey] = reduce_basis([(r, rows[r]) for r in sorted(mem) if rows[r]]) + combo = solve(cache[bkey], d['v']); d['tests'] += 1 + if combo is not None: + d['found'][variant] = dict(t=t, frame=Phi, combo={str(k): str(v) for k, v in combo.items()}, + dyadic=all(dyadic(v) for v in combo.values()), window=wi, members=len(mem)) + log(' FOUND fix[%s]: pair f=%s (%d,%d) deficit on %s at t=%d frame %s combo %s dyadic=%s' % ( + variant, cands[ci]['f'], i1_, i2_, X, t, Phi, d['found'][variant]['combo'], d['found'][variant]['dyadic'])) + keep.append(it) + active = keep + # apply event, update membership/version + oldf = None + if e[0] == 'scalar': oldf = frames[tuple(e[1][1])] + elif e[0] in ('warp', 'climb'): oldf = e[3] + elif e[0] == 'center': oldf = e[2] + d_role = apply(e, rows, frames) + if d_role is not None: + newf = frames[d_role] + if oldf != newf: + if oldf is not None: members[oldf].discard(d_role); version[oldf] += 1 + if newf is not None: members[newf].add(d_role) + if newf is not None: version[newf] += 1 + if t % 2000 == 0: + log(' t=%d/%d active=%d elapsed=%.0fs' % (t, n, len(active), time.time() - t0)) +# ---------- results ---------- +res = [] +for cd in cands: + ok = [v for v in ('early', 'late') if all(d['found'][v] is not None for d in cd['defs'])] + res.append(dict(f=cd['f'], i1=cd['i1'], i2=cd['i2'], E=cd['E'], F=cd['F'], G=cd['G'], all_fixable=ok, + defs=[dict(X=str(d['X']), Y=str(d['Y']), j=d['j'], q=str(d['q']), windows=d['windows'], + tests=d['tests'], found=d['found']) for d in cd['defs']])) +json.dump(res, open(f'result_{ORIENT}.json', 'w'), indent=1) +nfix = sum(1 for r in res if r['all_fixable']); ndef = sum(len(r['defs']) for r in res) +nfound = sum(1 for r in res for d in r['defs'] if any(d['found'].values())) +log('DONE %s: pairs %d, fully fixable pairs %d; deficits %d, fixable deficits %d' % (ORIENT, len(res), nfix, ndef, nfound)) +for r in res: + if r['all_fixable']: log(' FIXABLE PAIR ' + json.dumps(r)[:600]) diff --git a/research/fusion-pair-scalar-rewiring/verify.py b/research/fusion-pair-scalar-rewiring/verify.py new file mode 100644 index 0000000000..fbc1766167 --- /dev/null +++ b/research/fusion-pair-scalar-rewiring/verify.py @@ -0,0 +1,288 @@ +#!/usr/bin/env python3 +"""No H1+H1 -> H2 fusion pair in the #4610 word by free scalar rewiring (negative result, no new kappa). + +Mark (Matarener), with substantial Claude Code (Claude) assistance. Apache-2.0. + +Reads only the public #4610 package (Cao Yifan / intqwq): + research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz + research/kappa-round3-warp-20261022/ARITHMETIC.json +and the bar of research/fragmentation-ceiling (DreamingOfClouds, #5226). + +Question (#5226 Theorem B, #5243): is there a field with two consecutive rank-1 climbs E->F->G whose events +can be re-wired with free same-frame scalar operations so that it pays one rank-2 climb E->G instead? +Each such fusion lowers the fragmentation loss by 2 - 2^t* = 0.0041868 per call. + +This script certifies, exactly and in a few seconds, the structural obstruction: + (S1) every consecutive rank-1 pair has at least one event touching the field at the intermediate frame F; + (S2) for every pair whose intermediate events are plain ADDs (1261 of 1363 per orientation) at least one + partner field never occupies the target frame G at any time of the program, so the intermediate + interaction cannot be moved after a merged climb; + (S3) only 12 pairs (cold helpers at frame 0) have all partners in the start frame E at some time, and each + is blocked before the merged climb by exactly one read of the partner by a main field at F, and that + main never shares a frame with the helper afterwards; + (P) any repair that adds a paid job costs >= 1^t* = 1 > 0.0041868 (and a descent >= 1.99022, #5226 Thm D). +The exact row-level compensation searches (tools/compsearch.py, tools/cascade.py; 6 and 50 minutes) are +recorded in RESULT.json as evidence, not replayed here. + +Usage: python3 -I -W error -B verify.py [--write] +Exit 0 and marker PASS_NO_FUSION_PAIR_SCALAR_REWIRING iff every assertion passes and RESULT.json matches. +""" +import collections +import gzip +import hashlib +import json +import os +import sys +from decimal import Decimal as D, getcontext + +getcontext().prec = 50 +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(os.path.dirname(HERE)) +W3 = os.path.join(ROOT, 'research', 'kappa-round3-warp-20261022') +BAR = D('0.0030233') +WORD_SHA256 = '7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05' +COLD_PAIRS = [241, 243, 257, 259, 273, 275, 289, 291, 305, 307, 401, 417] + + +def need(ok, why): + if not ok: + raise AssertionError(why) + + +def pw(x, t): + x = D(x) + return D(0) if x == 0 else (t * x.ln()).exp() + + +def load_word(): + with open(os.path.join(W3, 'ACTUAL-WORD.json.gz'), 'rb') as fh: + raw = fh.read() + need(hashlib.sha256(raw).hexdigest() == WORD_SHA256, 'ACTUAL-WORD.json.gz bytes changed') + return json.loads(gzip.decompress(raw)) + + +def index(prog): + """touch[role] = [(idx, kind, partner)], hist[role] = [(idx, new_frame)], climbs[f] = [(idx, a, b, r)]""" + touch = collections.defaultdict(list) + hist = collections.defaultdict(list) + climbs = collections.defaultdict(list) + for i, e in enumerate(prog): + k = e[0] + if k == 'climb': + r = ('L', e[2]) + climbs[e[2]].append((i, e[3], e[4], e[5])) + touch[r].append((i, 'climb', None)) + hist[r].append((i, e[4])) + elif k == 'warp': + r = tuple(e[1]) + touch[r].append((i, 'warp', None)) + hist[r].append((i, e[4])) + elif k == 'center': + r = ('C', e[1]) + touch[r].append((i, 'center', None)) + hist[r].append((i, e[3])) + elif k == 'scalar': + g = e[1] + d = tuple(g[1]) + if g[0] in ('add', 'copy'): + s = tuple(g[2]) + touch[d].append((i, 'dst:' + g[0], s)) + touch[s].append((i, 'src:' + g[0], d)) + else: + touch[d].append((i, 'dst:' + g[0], None)) + if g[0] == 'clear': + hist[d].append((i, e[2])) + return touch, hist, climbs + + +def frame_at(start, hist, r, t): + f = start.get(r) + for i, ff in hist[r]: + if i <= t: + f = ff + else: + break + return f + + +def structural(word, orient, control=None): + """S1-S3 on one orientation. control='drop-main-read' deletes the blocking read of the first cold pair.""" + c = word['canonical'] + fr = c['frames'] + prog = list(word['programs'][orient]) + if control == 'drop-main-read': + # the read L70 += -L240 at frame 72 between the climbs of L240 (backward) / its transpose (forward) + idx = [i for i, e in enumerate(prog) if e[0] == 'scalar' and e[1][0] == 'add' + and sorted((tuple(e[1][1]), tuple(e[1][2]))) == [('L', 70), ('L', 240)] and e[2] == 72] + need(len(idx) == 1, 'control read not found') + prog[idx[0]] = ['phase', 'control_deleted_read'] + touch, hist, climbs = index(prog) + start = {('L', i): f for i, f in enumerate(c['start'])} + nf = len(c['start']) + # H1/H2 replay check as in fragmentation-ceiling/verify.py + cur = list(c['start']) + for e in prog: + if e[0] == 'climb': + f, a, b, r = e[2], e[3], e[4], e[5] + need(cur[f] == a and r == len(fr[b]) - len(fr[a]) and r > 0, 'climb not nested/ranked: %r' % (e,)) + cur[f] = b + elif e[0] == 'warp': + f, a, b = e[1][1], e[3], e[4] + need(cur[f] == a and len(fr[a]) == len(fr[b]), 'warp changes dimension: %r' % (e,)) + cur[f] = b + need(cur == list(c['final']), 'final frames') + out = collections.Counter() + out['climbs'] = sum(len(v) for v in climbs.values()) + out['rank1_climbs'] = sum(1 for v in climbs.values() for x in v if x[3] == 1) + cold_detail = [] + feasible_pairs = [] + for f, cl in climbs.items(): + for (i1, E, F, r1), (i2, F2, G, r2) in zip(cl, cl[1:]): + if r1 != 1 or r2 != 1: + continue + # F2 may differ from F when the field is warped between the climbs (those pairs are counted below) + out['pairs'] += 1 + between = [t for t in touch[('L', f)] if i1 < t[0] < i2] + if not between: + out['idle_pairs'] += 1 + continue + if any(t[1] not in ('src:add', 'dst:add') for t in between): + out['pairs_with_warp_or_nonadd'] += 1 + continue + out['pure_add_pairs'] += 1 + partners = [P for _, _, P in between] + ever_G = all(any(ff == G for _, ff in hist[P]) or start.get(P) == G for P in partners) + ever_E = all(any(ff == E for _, ff in hist[P]) or start.get(P) == E for P in partners) + if not ever_G: + out['pure_add_pairs_partner_never_in_G'] += 1 + if ever_E: + out['pure_add_pairs_all_partners_ever_in_E'] += 1 + # exact relocation test (frame-level): move every intervening event to a time when the field + # (in E before the merged climb, in G after it) and its partner share a frame, with the partner's + # value unchanged (field is dst) or only receiving commuting adds (field is src) in between. + n = len(prog) + nxt = min([t[0] for t in touch[('L', f)] if t[0] > i2], default=n) + prv = max([t[0] for t in touch[('L', f)] if t[0] < i1], default=-1) + + def quiet(P, lo, hi, p_is_dst): + for i, k, _ in touch[P]: + if lo < i < hi: + if k == 'climb': + continue + if p_is_dst and k == 'dst:add': + continue + if (not p_is_dst) and k.startswith('src:add'): + continue + return False + return True + ok_late = ok_early = True + for j, k, P in between: + p_is_dst = k.startswith('src') + good = False + for ci, _ in [(i2, None)] + [(ii, ff) for ii, ff in hist[P] if i2 < ii < nxt]: + if frame_at(start, hist, P, ci) == G and quiet(P, j, ci + 1, p_is_dst): + good = True + break + ok_late = ok_late and good + good = False + for ci, _ in [(prv, None)] + [(ii, ff) for ii, ff in hist[P] if prv < ii < i1]: + if frame_at(start, hist, P, max(ci, 0)) == E and quiet(P, ci, j, p_is_dst): + good = True + break + ok_early = ok_early and good + if ok_late or ok_early: + out['relocatable_pairs'] += 1 + feasible_pairs.append((f, i1, i2, 'late' if ok_late else 'early')) + if ever_E and f in COLD_PAIRS + [x - 1 for x in COLD_PAIRS]: + # S3 detail: the single blocking read of the partner by a main at F + need(len(between) == 1, 'cold pair has one intervening event') + j, k, P = between[0] + p_enter = max([i for i, ff in hist[P] if i < j and ff == F], default=-1) + # backward: a main reads P (M += q P); forward (the transpose): the main feeds P (P += q M) + reads = [(i, M) for i, kk, M in touch[P] if p_enter < i < j and kk in ('src:add', 'dst:add')] + mains = [M for _, M in reads if M[1] < 224] + shared_later = [] + for i, M in reads: + for tt, ff in hist[M]: + if tt > i and (ff == G or ff == E): + shared_later.append((M, tt, ff)) + cold_detail.append(dict(field=f, partner=P[1], E=E, F=F, G=G, blocking_events=[(i, M[1]) for i, M in reads], + main_readers=len(mains), reader_later_in_E_or_G=shared_later)) + for key in ('idle_pairs', 'pairs_with_warp_or_nonadd', 'pure_add_pairs', 'pure_add_pairs_partner_never_in_G', + 'pure_add_pairs_all_partners_ever_in_E', 'relocatable_pairs'): + out[key] += 0 + return dict(out), cold_detail, feasible_pairs + + +def main(): + write = '--write' in sys.argv + word = load_word() + with open(os.path.join(W3, 'ARITHMETIC.json'), encoding='utf-8') as fh: + A = json.load(fh) + need(sum(A['local_paid'].values()) == 3298 and A['local_paid']['1'] == 2201, 'ARITHMETIC local_paid census') + result = dict(schema='fusion-pair-scalar-rewiring/1', word_sha256=WORD_SHA256, bar=str(BAR), orientations={}) + for orient in ('forward', 'backward'): + out, cold, feas = structural(word, orient) + need(out['climbs'] == 3290 and out['rank1_climbs'] == 2201, '%s climb census' % orient) + need(out['pairs'] == 1363, '%s: 1363 consecutive rank-1 pairs' % orient) + need(out['idle_pairs'] == 0, 'S1: an idle pair exists') + need(out['pure_add_pairs'] == 1261 and out['pairs_with_warp_or_nonadd'] == 102, '%s pair classes' % orient) + need(out['pure_add_pairs_partner_never_in_G'] == 1261, 'S2: some pure-add pair has every partner in G at some time') + need(out['pure_add_pairs_all_partners_ever_in_E'] == 12, 'S3: 12 cold pairs') + need(out.get('relocatable_pairs', 0) == 0 and not feas, 'a relocatable pair exists: %r' % (feas,)) + need(len(cold) == 12 and all(len(x['blocking_events']) == 1 and x['main_readers'] == 1 and not x['reader_later_in_E_or_G'] + for x in cold), 'S3 detail: one main event on the partner, no later shared frame') + result['orientations'][orient] = dict(census=out, cold_pairs=cold) + print('[%s] %s' % (orient, json.dumps(out, sort_keys=True))) + # positive control: deleting the blocking main read makes the first cold pair relocatable in both orientations + for orient in ('forward', 'backward'): + out, _, feas = structural(word, orient, control='drop-main-read') + need(out['relocatable_pairs'] == 1 and len(feas) == 1 and feas[0][0] in (240, 241), 'control: %r' % (feas,)) + print('[control %s] deleting the main read makes exactly one pair relocatable: %r' % (orient, feas)) + # negative control: a wrong climb rank is rejected by the H2 replay + bad = json.loads(json.dumps(word)) + for e in bad['programs']['backward']: + if e[0] == 'climb': + e[5] += 1 + break + try: + structural(bad, 'backward') + except AssertionError: + print('[control] corrupted climb rank rejected') + else: + need(False, 'corrupted word accepted') + # prices at the bar t* and at the #4610 root + prices = {} + for name, t in (('bar_0.0030233', 1 - BAR), ('root_4610', 1 - D('0.0030217758'))): + merge = 2 - pw(2, t) + extra_job = pw(1, t) + descent = pw(1, t) + pw(10, t) - pw(9, t) + need(extra_job > merge * 200 and descent > merge, 'price order') + prices[name] = dict(t=str(t), merge_gain_1plus1_to_2=str(merge), extra_rank1_job=str(extra_job), descent_price_thmD=str(descent), + needed_per_call_for_bar='0.0209331969') + print('[price %s] merge gain %s, one extra paid rank-1 job %s, descent %s' % (name, merge, extra_job, descent)) + need(abs(D(prices['bar_0.0030233']['merge_gain_1plus1_to_2']) - D('0.0041868')) < D('1e-6'), 'merge value of #5226 [10]') + result['prices'] = prices + result['row_level_searches'] = { + 'note': 'exact rational row engine (same convention as PR #5377 native.py); run by tools/compsearch.py and tools/cascade.py ' + 'on the backward word; 6 and 50 minutes; not part of the registered replay', + 'compsearch_backward': dict(pairs=1261, deficits=2111, repayable_deficits=12, fully_repayable_pairs=0, + repayable_deficits_description='the 12 partner-helper deficits of the cold pairs, repaid at frame 0 before the climbs; ' + 'the main-read deficit of each of these pairs is never repayable'), + 'cascade_backward': dict(pair_variants=2522, successes=0, repayments=0, dead_over_24_deficient_fields=1446, unfinished_with_deficits=1076, + sampling='frames with more than 80 members tested every 100th version'), + 'forward': 'not run to completion; the forward program is the transpose of the backward program and shows the same obstruction (S1-S3 above)', + } + path = os.path.join(HERE, 'RESULT.json') + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + if write: + with open(path, 'w', encoding='utf-8', newline='\n') as fh: + fh.write(text) + else: + with open(path, encoding='utf-8', newline='') as fh: + need(fh.read() == text, 'RESULT.json differs from the recomputed result; run with --write to refresh') + print('PASS_NO_FUSION_PAIR_SCALAR_REWIRING') + + +if __name__ == '__main__': + main() From f5f10fc1ce4d753628faa78eda3af5c87a82f690 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 13:35:00 +0300 Subject: [PATCH 2/2] Point the current CI section at frontier5413 (exact repair from #5420) Canonical main still names make frontier4610-verify while the selected record requires frontier5413-verify, so the shared onboarding test fails before any package replay. This reuses byte-for-byte the docs/ci-verification.md repair of #5420 (head baa8fbb8345c2fab0bc213479539c338d4c80443, Clear1nsight); no scientific file changes. Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/ci-verification.md | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 494b7ca1d4..3bf623230e 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,40 @@ # CI verification -## Current selected-family replay: #4610 with #5241 +## Current selected-family replay: #5413 with #5407 and #5414 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.003027288235, the [promotion and scope](research/pr-intake-evidence/pr5413-promotion/PROMOTION.md), +[explicit source closure](../certificates/frontier5413-source.json), +[review validation](research/pr-intake-evidence/pr5413-promotion/VALIDATION.json), and +[integration receipt](research/pr-intake-evidence/pr5413-promotion/INTEGRATION.json). + +`make frontier5413-verify` authenticates the selected source manifest, derives +the certificate from frozen numerical evidence, and exports the complete +three-package execution closure. It replays #5407's five-stage provider audit, +#5413's eight-stage admission, and #5414's independent companion screen serially. +The exported inputs are checked again afterward. Source-bound #4610/#5241 and +earlier BIT/native/compiler/tape/analytic foundation coverage is explicitly +reused; its historical suites are not rerun. + +Each package runs under an external sampled 1 GiB aggregate descendant-memory +guard, with timeouts of 660 seconds for the provider and primary packages and +120 seconds for the companion. On macOS the replay uses the reviewed RLIMIT_AS +adapter; on Linux it invokes the unmodified package wrappers. The recorded +successful local macOS replay does not establish a hosted Linux pass. + +The [frontier5413 workflow](../.github/workflows/frontier5413.yml) is manual-only, +uses Python 3.12 on Ubuntu, materializes the declared source closure, and uploads +receipts and logs. Its status is separate from local validation and recorded in +the integration receipt. Routine donor PRs do not launch this selected replay. + +`make selected-record-check` verifies metadata and source/proof hashes. It does +not execute the operators or prove the five inherited framework assumptions. +The finite checks do not establish the full integer multiplication theorem, +and the uniform word remains unmaterialized. + +## Historical selected-family replay: #4610 with #5241 + +The historical [selected record](../certificates/checkpoints/frontier4610.json) binds conditional κ = 0.0030217758, the [review](research/pr-intake-evidence/pr4610/PROOF-REVIEW.md), [explicit source closure](../certificates/frontier4610-source.json), [review validation](research/pr-intake-evidence/pr4610/VALIDATION.json), and