From 25515d539fd5121fd263120f8794598e4e958c0b Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 19:43:48 +0000 Subject: [PATCH 1/2] research: P104 wire routing obstructions (sign, A2 triangle, cover, capacity, two-source lemma) Scoped negative result, no kappa claim. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011VhYmBDtuD9DJg3wmnRskB --- .../p104-wire-routing-obstructions/PROOF.md | 68 +++++++ .../p104-wire-routing-obstructions/README.md | 49 ++++++ .../RESULT.json | 12 ++ .../SOURCES.json | 24 +++ .../p104-wire-routing-obstructions/TASK.json | 123 +++++++++++++ .../VERIFY.json | 20 +++ .../lean/Axioms.lean | 3 + .../lean/WireSigns.lean | 60 +++++++ .../lean/lakefile.toml | 10 ++ .../lean/lean-toolchain | 1 + .../p104-wire-routing-obstructions/verify.py | 166 ++++++++++++++++++ 11 files changed, 536 insertions(+) create mode 100644 research/p104-wire-routing-obstructions/PROOF.md create mode 100644 research/p104-wire-routing-obstructions/README.md create mode 100644 research/p104-wire-routing-obstructions/RESULT.json create mode 100644 research/p104-wire-routing-obstructions/SOURCES.json create mode 100644 research/p104-wire-routing-obstructions/TASK.json create mode 100644 research/p104-wire-routing-obstructions/VERIFY.json create mode 100644 research/p104-wire-routing-obstructions/lean/Axioms.lean create mode 100644 research/p104-wire-routing-obstructions/lean/WireSigns.lean create mode 100644 research/p104-wire-routing-obstructions/lean/lakefile.toml create mode 100644 research/p104-wire-routing-obstructions/lean/lean-toolchain create mode 100644 research/p104-wire-routing-obstructions/verify.py diff --git a/research/p104-wire-routing-obstructions/PROOF.md b/research/p104-wire-routing-obstructions/PROOF.md new file mode 100644 index 0000000000..47df6ab141 --- /dev/null +++ b/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 +(` = 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 ` = G_jk - G_ki G_ji ∈ {-2, 0, 2}`. Since `|r_j ∓ t|^2 = 4 ∓ 2`, +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 ``, 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. diff --git a/research/p104-wire-routing-obstructions/README.md b/research/p104-wire-routing-obstructions/README.md new file mode 100644 index 0000000000..018ed2d348 --- /dev/null +++ b/research/p104-wire-routing-obstructions/README.md @@ -0,0 +1,49 @@ +# 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/`. + +## 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. diff --git a/research/p104-wire-routing-obstructions/RESULT.json b/research/p104-wire-routing-obstructions/RESULT.json new file mode 100644 index 0000000000..a97713b2c3 --- /dev/null +++ b/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 +} diff --git a/research/p104-wire-routing-obstructions/SOURCES.json b/research/p104-wire-routing-obstructions/SOURCES.json new file mode 100644 index 0000000000..f10e0ed3cb --- /dev/null +++ b/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" + } + ] +} diff --git a/research/p104-wire-routing-obstructions/TASK.json b/research/p104-wire-routing-obstructions/TASK.json new file mode 100644 index 0000000000..4817d0954a --- /dev/null +++ b/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" + } + ] +} diff --git a/research/p104-wire-routing-obstructions/VERIFY.json b/research/p104-wire-routing-obstructions/VERIFY.json new file mode 100644 index 0000000000..a82eb5418f --- /dev/null +++ b/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." + } + ] +} diff --git a/research/p104-wire-routing-obstructions/lean/Axioms.lean b/research/p104-wire-routing-obstructions/lean/Axioms.lean new file mode 100644 index 0000000000..3bd06c9707 --- /dev/null +++ b/research/p104-wire-routing-obstructions/lean/Axioms.lean @@ -0,0 +1,3 @@ +import WireSigns +#print axioms third_root_or_sign +#print axioms triangle_iff diff --git a/research/p104-wire-routing-obstructions/lean/WireSigns.lean b/research/p104-wire-routing-obstructions/lean/WireSigns.lean new file mode 100644 index 0000000000..acda1f4025 --- /dev/null +++ b/research/p104-wire-routing-obstructions/lean/WireSigns.lean @@ -0,0 +1,60 @@ +/- +Wire sign lemmas for P104 ports seen as E8 root lines (norm 2, inner products in {0, ±1} off the diagonal). +(1) third_root_or_sign: for roots r_k, r_i with = c = ±1 and a reader root r_j with , = ±1, + either r_j = ±(r_k - c r_i) (the third root of their A2), or * = c. +(2) triangle_iff: for three roots with pairwise inner products a, b, c in {±1} + (a = , b = , c = ), a*b*c = -1 iff r_i = c r_k + b r_m. +Apache-2.0. +-/ +import Mathlib + +open RealInnerProductSpace + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +lemma pm_one_sq {x : ℝ} (h : x = 1 ∨ x = -1) : x * x = 1 := by + rcases h with h | h <;> subst h <;> norm_num + +theorem third_root_or_sign (rj rk ri : E) + (hj : ⟪rj, rj⟫ = 2) (hk : ⟪rk, rk⟫ = 2) (hi : ⟪ri, ri⟫ = 2) + (c : ℝ) (hc : c = 1 ∨ c = -1) (hki : ⟪rk, ri⟫ = c) + (hjk : ⟪rj, rk⟫ = 1 ∨ ⟪rj, rk⟫ = -1) (hji : ⟪rj, ri⟫ = 1 ∨ ⟪rj, ri⟫ = -1) : + rj = rk - c • ri ∨ rj = -(rk - c • ri) ∨ ⟪rj, rk⟫ * ⟪rj, ri⟫ = c := by + have hc2 := pm_one_sq hc + have hik : ⟪ri, rk⟫ = c := by rw [real_inner_comm]; exact hki + have hkj : ⟪rk, rj⟫ = ⟪rj, rk⟫ := real_inner_comm _ _ + have hij : ⟪ri, rj⟫ = ⟪rj, ri⟫ := real_inner_comm _ _ + -- squared distances to the third root t = rk - c ri and to -t + have e1 : ⟪rj - (rk - c • ri), rj - (rk - c • ri)⟫ = 4 - 2 * (⟪rj, rk⟫ - c * ⟪rj, ri⟫) := by + simp only [inner_sub_left, inner_sub_right, real_inner_smul_left, real_inner_smul_right, hj, hk, hi, hki, hik, hkj, hij] + ring + have e2 : ⟪rj + (rk - c • ri), rj + (rk - c • ri)⟫ = 4 + 2 * (⟪rj, rk⟫ - c * ⟪rj, ri⟫) := by + simp only [inner_add_left, inner_add_right, inner_sub_left, inner_sub_right, real_inner_smul_left, + real_inner_smul_right, hj, hk, hi, hki, hik, hkj, hij] + ring + rcases hjk with hx | hx <;> rcases hji with hy | hy <;> rcases hc with hcv | hcv + all_goals first + | (right; right; rw [hx, hy, hcv]; norm_num; done) + | (left; exact sub_eq_zero.mp ((inner_self_eq_zero (𝕜 := ℝ)).mp (by rw [e1, hx, hy, hcv]; norm_num))) + | (right; left; exact eq_neg_of_add_eq_zero_left ((inner_self_eq_zero (𝕜 := ℝ)).mp (by rw [e2, hx, hy, hcv]; norm_num))) + +theorem triangle_iff (rk rm ri : E) + (hk : ⟪rk, rk⟫ = 2) (hm : ⟪rm, rm⟫ = 2) (hi : ⟪ri, ri⟫ = 2) + (a b c : ℝ) (ha : a = 1 ∨ a = -1) (hb : b = 1 ∨ b = -1) (hc : c = 1 ∨ c = -1) + (hkm : ⟪rk, rm⟫ = a) (hmi : ⟪rm, ri⟫ = b) (hki : ⟪rk, ri⟫ = c) : + a * b * c = -1 ↔ ri = c • rk + b • rm := by + have ha2 := pm_one_sq ha; have hb2 := pm_one_sq hb; have hc2 := pm_one_sq hc + have hmk : ⟪rm, rk⟫ = a := by rw [real_inner_comm]; exact hkm + have him : ⟪ri, rm⟫ = b := by rw [real_inner_comm]; exact hmi + have hik : ⟪ri, rk⟫ = c := by rw [real_inner_comm]; exact hki + -- squared distance from ri to c rk + b rm equals 2 + 2abc + have hd : ⟪ri - (c • rk + b • rm), ri - (c • rk + b • rm)⟫ = 2 + 2 * (a * b * c) := by + simp only [inner_sub_left, inner_sub_right, inner_add_left, inner_add_right, real_inner_smul_left, + real_inner_smul_right, hk, hm, hi, hkm, hmk, hmi, him, hki, hik] + nlinarith [ha2, hb2, hc2] + constructor + · intro h + rw [← sub_eq_zero, ← inner_self_eq_zero (𝕜 := ℝ), hd, h]; norm_num + · intro h + have : ⟪ri - (c • rk + b • rm), ri - (c • rk + b • rm)⟫ = 0 := by rw [h]; simp + linarith [hd] diff --git a/research/p104-wire-routing-obstructions/lean/lakefile.toml b/research/p104-wire-routing-obstructions/lean/lakefile.toml new file mode 100644 index 0000000000..ccf0d37b17 --- /dev/null +++ b/research/p104-wire-routing-obstructions/lean/lakefile.toml @@ -0,0 +1,10 @@ +name = "WireSigns" +defaultTargets = ["WireSigns"] + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "55b7917b472489c7c56a0fa6393af05cfd536599" + +[[lean_lib]] +name = "WireSigns" diff --git a/research/p104-wire-routing-obstructions/lean/lean-toolchain b/research/p104-wire-routing-obstructions/lean/lean-toolchain new file mode 100644 index 0000000000..fd85b262bf --- /dev/null +++ b/research/p104-wire-routing-obstructions/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.0-rc1 diff --git a/research/p104-wire-routing-obstructions/verify.py b/research/p104-wire-routing-obstructions/verify.py new file mode 100644 index 0000000000..52300bfa89 --- /dev/null +++ b/research/p104-wire-routing-obstructions/verify.py @@ -0,0 +1,166 @@ +#!/usr/bin/env python3 +"""Verifier for p104-wire-routing-obstructions (standard library only). + +Checks, on the 104 P104 ports pinned in research/p104-carrier-code-uniqueness/e8/ports.json: + V1 ports are odd-weight vectors of F_2^9; their E8 root lines r(q) (A8 coordinates) have norm 2; ports conflict + ( = 1) exactly when the roots are orthogonal, and |r.r'| = 1 on every non-conflicting pair; + V2 sign lemma: for non-conflicting k, i and every common non-conflicting reader j, G_jk*G_ji = G_ki unless + r_j = +-(r_k - G_ki r_i) (the third root of their A2); counts of pairs whose third root is a port; + V3 triangle lemma: for pairwise non-conflicting k, m, i, G_km*G_mi*G_ik = -1 iff r_i = G_ki r_k + G_mi r_m; + V4 cover lemma: |P(Q_j cap Q_a)| <= 24, and P(Q_j cap Q_a) u P(Q_j cap Q_b) = P(Q_j) iff {j, a, b} is an A2 triangle; + V5 capacity: every 7-dim frame Q_x cap Q_y (x, y non-conflicting) with 24 ports has at most 16 ports in any 6-dim subframe; + V6 two-source data: on each 24-port frame P(Q_x cap Q_y), the ratio G_yi/G_xi takes one value on 23 ports and the + other on exactly one port, the third vertex of the triangle; + controls: a perturbed port list and a sign-flipped Gram entry must be rejected; + RESULT.json must equal the recomputed counts. +Apache-2.0. Prepared for Matarener with Claude (Anthropic), via Claude Code. +""" +import json, sys, hashlib +from fractions import Fraction as F +from itertools import combinations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PORTS = ROOT / "research/p104-carrier-code-uniqueness/e8/ports.json" +PORTS_SHA = "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce" + + +def fail(msg): + print("FAIL:", msg); sys.exit(1) + + +def dot2(a, b): + return bin(a & b).count("1") & 1 + + +def root(q): + ones = [b for b in range(9) if q >> b & 1] + if len(ones) == 7: + z = [b for b in range(9) if not q >> b & 1] + r = [F(0)] * 9; r[z[0]] = F(1); r[z[1]] = F(-1); return r + if len(ones) == 3: + return [F(2, 3) if b in ones else F(-1, 3) for b in range(9)] + raise ValueError("port of weight %d" % len(ones)) + + +def ip(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def analyse(P, G=None): + N = len(P) + if N != 104 or len(set(P)) != 104 or not all(bin(q).count("1") & 1 for q in P): + raise ValueError("V1 port list") + R = [root(q) for q in P] + if G is None: + G = [[ip(R[i], R[j]) for j in range(N)] for i in range(N)] + if not all(G[i][i] == 2 for i in range(N)): + raise ValueError("V1 norms") + for i in range(N): + for j in range(N): + if i != j and ((dot2(P[i], P[j]) == 1) != (G[i][j] == 0) or (G[i][j] != 0 and abs(G[i][j]) != 1)): + raise ValueError("V1 conflict <=> orthogonal") + orth = lambda a, b: a != b and not dot2(P[a], P[b]) + line = {} + for m, r in enumerate(R): + line[tuple(r)] = m; line[tuple(-x for x in r)] = m + res = {} + # V2 + pairs = third_port = third_missing = 0 + for k in range(N): + for i in range(N): + if not orth(k, i): continue + pairs += 1 + t = tuple(a - G[k][i] * b for a, b in zip(R[k], R[i])) + if ip(t, t) != 2: raise ValueError("V2 third root norm") + tj = line.get(t) + if tj is None: third_missing += 1 + else: third_port += 1 + for j in range(N): + if j in (k, i) or not (orth(j, k) and orth(j, i)): continue + if (G[j][k] * G[j][i] != G[k][i]) != (j == tj): + raise ValueError("V2 sign lemma at %d %d %d" % (k, i, j)) + res["V2_ordered_pairs"] = pairs; res["V2_third_root_is_port"] = third_port; res["V2_third_root_missing_line"] = third_missing + # V3 + tri = a2 = 0; triangles = set() + for k in range(N): + for m in range(k + 1, N): + if not orth(k, m): continue + for i in range(m + 1, N): + if not (orth(k, i) and orth(m, i)): continue + tri += 1 + prod = G[k][m] * G[m][i] * G[i][k] + comb = [G[k][i] * a + G[m][i] * b for a, b in zip(R[k], R[m])] + if (prod == -1) != (comb == R[i]): raise ValueError("V3 triangle lemma") + if prod == -1: a2 += 1; triangles.add(frozenset((k, m, i))) + res["V3_triples"] = tri; res["V3_A2_triangles"] = a2 + # V4 + Qp = [frozenset(i for i in range(N) if orth(i, j)) for j in range(N)] + if any(len(q) != 48 for q in Qp): raise ValueError("V4 |P(Q_j)| != 48") + maxint = 0; cover = 0 + for j in range(N): + H = {a: Qp[j] & Qp[a] for a in range(N) if a != j} + maxint = max(maxint, max(len(s) for s in H.values())) + for a in H: + for b in H: + if a < b and (H[a] | H[b]) == Qp[j]: + cover += 1 + if frozenset((j, a, b)) not in triangles: raise ValueError("V4 cover pair not an A2 triangle") + for T in triangles: + if j in T: + a, b = sorted(T - {j}) + if (H[a] | H[b]) != Qp[j]: raise ValueError("V4 triangle does not cover") + res["V4_max_ports_in_Qj_cap_Qa"] = maxint; res["V4_unordered_cover_pairs"] = cover + # V5, V6 + best6 = 0; frames = 0; split = {} + for x in range(N): + for y in range(x + 1, N): + Fp = Qp[x] & Qp[y] + if len(Fp) != 24 or not orth(x, y): continue + frames += 1 + for u in range(1, 512): + if u in (P[x], P[y], P[x] ^ P[y]): continue # functionals vanishing on F give no hyperplane + best6 = max(best6, sum(1 for i in Fp if not dot2(P[i], u))) + for (s, o) in ((x, y), (y, x)): + z = [i for i in Fp if G[s][o] * G[o][i] * G[s][i] == -1] + ratios = {} + for i in Fp: ratios.setdefault(F(G[o][i], G[s][i]), []).append(i) + key = tuple(sorted(len(v) for v in ratios.values())) + if key != (1, 23) or [v for v in ratios.values() if len(v) == 1][0] != z: + raise ValueError("V6 split") + split[key] = split.get(key, 0) + 1 + if best6 > 16: raise ValueError("V5 capacity") + res["V5_frames_with_24_ports"] = frames; res["V5_max_ports_in_6dim_subframe"] = best6 + res["V6_ordered_frames_with_23_1_split"] = sum(split.values()) + return res + + +def main(): + raw = PORTS.read_bytes() + sha = hashlib.sha256(raw).hexdigest() + pins = json.loads((HERE / "SOURCES.json").read_text()) + pinned = [f["sha256"] for f in pins["files"] if f["path"].endswith("e8/ports.json")] + if pinned != [sha]: fail("ports.json does not match its SOURCES.json pin") + P = json.loads(raw) + try: + res = analyse(P) + except ValueError as e: + fail(str(e)) + for k, v in res.items(): print("%-40s %s" % (k, v)) + # controls + bad = list(P); bad[0] = bad[0] ^ 3 if bin(bad[0] ^ 3).count("1") & 1 else bad[0] ^ 6 + try: analyse(bad); fail("control: perturbed port list accepted") + except ValueError: print("control: perturbed port list rejected") + R = [root(q) for q in P]; G = [[ip(R[i], R[j]) for j in range(104)] for i in range(104)] + k, i = next((k, i) for k in range(104) for i in range(104) if k != i and G[k][i] == 1) + G[k][i] = G[i][k] = -1 + try: analyse(P, G); fail("control: sign-flipped Gram accepted") + except ValueError: print("control: sign-flipped Gram entry rejected") + want = json.loads((HERE / "RESULT.json").read_text()) + if want != res: fail("RESULT.json differs from recomputed counts") + print("PASS p104-wire-routing-obstructions") + + +if __name__ == "__main__": + main() From 6aa982f08190fb3f2bff8f4dee3eeaf0ba0412d9 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 19:51:07 +0000 Subject: [PATCH 2/2] p104-wire-routing-obstructions: fixed Lean proof, record build and axioms Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011VhYmBDtuD9DJg3wmnRskB --- .../p104-wire-routing-obstructions/README.md | 3 ++- .../lean/WireSigns.lean | 16 +++++++++++----- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/research/p104-wire-routing-obstructions/README.md b/research/p104-wire-routing-obstructions/README.md index 018ed2d348..76dd916fc6 100644 --- a/research/p104-wire-routing-obstructions/README.md +++ b/research/p104-wire-routing-obstructions/README.md @@ -34,7 +34,8 @@ python3.12 scripts/research_package.py --package research/p104-wire-routing-obst `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/`. +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 diff --git a/research/p104-wire-routing-obstructions/lean/WireSigns.lean b/research/p104-wire-routing-obstructions/lean/WireSigns.lean index acda1f4025..78f977dcf3 100644 --- a/research/p104-wire-routing-obstructions/lean/WireSigns.lean +++ b/research/p104-wire-routing-obstructions/lean/WireSigns.lean @@ -32,11 +32,17 @@ theorem third_root_or_sign (rj rk ri : E) simp only [inner_add_left, inner_add_right, inner_sub_left, inner_sub_right, real_inner_smul_left, real_inner_smul_right, hj, hk, hi, hki, hik, hkj, hij] ring - rcases hjk with hx | hx <;> rcases hji with hy | hy <;> rcases hc with hcv | hcv - all_goals first - | (right; right; rw [hx, hy, hcv]; norm_num; done) - | (left; exact sub_eq_zero.mp ((inner_self_eq_zero (𝕜 := ℝ)).mp (by rw [e1, hx, hy, hcv]; norm_num))) - | (right; left; exact eq_neg_of_add_eq_zero_left ((inner_self_eq_zero (𝕜 := ℝ)).mp (by rw [e2, hx, hy, hcv]; norm_num))) + have key : (⟪rj, rk⟫ - c * ⟪rj, ri⟫) = 2 ∨ (⟪rj, rk⟫ - c * ⟪rj, ri⟫) = -2 ∨ ⟪rj, rk⟫ * ⟪rj, ri⟫ = c := by + rcases hjk with hx | hx <;> rcases hji with hy | hy <;> rcases hc with hcv | hcv <;> + rw [hx, hy, hcv] <;> norm_num + rcases key with h | h | h + · left + have h0 : ⟪rj - (rk - c • ri), rj - (rk - c • ri)⟫ = 0 := by rw [e1, h]; norm_num + exact sub_eq_zero.mp ((inner_self_eq_zero (𝕜 := ℝ)).mp h0) + · right; left + have h0 : ⟪rj + (rk - c • ri), rj + (rk - c • ri)⟫ = 0 := by rw [e2, h]; norm_num + exact eq_neg_of_add_eq_zero_left ((inner_self_eq_zero (𝕜 := ℝ)).mp h0) + · right; right; exact h theorem triangle_iff (rk rm ri : E) (hk : ⟪rk, rk⟫ = 2) (hm : ⟪rm, rm⟫ = 2) (hi : ⟪ri, ri⟫ = 2)