[Matarener]

Change and mathematical scope

This PR adds a proof and a bounded search. It is a scoped negative result: no κ improvement and no paid-profile saving is claimed.

Theorem 3. Over F_3, the 104 P104 ports carry exactly one 8-dimensional decoding code, up to coordinate signs. A decoding code is a space containing, for every port l, a vector equal to 1 at l and 0 on the 55 ports that conflict with l.

• The code has minimum weight 49, in both rows and columns.
• It is the code that the carriers of PR5907 and of the selected PR6030 word already deliver: in each word, the ten owned deliveries of support 52 span it.

Structure. The ports are 104 of the 120 root lines of E8, in A8 coordinates. Two ports conflict exactly when their roots are orthogonal. The code is the roots' Gram matrix divided by 2.

Corollary 5 (scoped). Assume the partner code has dimension 8, the scalars are dyadic, and each carrier delivers directly to its receivers. Then every carrier needs a root frame of dimension at least 8 and a landing frame of dimension at most 1. So it pays at least 7, which is at least 56 per call, exactly PR5907's owned descent.

Remaining obligations, stated as limits:

• partner codes of dimension 9 or more are not covered (PR6030 has one, through a bookkeeping direction);
• multi-stage relays are not covered;
• a hand proof of uniqueness is open.

Task and overlap

• Base: 3f0152a32eeebac0df11946dbd50cabe5a7f7839.
• Inputs: the PR5907 and PR6030 WORD.json.gz files, pinned in SOURCES.json.
• Card: complex-rank-shape-decoder, scope refined to the decoder code of the local word. The reason is in TASK.json: the only paid mass not fixed by the local contract is the carriers' owned descent.
• Overlap: none found. I checked main and the open PRs up to Audit selected JSON locale failures without changing frozen sources #6165. The nearest work is fragmentation-ceiling, which treats lifts rather than carriers, and [Superseded by #6144] Conditional κ .003127137 (+1.333e-6 over #6030): owned registers 770 and 771 descend through the frames of helpers 705 and 706, which no longer relay them #6143/Conditional κ .003128386 (+2.582e-6 over #6030): owned registers 770, 771 and 772 descend through the frames of helpers 705, 706 and 731, which no longer relay them; helper 732 reads 771 at frame 117 #6144, which are relay-descent words.

Validation

python3.12 -B research/p104-carrier-code-uniqueness/verify.py --parts 0,1
python3.12 -B research/p104-carrier-code-uniqueness/verify.py --parts 2,3
python3.12 scripts/research_package.py --package research/p104-carrier-code-uniqueness

• Each verify.py command takes about 110 s and uses only the standard library.
• The certificate is a pre-order search tree of about 290k nodes, gzipped in four parts. The replay recomputes every option at every node and checks every dead end.
• Exactly one leaf is found. It has no free variable, and it is sign-equivalent to both words' codes and to the E8 Gram matrix / 2.
• f(7) = 36 and the E8 orthogonality are checked by enumeration.
• Controls:
  • a changed trit breaks the model equations;
  • a tampered dead node is rejected;
  • a premature solution leaf is rejected.
• Observed results:
  • PASS_P104_CARRIER_CODE_UNIQUENESS for both commands;
  • PASS_REGISTERED_RESEARCH_PACKAGE.

Lean (lean/, the same Mathlib revision as fragmentation-ceiling) formalises:

• the frame-decomposition lemma and the decoding-vector corollary;
• the ring-hom reduction to ZMod 3;
• dim B + dim B^⊥ = 9;
• carriers_cost.

CodeFact (from the certificate) and Capacity (from the enumeration) enter as hypotheses. The audit scripts/check_lean_axioms.py passes on 14 declarations, with only propext, Classical.choice and Quot.sound.

Credit

• The local word lineage is aliromman's PR5827 and DreamingOfClouds's PR5907 and PR6030.
• The checker rules follow PR5827's verifier.
• The package was prepared by Matarener with Claude (Anthropic) via Claude Code. The certificate was generated on Kaggle.

Open next questions

The open questions are listed in README.md and TASK.json:

1. A cheaper design with a partner code of dimension 9 or more.
2. Multi-stage relays.
3. A computer-free proof via E8 / S(3,4,8).

🤖 Generated with Claude Code

https://claude.ai/code/session_011VhYmAARGrLk38Gj9eUPzP

[Matarener]

Update (head 0969385): this PR now also contains a second, search-free proof of Theorem 3.

• e8/E8-PROOF.md: the 104 ports are 104 of the 120 root lines of E8, and two ports conflict exactly when their roots are orthogonal. The proof has five steps: frame factorisation over all 759 frames; frame sums of N = M ∘ Mᵀ; a per-row linear lemma, proved by hand with the tables in e8/handcert.md; an A2 triangle argument that makes M symmetric with ±1 entries; and a sign step giving M = D (Gram/2) D. e8/verify_e8hand.py re-checks the finite inputs in about a minute.
• lean/CarrierCode/E8*.lean: the whole argument formalized in Lean. The final theorem is CarrierCode.E8.decoding_unique. All finite inputs are checked with decide +kernel (no native_decide), and #print axioms gives only propext, Classical.choice, Quot.sound. These files are outside the default build target because each step-3 chunk needs about 8 GB of memory; the build commands and the exact scope are in e8/E8-PROOF.md. Not formalized: the link from decoding_unique to the word-level CodeFact hypothesis.

No κ change.

---

Generated by Claude Code