interfaceCost
plain-language theorem explainer
The interface recognition cost of an integer phi-rung field on a finite ordered edge set is the sum of single-edge J-costs over every adjacency whose endpoints sit on different rungs. Ledger and cosmology arguments cite it to isolate the paid part of a graded rung profile from the free same-rung bulk. The body is a filtered Finset sum of the per-edge cost at the rung gap; no proof content.
Claim. For an integer-valued rung field $k:V\to\mathbb{Z}$ and a finite ordered edge set $E\subseteq V\times V$, the interface recognition cost is $\sum_{(p,q)\in E,\,k(p)\neq k(q)} J(\varphi^{k(p)-k(q)})$, the sum of recognition costs over all different-rung adjacencies.
background
Phase 56 lifts the Phase-55 binary birth ledger to an arbitrary integer rung field. The engine's north star is to carry each region at the coarsest phi-rung its recognition allows, so the live profile is multi-valued, not a single sign flip. The only structural input the cost law needs is the forced minimal-distinction property: across every adjacency the rung changes by at most one.
The single-edge cost is $J(\varphi^{k(p)-k(q)})$, the Recognition J-cost evaluated at the rung gap (with $J(x)=(x+x^{-1})/2-1$). Equal-rung edges contribute $J(\varphi^0)=J(1)=0$; under unit-step gaps, different-rung edges contribute exactly $J(\varphi)$ by reciprocal symmetry. This definition packages the paid half of that split: sum only over edges with $k(p)\neq k(q)$.
It generalizes the polarized-birth interface sum (bichromatic edges of the diamond) to any finite ordered edge set and any integer rung field, without yet imposing unit-step.
proof idea
Pure definition: filter the edge Finset to pairs with unequal rung values, then sum the single-edge cost $J(\varphi^{k(p_1)-k(p_2)})$ over that filter. No tactics, no lemmas, no UnitStep hypothesis at this layer. Downstream theorems reintroduce UnitStep when they collapse each summand to $J(\varphi)$.
why it matters
This is the paid half of the graded-rung cost ledger. The headline theorem t56_graded_cost_ledger quotes it to state that total cost equals interface cost and equals (interface edge count) times $J(\varphi)$, with $J(\varphi)>0$. The equalities totalCost_eq_interfaceCost and interfaceCost_eq_card are proved directly from this sum: the former by splitting the full edge sum into equal-rung and unequal-rung parts and killing the carried part; the latter by evaluating every unequal-rung summand under UnitStep.
In the framework it is the multi-rung upgrade of the Phase-55 polarized interface cost. The binary birth field is recovered as the special case $k=$ polarized, so diamond and octahedron birth ledgers sit downstream once UnitStep is discharged by the Phase-55 level-difference facts. The economic content is the T5/T6 landmark: each forced unit-rung distinction costs one $J(\varphi)$, and same-rung bulk is free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.