diff --git a/research/p104-network-coded-carriers/PROOF.md b/research/p104-network-coded-carriers/PROOF.md
new file mode 100644
index 0000000000..dddca6c30a
--- /dev/null
+++ b/research/p104-network-coded-carriers/PROOF.md
@@ -0,0 +1,80 @@
+# Proofs: network-coded owned carriers on P104
+
+Tags: **PROVED-LEAN** = `lean/NetCode/Walk.lean` (Lean 4 + Mathlib, no `sorry`, axioms `propext`,
+`Classical.choice`, `Quot.sound`); **CHECKED-EXACT** = `verify.py` on the PR6030 word (exact rationals and F2).
+
+## 0. Model
+
+Frames are subspaces of F2^9. A public role only ascends (strict inclusion), an owned role only descends and pays
+the dimension drop, and arithmetic happens in a common frame. This is the verifier contract replayed by `verify.py`.
+Content is not tied to the frame. A public role may hold coordinates whose ports lie outside its frame, as long as
+they arrived through owned descents.
+
+Pass to duals. A frame C corresponds to C^perp. An ascent shrinks the dual for free. An owned descent C -> C'
+grows it and costs `dim C - dim C' = dim C'^perp - dim C^perp` (`descent_cost_dual`, PROVED-LEAN).
+In PR6030, X_j starts on the line <p_j> and Y_j ends in p_j^perp with p_j . p_j = 1 (CHECKED-EXACT). So a receiver
+Y_j can use only frames C with p_j in C^perp, and X_j and Y_j never share a frame.
+
+An **information walk** is a sequence of dual subspaces Z_0, Z_1, ... Each node k >= 1 comes from an earlier
+node par(k), either by shrinking (free) or by growing (paid). This covers stops, copies, branches and relays
+through public helpers: a helper reads at one frame and ascends, and that is a shrink.
+
+## 1. Walk bound and Lemma S (PROVED-LEAN `union_bound`, `lemma_S`)
+
+The union span of the visited nodes has dimension at most `dim Z_0` plus the total paid amount.
+*Proof.* A free step adds a subspace of its parent, which is already inside the union. A paid step adds Z_k ⊇ Z_par.
+By the modular law, `dim(U ⊔ Z_k) = dim U + dim Z_k - dim(U ⊓ Z_k) <= dim U + dim Z_k - dim Z_par`.
+
+**Lemma S.** Suppose a carrier holding t.x is collected in G = span of its source ports, so Z_0 = G^perp. Suppose
+it must reach every receiver j in R. Then it pays at least `dim(G^perp + span p_R) - dim G^perp`, whatever its stops,
+branches and relays. This number is the binary rank of the pairing [p_j . p_i] (j in R, i in S), the repository's
+COPY cost. One chain attains it. So stops do not make a single carrier cheaper.
+On PR6030 both sides equal 7 for each of the 8 carriers (CHECKED-EXACT).
+
+## 2. Lemma A: additions and shedding along one path (PROVED-LEAN `lemma_A`, `lemma_A_rows`)
+
+Let a port p_i lie in C. Let a receiver read at a frame C' ⊇ C, so that p_j ∈ C'^perp. Then p_j . p_i = 0.
+Hence content added at C from ports of C changes no costly pair (p_j . p_i = 1) of any receiver served higher on the
+same path. It can be loaded at the top instead, so a path with additions or shedding is one term with stops
+(Lemma S).
+
+## 3. Lemma M: merges
+
+Carriers c in U merge in a frame with dual W, with combination lambda. Path c has union span Z_c ⊇ W and starts on
+the line <g_c>, so it pays at least `dim Z_c - 1` (walk bound). The common tail has union span T ⊇ W and pays at
+least `dim T - dim W`. Every receiver of c reads c-content on path c or on the tail, so its port lies in Z_c ∪ T.
+
+*Finite facts (CHECKED-EXACT).*
+(i) <g_c> + span p_{R_c} = l_c^perp, of dimension 8.
+(ii) g_a . l_c = 1 for a ≠ c.
+Hence <g_a, g_c> + span p_{R_c} = F2^9 for a ≠ c, and Z_c ⊔ T = F2^9 (`sup_top_of_cover`).
+
+**General count (PROVED-LEAN `merge_count`).**
+`dim Z_c + dim T >= 9 + dim W` (`path_dim`), so `pay_c + tail >= 8` for each c. Therefore
+`total + (k-1) tail >= 8k`. A merge with tail <= 1 never beats the 7k of separate carriers, for any k.
+
+**Pairs (PROVED-LEAN `pair_merge` + CHECKED-EXACT `nocover`).**
+Suppose two merged carriers pay at most 13. Combining the bounds gives `dim Z_a, dim Z_b <= 6`.
+Let N be the receivers of a or b whose need (d_ja, d_jb) is not proportional to lambda.
+`must_read_path` (PROVED-LEAN) shows that each such receiver must read a pure path, so N ⊆ Z_a ∪ Z_b.
+The exhaustive check is over all 28 pairs, both ratios, and all 11,811 six-dimensional subspaces containing <g_a, g_b>
+(WLOG dim Z_a = 6). It finds no cover with the remainder in a subspace of dimension <= 6. So every pair merge costs
+at least 14 = 7 + 7.
+
+The decoder rows are unique: on the costly pairs of every port, the 8 carrier rows have rank 8 (CHECKED-EXACT).
+So the needs d_j are forced, and d_jc = ±2 exactly when j ∈ R_c.
+
+## 4. Scope
+
+Covered: the unique 8-carrier code of the P104 local word (PR6030 contents, unique up to sign by PR6166).
+Covered mechanisms: stops, copies, branches, public relays, additions and shedding along a path, any single merge
+with a tail of length <= 1, and every single merge of two carriers.
+
+Not covered:
+- merges of three or more carriers with a tail of length >= 2;
+- multi-stage merge trees;
+- codes with 9 or more carriers, which is the open masked floor C(P104) >= 56 beyond rank 8;
+- decoders that read X directly (P-ATOM), and different words or boundaries.
+
+The cut profile of PR6030 is tight: 8 crossings on each level 2..8 of the seven dimension cuts of
+`p104-owned-coding-boundaries` (CHECKED-EXACT).
diff --git a/research/p104-network-coded-carriers/README.md b/research/p104-network-coded-carriers/README.md
new file mode 100644
index 0000000000..487a2efd97
--- /dev/null
+++ b/research/p104-network-coded-carriers/README.md
@@ -0,0 +1,62 @@
+# Network-coded owned carriers on P104: stops, shedding and pair merges do not go below 56
+
+`research/fragmentation-ceiling/PROOF.md` §6.7 lists "network-coded carriers with stops and shedding" as one door
+outside the A30-CUT scope. This package tests that door on the selected PR6030 local word and its 8-carrier code,
+which PR6166 shows is unique up to sign.
+
+**Scoped negative result. No new word or kappa is claimed.**
+
+## Result
+
+| Mechanism | Result | Evidence |
+|---|---|---|
+| stops, copies, branches, relays through public helpers | a carrier pays at least its COPY cost (the F2 pairing rank) | Lemma S, PROVED-LEAN |
+| additions and shedding along one path | equivalent to loading at the top | Lemma A, PROVED-LEAN |
+| any merge of k carriers with a tail of length <= 1 | costs more than 7k | `merge_count`, PROVED-LEAN + finite facts |
+| any merge of two carriers | costs at least 14 = 7 + 7 | `pair_merge`, PROVED-LEAN + exhaustive check |
+
+The proofs use a dual picture. A frame C is replaced by C^perp. Public ascents shrink the dual for free, and owned
+descents grow it at their price. The union span of every visited dual grows by at most the paid amount. With this
+one inequality, stops, copies, branches and relays reduce to the COPY cost. For merges, each carrier must also
+reach the other carrier's normal g_a. Since g_a . l_c = 1 for a ≠ c, each content tree then spans all of F2^9.
+
+The PR6030 word already uses a coded owned network. It has 31 owned lifetimes, 14 owned-to-owned additions and
+owned reads at frame dimensions 0-8. It is tight against the seven dimension cuts of
+[p104-owned-coding-boundaries](../p104-owned-coding-boundaries/JOINT-BOUNDARY.md), with exactly 8 crossings on
+every level 2..8 (owned paid 56).
+
+## Reproduce
+
+```sh
+python3 -B research/p104-network-coded-carriers/verify.py
+```
+
+The check uses the standard library only and takes about 17 s. Expected marker: `PASS_P104_NETWORK_CODED_CARRIERS`.
+It replays the PR6030 word exactly and checks the Y/X frame facts and the 8 carriers. It extracts the delivery lines
+(removed E8 root lines), the normals g_c and the receivers R_c. It checks the Lemma S equality (dual walk cost =
+pairing rank = 7), the unique masked decoder (d_jc = ±2) and the `merge_count` spanning facts. It runs the
+exhaustive pair `nocover` check (28 pairs × 2 ratios × 11,811 subspaces) and compares the result with
+[RESULT.json](RESULT.json).
+
+Lean (optional, not run by `verify.py`): `cd lean && lake exe cache get && lake build && lake env lean Audit.lean`.
+Every theorem prints only `propext`, `Classical.choice` and `Quot.sound`. The Mathlib pin is the one used by
+`p104-carrier-code-uniqueness`.
+
+## Relation to existing work
+
+- `fragmentation-ceiling` §6.4 (single-commodity lemma) and §6.7 (the door). Lemma S is the P104 form of the
+  single-commodity statement, with arbitrary stops and public relays.
+- `p104-owned-coding-boundaries`: its seven cuts close arbitrary sharing for a fixed public boundary with
+  dimension-1 deliveries. This package removes the boundary premise for stops, shedding and pair merges.
+- Matarener's open PR6267 (owned-lineage factorization) asks whether its floor extends to merges. Pair merges are
+  answered here.
+- `p104-signed-mixed-carrier-bank` builds mixed carriers in a relaxed frame model. Here the actual frame rules are
+  used, and pair mixing does not pay.
+
+## Open next questions
+
+- Merges of 3 or more carriers with tails of length >= 2, and multi-stage merge trees.
+- Codes with 9 or more carriers (masked floor beyond rank 8).
+- Decoders reading X (P-ATOM).
+
+Prepared for Matarener with Claude (Anthropic), via Claude Code. Apache-2.0.
diff --git a/research/p104-network-coded-carriers/RESULT.json b/research/p104-network-coded-carriers/RESULT.json
new file mode 100644
index 0000000000..03840be5de
--- /dev/null
+++ b/research/p104-network-coded-carriers/RESULT.json
@@ -0,0 +1,124 @@
+{
+ "carriers": {
+  "g_dot_l_is_offdiagonal_one": true,
+  "lines": [
+   7,
+   25,
+   52,
+   67,
+   82,
+   137,
+   448,
+   491
+  ],
+  "normals_g": [
+   104,
+   162,
+   266,
+   97,
+   289,
+   127,
+   42,
+   76
+  ],
+  "receivers": [
+   52,
+   52,
+   52,
+   52,
+   52,
+   52,
+   52,
+   52
+  ],
+  "support_sizes": [
+   52,
+   52,
+   52,
+   52,
+   52,
+   52,
+   52,
+   52
+  ]
+ },
+ "decoder": {
+  "carriers_per_port": {
+   "2": 12,
+   "3": 24,
+   "4": 32,
+   "5": 24,
+   "6": 12
+  },
+  "support_equals_receivers": true,
+  "unique_rows": 104,
+  "values": [
+   -2,
+   2
+  ]
+ },
+ "frames": {
+  "X_start_is_p_line": 104,
+  "Y_final_is_p_perp": 104,
+  "p_dot_p_is_1": 104
+ },
+ "lemma_S": {
+  "dual_walk_cost": [
+   7,
+   7,
+   7,
+   7,
+   7,
+   7,
+   7,
+   7
+  ],
+  "pairing_rank": [
+   7,
+   7,
+   7,
+   7,
+   7,
+   7,
+   7,
+   7
+  ]
+ },
+ "merge_count_htop": {
+  "pairs": 56
+ },
+ "pair_nocover": {
+  "feasible_covers": 0,
+  "max_N": 75,
+  "min_N": 49,
+  "pairs": 28,
+  "ratios": 2,
+  "six_dim_subspaces_tested_each": 11811
+ },
+ "word": {
+  "cut_crossings_levels_1_to_9": [
+   0,
+   8,
+   8,
+   8,
+   8,
+   8,
+   8,
+   8,
+   0
+  ],
+  "owned_lifetimes": 31,
+  "owned_paid": 56,
+  "owned_reads_by_frame_dim": {
+   "0": 4,
+   "1": 25,
+   "2": 1,
+   "3": 10,
+   "4": 14,
+   "5": 17,
+   "7": 6,
+   "8": 8
+  },
+  "owned_to_owned_adds": 14
+ }
+}
diff --git a/research/p104-network-coded-carriers/SOURCES.json b/research/p104-network-coded-carriers/SOURCES.json
new file mode 100644
index 0000000000..8da2ceccb8
--- /dev/null
+++ b/research/p104-network-coded-carriers/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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-helper470-twin-rung-removal/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760",
+      "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f"
+    },
+    {
+      "path": "research/fragmentation-ceiling/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c4033090d7cd35d9c80744922c587ae115b1de8a",
+      "sha256": "28be45a551ed8491be1ebb8c64acba2834aaa402452cb02e3c71c83e49232264"
+    },
+    {
+      "path": "research/p104-owned-coding-boundaries/JOINT-BOUNDARY.md",
+      "usage": "provenance",
+      "git_blob": "7132967f594ee2e29ba0834c14bc5873488688de",
+      "sha256": "7a387cacb749f8cf9693d22d5a7f1495c8b73721b6244e9f08c811e16d6b8ac2"
+    },
+    {
+      "path": "research/p104-carrier-code-uniqueness/README.md",
+      "usage": "provenance",
+      "git_blob": "5a5e8af9252947f17bfc9278a60b26f14261a10e",
+      "sha256": "3312b892e0e35678a61521af34b9261b549b071dd93a2a485f4abbaaeb5f4ab8"
+    },
+    {
+      "path": "docs/research/complex-decoder-scope-map.md",
+      "usage": "provenance",
+      "git_blob": "727a8e0bd89da47e4842b02648c93466f42ff27f",
+      "sha256": "f22492089b77631cab712183beea11a8ed1ff0493d895a07f0022600d7af656c"
+    }
+  ]
+}
\ No newline at end of file
diff --git a/research/p104-network-coded-carriers/TASK.json b/research/p104-network-coded-carriers/TASK.json
new file mode 100644
index 0000000000..deded3c3e1
--- /dev/null
+++ b/research/p104-network-coded-carriers/TASK.json
@@ -0,0 +1,81 @@
+{
+ "schema_version": 1,
+ "task_id": "complex-rank-shape-decoder",
+ "priority_revision": 8,
+ "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+ "original_card": {
+  "id": "complex-rank-shape-decoder",
+  "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+  "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",
+   "docs/research/recursive-invoice-preflight.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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+  "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+  "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": [
+   "coframe",
+   "signed moment",
+   "5693",
+   "5698"
+  ],
+  "existing_checks": [
+   {
+    "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": "refined",
+ "actual_scope": "Network-coded owned carriers on the PR6030 P104 word (fragmentation-ceiling \u00a76.7 door): dual-span walk bound; stops, copies, branches and public relays cost at least the COPY pairing rank (Lemma S); additions/shedding along a path are equivalent to loading at the top (Lemma A); merges of k carriers with tail <= 1 and all pair merges cost more than separate carriers (Lemma M), for the unique 8-carrier code.",
+ "scope_change_reason": "The card asks whether a legal decoder change can improve the moment. fragmentation-ceiling \u00a76.7 names network-coded carriers with stops and shedding as an open door beyond A30-CUT; p104-owned-coding-boundaries closes arbitrary sharing only for a fixed boundary with dimension-1 deliveries. This package removes that premise for stops, shedding and pair merges.",
+ "bottleneck_link": "Side result for the decoder route: owned paid 56 (about 380 R0-equivalent per unit in PR6170's fitted law) cannot be lowered by network coding of the 8-carrier code in the covered classes. It does not change kappa.",
+ "budget_minutes": 240,
+ "stop_rule": "Stop when the replay, the carrier facts, the unique decoder, the spanning facts and the exhaustive pair cover check pass (or one fails), and the Lean lemmas build with standard axioms only.",
+ "outcome": "completed",
+ "evidence": "research/p104-network-coded-carriers/RESULT.json",
+ "author": "Matarener",
+ "ai_assistance": "Prepared with Claude (Anthropic) via Claude Code.",
+ "open_questions": [
+  {
+   "question": "Do merges of three or more carriers with tails of length >= 2, or multi-stage merge trees, lower owned paid below 56?",
+   "why_it_matters": "Together with Lemmas S, A and the pair result it would close network coding for the 8-carrier code.",
+   "first_step": "Extend the per-receiver correction constraint of must_read_path to k carriers and run the cover check with the k-carrier dimension bounds.",
+   "blocked_by": "For k >= 3 the dimension bounds from merge_count alone do not force small path unions."
+  },
+  {
+   "question": "Do Lemmas S/A reduce codes with 9 or more carriers to the masked decoder floor?",
+   "why_it_matters": "Then the masked floor C(P104) >= 56 beyond rank 8 would cover network-coded owned layers.",
+   "first_step": "Apply Lemma S to each carrier of a 9-term decoder and compare with the term COPY costs.",
+   "blocked_by": "The masked floor beyond rank 8 is itself open."
+  }
+ ]
+}
\ No newline at end of file
diff --git a/research/p104-network-coded-carriers/VERIFY.json b/research/p104-network-coded-carriers/VERIFY.json
new file mode 100644
index 0000000000..75df8af280
--- /dev/null
+++ b/research/p104-network-coded-carriers/VERIFY.json
@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-helper470-twin-rung-removal/WORD.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Authenticated input; exact replay of the PR6030 word with frame rules and endpoint rows; cut profile (8 crossings on levels 2..8, owned paid 56); Y_j final = p_j^perp, X_j start = <p_j>; 8 carriers at removed E8 root lines, normals g_c, receivers R_c, g_a.l_c = [a != c]; Lemma S equality (dual walk cost = F2 pairing rank = 7); unique masked decoder d_jc = +-2 on R_c; merge_count spanning facts; exhaustive pair nocover over 28 pairs x 2 ratios x 11,811 subspaces; result equals RESULT.json."
+    }
+  ]
+}
\ No newline at end of file
diff --git a/research/p104-network-coded-carriers/lean/.gitignore b/research/p104-network-coded-carriers/lean/.gitignore
new file mode 100644
index 0000000000..01f8cdb637
--- /dev/null
+++ b/research/p104-network-coded-carriers/lean/.gitignore
@@ -0,0 +1 @@
+.lake/
diff --git a/research/p104-network-coded-carriers/lean/Audit.lean b/research/p104-network-coded-carriers/lean/Audit.lean
new file mode 100644
index 0000000000..d90d954f9b
--- /dev/null
+++ b/research/p104-network-coded-carriers/lean/Audit.lean
@@ -0,0 +1,13 @@
+import NetCode
+
+#print axioms NetCode.finrank_add_orth
+#print axioms NetCode.descent_cost_dual
+#print axioms NetCode.union_bound
+#print axioms NetCode.lemma_S
+#print axioms NetCode.lemma_A
+#print axioms NetCode.lemma_A_rows
+#print axioms NetCode.sup_top_of_cover
+#print axioms NetCode.path_dim
+#print axioms NetCode.merge_count
+#print axioms NetCode.must_read_path
+#print axioms NetCode.pair_merge
diff --git a/research/p104-network-coded-carriers/lean/NetCode.lean b/research/p104-network-coded-carriers/lean/NetCode.lean
new file mode 100644
index 0000000000..eeb9949983
--- /dev/null
+++ b/research/p104-network-coded-carriers/lean/NetCode.lean
@@ -0,0 +1 @@
+import NetCode.Walk
diff --git a/research/p104-network-coded-carriers/lean/NetCode/Walk.lean b/research/p104-network-coded-carriers/lean/NetCode/Walk.lean
new file mode 100644
index 0000000000..3616ecd1ae
--- /dev/null
+++ b/research/p104-network-coded-carriers/lean/NetCode/Walk.lean
@@ -0,0 +1,220 @@
+import Mathlib
+
+/-!
+# Network-coded carriers on P104: the dual-span walk bound (Lemmas S, A, M of PROOF.md)
+
+Frames are subspaces `C` of `F₂⁹`.  We work with their orthogonal complements (`C^⊥` for the dot product).
+A public ascent `C ≤ C'` shrinks the dual (free), an owned descent `C' ≤ C` grows it and costs
+`dim C - dim C' = dim C'^⊥ - dim C^⊥` (`descent_cost_dual`).  A receiver whose final frame is `p^⊥` can read
+only in a frame `C` with `p ∈ C^⊥`.
+
+An information walk is a sequence of dual subspaces `Z 0, Z 1, …`; node `k ≥ 1` is produced from an earlier node
+`par k` (a copy, a stop, a relay through public helpers or a branch) either by shrinking (free) or by growing (paid).
+The union span of all visited nodes grows by at most the paid amount (`union_bound`).
+-/
+
+namespace NetCode
+
+open Module
+
+abbrev V := Fin 9 → ZMod 2
+abbrev Sub := Submodule (ZMod 2) V
+
+/-- The dot-product form on `F₂⁹`. -/
+def dotForm : LinearMap.BilinForm (ZMod 2) V := Matrix.toBilin' 1
+
+theorem dotForm_apply (x y : V) : dotForm x y = x ⬝ᵥ y := by
+  simp [dotForm, Matrix.toBilin'_apply', dotProduct]
+
+/-- The dual of a frame. -/
+def orth (C : Sub) : Sub := dotForm.orthogonal C
+
+theorem mem_orth {C : Sub} {p : V} : p ∈ orth C ↔ ∀ x ∈ C, x ⬝ᵥ p = 0 := by
+  simp [orth, LinearMap.BilinForm.mem_orthogonal_iff, dotForm_apply]
+
+/-- `dim C + dim C^⊥ = 9`. -/
+theorem finrank_add_orth (C : Sub) : finrank (ZMod 2) C + finrank (ZMod 2) (orth C) = 9 := by
+  have h := dotForm.finrank_add_finrank_orthogonal' C
+  have hker : LinearMap.ker dotForm = ⊥ := by
+    rw [eq_bot_iff]
+    intro x hx
+    rw [Submodule.mem_bot]
+    funext i
+    have := congrArg (fun f => f (Pi.single i 1)) (LinearMap.mem_ker.mp hx)
+    simp only [dotForm_apply, LinearMap.zero_apply] at this
+    simpa [dotProduct_single] using this
+  rw [show (dotForm.ker : Submodule (ZMod 2) V) = LinearMap.ker dotForm from rfl, hker, inf_bot_eq,
+    finrank_bot, add_zero, Module.finrank_fin_fun] at h
+  exact h
+
+theorem orth_anti {C C' : Sub} (h : C' ≤ C) : orth C ≤ orth C' := by
+  intro p hp
+  rw [mem_orth] at hp ⊢
+  exact fun x hx => hp x (h hx)
+
+/-- An owned descent `C → C'` (`C' ≤ C`) costs exactly the growth of the dual. -/
+theorem descent_cost_dual {C C' : Sub} (_h : C' ≤ C) :
+    finrank (ZMod 2) C - finrank (ZMod 2) C' =
+      finrank (ZMod 2) (orth C') - finrank (ZMod 2) (orth C) := by
+  have := finrank_add_orth C
+  have := finrank_add_orth C'
+  omega
+
+/-! ## The walk bound (Lemma S) -/
+
+attribute [local instance] Classical.propDecidable
+
+/-- Paid amount of step `k`: zero for a shrinking (free) step, the dimension growth otherwise. -/
+noncomputable def cost (Z : ℕ → Sub) (par : ℕ → ℕ) (k : ℕ) : ℕ :=
+  if Z k ≤ Z (par k) then 0 else finrank (ZMod 2) (Z k) - finrank (ZMod 2) (Z (par k))
+
+/-- Union span of the first `n + 1` nodes. -/
+def U (Z : ℕ → Sub) : ℕ → Sub
+  | 0 => Z 0
+  | n + 1 => U Z n ⊔ Z (n + 1)
+
+theorem le_U (Z : ℕ → Sub) : ∀ {i n : ℕ}, i ≤ n → Z i ≤ U Z n
+  | i, 0, h => by
+    rw [Nat.le_zero.mp h]; exact le_rfl
+  | i, n + 1, h => by
+    rcases Nat.lt_or_eq_of_le h with h | h
+    · exact le_trans (le_U Z (Nat.lt_succ_iff.mp h)) le_sup_left
+    · rw [h]; exact le_sup_right
+
+/-- **Walk bound.** If every step shrinks or grows its (earlier) parent, the union span of all visited dual subspaces
+has dimension at most `dim Z 0` plus the total paid amount. -/
+theorem union_bound (Z : ℕ → Sub) (par : ℕ → ℕ) (hpar : ∀ k, 0 < k → par k < k)
+    (hstep : ∀ k, 0 < k → Z k ≤ Z (par k) ∨ Z (par k) ≤ Z k) :
+    ∀ n, finrank (ZMod 2) (U Z n) ≤
+      finrank (ZMod 2) (Z 0) + ∑ k ∈ Finset.Icc 1 n, cost Z par k
+  | 0 => Nat.le_add_right _ _
+  | n + 1 => by
+    have ih := union_bound Z par hpar hstep n
+    have hp : par (n + 1) ≤ n := Nat.lt_succ_iff.mp (hpar (n + 1) (Nat.succ_pos n))
+    have hparU : Z (par (n + 1)) ≤ U Z n := le_U Z hp
+    rw [Finset.sum_Icc_succ_top (by omega : 1 ≤ n + 1)]
+    show finrank (ZMod 2) ((U Z n ⊔ Z (n + 1) : Sub)) ≤ _
+    by_cases hfree : Z (n + 1) ≤ Z (par (n + 1))
+    · have hc : cost Z par (n + 1) = 0 := by simp [cost, hfree]
+      have : (U Z n ⊔ Z (n + 1) : Sub) = U Z n := sup_eq_left.mpr (le_trans hfree hparU)
+      rw [this, hc]
+      omega
+    · have hgrow : Z (par (n + 1)) ≤ Z (n + 1) := (hstep (n + 1) (Nat.succ_pos n)).resolve_left hfree
+      have hc : cost Z par (n + 1) =
+          finrank (ZMod 2) (Z (n + 1)) - finrank (ZMod 2) (Z (par (n + 1))) := by simp [cost, hfree]
+      have hmod := Submodule.finrank_sup_add_finrank_inf_eq (U Z n) (Z (n + 1))
+      have hinf : finrank (ZMod 2) (Z (par (n + 1))) ≤ finrank (ZMod 2) ((U Z n ⊓ Z (n + 1) : Sub)) :=
+        Submodule.finrank_mono (le_inf hparU hgrow)
+      have hmono := Submodule.finrank_mono hgrow
+      rw [hc]
+      omega
+
+/-- **Lemma S.** A walk starting at `Z 0` that visits, for every receiver vector `p ∈ R`, some node containing `p`
+pays at least `dim (Z 0 ⊔ span R) - dim Z 0`.  With `Z 0 = (span S)^⊥` this is the binary rank of the pairing between
+the receivers and the sources (`verify.py` checks the equality), so stops, branches, copies and relays through public
+helpers never make one carrier cheaper than its COPY cost. -/
+theorem lemma_S (Z : ℕ → Sub) (par : ℕ → ℕ) (hpar : ∀ k, 0 < k → par k < k)
+    (hstep : ∀ k, 0 < k → Z k ≤ Z (par k) ∨ Z (par k) ≤ Z k) (n : ℕ) (R : Set V)
+    (hR : ∀ p ∈ R, ∃ i ≤ n, p ∈ Z i) :
+    finrank (ZMod 2) ((Z 0 ⊔ Submodule.span (ZMod 2) R : Sub)) ≤
+      finrank (ZMod 2) (Z 0) + ∑ k ∈ Finset.Icc 1 n, cost Z par k := by
+  have hle : Z 0 ⊔ Submodule.span (ZMod 2) R ≤ U Z n := by
+    refine sup_le (le_U Z (Nat.zero_le n)) (Submodule.span_le.mpr ?_)
+    intro p hp
+    obtain ⟨i, hi, hpi⟩ := hR p hp
+    exact le_U Z hi hpi
+  exact le_trans (Submodule.finrank_mono hle) (union_bound Z par hpar hstep n)
+
+/-! ## Lemma A: free additions along one path touch only free pairs -/
+
+/-- If a port `pi` lies in a frame `C` and a receiver `pj` reads in a frame `C' ⊇ C` (so `pj ∈ C'^⊥`), the pair is
+free: `pj · pi = 0`.  Hence content added at `C` from ports of `C` changes no costly pair of any receiver served higher
+on the same path, and could have been loaded at the top. -/
+theorem lemma_A {C C' : Sub} (h : C ≤ C') {pi pj : V} (hi : pi ∈ C) (hj : pj ∈ orth C') :
+    pj ⬝ᵥ pi = 0 := by
+  rw [mem_orth] at hj
+  rw [dotProduct_comm]
+  exact hj pi (h hi)
+
+/-- Content form of Lemma A: an addition `f` supported on ports of `C` vanishes on every costly pair
+(`port j · port i = 1`) of a receiver `j` reading in a frame containing `C`. -/
+theorem lemma_A_rows {L K : Type*} [Zero K] (port : L → V) (f : L → K) {C C' : Sub} (h : C ≤ C')
+    (hf : ∀ i, f i ≠ 0 → port i ∈ C) (j : L) (hj : port j ∈ orth C') (i : L)
+    (hcost : port j ⬝ᵥ port i = 1) : f i = 0 := by
+  by_contra hne
+  have := lemma_A h (hf i hne) hj
+  rw [this] at hcost
+  exact zero_ne_one hcost
+
+/-! ## Lemma M: merging carriers -/
+
+/-- If the receivers `S` of a carrier lie in `Z ∪ T`, `G ≤ Z` and `G ⊔ span S = ⊤`, then `Z ⊔ T = ⊤`. -/
+theorem sup_top_of_cover {Z T G : Sub} {S : Set V} (hS : ∀ p ∈ S, p ∈ Z ∨ p ∈ T) (hG : G ≤ Z)
+    (htop : G ⊔ Submodule.span (ZMod 2) S = ⊤) : Z ⊔ T = ⊤ := by
+  rw [eq_top_iff, ← htop]
+  refine sup_le (le_trans hG le_sup_left) (Submodule.span_le.mpr ?_)
+  intro p hp
+  rcases hS p hp with h | h
+  · exact (le_sup_left : Z ≤ Z ⊔ T) h
+  · exact (le_sup_right : T ≤ Z ⊔ T) h
+
+/-- Dimension count behind Lemma M: if `Z ⊔ T = ⊤` and `W ≤ Z ⊓ T` then `dim Z ≥ 9 - (dim T - dim W)`. -/
+theorem path_dim {Z T W : Sub} (htop : Z ⊔ T = ⊤) (hW : W ≤ Z ⊓ T) :
+    9 + finrank (ZMod 2) W ≤ finrank (ZMod 2) Z + finrank (ZMod 2) T := by
+  have hmod := Submodule.finrank_sup_add_finrank_inf_eq Z T
+  rw [htop, finrank_top, Module.finrank_fin_fun] at hmod
+  have := Submodule.finrank_mono hW
+  omega
+
+/-- **Lemma M, general count.** Carriers `c ∈ Fin k` merge in a frame with dual `W`; path `c` has union span `Z c`
+(from a line, so it pays at least `dim Z c - 1`), the common tail has union span `T ⊇ W` and pays at least
+`dim T - dim W`.  If every carrier's content tree spans everything (`Z c ⊔ T = ⊤`), then
+`total + (k - 1)·tail ≥ 8 k`.  Short tails therefore never beat `7 k`. -/
+theorem merge_count (k : ℕ) (Z : Fin k → Sub) (T W : Sub) (hW : ∀ c, W ≤ Z c ⊓ T)
+    (htop : ∀ c, Z c ⊔ T = ⊤) (pay : Fin k → ℕ) (hpay : ∀ c, finrank (ZMod 2) (Z c) ≤ pay c + 1)
+    (tail : ℕ) (htail : finrank (ZMod 2) T ≤ tail + finrank (ZMod 2) W) :
+    8 * k ≤ (∑ c, pay c) + tail + (k - 1) * tail := by
+  have h : ∀ c, 8 ≤ pay c + tail := by
+    intro c
+    have := path_dim (htop c) (hW c)
+    have := hpay c
+    omega
+  have hsum : ∑ _c : Fin k, 8 ≤ ∑ c, (pay c + tail) := Finset.sum_le_sum fun c _ => h c
+  simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul,
+    Finset.sum_add_distrib] at hsum
+  rcases k with _ | k
+  · simp
+  · simp only [Nat.add_sub_cancel]
+    nlinarith
+
+/-- A receiver whose need is not proportional to the merged ratio must read some pure path. -/
+theorem must_read_path {K : Type*} [Field K] {k : ℕ} (lam d : Fin k → K) (μ : K) (ν : Fin k → K)
+    (hd : d = μ • lam + ν) (hnot : ∀ μ' : K, d ≠ μ' • lam) : ∃ c, ν c ≠ 0 := by
+  by_contra h
+  push Not at h
+  apply hnot μ
+  rw [hd]
+  funext c
+  simp [h c]
+
+/-- **Lemma M for pairs.** Two carriers whose paths start on lines merge; the network pays
+`pay a + pay b + tail` with the bounds of `merge_count`.  A network cheaper than 14 forces both path unions to have
+dimension at most 6.  If no two subspaces containing `G`, each of dimension at most 6, cover the non-proportional
+receivers `N` (the finite fact checked by `verify.py`), the merged network costs at least 14, the price of the two
+separate carriers. -/
+theorem pair_merge (Za Zb T W G : Sub) (hG : G ≤ W) (hWa : W ≤ Za ⊓ T) (hWb : W ≤ Zb ⊓ T)
+    (hta : Za ⊔ T = ⊤) (htb : Zb ⊔ T = ⊤) (N : Set V) (hN : ∀ p ∈ N, p ∈ Za ∨ p ∈ Zb)
+    (nocover : ∀ A B : Sub, G ≤ A → G ≤ B →
+      finrank (ZMod 2) A ≤ 6 → finrank (ZMod 2) B ≤ 6 → ¬ ∀ p ∈ N, p ∈ A ∨ p ∈ B)
+    (pa pb tail : ℕ) (hpa : finrank (ZMod 2) Za ≤ pa + 1) (hpb : finrank (ZMod 2) Zb ≤ pb + 1)
+    (htail : finrank (ZMod 2) T ≤ tail + finrank (ZMod 2) W) :
+    14 ≤ pa + pb + tail := by
+  have h1 := path_dim hta hWa
+  have h2 := path_dim htb hWb
+  by_contra hlt
+  have ha6 : finrank (ZMod 2) Za ≤ 6 := by omega
+  have hb6 : finrank (ZMod 2) Zb ≤ 6 := by omega
+  exact nocover Za Zb (le_trans hG (le_trans hWa inf_le_left)) (le_trans hG (le_trans hWb inf_le_left))
+    ha6 hb6 hN
+
+end NetCode
diff --git a/research/p104-network-coded-carriers/lean/lake-manifest.json b/research/p104-network-coded-carriers/lean/lake-manifest.json
new file mode 100644
index 0000000000..a9d9cd1a47
--- /dev/null
+++ b/research/p104-network-coded-carriers/lean/lake-manifest.json
@@ -0,0 +1,117 @@
+{
+ "version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages": [
+  {
+   "url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "55b7917b472489c7c56a0fa6393af05cfd536599",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "55b7917b472489c7c56a0fa6393af05cfd536599",
+   "inherited": false,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "57d3325be72a842920813bcb40f96a6f7393c185",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  }
+ ],
+ "name": "NetCode",
+ "lakeDir": ".lake",
+ "fixedToolchain": false
+}
diff --git a/research/p104-network-coded-carriers/lean/lakefile.toml b/research/p104-network-coded-carriers/lean/lakefile.toml
new file mode 100644
index 0000000000..522d0058dd
--- /dev/null
+++ b/research/p104-network-coded-carriers/lean/lakefile.toml
@@ -0,0 +1,10 @@
+name = "NetCode"
+defaultTargets = ["NetCode"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "55b7917b472489c7c56a0fa6393af05cfd536599"
+
+[[lean_lib]]
+name = "NetCode"
diff --git a/research/p104-network-coded-carriers/lean/lean-toolchain b/research/p104-network-coded-carriers/lean/lean-toolchain
new file mode 100644
index 0000000000..fd85b262bf
--- /dev/null
+++ b/research/p104-network-coded-carriers/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.33.0-rc1
diff --git a/research/p104-network-coded-carriers/verify.py b/research/p104-network-coded-carriers/verify.py
new file mode 100644
index 0000000000..cf52884d41
--- /dev/null
+++ b/research/p104-network-coded-carriers/verify.py
@@ -0,0 +1,335 @@
+#!/usr/bin/env python3
+"""Network-coded owned carriers on the PR6030 P104 word: finite facts for the Lean lemmas.  Apache-2.0.
+
+Prepared for Matarener with Claude (Anthropic), via Claude Code.  Python 3.12, standard library only.
+
+Checks:
+  1. exact replay of the PR6030 word: frame rules (public ascents, owned strict descents, common-chart arithmetic),
+     endpoint rows, owned lifetimes, owned-to-owned transfers, read dimensions, and the crossing profile of the seven
+     dimension cuts of p104-owned-coding-boundaries (8 crossings on every level 2..8, owned paid 56);
+  2. Y_j final frame = p_j^perp with p_j . p_j = 1, so X_j and Y_j never share a frame;
+  3. the eight dimension-1 delivery lines l_c are the eight removed E8 root lines that carry deliveries; carrier
+     contents s_c (52 live coordinates, +-1/4) are collected in G_c = span of their ports (dimension 8, normal g_c);
+     receivers R_c = {j : p_j . l_c = 0} (52 each); <g_c> + span p_{R_c} = l_c^perp; g_a . l_c = [a != c];
+  4. Lemma S equality: dual walk cost dim(<g_c> + span p_{R_c}) - 1 = binary rank of the pairing [p_j . p_i] = 7;
+  5. the masked decoder: on the costly pairs of every port j (p_i . p_j = 1, i = j included) the eight carrier
+     rows have rank 8, so d_j is unique; d_jc = +-2 exactly on the carriers with j in R_c;
+  6. htop facts of Lean `merge_count`: <g_a, g_c> + span p_{R_c} = F2^9 for every a != c;
+  7. Lean `pair_merge` finite fact `nocover`: for every pair {a, b} and ratio +-1, no two subspaces containing
+     <g_a, g_b>, each of dimension <= 6, cover the non-proportional receivers N;
+  8. the computed record equals RESULT.json.
+"""
+from collections import Counter
+from fractions import Fraction as Q
+from hashlib import sha256
+from pathlib import Path
+import gzip, itertools, json, sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+WORD = 'research/p104-helper470-twin-rung-removal/WORD.json.gz'
+
+
+def need(ok, why):
+    if not ok:
+        raise SystemExit('FAIL ' + why)
+
+
+def log(kind, **data):
+    print(kind, json.dumps(data, sort_keys=True, default=str)[:300], flush=True)
+
+
+def dot(a, b):
+    return bin(a & b).count('1') & 1
+
+
+def rank(vs):
+    b = []
+    for v in vs:
+        for x in b:
+            v = min(v, v ^ x)
+        if v:
+            b.append(v)
+    return len(b)
+
+
+def span(basis):
+    s = {0}
+    for v in basis:
+        s |= {x ^ v for x in s}
+    return frozenset(s)
+
+
+def normals(vs):
+    return [u for u in range(1, 512) if all(dot(u, v) == 0 for v in vs)]
+
+
+def qrank(rows):
+    m = [list(r) for r in rows]
+    r = 0
+    for c in range(len(m[0]) if m else 0):
+        p = next((i for i in range(r, len(m)) if m[i][c] != 0), None)
+        if p is None:
+            continue
+        m[r], m[p] = m[p], m[r]
+        for i in range(len(m)):
+            if i != r and m[i][c] != 0:
+                f = m[i][c] / m[r][c]
+                m[i] = [x - f * y for x, y in zip(m[i], m[r])]
+        r += 1
+    return r
+
+
+def qsolve(A, b):
+    """Unique exact solution of A x = b (A has full column rank), else None."""
+    n = len(A[0])
+    m = [list(r) + [bb] for r, bb in zip(A, b)]
+    r = 0
+    piv = []
+    for c in range(n):
+        p = next((i for i in range(r, len(m)) if m[i][c] != 0), None)
+        if p is None:
+            return None
+        m[r], m[p] = m[p], m[r]
+        inv = 1 / m[r][c]
+        m[r] = [x * inv for x in m[r]]
+        for i in range(len(m)):
+            if i != r and m[i][c] != 0:
+                f = m[i][c]
+                m[i] = [x - f * y for x, y in zip(m[i], m[r])]
+        piv.append(c)
+        r += 1
+    if any(m[i][n] != 0 for i in range(r, len(m))):
+        return None
+    return [m[i][n] for i in range(n)]
+
+
+def replay(w):
+    S = [span(b) for b in w['frames']]
+    dims = [len(b) for b in w['frames']]
+    n, m = w['public'], w['owned_fields']
+    live = list(w['live'])
+    lset = set(live)
+    cur = list(w['initial']) + [None] * m
+    rows = [{r: Q(1)} for r in range(n + m)]
+    owned = set()
+    lifetimes, life = [], {}
+    deliveries = {}
+    reads = Counter()
+    o2o = 0
+    for e in w['program']:
+        op, r = e[0], e[1]
+        if op == 'MOVE':
+            a, b, private = e[2], e[3], e[4]
+            need(cur[r] == a and (r in owned) == private, 'move source')
+            need(S[b] < S[a] if private else S[a] < S[b], 'strict nesting')
+            cur[r] = b
+            if private:
+                life[r]['path'].append(dims[b])
+            continue
+        if op == 'INIT':
+            need(r >= n and r not in owned, 'init')
+            owned.add(r)
+            cur[r] = e[2]
+            rows[r] = {}
+            life[r] = {'path': [dims[e[2]]]}
+            lifetimes.append(life[r])
+            continue
+        if op == 'CLEAR':
+            need(r in owned and cur[r] == e[2], 'clear')
+            owned.discard(r)
+            cur[r] = None
+            rows[r] = {}
+            continue
+        q, f = Q(e[-2]), e[-1]
+        need(q != 0 and cur[r] == f, 'destination chart')
+        if op == 'SCALE':
+            rows[r] = {k: q * v for k, v in rows[r].items()}
+            continue
+        s = e[2]
+        need(cur[s] == f, 'common chart')
+        if s >= n and r >= n:
+            o2o += 1
+        if s >= n and r < n:
+            reads[dims[f]] += 1
+            if dims[f] == 1:
+                line = min(v for v in S[f] if v)
+                vec = {k: v for k, v in rows[s].items() if k in lset}
+                deliveries.setdefault(line, []).append(vec)
+        if op == 'COPY':
+            need(r in owned and not rows[r], 'copy')
+            rows[r] = {k: q * v for k, v in rows[s].items()}
+        else:
+            need(op == 'ADD', 'opcode')
+            t = dict(rows[r])
+            for k, v in rows[s].items():
+                x = t.get(k, 0) + q * v
+                if x:
+                    t[k] = x
+                else:
+                    t.pop(k, None)
+            rows[r] = t
+    need(not owned and cur[:n] == w['final'], 'exits')
+    for r in range(n):
+        exp = {r: Q(1)}
+        if r - 112 in lset:
+            exp[r - 112] = Q(1)
+        need(rows[r] == exp, 'endpoint row %d' % r)
+    return lifetimes, deliveries, reads, o2o
+
+
+def subspaces(nn, d):
+    out = []
+    for piv in itertools.combinations(range(nn), d):
+        free = [(r, c) for r in range(d) for c in range(piv[r] + 1, nn) if c not in piv]
+        for bits in range(1 << len(free)):
+            rows = [1 << piv[r] for r in range(d)]
+            for t, (r, c) in enumerate(free):
+                if bits >> t & 1:
+                    rows[r] |= 1 << c
+            out.append(span(rows))
+    return out
+
+
+def main():
+    src = json.loads((HERE / 'SOURCES.json').read_text())
+    for row in src['files']:
+        if row['usage'] == 'input':
+            need(sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], 'source pin ' + row['path'])
+    w = json.loads(gzip.decompress((ROOT / WORD).read_bytes()))
+    P = w['ports']
+    live = list(w['live'])
+    lidx = {r: k for k, r in enumerate(live)}
+    res = {}
+
+    # 1. replay and cut profile
+    lifetimes, deliveries, reads, o2o = replay(w)
+    cross = Counter()
+    paid = 0
+    for L in lifetimes:
+        for a, b in zip(L['path'], L['path'][1:]):
+            paid += a - b
+            for k in range(b + 1, a + 1):
+                cross[k] += 1
+    res['word'] = {'owned_lifetimes': len(lifetimes), 'owned_to_owned_adds': o2o, 'owned_paid': paid,
+                   'cut_crossings_levels_1_to_9': [cross[k] for k in range(1, 10)],
+                   'owned_reads_by_frame_dim': {str(k): v for k, v in sorted(reads.items())}}
+    need(paid == 56 and all(cross[k] == 8 for k in range(2, 9)), 'cut profile')
+    log('REPLAY', **res['word'])
+
+    # 2. Y_j final frame
+    S = [span(b) for b in w['frames']]
+    yn = []
+    for k, r in enumerate(live):
+        nv = normals([v for v in S[w['final'][r + 112]] if v])
+        need(len(nv) == 1 and nv[0] == P[k] and dot(P[k], P[k]) == 1, 'Y final = p^perp')
+        need(min(v for v in S[w['initial'][r]] if v) == P[k] and len(S[w['initial'][r]]) == 2, 'X start = <p>')
+        yn.append(nv[0])
+    res['frames'] = {'Y_final_is_p_perp': 104, 'X_start_is_p_line': 104, 'p_dot_p_is_1': 104}
+
+    # 3. carriers
+    lines = sorted(deliveries)
+    need(len(lines) == 8, 'eight delivery lines')
+    carriers = []
+    for l in lines:
+        vecs = {json.dumps(sorted((lidx[k], str(v)) for k, v in d.items())) for d in deliveries[l]}
+        need(len(vecs) == 1, 'one content per line')
+        d0 = deliveries[l][0]
+        carriers.append({lidx[k]: v for k, v in d0.items()})
+    weight3or7 = [q for q in range(512) if bin(q).count('1') in (3, 7)]
+    removed = [q for q in weight3or7 if q not in P]
+    need(len(removed) == 16 and all(l in removed for l in lines), 'lines are removed root lines')
+    g, R = [], []
+    for c, l in enumerate(lines):
+        s = carriers[c]
+        need(len(s) == 52 and set(abs(v) for v in s.values()) == {Q(1, 4)}, 'carrier content')
+        ports = [P[i] for i in s]
+        need(rank(ports) == 8, 'G_c dim 8')
+        nv = normals(ports)
+        need(len(nv) == 1, 'normal')
+        g.append(nv[0])
+        R.append([j for j in range(104) if dot(P[j], l) == 0])
+        need(len(R[c]) == 52, '52 receivers')
+        need(rank([g[c]] + [P[j] for j in R[c]]) == 8 and all(dot(v, l) == 0 for v in [g[c]] + [P[j] for j in R[c]]),
+             '<g_c> + p_R = l^perp')
+    gl = [[dot(g[a], lines[c]) for a in range(8)] for c in range(8)]
+    need(all(gl[c][a] == (a != c) for a in range(8) for c in range(8)), 'g_a . l_c = [a != c]')
+    res['carriers'] = {'lines': lines, 'normals_g': g, 'support_sizes': [len(s) for s in carriers],
+                       'receivers': [len(r) for r in R], 'g_dot_l_is_offdiagonal_one': True}
+    log('CARRIERS', lines=lines, g=g)
+
+    # 4. Lemma S equality: dual walk cost = F2 pairing rank = 7
+    walk = [rank([g[c]] + [P[j] for j in R[c]]) - 1 for c in range(8)]
+    pair = [rank([sum(dot(P[j], P[i]) << t for t, i in enumerate(sorted(carriers[c]))) for j in R[c]])
+            for c in range(8)]
+    need(walk == [7] * 8 and pair == [7] * 8, 'Lemma S equality')
+    res['lemma_S'] = {'dual_walk_cost': walk, 'pairing_rank': pair}
+
+    # 5. masked decoder
+    D = []
+    for j in range(104):
+        costly = [i for i in range(104) if dot(P[i], P[j]) == 1]
+        A = [[carriers[c].get(i, Q(0)) for c in range(8)] for i in costly]
+        need(qrank(A) == 8, 'unique decoder row')
+        x = qsolve(A, [Q(1) if i == j else Q(0) for i in costly])
+        need(x is not None, 'decoder solvable')
+        need(all((x[c] != 0) == (j in R[c]) for c in range(8)) and all(v in (0, 2, -2) for v in x), 'decoder support')
+        D.append(x)
+    res['decoder'] = {'unique_rows': 104, 'values': [-2, 2], 'support_equals_receivers': True,
+                      'carriers_per_port': dict(sorted(Counter(sum(1 for v in d if v) for d in D).items()))}
+
+    # 6. htop facts
+    for a in range(8):
+        for c in range(8):
+            if a != c:
+                need(rank([g[a], g[c]] + [P[j] for j in R[c]]) == 9, 'htop')
+    res['merge_count_htop'] = {'pairs': 56}
+
+    # 7. pair nocover
+    S4 = subspaces(7, 4)
+    need(len(S4) == 11811, 'subspace count')
+    rows = []
+    for a, b in itertools.combinations(range(8), 2):
+        G = [g[a], g[b]]
+        Gb = []
+        for v in sorted(G, reverse=True):
+            for x in Gb:
+                v = min(v, v ^ x)
+            Gb.append(v)
+            Gb.sort(reverse=True)
+
+        def red(v):
+            for x in Gb:
+                v = min(v, v ^ x)
+            return v
+        comp = []
+        for e in range(9):
+            if rank([red(c) for c in comp] + [red(1 << e)]) > len(comp):
+                comp.append(1 << e)
+        coord = {}
+        for mm in range(128):
+            x = 0
+            for i in range(7):
+                if mm >> i & 1:
+                    x ^= red(comp[i])
+            coord[x] = mm
+        need(len(coord) == 128, 'quotient')
+        for lam in (1, -1):
+            N = [j for j in range(104) if (D[j][a] or D[j][b]) and not (D[j][a] and D[j][b] and D[j][b] == lam * D[j][a])]
+            Nq = [coord[red(P[j])] for j in N]
+            feas = sum(1 for Sx in S4 if rank([x for x in Nq if x not in Sx]) <= 4)
+            need(feas == 0, 'pair cover %s' % ((a, b, lam),))
+            rows.append(len(N))
+    res['pair_nocover'] = {'pairs': 28, 'ratios': 2, 'six_dim_subspaces_tested_each': 11811,
+                           'min_N': min(rows), 'max_N': max(rows), 'feasible_covers': 0}
+    log('PAIRS', **res['pair_nocover'])
+
+    out = json.dumps(res, indent=1, sort_keys=True) + '\n'
+    if '--write' in sys.argv:
+        (HERE / 'RESULT.json').write_text(out)
+    need((HERE / 'RESULT.json').read_text() == out, 'RESULT.json')
+    print('PASS_P104_NETWORK_CODED_CARRIERS')
+
+
+if __name__ == '__main__':
+    main()