Show that commuting staged544 moves cannot retarget a rank-1 ADD line

research/staged544-moved-add-pair/PROOF.md

@@ -0,0 +1,118 @@
+# Commuting moves cannot retarget a staged544 line
+
+This is a finite obstruction on two pinned words, plus one scalar identity.
+It is not a supplier, a kappa bound, or a theorem about every circuit.
+
+The move contract is `apply_move` from the vendored tracer: one ADD stays in
+its section, crosses only gates accepted by `crosses`, and may replace its
+common frame. Entrances, warps, and every other gate's frame stay fixed.
+`crosses` is the scalar normal form: an ADD crosses another ADD when neither
+destination is the other's source, and it crosses a nonzero scale on a
+touched register. It does not cross a warp.
+
+## 1. Witness for every rank-1 ADD
+
+On each provider, 735 ADD gates have a rank-1 common frame `M`. For each such
+gate `g` the checker finds an operand register `r` whose incoming frame is
+already `M`, and an event that first put `M` into `r`:
+
+| Witness | Gates | What creates `M` on `r` |
+|---|---:|---|
+| Entrance | 653 | `r` starts inside `M` |
+| Map | 70 | A warp map, earlier in the same section or in an earlier section |
+| Dependence | 12 | An earlier rank-1 ADD that does not commute with `g` |
+
+These three classes partition the 735 gates. Both providers give the same
+counts and the same twelve dependence pairs. The two provider files are not
+equal.
+
+The twelve pairs are adjacent ADDs in section `A`. The later gate reads the
+register written by the earlier gate, so `crosses` fails in both directions:
+
+| Producer | Consumer | Register |
+|---:|---:|---:|
+| 2027 | 2028 | 240 |
+| 2029 | 2030 | 242 |
+| 2181 | 2182 | 256 |
+| 2183 | 2184 | 258 |
+| 2335 | 2336 | 272 |
+| 2337 | 2338 | 274 |
+| 2489 | 2490 | 288 |
+| 2491 | 2492 | 290 |
+| 2643 | 2644 | 304 |
+| 2645 | 2646 | 306 |
+| 3569 | 3570 | 400 |
+| 3723 | 3724 | 416 |
+
+## 2. The witness survives every commuting move
+
+**Persistence.** `tracing` accepts a word only when every non-map event's
+frame contains that register's incoming state. A map may replace the state.
+Its frame belongs to a warp, and `apply_move` neither relocates a warp nor
+edits frame. Thus, once register `r` contains a subspace `M`, every later
+non-map event on `r` still contains `M`, up to the next map. An ADD whose
+incoming state contains `M` can be given only a frame that contains `M`.
+A gate that commutes past `g` and lands on `r` while `r` already contains `M`
+is under the same restriction, so it does not erase `M`.
+
+**Finite hypotheses.** On both providers, for every rank-1 ADD and its witness
+register, every frame from the witness source through that register's incoming
+state contains `M`. An entrance or dependence window contains no map. A map
+window starts at the witness warp and contains no second map. The checker
+tests these facts; it does not enumerate move sequences.
+
+**Theorem.** After any finite sequence of `apply_move` steps, every originally
+rank-1 ADD still has a common frame containing its original line.
+
+The proof is induction on the original index in the section. The witness
+source still supplies `M` before the gate, and no warp on the witness register
+can enter the open interval after that source: warps do not move, and
+`crosses` rejects passing a warp.
+
+- **Entrance.** The start frame is immutable and contains `M`. The window has
+  no map, so every event on the register before the gate is a climb or a
+  check. Persistence keeps `M`.
+- **Map.** The witness warp is immutable, fails `crosses` with the gate, and
+  sits earlier in the section or in an earlier section. Its map frame contains
+  `M`. Persistence keeps `M` from that map until the gate.
+- **Dependence.** The producer is an earlier rank-1 ADD and neither order
+  commutes, so the order is invariant. By induction its frame still contains
+  `M`. The window has no map. Persistence keeps `M` until the consumer.
+
+In each case the incoming state contains `M`, so every legal frame of the gate
+contains `M`. No legal image is a line disjoint from `M`. In particular, no
+sequence of commuting moves realizes the crossed-line pattern on these words:
+that pattern replaces `M` by a disjoint line on both gates.
+
+## 3. The crossed-line identity has histogram delta zero
+
+The pattern left open by PR #3964 is still a real scalar identity. It just
+does not occur under this move contract, and it does not improve the bill.
+PR #4122 already invoices a richer swap-and-restore identity at delta zero
+and explicitly does not search these providers. The calculation below is the
+#3964 synthetic control, not a second claim on that invoice.
+
+On helpers `h = 300` and `s = 301`, with fixed terminal frame `span(e1, e2)`:
+
+```text
+h += 1 * s    frame span(e1)
+h += 1 * s    frame span(e1)
+```
+
+Replacing both frames by `span(e2)` keeps every opcode, operand, and
+coefficient. Each helper climbs `0 → line → line → plane`: two rank-1 children
+per helper, four rank-1 children altogether, before and after. The histogram
+delta is zero. Either one-edit intermediate is illegal, because `span(e1)` and
+`span(e2)` are incomparable. The same rejection is reproduced by the vendored
+tracer; its fixed target-register epilogue is identical on both words, so the
+full tracer bill is unchanged as well.
+
+An unchanged histogram is not a kappa gain. The favorable exchange
+`H1 - 2 H2 + H3` is a different signed row and is not this delta.
+
+## 4. What is not claimed
+
+Noncommuting rewrites are outside `apply_move`. Frames that properly contain
+the old line are outside the theorem. Cleanup, native phases, owners, and
+all-size transfer are not repriced, because no disjoint-line move exists to
+price. The selected conditional kappa stays `0.001672660197076918`.

research/staged544-moved-add-pair/README.md

@@ -0,0 +1,87 @@
+# Commuting moved-ADD pairs do not retarget a staged544 line
+
+**Negative result. No new kappa.** Selected kappa stays `0.001672660197076918`.
+
+On both pinned PR3734 providers, every rank-1 ADD frame has a witness operand
+whose line is created by an entrance, a warp map, or an earlier rank-1 ADD
+that does not commute with it. Those witnesses are invariant under
+`apply_move`. No finite sequence of commuting ADD moves can put that frame on
+a disjoint line. The crossed-line pattern asked for by PR #3964 therefore does
+not occur in this contract.
+
+The same pattern, written as two scalar ADDs, keeps its opcodes and
+coefficients. Each of the two helpers contributes two rank-1 climbs before and
+after the retarget, so the child-histogram delta is zero. Either single-frame
+intermediate is illegal. An unchanged histogram is not a paid-profile gain.
+
+The argument and the twelve dependence pairs are in [PROOF.md](PROOF.md).
+
+PR #4122 prices a different scalar identity for the same open question: a
+swap of `y += x` with `y += z`, plus restoration, also at histogram delta 0.
+That package does not search these providers. The obstruction above is the
+provider half it leaves open. The two-ADD identity in section 3 of the proof
+is the synthetic control already named by PR #3964, recomputed here only to
+show that its bill is zero and that it is not an occurrence.
+
+## Scope and evidence
+
+Original card: `scalar-to-moment`, scope **refined**. The card asks for one
+scalar simplification and its histogram. This package takes the released
+moved-ADD question: a frame edit that does not change the scalar program.
+Details, the stop rule, and the bottleneck link are in [TASK.json](TASK.json).
+
+| Provider | SHA-256 | Rank-1 ADDs | Entrance | Map | Dependence |
+|---|---|---:|---:|---:|---:|
+| `BORROW-WORD-43base.json.gz` | `5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699` | 735 | 653 | 70 | 12 |
+| `BORROW-WORD-43extra.json.gz` | `965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e` | 735 | 653 | 70 | 12 |
+
+The gzip bytes and `vendor/retiming.py`
+(`591d7278541ac4de9e9b6fc1e17aba23b205ac4b6c81824a28fc08294658ef0d`) are
+unmodified copies of PR #3964 at `8a8bfb8d36cf5c9f7681b9e7f5d7876a4ba0f5a0`,
+paths `research/staged544-stationary-pairs/inputs/` and
+`vendor/retiming.py`. That commit is not an ancestor of this package's base
+`bb4bccbf42844d2801487450727c2f63e10d1d0f`, so [SOURCES.json](SOURCES.json) pins
+only the catalogue and selected record. `verify.py` checks the three SHA-256
+values directly.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root:
+
+```sh
+python3.12 -B research/staged544-moved-add-pair/verify.py
+python3.12 -B scripts/research_package.py --package research/staged544-moved-add-pair
+```
+
+Expected marker:
+
+```text
+PASS_MOVED_ADD_PAIR providers=2 rank1=735 entrance=653 map=70 dependence=12 disjoint_line_moves=0 toy_helper_bill=4xrank1 toy_delta=0 no_new_kappa
+```
+
+The direct command also passes under `-O`. No Lean, Docker, or selected cold
+replay was run.
+
+## Open next questions
+
+1. Can one explicit noncommuting transposition, with a scalar correction, put
+   a rank-1 ADD on a disjoint line and strictly lower the histogram for every
+   real `0<a<1`? The twelve read-after-write pairs are the place to start.
+   This obstruction stops at `crosses`, so that rewrite is a different
+   identity. No such correction is specified here.
+2. Does a commuting move whose new frame properly contains the old line improve
+   the histogram? Containing frames are outside this theorem. PR #3970 already
+   prices fixed-frame displacement two; a containing-frame census needs its
+   own domain.
+
+## Credit
+
+The providers are dataisfire's PR #3734 words as vendored by Chris R /
+Clear1nsight in PR #3964. The stationary legality theorem, the crossed-line
+control, and `retiming.py` are from that PR and its credited PR #3886 /
+PR #3942 lineage. Parallel PR #4122, discussion comment 19056694, invoices a
+swap-and-restore identity and does not search these words. The witness
+partition and the invariance argument are the part added here.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent
+human or formal-kernel review is claimed. Apache-2.0.

research/staged544-moved-add-pair/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/staged544-moved-add-pair/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "scalar-to-moment",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "original_card": {
+    "id": "scalar-to-moment",
+    "question": "Can one known scalar simplification be converted into an actual paid-profile improvement?",
+    "starting_points": [
+      "research/r439-bsection-stars-seed01/README.md",
+      "certificates/selected-result.json"
+    ],
+    "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",
+        "research/r439-bsection-stars-seed01/verify.py"
+      ],
+      "expected": "PASS_R439_BSECTION_STARS",
+      "inspect": "Observe that the positive control improves scalar counts while retaining the paid histogram.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Choose one simplification and derive the complete changed frame itinerary, or prove why it cannot change the histogram.",
+    "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"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "On both pinned PR3734 staged544 providers, no finite sequence of commuting ADD moves can retarget a rank-1 common frame onto a disjoint line. The crossed-line scalar identity has child-histogram delta 0.",
+  "scope_change_reason": "The card allows one scalar simplification and its frame itinerary. This session takes the released moved-ADD question from #3964: the crossed-line frame pattern, whose scalar program does not change. The domain is the two pinned providers and the apply_move commutation contract, not a new R439 word.",
+  "bottleneck_link": "A legal histogram change, not an unchanged scalar program, is what could move the moment. This pattern's histogram delta is zero and the pattern is unreachable by commuting moves on these words, so it does not change kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once every rank-1 ADD has an entrance, map, or noncommuting rank-1 producer witness and the toy identity's histogram delta is zero. Do not search noncommuting rewrites or frames that contain the old line.",
+  "outcome": "negative-result",
+  "evidence": "verify.py replays both vendored providers and the two-ADD identity. PASS_MOVED_ADD_PAIR reports entrance=653, map=70, dependence=12 on each provider and toy_delta=0.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok 4.7 wrote the checker and the argument. The providers and retiming.py are unmodified bytes from PR #3964.",
+  "open_questions": [
+    {
+      "question": "Can one explicit noncommuting transposition, with its scalar correction, put a rank-1 ADD on a disjoint line and strictly lower the child histogram for every real 0<a<1?",
+      "why_it_matters": "The obstruction stops at the crosses normal form. A read-after-write rewrite is a different scalar identity and could change the histogram.",
+      "first_step": "Take one of the twelve dependence pairs, write the transposed operators and the coefficient correction, and recompute the frame bill before any search.",
+      "blocked_by": "No legal noncommuting correction is specified in this package."
+    },
+    {
+      "question": "Does any commuting move whose new frame properly contains the old line improve the histogram?",
+      "why_it_matters": "Containing frames are outside this disjoint-line obstruction and could still be a paid-profile change.",
+      "first_step": "Price one commuting window whose upper frame has rank at least 2, using the same sign certificate as PR #3886.",
+      "blocked_by": "PR #3970 already prices fixed-frame displacement two; a containing-frame census needs its own domain."
+    }
+  ]
+}

research/staged544-moved-add-pair/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Both providers have 735 rank-1 ADDs, each with an entrance, map, or noncommuting producer witness whose window keeps the original line and has no interrupting map; the crossed-line identity keeps its scalar program and has histogram delta 0; one-edit intermediates are rejected."
+    }
+  ]
+}