Price one moved-ADD crossed-frame pair at histogram delta zero.

research/moved-add-crossed-invoice/README.md

@@ -0,0 +1,118 @@
+# Moved-ADD crossed frames have a zero local invoice
+
+**No new κ.** Selected conditional κ stays `0.001672660197076918`.
+
+On three scalar registers, swapping two commuting additions and retargeting both
+frames from one line to the other crossed line is a legal final word. Each
+one-move intermediate is frame-illegal. The scalar map is the identity
+`y := y + x + z`, including arbitrary initial values, and the inverse cleanup
+restores those values. The charged rank histogram is six rank-1 children on
+both words, so the delta is zero.
+
+## Scope and evidence
+
+Catalogue card `scalar-to-moment`, scope **refined**. The card asks whether one
+scalar simplification changes a paid histogram. This package answers that for
+the moved-ADD pair requested by
+[discussion #1166 comment 19034220](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19034220),
+not for an R439 helper-star word.
+
+The predecessor stationary census (open PR #3964) proves that no such pair
+exists while both ADD addresses stay fixed on the pinned PR #3734 providers.
+Its synthetic control, old frames `span(e1)` and new frames `span(e2)` between
+`{0}` and `span(e1,e2)`, is not a gate move. The witness here is that same
+frame pattern realized by a move that the predecessor reorder test allows.
+
+### Identity
+
+Let `A` be `y += x` and `B` be `y += z`, with coefficient 1. Each gate's target
+is not the other gate's source, so the predecessor reorder test lets either
+gate pass the other and does not change the coefficient. Over any ring,
+
+```text
+A then B  =  B then A  =  (x, y + x + z, z)
+```
+
+from an arbitrary initial triple. The cleanup `y -= z` then `y -= x`, also at
+coefficient 1, restores the initial triple after either order. Replacing either
+coefficient by 2, or swapping the noncommuting pair `y += x` then `z += y`,
+breaks the equality. Both of those controls are checked.
+
+### Frames and invoice
+
+Frames are subspaces of `F_2^9`, stored as bit masks. A visit is legal only
+when the current frame is contained in the gate frame. The charged child has
+rank equal to the dimension gap. Every register starts at `{0}` and must finish
+at `V = span(e1, e2)`.
+
+| Word | Order and frames | `y` chain | Histogram |
+|---|---|---|---|
+| Original | `A` at `L`, `B` at `L`, then cleanup at `V` | `{0} ⊆ L ⊆ L ⊆ V` | six `H1` |
+| Moved pair | `B` at `M`, `A` at `M`, then the same cleanup | `{0} ⊆ M ⊆ M ⊆ V` | six `H1` |
+| Only `A` moved | `B` at `L`, `A` at `M` | `{0} ⊆ L ⊆ M` | illegal |
+| Only `B` moved | `B` at `M`, `A` at `L` | `{0} ⊆ M ⊆ L` | illegal |
+
+`L = span(e1)` and `M = span(e2)` are distinct lines, so neither contains the
+other. The `x` and `z` chains are one line visit plus the climb into `V` on
+both legal words. Cleanup uses frame `V` and adds the three remaining rank-1
+climbs. Rank mass is 6 on both words. The histogram delta is the zero vector,
+so `sum_r delta_r r^a = 0` for every real `a`. An unchanged histogram is not a
+κ gain.
+
+The same-line swap, both frames `L`, is legal. Illegality comes from the
+crossed lines, not from the reorder itself.
+
+### What this does not separate from a saving
+
+Widening both moved frames to `V` has delta `-6 H1 + 3 H2` against the original
+word. For every integer fraction `0 < p/q < 1`, `2^p < 2^q`, so
+`3 (2^a - 2) < 0` throughout `0 < a < 1`. That local moment decreases. The
+one-move intermediate that widens only `A` and leaves `B` on `L` is legal, so
+this saving sits in the sequential contract. It is a control, not a provider
+occurrence and not a supplier admission.
+
+No PR #3734 word was searched. Native warps, centre cuts, stock, precision,
+tape, all-size transfer and both supplier caps are absent. They are not priced
+as zero.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B research/moved-add-crossed-invoice/verify.py
+python3 scripts/research_package.py --package research/moved-add-crossed-invoice
+```
+
+Expected marker:
+
+```text
+PASS_MOVED_ADD_CROSSED_INVOICE registers=3 adds=2 cleanup=2 histogram_H1=6 delta=0 rank_mass_delta=0 both_intermediates=illegal scalar=commuting_identity favorable_sequential=-6H1+3H2 one_intermediate=legal no_new_kappa
+```
+
+The checker raises on a failed containment, a broken identity, or a histogram
+mismatch. It does not sample the providers.
+
+## Open next questions
+
+Does any moved-ADD pair on the two pinned PR #3734 providers have a legal final
+frame assignment, two illegal one-move intermediates, and a strictly negative
+moment for every real `a` in `(0,1)`? The three-register witness only shows that
+a move can create the crossed-line pattern, and that this pattern can have
+invoice zero. The first step is one scalar segment and the crossed-line
+assignment on pairs the reorder test already allows to cross. The provider trace
+lives in open PR #3964 rather than on this main checkout, and a full pair census
+is a separate budget.
+
+## Credit
+
+The stationary census, the synthetic crossed-line control and the reorder test
+are Chris R / Clear1nsight, PR #3964, head `8a8bfb8d36cf5c9f7681b9e7f5d7876a4ba0f5a0`.
+The open question is discussion #1166 comment 19034220. The legal-sequential
+predecessor is PR #3942. The paid exchange that motivates a histogram change is
+Dugongue's PR #3863; this witness does not realize that `H1 - 2 H2 + H3`
+exchange. The pinned providers are dataisfire's PR #3734 and are not replayed
+here.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent
+human review is claimed. Apache-2.0.

research/moved-add-crossed-invoice/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/moved-add-crossed-invoice/TASK.json

@@ -0,0 +1,60 @@
+{
+  "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": "Price one exact moved-ADD pair whose final frames are legal while both direct one-move intermediates are illegal, including the scalar identity and the cleanup invoice.",
+  "scope_change_reason": "The catalogue card starts from an R439 scalar-count saving. Discussion #1166 comment 19034220 asks for a different object: one moved ADD pair outside the stationary staged544 census, with its identity and complete local invoice, before any search. The card's histogram question is unchanged; the word is not an R439 helper-star.",
+  "bottleneck_link": "A local histogram change is the bridge from a scalar identity to a moment. This witness has histogram delta zero, so the identity is not an exponent improvement. The neighboring rank-2 widening does change the histogram but has a legal intermediate, so it is inside the sequential contract already studied.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one explicit pair, its identity and its invoice. Do not search the PR3734 providers or widen the gate set.",
+  "outcome": "completed",
+  "evidence": "verify.py checks the commuting identity, restoration, the zero histogram delta, both illegal intermediates, and the sequential favorable control.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok 4.7 agent, substantial assistance with the selection, the writeup and the checker.",
+  "open_questions": [
+    {
+      "question": "Does any moved-ADD pair on the two pinned PR3734 providers have a legal final frame assignment, two illegal one-move intermediates, and a strictly negative moment for every real a in (0,1)?",
+      "why_it_matters": "The three-register witness shows that moving gates can create the crossed-line pattern, but its invoice is zero. A provider occurrence with a negative moment would be a real sequentialization gap; absence would confine that gap to words outside this entrance and exit contract.",
+      "first_step": "Restrict to one scalar segment and to pairs that the predecessor reorder test allows to cross, then test only the crossed-line frame assignment on their shared target.",
+      "blocked_by": "The provider words and their trace are in open PR #3964, not on this main checkout. A full pair census is a different budget."
+    }
+  ]
+}

research/moved-add-crossed-invoice/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": 120,
+      "checks": "Commuting identity and cleanup restoration, zero histogram delta, both intermediates illegal, sequential favorable control, and noncommuting and coefficient rejections."
+    }
+  ]
+}

research/moved-add-crossed-invoice/verify.py

@@ -0,0 +1,170 @@
+#!/usr/bin/env python3
+"""Invoice one moved-ADD pair with two illegal direct intermediates.
+
+The frame predicate is the containment rule used by the staged544 retiming
+trace: a gate frame must contain each operand's current frame, and the rank
+gap is the charged child. Terminal frames are fixed. This file does not import
+the unmerged predecessor.
+"""
+from collections import Counter
+from fractions import Fraction
+
+X, Y, Z = 0, 1, 2
+REGISTERS = (X, Y, Z)
+
+
+def require(ok, why):
+    if not ok:
+        raise ValueError(why)
+
+
+def span(vectors):
+    points = {0}
+    for vector in vectors:
+        require(type(vector) is int and 0 <= vector < 512, "bad frame vector")
+        points |= {point ^ vector for point in tuple(points)}
+    return sum(1 << point for point in points)
+
+
+def rank(mask):
+    size = mask.bit_count()
+    require(size and size & (size - 1) == 0, "not a subspace")
+    return size.bit_length() - 1
+
+
+def contained(inner, outer):
+    return not inner & ~outer
+
+
+def crosses(left, right):
+    """Predecessor sufficient reorder test: targets are not each other's sources."""
+    require(left[0] == "add" and right[0] == "add", "reorder test is for ADDs")
+    return left[1] != right[2] and right[1] != left[2]
+
+
+def histogram(gates, ends):
+    current = {register: span(()) for register in REGISTERS}
+    paid = Counter()
+
+    def visit(register, frame):
+        require(contained(current[register], frame), "frame containment")
+        gap = rank(frame) - rank(current[register])
+        if gap:
+            paid[gap] += 1
+        current[register] = frame
+
+    for gate in gates:
+        require(gate[0] == "add" and gate[1] != gate[2], "binary ADD")
+        for register in gate[1:3]:
+            visit(register, gate[5])
+    for register in REGISTERS:
+        visit(register, ends[register])
+    return tuple(paid[rank_index] for rank_index in range(10))
+
+
+def legal(gates, ends):
+    try:
+        histogram(gates, ends)
+    except ValueError:
+        return False
+    return True
+
+
+def execute(gates, state):
+    values = [row[:] for row in state]
+    for gate in gates:
+        target, source = gate[1], gate[2]
+        coefficient = Fraction(gate[3], gate[4])
+        values[target] = [
+            left + coefficient * right
+            for left, right in zip(values[target], values[source])
+        ]
+    return values
+
+
+def identity():
+    return [[Fraction(i == j) for j in range(3)] for i in range(3)]
+
+
+def add(target, source, numerator, frame):
+    return ("add", target, source, numerator, 1, frame)
+
+
+def cleanup(frame):
+    return [add(Y, Z, -1, frame), add(Y, X, -1, frame)]
+
+
+def moment_sign_known(delta):
+    """Exact sign of sum delta_r r^a is not needed when the histogram is zero."""
+    return sum(delta) == 0 and all(entry == 0 for entry in delta)
+
+
+def main():
+    zero, line_a, line_b = span(()), span((1,)), span((2,))
+    plane = span((1, 2))
+    require(rank(line_a) == rank(line_b) == 1 and rank(plane) == 2, "line dimensions")
+    require(not contained(line_a, line_b) and not contained(line_b, line_a), "crossed lines")
+    ends = {X: plane, Y: plane, Z: plane}
+    forward_a = add(Y, X, 1, line_a)
+    forward_b = add(Y, Z, 1, line_a)
+    moved_b = add(Y, Z, 1, line_b)
+    moved_a = add(Y, X, 1, line_b)
+    require(crosses(forward_a, forward_b) and crosses(forward_b, forward_a),
+            "commuting ADDs are outside the reorder test")
+
+    original = [forward_a, forward_b, *cleanup(plane)]
+    moved = [moved_b, moved_a, *cleanup(plane)]
+    only_a = [forward_b, moved_a, *cleanup(plane)]
+    only_b = [moved_b, forward_a, *cleanup(plane)]
+    original_bill = histogram(original, ends)
+    moved_bill = histogram(moved, ends)
+    require(original_bill == moved_bill == (0, 6, 0, 0, 0, 0, 0, 0, 0, 0),
+            "crossed witness histogram")
+    delta = tuple(new - old for old, new in zip(original_bill, moved_bill))
+    require(moment_sign_known(delta), "nonzero invoice")
+    require(sum(rank_index * count for rank_index, count in enumerate(delta)) == 0, "mass")
+    require(not legal(only_a, ends) and not legal(only_b, ends), "an intermediate is legal")
+    start = identity()
+    restored = execute(original, start)
+    require(restored == execute(moved, start) == start, "cleanup does not restore")
+    require(execute(original[:2], start) == execute(moved[:2], start), "forward maps differ")
+
+    same_line = [add(Y, Z, 1, line_a), add(Y, X, 1, line_a), *cleanup(plane)]
+    require(legal(same_line, ends), "parallel swap must stay legal")
+    widened = add(Y, X, 1, plane)
+    widened_b = add(Y, Z, 1, plane)
+    favorable = [widened_b, widened, *cleanup(plane)]
+    favorable_only_a = [forward_b, widened, *cleanup(plane)]
+    favorable_only_b = [widened_b, forward_a, *cleanup(plane)]
+    favorable_bill = histogram(favorable, ends)
+    require(favorable_bill == (0, 0, 3, 0, 0, 0, 0, 0, 0, 0), "favorable histogram")
+    favorable_delta = tuple(new - old for old, new in zip(original_bill, favorable_bill))
+    require(favorable_delta == (0, -6, 3, 0, 0, 0, 0, 0, 0, 0), "favorable delta")
+    require(legal(favorable_only_a, ends) and not legal(favorable_only_b, ends),
+            "favorable escape is not sequential on one side")
+    # 3*(2^a-2) < 0 for every real a in (0,1), checked on reduced fractions.
+    for denominator in range(2, 9):
+        for numerator in range(1, denominator):
+            require(pow(2, numerator) < pow(2, denominator), "power comparison")
+
+    noncommuting = [add(Y, X, 1, line_a), add(Z, Y, 1, line_a)]
+    swapped_noncommuting = [add(Z, Y, 1, line_a), add(Y, X, 1, line_a)]
+    require(execute(noncommuting, start) != execute(swapped_noncommuting, start),
+            "noncommuting swap was treated as an identity")
+    scaled = [add(Y, X, 2, line_a), forward_b]
+    require(execute(scaled, start) != execute(original[:2], start), "coefficient control")
+    require(not crosses(add(Y, X, 1, line_a), add(Z, Y, 1, line_a)),
+            "dependent ADD passed the reorder test")
+
+    print(
+        "PASS_MOVED_ADD_CROSSED_INVOICE"
+        " registers=3 adds=2 cleanup=2"
+        " histogram_H1=6 delta=0 rank_mass_delta=0"
+        " both_intermediates=illegal scalar=commuting_identity"
+        " favorable_sequential=-6H1+3H2 one_intermediate=legal"
+        " no_new_kappa"
+    )
+
+
+if __name__ == "__main__":
+    main()