Prove price-null fibres need irreducible cycle exchanges (no κ)

research/price-null-cycle-exchanges/PROOF.md

@@ -0,0 +1,84 @@
+# Proof: price-null exchanges need irreducible cycles
+
+## Model
+
+This is the register-tax model of PR6345 (`research/p104-frontier-symmetric-ladders`,
+DreamingOfClouds). A register's timeline is a chain `c = (c_0, …, c_m)` of integer
+dimensions. Its tax is the multiset `{|c_{i+1} − c_i|}` of step sizes, minus one copy of the
+span `c_m − c_0` when the register is a helper. The price of a word depends on the word only
+through the summed tax over all registers. A change replaces some chains by others. Write
+`Δ_r = tax(new_r) − tax(old_r)` as a signed multiset. The change is **price-null** when
+`Σ_r Δ_r = 0`.
+
+PR6345 names three freedoms:
+
+- **F1.** A helper with one step may re-span; PR6345 shows its tax stays zero.
+- **F2.** One register keeps its endpoints and its step multiset and reorders its stops (`Δ_r = 0`).
+- **F3.** A stop move in one register cancels a stop move in another (`Δ_A + Δ_B = 0`).
+
+A *one-stop window chain* is `(a, s, b)` with `a < s < b`. Its steps are `{s − a, b − s}` and
+their sum is the window length `L = b − a`. Endpoints stay fixed in every change below, so a
+helper's span term cancels inside its own `Δ`. The statements below hold for helpers as well as
+main registers.
+
+## Theorem 1: no pairwise exchange across window lengths
+
+Let `A` and `B` be one-stop window chains with lengths `L_A ≠ L_B`, and let each change only its
+stop. If `Δ_A + Δ_B = 0`, then `Δ_A = Δ_B = 0`.
+
+*Proof.* Write `P = {s, L_A − s}` and `P' = {s', L_A − s'}` for `A`'s old and new step pairs, and
+`Q`, `Q'` for `B`'s. If `s'` lies in `P`, then `s' = s` or `s' = L_A − s`, so `P' = P` and
+`Δ_A = 0`. Then `Δ_B = 0` too. Otherwise `P'` and `P` are disjoint, so `Δ_A = P' − P` has the
+two-element positive part `P'`. The hypothesis says `P' − P = Q − Q'`, whose positive part is
+contained in `Q`, which has two elements. Therefore `P' = Q` as multisets, and summing gives
+`L_A = L_B`. This contradicts `L_A ≠ L_B`. ∎
+
+**Corollary (F1–F3 do not connect the fibre).** Take a configuration consisting only of
+one-stop window main chains with pairwise distinct window lengths. Every configuration reachable
+by any finite sequence of F1, F2 and F3 moves gives every register its original step multiset.
+F1 does not apply to main chains, F2 keeps the multiset by definition, and by Theorem 1 every F3
+move between two such registers has `Δ_A = Δ_B = 0`.
+
+## Theorem 2: irreducible cycles of every length
+
+Let `k ≥ 3`. Take positive integers `u_1, …, u_k` and `c > 0` such that the `2k` numbers
+`u_j` and `u_j + c` are pairwise distinct. Indices are mod `k`. Register `i` has window
+`[0, L_i]`, `L_i = u_i + u_{i+1} + c`, and moves its stop from `u_i` to `u_i + c`. Its steps
+change from `{u_i, u_{i+1} + c}` to `{u_i + c, u_{i+1}}`. Then:
+
+1. both stops are interior, since `u_i > 0` and `u_{i+1} > 0`;
+2. the whole change is price-null;
+3. no nonempty proper subset `S` of the registers has `Σ_{i∈S} Δ_i = 0`.
+
+*Proof.* `Δ_i = [u_i + c] + [u_{i+1}] − [u_i] − [u_{i+1} + c]`. All `2k` values are distinct,
+so in `Σ_{i∈S} Δ_i` the coefficient of `[u_j]` is `[j − 1 ∈ S] − [j ∈ S]`, and that of `[u_j + c]`
+is `[j ∈ S] − [j − 1 ∈ S]`. All coefficients vanish exactly when `j ∈ S ⇔ j − 1 ∈ S` for every
+`j`, that is when `S` is empty or everything. Taking `S` = everything gives (2). ∎
+
+With `u_j = 2^{j−1}` and `c = 2^k`, the values `u_j < 2^k < u_j + c` are distinct. The windows
+`2^{i−1} + 2^i + 2^k` (and `2^{k−1} + 1 + 2^k` for the wrapping register) are pairwise
+distinct because their binary forms differ. The corollary then applies: for every `k ≥ 3` this
+price-null change is not reachable from its start by F1–F3, even through intermediate states.
+
+## Smallest three-register example
+
+The checker searches every change of three one-stop window chains with distinct lengths
+`L_1 < L_2 < L_3`. For each `L_3` from 4 up, it checks every unordered old and new stop with
+every register changed. None exists with `L_3 ≤ 5`. At `L_3 = 6` the first is
+
+| window | old steps | new steps |
+|---|---|---|
+| 4 | {1, 3} | {2, 2} |
+| 5 | {2, 3} | {1, 4} |
+| 6 | {2, 4} | {3, 3} |
+
+Old and new totals are both `{1, 2, 2, 3, 3, 4}`. By Theorem 1 no two of these changes cancel.
+Every dimension in the example is at most 6, inside the rank range 1..9 that PR6345 reports
+for its helpers.
+
+## Scope
+
+This is a statement about the tax model and the three freedoms as PR6345 states them. It does
+not say whether the PR6167 frame table, event order and legality checker admit such a cycle in
+the actual word, or whether the 59 words PR6345 found contain one. A legal word must also keep
+the frame table, inventories and replay fields fixed; the tax model ignores those constraints.

research/price-null-cycle-exchanges/README.md

@@ -0,0 +1,72 @@
+# Price-null fibres need irreducible cycle exchanges (no κ)
+
+This answers Open next question 1 of DreamingOfClouds'
+[PR6345](https://github.com/CrocSwap/integer-mult-bounds/pull/6345)
+(`research/p104-frontier-symmetric-ladders`) at the level of that package's own
+register-tax model. The question: is the set of optimal frame assignments exactly the union
+of its three freedoms? Those are one-step helper re-spans (F1), stop reorders with fixed
+endpoints (F2), and a stop move in one register cancelled by a stop move in another (F3).
+
+**Answer in the tax model: no.** Claim type: scoped written proof with exact finite
+corroboration. No κ change.
+
+- **Theorem 1.** Two one-stop window chains `(a, s, b)` with different window lengths never
+  cancel each other's tax change unless neither changes. So F3 can only pair registers with
+  equal windows.
+- **Corollary.** In a configuration of one-stop main chains with pairwise distinct windows,
+  every configuration reachable by any sequence of F1–F3 keeps each register's step multiset.
+- **Theorem 2.** For every `k ≥ 3` there are `k`-register price-null changes in which no
+  nonempty proper subset is price-null. Register `i` has window `u_i + u_{i+1} + c` and moves its
+  stop from `u_i` to `u_i + c`. Irreducibility holds when the `2k` values `u_j` and `u_j + c` are
+  distinct. With `u_j = 2^(j−1)` and `c = 2^k` the windows are also distinct, so the corollary
+  shows F1–F3 cannot reach these changes, even through intermediate states.
+- **Smallest case.** An exhaustive search finds no three-register cycle with distinct windows
+  below largest window 6. At 6: window 4 `{1,3}→{2,2}`, window 5 `{2,3}→{1,4}`, window 6
+  `{2,4}→{3,3}`. All dimensions are at most 6, inside the rank range 1..9 that PR6345 reports.
+
+A complete classifier or local search for the fibre therefore needs multi-register cyclic
+exchanges, not only pairs. [PROOF.md](PROOF.md) has the proofs and exact scope.
+
+## Scope and limits
+
+This is a statement about the tax model and the freedoms as PR6345 defines them. It does not
+show that the PR6167 word admits a legal cycle. Frames must exist at the right dimensions and
+events, and the frame table, inventories and replay fields must stay fixed. The tax model
+ignores those constraints. PR6167 and PR6345 are cited, not replayed or audited. No supplier,
+caller, native, compiler, Lean or Docker obligation is discharged.
+
+## Reproduce
+
+From the repository root, standard library only:
+
+```sh
+python3.12 -I -W error -B research/price-null-cycle-exchanges/verify.py
+python3.12 -I -W error -O -B research/price-null-cycle-exchanges/verify.py
+python3.12 -B scripts/research_package.py --package research/price-null-cycle-exchanges
+```
+
+Each verifier run prints `PASS_PRICE_NULL_CYCLE_EXCHANGES` in under a second. It checks:
+
+- Theorem 1 over all 216,062 combinations of two one-stop chain changes (old and new stop each, unchanged included) with distinct windows up to 12;
+- Theorem 2 nullity, irreducibility, interior stops and distinct windows for `k = 3..8`;
+- the exhaustive smallest three-register cycle and its pinned witness;
+- three rejecting controls. Dropping one register breaks nullity. Equal windows do admit a
+  pairwise exchange. A non-generic cycle (`u = (1,2,1,2)`, `c = 3`) splits into null pairs.
+
+## Open next questions
+
+1. **Does the PR6167 frame table admit a legal three-register cycle on its actual events?**
+   First step: list the actual word's one-stop chains by window, find triples whose step pairs
+   admit a cycle, and test each candidate reassignment with the pinned PR6167 replay. Blocker:
+   frame dimensions, event positions and fixed inventories.
+2. **Is every price-null change a composition of irreducible cycles on multi-stop chains?**
+   Multi-stop chains change several steps at once, so Theorem 1's argument does not carry over
+   directly.
+3. **Can an irreducible cycle enable a stop drop that no single freedom reaches?** Price-null
+   moves matter only if they unlock a strict improvement later.
+
+## Credit
+
+The register-tax model, the three freedoms and the question are DreamingOfClouds' (PR6345),
+over Ali Romman's PR6167 word and its predecessors. The new theorems, checker and examples
+were produced by Nick Petalas. Apache-2.0.

research/price-null-cycle-exchanges/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-frontier-symmetric-ladders/README.md",
+      "usage": "provenance",
+      "git_blob": "5c8f2af74ba2f44485fb446027c02ef00ccbe666",
+      "sha256": "7606e0c63a4a958fc0da9aba0a6fcadb947ef4575b846774b824f12e0d16b45a"
+    }
+  ]
+}

research/price-null-cycle-exchanges/TASK.json

@@ -0,0 +1,129 @@
+{
+  "schema_version": 1,
+  "task_id": "p104-side-correction",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "p104-side-correction",
+    "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "research/p104-helper-subspace-splits/README.md",
+      "research/dyadic-helper-channel-capacity/README.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "P104",
+      "helper basis",
+      "helper split",
+      "5718",
+      "dyadic capacity"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4133: literal-slot defect",
+        "evidence": "research/p104-literal-slot-defect/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4136: uniform commutation gap",
+        "evidence": "research/p104-uniform-commutation-gap/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4140: uniform encoding gap",
+        "evidence": "research/p104-uniform-encoding-gap/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance",
+        "evidence": "research/p104-source-chart-shortcut/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4154: fiber-tag seam mismatch",
+        "evidence": "research/p104-fiber-tag-seam/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Open next question 1 of PR6345 in its register-tax model: is every price-null change a union of the three named freedoms (one-step helper re-span, stop reorder with fixed endpoints, two-register stop-move cancellation)? Answer: no. Two one-stop window chains with different window lengths never cancel nontrivially, and for every k>=3 there are irreducible k-register price-null cycles with distinct windows that F1-F3 cannot reach; the smallest three-register cycle has largest window 6.",
+  "scope_change_reason": "The card asks for an improved complete P104 invoice. This package instead answers a structural question about the price-null fibre left open by PR6345, at the level of that package's own tax model. It does not test legality in the actual PR6167 word.",
+  "bottleneck_link": "Side result for P104 word search: a classifier or local search that explores only the three PR6345 freedoms misses whole price-null families, so moves that look price-neutral (and may enable later stop drops) need multi-register cyclic exchanges.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the model-level theorem, the all-k irreducible family and the exhaustive smallest three-register example; leave legality in the actual word open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md (Theorems 1 and 2, corollary); verify.py checks Theorem 1 exhaustively for windows <= 12, Theorem 2 for k = 3..8, the minimal three-register example and rejecting controls, in normal and optimized Python.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does the PR6167 frame table admit a legal three-register cyclic exchange on its actual events?",
+      "why_it_matters": "Only a legal cycle would show the actual optimal-assignment set exceeds the three freedoms, rather than the tax model.",
+      "first_step": "List the actual word's main and helper chains by window, find triples of one-stop chains whose step pairs admit a Theorem-2-style cycle, and test each candidate frame reassignment with the pinned PR6167 replay.",
+      "blocked_by": "Each stop must be a frame of the right dimension at the right event, and inventories and replay fields must stay fixed."
+    },
+    {
+      "question": "Is every price-null change a composition of irreducible cycles on multi-stop chains, and which cycle lengths occur?",
+      "why_it_matters": "That would give a complete generating set for the fibre in the tax model.",
+      "first_step": "Treat each register's achievable step multisets as nodes and price-null changes as cycles in the signed multiset lattice; enumerate small windows exhaustively.",
+      "blocked_by": "Multi-stop chains can change several steps at once, so the one-stop argument of Theorem 1 no longer applies directly."
+    },
+    {
+      "question": "Can an irreducible cycle enable a stop drop that no single freedom reaches?",
+      "why_it_matters": "Price-null moves matter only if they unlock a strict price improvement later.",
+      "first_step": "On the smallest example, add a fourth register whose stop becomes droppable only after the cycle and compute the resulting tax.",
+      "blocked_by": "Requires the legality model of the actual word."
+    }
+  ]
+}