edgeCost_interface
plain-language theorem explainer
Every forced bichromatic interface edge on the polarized birth lattice costs exactly J(φ). Cosmologists auditing the recognition-cost ledger cite this to pin each interface adjacency at one phi-rung. The proof unpacks membership in the interface set, then applies the absolute-one rung identity to the charge gap.
Claim. For every $t\in\mathbb{N}$ and every ordered pair of vertices $p$ in the bichromatic interface edge set $B(t)$, the recognition cost of that adjacency equals $J(\varphi)$, where $J(x)=(x+x^{-1})/2-1$ and $\varphi$ is the golden-ratio fixed point.
background
The module weights the Phase-54 edge-count ledger by the forced recognition cost $J(x)=(x+x^{-1})/2-1$ (unique by the cost functional equation), evaluated at the phi-rung gap between cell charges. Charges of the polarized birth field live in ${+1,0,-1}$. An ordered adjacency costs $J(\varphi^{c(p)-c(q)})$.
Carried (monochromatic) edges have equal charges, span zero rungs, and cost $J(1)=0$. Interface (bichromatic) edges join the $x=0$ spine to an $x=\pm 1$ cell, so charges differ by exactly $\pm 1$. The generic graded-rung fact is that under the unit-step law any different-rung edge costs $J(\varphi)$ by reciprocal symmetry $J(\varphi^{\pm 1})=J(\varphi)$.
Here $B(t)$ is the finset of those forced interface pairs at radius $t$, and the local edge-cost map is the specialization of the graded rung cost to the polarized charge field.
proof idea
Term-mode, four steps. First simp unpacks $p\in B(t)$ into adjacency plus the polarization (bichromatic) witness. Destructure that pair. Unfold the local edgeCost definition to expose $J(\varphi^{\mathrm{level_diff}})$. Finish by exact Jpow_of_abs_one applied to level_diff, which already proves the absolute charge gap is one on any interface adjacency. No case split on the sign is needed: reciprocal symmetry is baked into that lemma.
why it matters
This is the per-edge pin that turns the interface count into a cost. Downstream, interfaceCost_eq_card rewrites the sum of edge costs over $B(t)$ as $|B(t)|\cdot J(\varphi)$ by sum_congr plus this identity, then sum_const. The module doc records the north-star compute-watch law: total recognition cost scales with the codimension-1 interface, not bulk volume, because carried cost vanishes identically.
Concrete corollaries are the closed forms for the 2D diamond ($(8t-4)\cdot J(\varphi)$) and 3D octahedron ($(8t^2-8t+4)\cdot J(\varphi)$). $J(\varphi)=(\sqrt{5}-2)/2>0$ is a genuine positive unit cost. The argument sits on T5 J-uniqueness and T6 $\varphi$ as the self-similar fixed point; it does not itself re-derive those forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.