interfaceCost_card
plain-language theorem explainer
For the polarized diamond birth field at radius t ≥ 1, the interface recognition cost equals (8t − 4) times J(φ). Anyone citing the compute-watch law for 2D coarsening needs this exact scalar. The proof is a two-step rewrite: unit-step edges each cost J(φ), and the interface edge count is 8t − 4.
Claim. For every natural number $t \ge 1$, the interface recognition cost of the polarized diamond field of radius $t$ equals $(8t-4)\,J(\varphi)$, where $J(x)=(x+x^{-1})/2-1$ is the unique recognition cost and $\varphi$ is the golden-ratio fixed point.
background
This module weights the polarized-birth edge ledger by recognition cost. Every adjacency is either monochromatic (carried) or bichromatic (interface). Cost of an ordered edge is $J(\varphi^{\Delta q})$, with $J$ the unique solution of the recognition composition law and $\varphi$ the self-similar fixed point from the forcing chain.
Carried edges have equal charges, so $\Delta q=0$ and $J(\varphi^0)=J(1)=0$: the bulk is free. Interface edges join the spine charge $0$ to a lobe charge $\pm 1$, so $\Delta q=\pm 1$ and $J(\varphi^{\pm 1})=J(\varphi)$ by reciprocal symmetry. Thus total cost collapses to interface cardinality times $J(\varphi)$.
Upstream, the graded-rung lemma states that under the unit-step hypothesis every different-rung edge costs exactly one $J(\varphi)$, so interface cost equals that card times $J(\varphi)$. The diamond edge-count ledger supplies the card $8t-4$ for $t\ge 1$.
proof idea
Term-mode proof by two successive rewrites. First apply the graded-rung identity that, under unit-step grading, interface cost equals the number of different-rung edges times $J(\varphi)$. Then rewrite that cardinality by the diamond interface-count lemma, which evaluates it to $8t-4$ for $t\ge 1$. No further arithmetic or case splits.
why it matters
Direct input to the sibling total-cost theorem, which concludes that the whole polarized diamond costs $(8t-4),J(\varphi)$ because carried cost vanishes. That is the cost-unit form of the compute-watch law for 2D coarsening: cost scales with the codimension-1 interface, not bulk volume.
The module places the same pattern on the 3D octahedron as $(8t^2-8t+4),J(\varphi)$. Both rest on T5 uniqueness of $J$ and T6 forcing of $\varphi$, with $J(\varphi)=(\sqrt{5}-2)/2>0$ a strictly positive unit. Closes the 2D half of the Phase-54 cost ledger with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.