research: P104 wire routing obstructions (scoped negative, no κ)

research/p104-wire-routing-obstructions/PROOF.md

@@ -0,0 +1,68 @@
+# Proofs
+
+Notation. The 104 ports `q` are odd-weight vectors of `F_2^9`. Each port carries an E8 root line `r(q)` in A8 coordinates:
+weight 7 gives `e_a - e_b` on its two zero coordinates, weight 3 gives `2/3` on its three coordinates and `-1/3` elsewhere
+(as in `research/p104-carrier-code-uniqueness/e8/`). `G` is the Gram matrix: `G_ii = 2`, `G_ij = 0` when ports conflict
+(`<q_i, q_j> = 1`), and `G_ij = ±1` otherwise (V1). The partner residual is `E = D (G/2) D^{-1}` for a diagonal gauge `D`
+(rank-8 uniqueness, #1212 / `p104-carrier-code-uniqueness`). `Q_j = q_j^perp`, and `P(F)` is the set of ports in a frame `F`.
+
+## Lemma 1 (sign lemma). Lean: `third_root_or_sign`
+
+Let `k, i` be non-conflicting and let `j` be non-conflicting with both. Then either `r_j = ±(r_k - G_ki r_i)`, the third root
+of the A2 spanned by `r_k, r_i`, or `G_jk G_ji = G_ki`.
+
+*Proof.* `t = r_k - G_ki r_i` has norm 2, and `<r_j, t> = G_jk - G_ki G_ji ∈ {-2, 0, 2}`. Since `|r_j ∓ t|^2 = 4 ∓ 2<r_j, t>`,
+the value `±2` forces `r_j = ±t`. Otherwise `G_jk = G_ki G_ji`. ∎
+
+Consequence. The ratio `E_ji / E_jk = (d_k/d_i) G_ji G_jk` is the same for every common reader `j` except the third root.
+So a register carrying `x_k + Σ s_i x_i` with `s_i = (d_k/d_i) G_ki` serves all its readers except at most one per carried port.
+V2 checks every case: 4992 ordered pairs, the third root is a port in 4224 of them and one of the 16 missing lines in 768.
+
+## Lemma 2 (triangle lemma). Lean: `triangle_iff`
+
+For pairwise non-conflicting `k, m, i` with `a = G_km`, `b = G_mi`, `c = G_ki`: `abc = -1` iff `r_i = c r_k + b r_m`.
+
+*Proof.* `|r_i - c r_k - b r_m|^2 = 2 + 2abc`. ∎
+
+So the cocycle `G_km G_mi G_ik` is `-1` exactly on A2 triangles of ports. There are 704 of them among 19712 triples (V3).
+
+## Lemma 3 (cover lemma). Computer-checked (V4)
+
+For all ports `j ≠ a`, `|P(Q_j ∩ Q_a)| ≤ 24`. For `a ≠ b`, `P(Q_j ∩ Q_a) ∪ P(Q_j ∩ Q_b) = P(Q_j)` (48 ports) holds iff
+`{j, a, b}` is an A2 triangle. In that case the two halves are disjoint, 24 + 24.
+
+## Lemma 4 (capacity). Computer-checked (V5)
+
+If `x, y` are non-conflicting and `P(Q_x ∩ Q_y)` has 24 ports, then every 6-dimensional subframe holds at most 16 of them.
+
+## Lemma 5 (two sources). Hand proof from Lemmas 1, 3, 4 and V6
+
+*Setting* (the minimal "lives as wires" architecture): a partner's public chain is `{0} → G_y → Q_y` with `dim G_y = 7`.
+Every live has as its 8-dimensional frame some `Q`, with one live per `Q` (a "wire") or a carrier root. No public helpers.
+Lives do not read owned registers.
+
+*Claim.* There is no such legal word.
+
+*Proof.* Content-in-frame (`p104-carrier-code-uniqueness`, Lemma 1): a public register's lives-part stays on the ports of
+its frame. At `Q_y` partner `y` can only add the value of its wire, supported on that wire's 7-frame `F_y`. So
+`P(G_y) ∪ P(F_y) = P(Q_y)`. By Lemma 3, `G_y = Q_y ∩ Q_x` and `F_y = Q_y ∩ Q_z` for an A2 triangle `{x, y, z}`.
+
+The registers present at `G_y` are `Y_y` and lives whose 7-frame is `G_y`. Their 8-frames contain `G_y`, so they are `Q_x`,
+`Q_y` or the non-port hyperplane `(q_x + q_y)^perp`. The wire of `y` is excluded, since its frame must cover the other half.
+Hence the only other register is the wire of `x` (up to at most 8 frames equal to a carrier root). Let `A_w` and `A_y` be the
+lives-parts with which the two arrive. Every write at `G_y` reads a register present at `G_y` (frame-rank law, cf. #6170 Theorem JR (i)), so by induction over the
+events every lives-part held at `G_y` lies in `span(A_w, A_y)`.
+
+Partner `x` reads the ports of `G_y = F_x` only through its wire. Partner `y` keeps its `G_y`-ports from `G_y` onward, because
+its wire lives on the disjoint half. So `v_x|G_y` and `v_y|G_y` both lie in `span(A_w, A_y)`.
+
+By Lemma 1 and V6, `v_y = λ v_x` on 23 ports of `G_y` and `v_y = -λ v_x` on the third vertex `z`. Hence these two rows are
+independent and span the whole of `span(A_w, A_y)`. Every nonzero vector of that span has support of size at least 23, or is
+a multiple of `e_z`. But `A_w` lies in the wire's 6-frame and `A_y` lies in `Y_y`'s previous frame, which is a subframe of
+`G_y` of dimension ≤ 6. By Lemma 4 each has support ≤ 16. So both are multiples of `e_z`, a contradiction. ∎
+
+## Remarks
+
+- The triangle structure forces partners into disjoint A2 triangles, and 104 is not divisible by 3.
+- A single extra port on the partner side (an extra stop at `<p_z>`, where the live is still pure) repairs the sign defect alone,
+  and was checked exactly. Lemma 5 shows that the capacity defect needs a third source at `G_y`, that is, a helper.

research/p104-wire-routing-obstructions/README.md

@@ -0,0 +1,50 @@
+# Wire routing obstructions for the P104 residual
+
+**This is a scoped negative result. No new κ is claimed.**
+
+Most of the P104 local word's cost is the delivery of the residual `E = M - I` to the partners. Swarm words use about two
+dedicated helpers per partner for the last mile into `Q_j`. Every helper carries its own unit row, so it must also be cancelled
+("pollution"). A natural alternative is to let **lives themselves act as wires**: a live carries other lives' content into a
+partner's final frame. Its own row is wanted there, because `|E| = 1/2` on every non-conflicting pair.
+
+This package records exact structural facts about that idea and closes its minimal form:
+
+1. **Sign lemma** (hand proof + Lean). All common readers of a non-conflicting pair `k, i` want the same ratio sign, except
+   the reader whose root is the third root of the A2 through `r_k, r_i`. Universal wire contents therefore exist.
+2. **Triangle lemma** (hand proof + Lean). `G_km G_mi G_ik = -1` iff the three roots form an A2. There are 704 port triangles.
+3. **Cover lemma** (computer-checked). Two 7-frames `Q_j ∩ Q_a` and `Q_j ∩ Q_b` cover the 48 ports of `Q_j` iff `{j, a, b}` is an
+   A2 triangle, and then they split them 24 + 24.
+4. **Capacity** (computer-checked). Such a 24-port frame has at most 16 ports in any 6-dimensional subframe.
+5. **Two-source lemma** (hand proof). Assume a partner chain `{0} → G → Q`, every live a wire with one wire per `Q`, and no helpers.
+   Then no legal word exists: the two registers that meet in `G` cannot span both partners' rows.
+
+So a pollution-free "wire" architecture is impossible in its minimal form. Each partner needs a third source in its 7-frame,
+and with all lives used as wires that source is a helper. The variant "wires plus one helper per partner" is left open.
+
+Proofs: [PROOF.md](PROOF.md). Lean: [lean/WireSigns.lean](lean/WireSigns.lean).
+
+**Card:** `p104-side-correction`. See [TASK.json](TASK.json). Inputs are pinned in [SOURCES.json](SOURCES.json).
+
+## Reproduce
+
+```sh
+python3 scripts/research_package.py --package research/p104-wire-routing-obstructions --check-only
+python3.12 scripts/research_package.py --package research/p104-wire-routing-obstructions
+```
+
+`verify.py` uses only the standard library. It takes about 10 s and checks V1–V6, two failure controls and `RESULT.json`.
+The Lean file needs Mathlib (same revision as `research/p104-carrier-code-uniqueness/lean`). Build it with `lake build`
+inside `lean/`. Checked build (Lean v4.33.0-rc1, Mathlib `55b7917b`): `lake build` OK, and
+`lean/Axioms.lean` prints only `propext`, `Classical.choice`, `Quot.sound` for both theorems.
+
+## Open next questions
+
+- Is "lives as wires plus one helper per partner `G`-frame" cheaper than the swarm's two polluted helpers per partner?
+  The lower bounds here leave plenty of room. A first step is a constructive test on one triangle with an exact replay.
+- 104 is not divisible by 3, so at least 2 partners need another scheme; the best packing we found has 33 triangles (not proved maximal).
+
+## Credit
+
+Prepared by Matarener with Claude (Anthropic), via Claude Code. It builds on the E8 description of the ports and the
+content-in-frame lemma in `research/p104-carrier-code-uniqueness`, and on the frame-rank law (Theorem JR) of the P104
+designer toolkit (#6170). Apache-2.0.

research/p104-wire-routing-obstructions/RESULT.json

@@ -0,0 +1,12 @@
+{
+ "V2_ordered_pairs": 4992,
+ "V2_third_root_is_port": 4224,
+ "V2_third_root_missing_line": 768,
+ "V3_triples": 19712,
+ "V3_A2_triangles": 704,
+ "V4_max_ports_in_Qj_cap_Qa": 24,
+ "V4_unordered_cover_pairs": 2112,
+ "V5_frames_with_24_ports": 2112,
+ "V5_max_ports_in_6dim_subframe": 16,
+ "V6_ordered_frames_with_23_1_split": 4224
+}

research/p104-wire-routing-obstructions/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "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-carrier-code-uniqueness/e8/ports.json",
+      "usage": "input",
+      "git_blob": "b964c3ae2ea54d3763d74639d691ea9f5b02920e",
+      "sha256": "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce"
+    }
+  ]
+}

research/p104-wire-routing-obstructions/TASK.json

@@ -0,0 +1,123 @@
+{
+  "schema_version": 1,
+  "task_id": "p104-side-correction",
+  "priority_revision": 8,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "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": "refined",
+  "actual_scope": "Exact sign, triangle, cover and capacity facts for routing the P104 residual through lives used as wires, and an obstruction for the minimal pollution-free wire architecture (partner chain {0}->G->Q, one live wire per Q, no helpers).",
+  "scope_change_reason": "The card asks about joint helper bases; this package studies the extreme case of replacing last-mile helpers by lives and shows its minimal form is infeasible.",
+  "bottleneck_link": "Helper lifetimes (pollution bookkeeping at F0 and F9) are the largest R0 component of the P104 local word; removing helpers by using lives as wires was the natural route to cut them. This side result bounds that route.",
+  "budget_minutes": 240,
+  "stop_rule": "Stop once the minimal wire architecture is either constructed or excluded; the helper-assisted variant is a separate scope.",
+  "outcome": "completed",
+  "evidence": "verify.py V1-V6 (exhaustive over all ports, pairs, triples and 24-port frames) with two failure controls; Lean proofs of Lemmas 1-2 in lean/WireSigns.lean; hand proof of Lemma 5 in PROOF.md.",
+  "author": "Matarener",
+  "ai_assistance": "Claude (Anthropic) via Claude Code: derivations, scripts, Lean proofs and text; reviewed by Matarener.",
+  "open_questions": [
+    {
+      "question": "Is 'lives as wires plus one helper per partner G-frame' cheaper than two polluted helpers per partner?",
+      "why_it_matters": "It is the cheapest architecture not excluded here; crude chain-tax lower bounds leave a large margin below the current word.",
+      "first_step": "Construct one A2 triangle (three partners, three wires, three helpers) and replay it exactly.",
+      "blocked_by": "none"
+    },
+    {
+      "question": "Which scheme serves the partners left outside a triangle packing?",
+      "why_it_matters": "104 is not divisible by 3, so a pure triangle scheme cannot cover all partners.",
+      "first_step": "Prove or refute that 33 is the maximum packing of the 704 port triangles.",
+      "blocked_by": "none"
+    }
+  ]
+}

research/p104-wire-routing-obstructions/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-carrier-code-uniqueness/e8/ports.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate pinned ports; V1 E8 root model and conflict <=> orthogonal; V2 sign lemma on all 4992 pairs; V3 triangle lemma on all 19712 triples (704 A2); V4 cover pairs = A2 triangles, |P(Q_j cap Q_a)| <= 24; V5 6-dim subframes of the 2112 triangle frames hold <= 16 ports; V6 23:1 ratio split at the third vertex; controls (perturbed port, flipped Gram sign); RESULT.json equality."
+    }
+  ]
+}

research/p104-wire-routing-obstructions/lean/Axioms.lean

@@ -0,0 +1,3 @@
+import WireSigns
+#print axioms third_root_or_sign
+#print axioms triangle_iff