edgeCost
plain-language theorem explainer
Per ordered adjacency of the polarized birth diamond, the recognition cost is J at the phi-rung gap between the two cells' charges. Anyone building the coarsening cost ledger (interface paid, bulk free) cites this as the atomic weight on each edge. It is a one-line specialization of the graded rung cost to the polarized sign field.
Claim. For each $t \in \mathbb{N}$ and ordered adjacency $(p,q)$ of lattice vertices in the diamond ball of radius $t$, the edge cost is $J(\varphi^{c_t(p)-c_t(q)})$, where $c_t$ is the polarized charge of a cell ($\mathrm{sign}(x)\in\{+1,0,-1\}$) and $J(x)=(x+x^{-1})/2-1$.
background
The module weights the Phase-54 edge-count ledger of the polarized birth field by actual recognition cost. Every adjacency is either monochromatic (carried, equal charge) or bichromatic (interface). The forced cost is the unique $J$ solving the recognition composition law, $J(x)=(x+x^{-1})/2-1$, evaluated at a phi-rung gap.
Vertices are lattice points in the L1 ball of radius $t$. The polarized charge of a cell is $\mathrm{sign}(x)\in{+1,0,-1}$. The graded rung cost of an ordered pair under a field $k:V\to\mathbb{Z}$ is $J(\varphi^{k(p)-k(q)})$. Here $k$ is specialized to the polarized charge at time $t$.
Upstream, the generic edge cost is exactly that $J\circ\varphi^{\Delta k}$ construction; carried edges are the equal-charge filter of the adjacency set. The module goal is the compute-watch law: bulk volume is free, only the codimension-1 interface is paid.
proof idea
Definitional one-liner. Apply the powered cost $J(\varphi^{\cdot})$ to the integer difference of polarized charges on the two endpoints of the ordered pair. No lemmas are invoked; the body is the specialization of the graded rung edge cost to $k=\mathrm{polarized},t$.
why it matters
This is the atomic cost that turns the interface/carried edge split into a recognition-cost ledger. Downstream it feeds the carried sum, the interface sum, the total sum, and the equalities that collapse total cost to (interface cardinality)$\cdot J(\varphi)$ with carried cost identically zero.
That collapse is the literal cost-unit form of the north-star compute-watch law: cost scales with recognition activity on the interface, not with bulk volume the engine carries coarse for free. In 2D the total is $(8t-4)\cdot J(\varphi)$; in 3D, $(8t^2-8t+4)\cdot J(\varphi)$, with $J(\varphi)=(\sqrt{5}-2)/2>0$. The definition sits on the T5 uniqueness of $J$ and the phi fixed point from the forcing chain, specialized to the polarized birth geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.