totalCost_eq_interfaceCost
plain-language theorem explainer
For any integer rung field on a finite ordered edge set, the total recognition cost equals the interface cost alone: equal-rung (carried) edges contribute nothing. Cosmology and ledger arguments cite this to drop bulk terms before counting interface edges. The proof splits the edge sum by rung equality and kills the carried part with the zero-cost lemma for equal rungs.
Claim. For any integer-valued rung field $k:V\to\mathbb{Z}$ and any finite ordered edge set $E\subseteq V\times V$, the total recognition cost $\sum_{p\in E} J(\varphi^{k(p_1)-k(p_2)})$ equals the sum of the same cost only over edges with $k(p_1)\neq k(p_2)$. Equivalently, the carried (equal-rung) bulk contributes zero.
background
This module lifts the Phase-55 binary birth ledger to a graded phi-rung field. The live engine carries each region at the coarsest phi-rung its recognition allows, so the charge is an integer map $k:V\to\mathbb{Z}$, not a single sign flip. Recognition cost on an ordered adjacency is the J-cost of the rung gap: $\mathrm{edgeCost}(k,p)=J(\varphi^{k(p_1)-k(p_2)})$.
Interface cost sums that quantity over edges with unequal rungs; carried cost sums it over equal-rung edges; total cost sums over all of $E$. The key algebraic fact upstream is that equal rungs give gap zero, and $J(\varphi^0)=J(1)=0$, so each carried edge costs exactly zero (edgeCost_carried). The unit-step law (gaps in ${0,\pm 1}$) is not needed for this equality; it enters only when one wants the closed form that every interface edge costs exactly $J(\varphi)$.
proof idea
Split the Finset sum of edgeCost over $E$ into the filter where rungs differ and its complement (rungs equal), via Finset.sum_filter_add_sum_filter_not. On the equal-rung filter, apply Finset.sum_eq_zero pointwise: membership in the filter plus double negation yields $k(p_1)=k(p_2)$, so edgeCost_carried gives zero. Rewrite the split identity with that zero sum and add_zero, unfold totalCost and interfaceCost, and take the symmetric form of the remaining equality.
why it matters
This is the bulk-vanishing step in the graded-rung cost ledger (Phase 56). The headline t56_graded_cost_ledger packages it with carried-cost zero, the card formula $\mathrm{totalCost}=(#\mathrm{interface})\cdot J(\varphi)$, and positivity of $J(\varphi)$. Downstream, totalCost_eq_card is a one-line rewrite through this theorem plus interfaceCost_eq_card.
The same identity is the abstract form of the Phase-55 polarized birth equality used in t55_cost_ledger and totalCost_card on the diamond: carry the bulk free, pay only for forced distinctions. In RS terms it is the cost-side statement that same-rung bulk is free under the J-cost forced by T5, while each unit rung step across an adjacency pays $J(\varphi)$. It is not a fitted parameter; it follows from $J(1)=0$ and the filter decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.