edgeCost_carried_zero
plain-language theorem explainer
Carried monochromatic edges of the polarized birth field cost exactly zero recognition: equal charges span no phi-rung, so the forced cost evaluates at φ^0 and vanishes. Cosmologists auditing the coarsening ledger cite this to separate free bulk from paid interface. The proof rewrites carried-filter membership to force charge difference zero, then applies the zero-power identity for the rung cost.
Claim. For every $t \in \mathbb{N}$ and every ordered adjacency $p$ of lattice-ball vertices that belongs to the carried (monochromatic) edge set at time $t$, the recognition cost of that edge is $0$.
background
This module weights the polarized-birth edge ledger by recognition cost. Phase 54 (LatticeBallEdges) already split every adjacency into carried monochromatic edges versus forced bichromatic interface edges. Here each ordered adjacency is scored by the unique cost $J(x)=(x+x^{-1})/2-1$ at the phi-rung gap between endpoint charges.
The polarized field assigns each vertex a charge in ${+1,0,-1}$. The edge cost is $J(\varphi^{c(p_1)-c(p_2)})$, written via the graded rung helper that evaluates $J$ at a power of $\varphi$. Carried edges are exactly those with equal charges: they are internal to a locked domain and are the bulk the engine is meant to carry coarse for free.
Upstream, the carried set is the filter of the full edge set on equal polarized charges. The zero-power identity $J(\varphi^0)=J(1)=0$ is the algebraic fact that turns equal charges into a free edge.
proof idea
Term-mode rewrite proof. Unfold membership in the carried set to obtain the filter witness that the two polarized charges are equal. Convert equality of charges into a zero difference via sub_eq_zero. Unfold the edge-cost definition (cost of the rung gap) and substitute the zero difference, then finish with the sibling identity that the rung cost at exponent zero is zero.
why it matters
This is the per-edge half of the compute-watch law in the module: bulk is free, only the codimension-1 interface is paid. It is the direct input to carriedCost_eq_zero, which sums the identity over the whole carried set, and thereby to totalCost_eq_interfaceCost, which equates total recognition cost with interface cost alone.
Downstream the ledger closes in closed form: 2D diamond total cost $(8t-4)\cdot J(\varphi)$ and 3D octahedron $(8t^2-8t+4)\cdot J(\varphi)$, both with carried cost identically zero. That matches the north-star claim that cost scales with recognition activity (the interface), not bulk volume. The positive unit $J(\varphi)=(\sqrt{5}-2)/2$ comes from T5 J-uniqueness and the golden fixed point $\varphi$ forced at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.