interfaceCost_eq_card
plain-language theorem explainer
The interface recognition cost of the polarized birth field at time t equals the interface-edge count times J(φ). Cosmology and ledger auditors cite it to convert edge counts into recognition cost. The proof unfolds the sum definition, replaces every summand by J(φ) via the unit-step interface lemma, and collapses the constant sum.
Claim. For every natural number $t$, the interface recognition cost at time $t$ equals $|B(t)| \cdot J(\varphi)$, where $B(t)$ is the finite set of bichromatic (interface) edges of the polarized birth field, $J$ is the recognition cost $J(x)=(x+x^{-1})/2-1$, and $\varphi$ is the golden-ratio fixed point.
background
The module weights the polarized-birth edge ledger by recognition cost. Every ordered adjacency is either monochromatic (carried bulk) or bichromatic (interface). Cost of an adjacency spanning rung gap $d$ is $J(\varphi^d)$, with $J(x)=(x+x^{-1})/2-1$ the unique cost solving the Recognition Composition Law (T5).
Carried edges have equal charges, so $d=0$ and $J(1)=0$: bulk is free. Interface edges meet the unit-step law (charges differ by exactly $\pm 1$), so each costs $J(\varphi^{\pm 1})=J(\varphi)$ by reciprocal symmetry. The local interface cost is therefore the sum of edge costs over the interface set $B(t)$.
Upstream, edgeCost_interface under UnitStep forces every different-rung edge to cost exactly $J(\varphi)$. The graded-rung abstract form of the same identity already exists; this declaration specializes it to the polarized birth field at discrete time $t$.
proof idea
Term-mode, three steps. Unfold the definition of interface cost (a Finset sum of edge costs over $B(t)$). Apply Finset.sum_congr with the specialized interface lemma: every $p\in B(t)$ satisfies edgeCost_interface, so each summand equals $J(\varphi)$. Finish with Finset.sum_const, converting a constant sum into cardinality times $J(\varphi)$.
why it matters
This is the cost-unit half of the compute-watch law for polarized birth: cost scales with the codimension-1 interface, not bulk volume. Downstream, interfaceCost_card rewrites through this identity and the explicit diamond count to obtain $(8t-4)\cdot J(\varphi)$ for $t\ge 1$; the total-cost headline then follows because carried cost vanishes. The same pattern feeds the graded-rung totalCost_eq_card abstract ledger.
Framework landmarks: $J$ is the T5-unique cost; $\varphi$ is the T6 self-similar fixed point; $J(\varphi)=(\sqrt{5}-2)/2>0$ is a genuine positive unit. The result closes the weighting step between the Phase-54 edge-count ledger and the Phase-56 cost ledger over $\mathbb{R}$ and $\mathbb{N}$, with no sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.