diff --git a/research/price-null-cycle-exchanges/PROOF.md b/research/price-null-cycle-exchanges/PROOF.md
new file mode 100644
index 0000000000..cbfb29818e
--- /dev/null
+++ b/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.
diff --git a/research/price-null-cycle-exchanges/README.md b/research/price-null-cycle-exchanges/README.md
new file mode 100644
index 0000000000..5331576fb6
--- /dev/null
+++ b/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.
diff --git a/research/price-null-cycle-exchanges/SOURCES.json b/research/price-null-cycle-exchanges/SOURCES.json
new file mode 100644
index 0000000000..6dd1053e18
--- /dev/null
+++ b/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"
+    }
+  ]
+}
diff --git a/research/price-null-cycle-exchanges/TASK.json b/research/price-null-cycle-exchanges/TASK.json
new file mode 100644
index 0000000000..2765165e16
--- /dev/null
+++ b/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."
+    }
+  ]
+}
diff --git a/research/price-null-cycle-exchanges/VERIFY.json b/research/price-null-cycle-exchanges/VERIFY.json
new file mode 100644
index 0000000000..eef05bbdc1
--- /dev/null
+++ b/research/price-null-cycle-exchanges/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Theorem 1 exhaustively for one-stop chains with distinct windows <= 12; Theorem 2 irreducibility and distinct windows for k = 3..8; exhaustive smallest three-register cycle (largest window 6, pinned witness); rejecting controls (dropped register, equal-window exchange, non-generic split)."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Theorem 1 exhaustively for one-stop chains with distinct windows <= 12; Theorem 2 irreducibility and distinct windows for k = 3..8; exhaustive smallest three-register cycle (largest window 6, pinned witness); rejecting controls (dropped register, equal-window exchange, non-generic split)."
+    }
+  ]
+}
diff --git a/research/price-null-cycle-exchanges/verify.py b/research/price-null-cycle-exchanges/verify.py
new file mode 100644
index 0000000000..005c7e6e05
--- /dev/null
+++ b/research/price-null-cycle-exchanges/verify.py
@@ -0,0 +1,155 @@
+"""Exact checks for irreducible price-null cycle exchanges in the PR6345 register-tax model.
+
+Produced by Nick Petalas. Apache-2.0. Standard library only.
+
+Model (PR6345, research/p104-frontier-symmetric-ladders): a register's timeline is a chain of
+integer dimensions; its tax is the multiset of step sizes, minus one copy of its span if it is a
+helper. A change of several registers is price-null when the summed tax change is zero.
+"""
+from collections import Counter
+from itertools import combinations
+import sys
+
+STATUS = 'PASS_PRICE_NULL_CYCLE_EXCHANGES'
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def tax(chain, helper=False):
+    t = Counter(abs(y - x) for x, y in zip(chain, chain[1:]))
+    if helper:
+        t[chain[-1] - chain[0]] -= 1
+    return t
+
+
+def delta(old, new, helper=False):
+    d = Counter(tax(new, helper))
+    d.subtract(tax(old, helper))
+    return {k: v for k, v in d.items() if v}
+
+
+def total(deltas):
+    s = Counter()
+    for d in deltas:
+        s.update(d)
+    return {k: v for k, v in s.items() if v}
+
+
+def irreducible(deltas):
+    """True when the whole family is null and no nonempty proper subfamily is."""
+    k = len(deltas)
+    if total(deltas):
+        return False
+    return all(total([deltas[i] for i in S]) for r in range(1, k) for S in combinations(range(k), r))
+
+
+def cycle(u, c):
+    """Theorem 2 family: register i has window [0, u_i+u_{i+1}+c]; its stop moves from u_i to u_i+c."""
+    k = len(u)
+    regs = []
+    for i in range(k):
+        L = u[i] + u[(i + 1) % k] + c
+        regs.append(((0, u[i], L), (0, u[i] + c, L)))
+    return regs
+
+
+def check_theorem1(N):
+    """Two one-stop monotone chains with different windows never cancel unless both are unchanged."""
+    count = 0
+    for LA in range(2, N + 1):
+        for LB in range(2, N + 1):
+            if LA == LB:
+                continue
+            for s in range(1, LA):
+                for s2 in range(1, LA):
+                    dA = delta((0, s, LA), (0, s2, LA))
+                    for t in range(1, LB):
+                        for t2 in range(1, LB):
+                            dB = delta((0, t, LB), (0, t2, LB))
+                            if not total([dA, dB]):
+                                need(not dA and not dB, 'Theorem 1 counterexample %r' % ((LA, s, s2, LB, t, t2),))
+                            count += 1
+    # helpers with fixed endpoints: the span term cancels inside each delta
+    for s in range(1, 7):
+        for s2 in range(1, 7):
+            need(delta((0, s, 7), (0, s2, 7), True) == delta((0, s, 7), (0, s2, 7)), 'Helper span cancels')
+    return count
+
+
+def check_theorem2(kmax):
+    for k in range(3, kmax + 1):
+        u = [2 ** j for j in range(k)]
+        c = 2 ** k
+        regs = cycle(u, c)
+        windows = [r[0][2] for r in regs]
+        need(len(set(windows)) == k, 'Distinct windows k=%d' % k)
+        need(all(0 < new[1] < new[2] for _, new in regs), 'Interior stops k=%d' % k)
+        deltas = [delta(o, n) for o, n in regs]
+        need(all(deltas), 'Every register changes k=%d' % k)
+        need(irreducible(deltas), 'Irreducible k=%d' % k)
+    return kmax - 2
+
+
+def minimal_three_cycle(N):
+    """Exhaustive: least max window of an irreducible price-null change of three one-stop chains
+    with pairwise distinct windows, every register changed. Stops are unordered (s ~ L-s)."""
+    moves = {}
+    for L in range(2, N + 1):
+        out = []
+        for s in range(1, L // 2 + 1):
+            for s2 in range(1, L // 2 + 1):
+                if s != s2:
+                    out.append(((0, s, L), (0, s2, L), delta((0, s, L), (0, s2, L))))
+        moves[L] = out
+    best = None
+    for L3 in range(4, N + 1):
+        for L2 in range(3, L3):
+            for L1 in range(2, L2):
+                for a in moves[L1]:
+                    for b in moves[L2]:
+                        ab = total([a[2], b[2]])
+                        for c in moves[L3]:
+                            if not total([ab, c[2]]):
+                                need(irreducible([a[2], b[2], c[2]]), 'A three-register null change is irreducible')
+                                if best is None:
+                                    best = (L3, [(a[0], a[1]), (b[0], b[1]), (c[0], c[1])])
+        if best:
+            return best
+    return best
+
+
+def controls():
+    # a cycle with one register's shift removed is no longer null
+    regs = cycle([1, 2, 4], 8)
+    deltas = [delta(o, n) for o, n in regs]
+    need(total(deltas[:2]), 'Control: dropping a register breaks nullity')
+    # equal windows do admit a pairwise exchange (freedom 3 is real there)
+    dA, dB = delta((0, 1, 6), (0, 2, 6)), delta((0, 2, 6), (0, 1, 6))
+    need(dA and not total([dA, dB]), 'Control: equal windows exchange')
+    # a non-generic shift (c collides with a value) can split into smaller null families
+    regs = cycle([1, 2, 1, 2], 3)
+    deltas = [delta(o, n) for o, n in regs]
+    need(not total(deltas), 'Control: degenerate cycle is still null')
+    need(not irreducible(deltas), 'Control: genericity is needed for irreducibility')
+
+
+def main():
+    n1 = check_theorem1(12)
+    print('PASS Theorem 1: %d one-stop pairs with distinct windows <= 12 checked; no nontrivial cancellation' % n1)
+    n2 = check_theorem2(8)
+    print('PASS Theorem 2: irreducible cycles with distinct windows for k = 3..8 (%d sizes)' % n2)
+    L, witness = minimal_three_cycle(12)
+    need(L == 6, 'Minimal largest window is 6, got %d' % L)
+    need(witness == [((0, 1, 4), (0, 2, 4)), ((0, 2, 5), (0, 1, 5)), ((0, 2, 6), (0, 3, 6))], 'Pinned witness')
+    print('PASS minimal three-register cycle: largest window %d, first witness %r' % (L, witness))
+    controls()
+    print('PASS controls')
+    print(STATUS)
+
+
+if __name__ == '__main__':
+    sys.dont_write_bytecode = True
+    main()