[Matarener]

Requested by Mark · project thread

Change and mathematical scope

New package research/p104-network-coded-carriers. It is a scoped negative result (proof + exhaustive finite check).
It claims no new word or κ.

fragmentation-ceiling §6.7 lists "network-coded carriers with stops and shedding" as a door outside A30-CUT.
On the selected PR6030 local word and its 8-carrier code (unique up to sign by #6166):

• Lemma S (Lean). Pass to duals: public ascents shrink C^⊥ for free, owned descents grow it at their price. The
  union span of all visited duals grows by at most the paid amount. Hence a carrier with any stops, copies, branches
  or relays through public helpers pays at least its COPY cost, the F2 pairing rank. On PR6030 this is 7 for each
  carrier, checked exactly.
• Lemma A (Lean). Additions and shedding along one path touch only free pairs of the receivers above, so they
  are equivalent to loading at the top.
• Lemma M (Lean + finite facts). Merging requires a common frame, so carrier c must reach g_a. Since
  g_a · l_c = 1 for a ≠ c, each content tree spans F2^9.
  • Merges of k carriers with a tail of length ≤ 1 cost more than 7k.
  • Every pair merge costs ≥ 14 = 7 + 7. This is exhaustive over 28 pairs × 2 ratios × 11,811 six-dimensional
    subspaces.

Remaining obligations (not claimed):

• merges of ≥ 3 carriers with tails ≥ 2, and merge trees;
• codes with ≥ 9 carriers (masked floor beyond rank 8);
• decoders reading X (P-ATOM).

Task and overlap

• Base 2485805a6d47f36ea83ddde6327d453ac82d44dc. Card complex-rank-shape-decoder, scope refined (see TASK.json).
• Input: research/p104-helper470-twin-rung-removal/WORD.json.gz (PR6030 word, sha256 7834725d…).
• Nearest work:
  • fragmentation-ceiling §6.4/§6.7. Lemma S is the P104 single-commodity statement with arbitrary stops and
    relays.
  • p104-owned-coding-boundaries (JOINT-BOUNDARY): its seven cuts need a fixed boundary with dimension-1
    deliveries. Here that premise is removed for the covered classes, and PR6030 is shown tight on all seven cuts
    (8 crossings per level).
  • Add P104 owned-lineage factorization and scoped review of PR6170's owned-layer floor #6267 (open, ours): it asks whether the lineage floor extends to merges. Pair merges are answered here.
  • p104-signed-mixed-carrier-bank: mixed carriers in a relaxed frame model. Here the actual frame rules are used.
• Open PR heads Prove exact rational cube-query costs for cubic reader repair (no κ) #6200–No new κ: shared partial sums and row sharing cut PR6167's word from 22,821 to 17,445 events #6314 were scanned. None treats network-coded carriers.

Validation

python3 -B research/p104-network-coded-carriers/verify.py            # PASS_P104_NETWORK_CODED_CARRIERS, ~17 s, stdlib
python3 -B scripts/research_package.py --package research/p104-network-coded-carriers   # PASS_REGISTERED_RESEARCH_PACKAGE (Python 3.12)
python3 -B scripts/check_research_commit.py --package research/p104-network-coded-carriers  # PASS_RESEARCH_COMMIT_BYTES

• verify.py replays the word exactly, with frame rules and endpoint rows. It then checks the carrier, decoder and
  spanning facts and the pair cover search, and compares with RESULT.json. The decoder has a uniqueness check
  (rank 8 on the costly pairs of every port).
• Lean: cd research/p104-network-coded-carriers/lean && lake exe cache get && lake build && lake env lean Audit.lean.
  It uses the Mathlib pin of p104-carrier-code-uniqueness. It has no sorry, and every theorem depends only on
  propext, Classical.choice and Quot.sound. Built locally in the cloud session; Lean is not run by CI.

Credit

DreamingOfClouds (PR6030 word), the authors of fragmentation-ceiling and p104-owned-coding-boundaries (the door
and the cut framework), and the P104 decoder lineage cited in complex-decoder-scope-map.md.
Prepared with substantial AI assistance (Claude, Anthropic, via Claude Code).

Open next questions

See the package README and TASK.json:

• k ≥ 3 merges with long tails and merge trees: extend must_read_path to k carriers and rerun the cover check;
• reduce 9+ carrier codes to the masked decoder floor via Lemmas S/A.

---

🤖 Generated with Claude Code

https://claude.ai/code/session_011VhYm8VQDouHFXnykwkJzW