carriedCost_eq_zero
plain-language theorem explainer
For every radius t, the total recognition cost on monochromatic (carried) edges of the polarized birth field is exactly zero. Phase-55 cost-ledger arguments cite this to separate free bulk from paid interface. The proof unfolds the sum and applies the per-edge vanishing lemma on carried adjacencies.
Claim. For every natural number $t$, the sum of recognition edge costs over all monochromatic edges of the polarized diamond of radius $t$ equals $0$.
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 cost functional equation. On the polarized birth field, each ordered adjacency costs $J(\varphi^{\mathrm{charge}(p)-\mathrm{charge}(q)})$, with charges in ${+1,0,-1}$.
A carried edge is monochromatic: equal charges, zero rung gap, so $J(\varphi^0)=J(1)=0$. An interface edge is bichromatic (spine $x=0$ to $x=\pm 1$), spans one rung, and costs exactly $J(\varphi)>0$. The local carried-cost sum is therefore the sum of edge costs over the monochromatic edge set at radius $t$.
The same vanishing statement appears in the graded-rung setting for arbitrary integer rung fields on equal-rung edges; here it is specialized to the polarized diamond.
proof idea
Term-mode proof. Unfold the definition of carried cost as a finite sum of edge costs over the monochromatic edge set. Apply Finset.sum_eq_zero, then for each summand invoke the sibling lemma that every carried edge has edge cost zero (equal charges force $J(1)=0$). No further algebraic work.
why it matters
First conjunct of the Phase-55 2D headline ledger: carried bulk costs zero, total cost equals interface cost, and total cost is $(8t-4)\cdot J(\varphi)$ with $J(\varphi)>0$. That is the exact cost-unit form of the compute-watch law: cost scales with the codimension-1 interface, not bulk volume.
It also aligns with the graded-rung Phase-56 ledger, where the same vanishing holds for any unit-step rung field. Framework-wise it uses the T5-unique $J$ and the self-similar fixed point $\varphi$, turning the monochromatic bulk into a free carry. Without this identity the interface-only cost formula would not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.