totalCost_eq_interfaceCost
plain-language theorem explainer
For the polarized birth diamond of radius t, total recognition cost equals interface cost alone: monochromatic carried edges contribute nothing. Phase-55 cost-ledger arguments cite this to collapse bulk-plus-boundary into pure interface accounting. The proof splits the edge sum by polarization agreement, matches the parts to the interface and carried sets, and kills the carried sum via the equal-charge zero-cost lemma.
Claim. For every natural number $t$, the sum of recognition edge costs over all ordered adjacencies of the polarized birth diamond of radius $t$ equals the sum restricted to bichromatic interface edges (those whose endpoints have unequal polarization charges).
background
This module weights the Phase-54 edge-count ledger by the forced recognition cost $J(x)=(x+x^{-1})/2-1$, unique by the Recognition Composition Law and T5. Each ordered adjacency pays $J(\varphi^{\Delta q})$ where $\Delta q$ is the charge gap between endpoints; charges are the polarized field values in ${+1,0,-1}$.
A carried (monochromatic) edge has equal charges, so $\Delta q=0$ and $J(\varphi^0)=J(1)=0$. An interface (bichromatic) edge joins the spine $x=0$ to a wing $x=\pm 1$, so $\Delta q=\pm 1$ and the cost is exactly $J(\varphi)$ by reciprocal symmetry. The module therefore claims the whole field costs only the interface count times $J(\varphi)$.
The same identity already exists abstractly for any integer rung field on any finite edge set (GradedRungCost): total cost equals interface cost because equal-rung bulk sums to zero. Here the rung field is specialized to the polarized diamond charges, and the edge partition is the concrete carried/interface split of LatticeBallEdges.
proof idea
Split the sum of edge costs over the full ordered edge set $E(t)$ into the filter where polarization charges differ and the complementary filter, via Finset.sum_filter_add_sum_filter_not.
Rewrite the differing filter as the interface set $B(t)$ by unfolding $E$ and $B$ and collapsing the double filter. Rewrite the complementary filter as the carried set by definition of carried and a pointwise simp congruence.
The carried sum vanishes: apply Finset.sum_eq_zero and invoke edgeCost_carried_zero on each monochromatic edge. After add_zero, the split identity is exactly total cost equals interface cost (definitions unfolded, symmetry of equality).
why it matters
This is the cost-unit half of the Phase-55 headline: carry the bulk free, pay only for the interface. It is quoted directly inside t55_cost_ledger (the 2D diamond ledger) and inside totalCost_card, which upgrades the equality to the exact formula $(8t-4)\cdot J(\varphi)$ for $t\ge 1$.
Downstream, the same pattern feeds the graded-rung Phase-56 ledger, where any unit-step rung field on any finite edge set obeys carried cost zero, total equals interface, and total equals interface-cardinality times $J(\varphi)$. The argument realizes the north-star compute-watch law in exact cost units: cost scales with codimension-1 recognition activity, not bulk volume.
Framework landmarks: $J$ is the T5-unique cost; $\varphi$ is the T6 self-similar fixed point; $J(\varphi)=(\sqrt{5}-2)/2>0$ supplies a genuine positive unit. No scaffolding remains; the theorem is fully proved over $\mathbb{R}$ and $\mathbb{N}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.