interfaceCost
plain-language theorem explainer
Total recognition cost of the polarized birth interface at discrete radius t equals the sum of single-edge costs over all ordered bichromatic adjacencies. Cosmology proofs of the coarsening ledger cite it as the paid side of the bulk/interface split. It is a direct Finset-sum definition specializing the graded-rung interface cost to the polarized diamond field.
Claim. For each natural number $t$, the total interface recognition cost is the sum, over the finite set $B_t$ of ordered bichromatic edges of the polarized birth diamond of radius $t$, of the single-edge cost $J(\varphi^{\Delta q})$ at the charge gap of that adjacency.
background
Phase 54 (LatticeBallEdges) closed the unweighted edge ledger for the polarized birth field: every adjacency is either monochromatic (carried bulk) or bichromatic (forced interface), with exact counts. This module weights that ledger by the forced recognition cost $J(x)=(x+x^{-1})/2-1$, unique by the Recognition Composition Law / functional equation, evaluated at the phi-rung gap between cell charges.
Charge is $\mathrm{sign}(x)\in{+1,0,-1}$. A monochromatic edge has equal charges, so gap $0$ and cost $J(\varphi^0)=J(1)=0$. A bichromatic edge joins the spine $x=0$ to $x=\pm 1$, so the gap is exactly $\pm 1$ and the cost is $J(\varphi)$ by reciprocal symmetry. The local edge cost is therefore the graded-rung form $J(\varphi^{k(p_1)-k(p_2)})$ specialized to this charge field; $B_t$ is the bichromatic slice of the diamond edge set at radius $t$.
Upstream, the general graded interface cost sums edge costs over different-rung edges of an arbitrary finite ordered edge set. The present definition is the polarized-diamond specialization of that sum.
proof idea
Pure definition: a noncomputable real-valued Finset sum of the local edge cost over the bichromatic edge set $B_t$. No lemmas are applied and there is no tactic proof body; the mathematical content is exactly that sum.
why it matters
This is the paid side of the coarsening cost ledger. Downstream, interfaceCost_eq_card and interfaceCost_card convert the sum into the closed form $(8t-4)\cdot J(\varphi)$ for $t\ge 1$, using that every bichromatic edge costs exactly one $J(\varphi)$. That identity feeds the total-cost theorems: carried bulk is free, total cost equals interface cost, and cost scales with the codimension-1 interface rather than bulk volume (the compute-watch law stated in the module doc for the 2D diamond and 3D octahedron).
In the broader framework this is the cost-unit reading of T5 ($J$-uniqueness) applied to the polarized birth geometry forced by the eight-tick / $D=3$ chain. The graded-rung headline t56_graded_cost_ledger is the abstract parent pattern; this definition is the concrete polarized instance those diamond formulas rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.