Price flag 9's head-step co-host at exactly +2 rank mass

research/p104-flag9-head-step-repair/PROOF.md

@@ -0,0 +1,184 @@
+# Proof: flag-9 head-step repair, its bill, and the order-preserving floor
+
+## Setup
+
+Pin CrocSwap main `bb4bccbf42844d2801487450727c2f63e10d1d0f`. Inputs:
+
+- The #2981 flag matching (`research/p104-joint-unit-flags/CERTIFICATE.json`).
+  Flag 9 has source 4, target 23 and basis head `196`.
+- The reviewed #1991 witness, recipes and checker in `research/p104-native-channel/`.
+
+All of these are hash-pinned. The channel semantics are those of
+`research/p104-native-channel/PROOF.md` §2–§3: a transport changes only the
+frame and pays the absolute dimension gap; an ADD is allowed only in a common
+frame and changes only the destination row.
+
+#3443 records that the published word lists `196` on `Y23` only in the
+after-frame of the terminal transport at event 3489, and that the generator
+list of `X4` drops `196` at event 500. This note does not rerun that literal
+census. It uses span membership, which is the chart-independent reading.
+
+## 1. The source drop is a chart change
+
+Event 500 transports `X4` from `[196]` to `[8, 64, 132, 260]`. The after-list
+does not contain `196`, but
+
+```text
+64 XOR 132 = 196.
+```
+
+So `196` stays in the span. Direct inspection of all 7 source frames (the
+initial frame and six transports) and of the live frame at all 21 events that
+name `X4` finds `196` in every one. From event 1326 on, that frame is the
+rank-9 full chart. The present-head obstruction on this flag is entirely on
+the target side. This is the same phenomenon #3451 found for flag 1, which
+#3443's generator-only wording does not record.
+
+`Y23` does not span `196` at any of its nine ADDs. Its final frame does.
+`Y28`'s final frame does not.
+
+## 2. The delivering update
+
+The only ADD into `Y23` that carries a nonzero `X4` coefficient is event 3124,
+
+```text
+Y23 += D28/4    in the chart [447, 127, 192].
+```
+
+`D28`'s row contributes `-1/2`, and that ADD leaves `Y23`'s `X4` coefficient
+at its final value `-1/2`. No earlier `Y23` ADD carries `X4`. The next event
+that names `D28` is 3126, `Y28 += D28/4`, in the same chart. Event 3125 does
+not name `D28`.
+
+## 3. Repair R0
+
+Let `CH3 = [447, 127, 192]` and `CH4 = CH3 + [196]`. Rank(`CH3`) is 3 and
+rank(`CH4`) is 4. `CH4` is contained in `Y23`'s final frame. R0 keeps every
+published event in order, with the same ADD registers and coefficients, and
+inserts one transport:
+
+| Published index | Published | R0 |
+|---|---|---|
+| 3122 | `D28: [447, 192] -> CH3`, rank 1 | `D28: [447, 192] -> CH4`, rank 2 |
+| 3123 | `Y23: [447, 127] -> CH3`, rank 1 | `Y23: [447, 127] -> CH4`, rank 2 |
+| 3124 | `Y23 += D28/4` in `CH3` | same ADD in `CH4`, then `D28: CH4 -> CH3`, rank 1 |
+| 3489 | `Y23: CH3 -> final`, rank 5 | `Y23: CH4 -> final`, rank 4 |
+
+Every changed transport is nested, and its rank equals the frame gap. `Y23`
+has no event between 3124 and 3489, so it stays in `CH4` until the terminal
+transport. `D28` is back in `CH3` before event 3126, so `Y28`, `Y29`, `Y22`,
+`Y31` and `Y103` keep their published charts.
+
+`verify.py` builds this word in memory and calls the published
+`check_native.validate()` unchanged. That checks every native edge (two
+published edges drop out and four new ones enter; 742 distinct edges), all
+208 endpoint adapters, and all 280 framed rows, including restoration of the
+72 dirty helpers. `independent.py` replays both words with exact rational rows
+and finds all 280 final rows equal to the published rows. In R0 the ADD at
+index 3124 runs in `CH4` while `X4` is in the full chart, and `X4` still has
+reads at repaired indices 3696, 3803, 3855, 3959 and 4010.
+
+Per-register rank mass changes only on `D28`, by `+2` (the extra rank on the
+way into `CH4`, and the rank-1 drop back). `Y23`'s entry grows by 1 and its
+terminal transport shrinks by 1. The paid-profile delta is
+
+```text
+-H1 + 2 H2 + H4 - H5.
+```
+
+For an affine price `H(r) = a + b r` this is `a + 2b`: one added transport
+occurrence and two added rank units. For `H(r) = r^2` the same delta is `-2`.
+The sign is not uniform across convex prices.
+
+## 4. Repair R1
+
+R1 deletes the published events 3123, 3124 and 3489 and, immediately after
+`D28`'s lift to the full chart at 3634 and before `D28 += Q7`, inserts
+
+```text
+Y23: [447, 127] -> FULL, rank 7
+Y23 += D28/4 in FULL
+Y23: FULL -> final, rank 1
+```
+
+`D28` is not written between 3124 and 3635, so the same coefficient still
+delivers `-1/2`. Nothing reads `Y23`, so moving that single ADD does not
+change any other row. Event count, ADD count and transport count stay at the
+published values. Rank mass grows by 2, all of it on `Y23`. The profile delta
+is `H7 - H5`, which is `2b` for every affine price and `+24` for `H(r) = r^2`.
+The published checker passes, with 741 distinct native edges. The co-hosted
+ADD is at repaired index 3633, and `X4` still has its five later reads.
+
+R1 is not order-preserving: it moves the delivering ADD. It matches R0's rank
+mass and removes R0's extra event. Under a positive per-event price it is the
+cheaper of the two exhibited repairs. Under a steep convex rank price, R0's
+profile can cost less.
+
+## 5. Order-preserving floor
+
+**Class P.** A repair is in class P when:
+
+1. every published event is kept, in published order, with the same opcode,
+   registers and ADD coefficient (transport frames may change, ADD chart
+   fields may change, and transports may be inserted);
+2. every initial and final frame is kept;
+3. every transport rank equals the absolute dimension gap of a nested pair.
+
+**Parity.** On one register the sum of absolute dimension gaps is congruent
+modulo 2 to `rank(final) - rank(initial)`, because every descent has to be
+matched by a later ascent. All 280 non-private registers of the published word
+already meet that floor, so every class-P repair adds a nonnegative even
+integer of rank mass on each of them. The total added rank mass is therefore
+0 or at least 2.
+
+**Zero is impossible for the delivering ADD.** Suppose a class-P repair adds
+no rank mass. Then every non-private path is monotone: a vector that enters a
+frame stays in every later frame of that register. The delivering ADD is still
+`Y23 += D28/4`, still followed, after whatever transports are inserted, by the
+published event 3126 `Y28 += D28/4`. Co-hosting requires `196` in `D28`'s
+frame at the ADD.
+
+- If some inserted transport removes `196` from `D28` before event 3126, that
+  transport is a descent, so `D28`'s mass is at least 2 above its floor.
+- If not, `D28` still spans `196` at event 3126, so the common chart forces
+  `Y28` to span `196` there. `Y28`'s final frame does not span `196`, and a
+  monotone path cannot drop it. So `Y28`'s mass is at least 2 above its floor.
+
+Thus every class-P repair that co-hosts `196` on `X4` and `Y23` at the
+delivering ADD adds at least 2 rank units. R0 adds exactly 2, so that floor
+is sharp. R0's extra unit is the descent on `D28`; `Y23` pays nothing because
+its final frame already contains `CH4`.
+
+The same monotone closure, applied to all nine `Y23` ADDs on the published
+word, finds no admissible update. Each forces the head into at least one
+register whose final frame excludes it:
+
+| Update | Partner | Final-excluding registers | First |
+|---:|---|---:|---|
+| 74 | `Q2` | 56 | `Y24` at 77 |
+| 75 | `Q5` | 56 | `Y24` at 79 |
+| 76 | `Q7` | 56 | `Y24` at 80 |
+| 2070 | `D20` | 56 | `Y28` at 2071 |
+| 2160 | `D10` | 56 | `Y28` at 2161 |
+| 2296 | `D28` | 56 | `Y28` at 2297 |
+| 2640 | `D20` | 23 | `Y28` at 2642 |
+| 2826 | `D10` | 14 | `Y28` at 2828 |
+| 3124 | `D28` | 5 | `Y28` at 3126 |
+
+`verify.py` computes this closure with a worklist. `independent.py` recomputes
+the final-excluding part with a forward sweep. The two agree on all nine rows.
+
+## 6. What this does not say
+
+Class P does not include repairs that reorder ADDs, change ADD coefficients,
+or change a final frame. R1 shows one legal reordering and still pays `+2`.
+It does not prove that every reordering pays `+2`. A zero-mass repair would
+have to introduce `196` on `D28` only after every later partner whose final
+frame excludes `196` has already read `D28`, and then keep `196` on the
+monotone path to `D28`'s full final frame. No such schedule is constructed
+or excluded here.
+
+Neither repair is an `I - G/2` correction, a dirty-restoration program, or a
+change to the selected conditional κ `0.001672660197076918`. The channel still
+implements the published `G/2` map. The co-hosted chart only removes the
+geometric obstruction recorded for this one flag.

research/p104-flag9-head-step-repair/README.md

@@ -0,0 +1,103 @@
+# Flag 9's delivering update can be co-hosted for exactly two added rank units
+
+**Finite repaired words with an exact bill, plus a sharp order-preserving floor. No new exponent.**
+
+Open [#3443](https://github.com/CrocSwap/integer-mult-bounds/pull/3443) shows that
+on the published 4,058-event P104 word, present-head flag 9 (`X4` → `Y23`,
+basis head `196`) never updates `Y23` while both endpoints list the head. Its
+open question asks what a changed schedule that co-hosts the head would cost.
+The same question is open for this flag in
+[#3508](https://github.com/CrocSwap/integer-mult-bounds/pull/3508) and was released
+without a submission. Flag 1's repair is the separate open
+[#3532](https://github.com/CrocSwap/integer-mult-bounds/pull/3532); this package
+does not recompute it. Flag 43's zero-mass repair is the method being followed,
+not the result: flag 9 has no zero-mass order-preserving repair.
+
+## Result
+
+The published source "drop" at event 500 does not remove `196` from the span.
+The after-list is `[8, 64, 132, 260]` and `64 XOR 132 = 196`. All 7 source
+frames and all 21 events that name `X4` span `196`. The obstruction is on
+`Y23` only.
+
+The only `Y23` update that carries `X4` is event 3124, `Y23 += D28/4`. It
+delivers `-1/2` and settles `Y23`'s final `X4` coefficient. Two repaired words
+make that ADD co-host `196` while `X4` is in its rank-9 chart and still has
+five later reads. The published `check_native.validate()` passes on both.
+
+- **R0 (order-preserving).** `D28` and `Y23` enter the published 3124 chart
+  plus `196`. The ADD runs there. One inserted transport drops `D28` back
+  before `Y28` reads it. `Y23` keeps the head until its terminal transport.
+  Added rank mass is `+2`, all of it on `D28`.
+- **R1 (relocation).** The delivering ADD moves into `D28`'s full-chart window
+  just after event 3634. `Y23` lifts from `[447, 127]` to the full chart, takes
+  the ADD, and drops to its final frame. No event is added or removed. Added
+  rank mass is `+2`, all of it on `Y23`.
+
+| Bill term | Published | R0 | R1 |
+|---|---:|---:|---:|
+| Events | 4,058 | 4,059 | 4,058 |
+| Scalar ADDs | 2,624 | 2,624 | 2,624 |
+| Transport occurrences | 1,410 | 1,411 | 1,410 |
+| Rank mass | 2,368 | 2,370 | 2,370 |
+| Distinct native edges | 740 | 742 | 741 |
+| Where the +2 sits | — | `D28` | `Y23` |
+| Paid profile delta | — | `-H1 + 2H2 + H4 - H5` | `H7 - H5` |
+
+Under an affine price `H(r) = a + b r`, R0 costs `a + 2b` and R1 costs `2b`.
+Under `H(r) = r^2`, R0 costs `-2` and R1 costs `+24`. R1 is cheaper when each
+event has a positive price. R0 can be cheaper for a steep convex rank price.
+
+In the order-preserving class (published events kept in order, endpoint frames
+kept, nested rank-gap transports, insertions allowed), added rank mass is even,
+and zero is impossible: keeping `196` on `D28` through event 3126 forces it
+into `Y28`, whose final frame excludes it, and dropping it before 3126 costs
+2 on `D28`. R0 meets the floor. The same closure obstructs all nine `Y23`
+updates. Reordering those reads is not ruled out and is not given a zero-mass
+schedule here.
+
+Selected κ stays `0.001672660197076918`. The argument is in [PROOF.md](PROOF.md).
+
+## Reproduce
+
+From the repository root, CPython 3.12:
+
+```sh
+python3.12 -I -B research/p104-flag9-head-step-repair/verify.py
+python3.12 -I -O -Werror -B research/p104-flag9-head-step-repair/verify.py
+python3.12 -I -O -Werror -B research/p104-flag9-head-step-repair/independent.py
+python3.12 -I -O -Werror -B research/p104-flag9-head-step-repair/test_package.py
+python3.12 -B scripts/research_package.py --package research/p104-flag9-head-step-repair
+```
+
+`verify.py` is read-only. It loads the pinned `check_native.py` by path and runs
+its `validate()` on each repaired word built in memory. Admission goes through
+`need()` and still fires under `-O`. `independent.py` imports neither `verify.py`
+nor the native checker. `test_package.py` corrupts temporary copies and checks
+that both scanners reject all 10 mutations, including deletion of R0's return
+transport and an undercharged terminal rank. `build.py` is the producer and is
+not part of the replay.
+
+## Credit
+
+Credit #3443 for flag 9's published literal chronology, #3451 for the span
+reading on flag 1, and #3508 for the head-step repair method and the class-P
+closure rule. Credit #3349 for the present-head census. Credit Nick Petalas /
+#2981 for the flag matching, and the reviewed #1991 native channel (Chafik
+Boukhalfa) for the witness, checker and compiler. #3532 is the flag-1 repair
+this package deliberately does not repeat; its open question 3 asks for this
+flag. Prepared by unpaidmoon with substantial Cursor Grok assistance. No
+independent human or formal-kernel review is claimed. Apache-2.0.
+
+## Open next questions
+
+1. Is there a zero-added-mass co-hosting repair that reorders `D28`'s reads?
+   Every partner whose final frame excludes `196` would have to read `D28`
+   before `196` enters, and `196` would then have to stay on `D28`'s monotone
+   path to the full chart. R1 still pays `+2`, so the exhibited relocation is
+   not that schedule.
+2. Can a side correction use R0's chart `[447, 127, 192, 196]` at the repaired
+   index 3124, or R1's full chart at 3633, to restore `X4` into `Y23`, and what
+   does the `I - G/2` correction cost at that cut?
+3. Which of R0 and R1 is cheaper under the channel's actual per-rank weights?
+   Affine prices prefer R1; `H(r) = r^2` prefers R0.