Jpow
plain-language theorem explainer
The recognition cost of an ordered adjacency whose charges differ by an integer d of phi-rungs is J(φ^d), with J the forced cost and φ the golden ratio. Lattice-cost and polarized-birth arguments cite it as the atomic weight on each edge. It is a one-line definitional wrapper of Cost.Jcost at the integer power of φ.
Claim. For each integer $d$, the rung-gap cost is $J(\varphi^d)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost functional and $\varphi$ is the golden ratio.
background
The module weights the polarized-birth edge ledger of LatticeBallEdges: every adjacency is either a monochromatic carried edge or a bichromatic interface edge. The engine posts recognition cost $J$ at the phi-rung gap between the two cells' charges, with charge in ${+1,0,-1}$.
The forced cost is $J(x)=\frac{x+x^{-1}}{2}-1$ (Cost.Jcost), unique by the Recognition Composition Law / functional equation (T5). The scale $\varphi$ is the self-similar fixed point (T6). A zero gap gives $J(\varphi^0)=J(1)=0$; a unit gap gives $J(\varphi^{\pm 1})=J(\varphi)$ by reciprocal symmetry.
Upstream, carried isolates equal-charge edges (bulk free), and the same $J$ appears in refine-trigger and gravity coherence modules as the RS cost of a positive ratio.
proof idea
Definitional one-liner: evaluate Cost.Jcost at Constants.phi raised to the integer power $d$. No tactics, no lemmas; unfolding is the entire content.
why it matters
This is the atomic cost weight for the coarsening ledger. Downstream, edgeCost in this module and in GradedRungCost set the cost of an ordered adjacency to $J(\varphi^{k(p)-k(q)})$. Specializations Jpow_zero, Jpow_one, Jpow_neg_one, and Jpow_of_abs_one then prove carried edges cost exactly $0$ and interface edges cost exactly $J(\varphi)>0$.
That yields the north-star compute-watch law in cost units: total cost scales with the codimension-1 interface count times $J(\varphi)$, while bulk volume is carried free (2D diamond and 3D octahedron formulas in the module doc). It sits on T5 (J-uniqueness) and T6 ($\varphi$ forced), and closes the cost side of the Phase-54 edge-count ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.