diff --git a/research/moved-add-crossed-invoice/README.md b/research/moved-add-crossed-invoice/README.md new file mode 100644 index 0000000000..d7a98783ba --- /dev/null +++ b/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. diff --git a/research/moved-add-crossed-invoice/SOURCES.json b/research/moved-add-crossed-invoice/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/moved-add-crossed-invoice/TASK.json b/research/moved-add-crossed-invoice/TASK.json new file mode 100644 index 0000000000..eb35c3b3de --- /dev/null +++ b/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." + } + ] +} diff --git a/research/moved-add-crossed-invoice/VERIFY.json b/research/moved-add-crossed-invoice/VERIFY.json new file mode 100644 index 0000000000..5aa85ce333 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/moved-add-crossed-invoice/verify.py b/research/moved-add-crossed-invoice/verify.py new file mode 100644 index 0000000000..20ae98e2f3 --- /dev/null +++ b/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()