P104 network-coded owned carriers: stops, shedding and pair merges do not lower owned paid 56

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).

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.

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
+ }
+}

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"
+    }
+  ]
+}