Certify no H1+H1->H2 fusion pair in the #4610 word by free scalar rewiring (negative result, no new kappa)

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

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 |

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.