interfaceCost_eq_card
plain-language theorem explainer
Under the unit-step law, the interface recognition cost of any integer rung field equals the number of different-rung edges times J(φ). Cosmology and ledger arguments cite this to collapse the interface sum to a pure count. The proof applies the per-edge interface cost lemma, then rewrites the filtered sum as a constant sum.
Claim. Let $k:V\to\mathbb{Z}$ be a rung field and $E$ a finite set of ordered edges. If $k$ is unit-step on $E$ (every adjacency changes rung by at most one), then the interface cost equals $N\cdot J(\varphi)$, where $N$ is the number of edges with $k(p)\neq k(q)$ and $J$ is the recognition cost.
background
This module lifts the Phase-55 binary birth ledger to arbitrary graded phi-rung fields. The engine carries each region at the coarsest rung recognition allows, so cost must be tracked for multi-valued $k:V\to\mathbb{Z}$, not only a sign flip.
The key hypothesis is the forced minimal-distinction property: across every edge in $E$, the rung gap lies in ${0,+1,-1}$. A unit recognition step resolves at most one phi-rung; the live engine keeps this because T-3 descends one rung at a time.
Edge cost is $J(\varphi^{k(p)-k(q)})$. Carried (equal-rung) edges cost $J(1)=0$. Interface edges, under unit-step, have gap $\pm 1$, so cost $J(\varphi)$ by reciprocal symmetry of $J$. Interface cost is the sum of edge costs over the different-rung filter of $E$.
proof idea
First prove a pointwise fact on the filtered set: every interface edge $p$ satisfies $\mathrm{edgeCost},k,p = J(\varphi)$, by membership in the filter plus the upstream lemma that unit-step forces interface edges to cost exactly $J(\varphi)$.
Unfold the definition of interface cost (sum of edge costs over different-rung edges). Rewrite the sum by congruence with that pointwise equality, then apply the constant-sum identity so the sum becomes cardinality times $J(\varphi)$.
why it matters
This is the closed-form step for the graded-rung cost ledger (Phase 56). It feeds totalCost_eq_card, which states that total recognition cost of any unit-step rung field is exactly (interface edge count) times $J(\varphi)$: carried bulk is free.
Downstream, the polarized birth specializations reuse the same pattern to get exact counts such as $(8t-4)\cdot J(\varphi)$ on the diamond. The module recovers Phase 55 as the polarized case once unit-step is discharged by level-diff.
In the broader RS picture, $J$ is the unique cost from the forcing chain (T5), and $\varphi$ is the self-similar fixed point (T6). Paying $J(\varphi)$ per forced unit-rung distinction is the ledger law the engine maintains under single-rung refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.