Jpow_zero
plain-language theorem explainer
A zero-rung charge gap on the phi-ladder costs nothing: J(φ^0) = J(1) = 0. Cosmology proofs that separate carried bulk from interface edges cite this to show monochromatic adjacencies are free. The proof is a three-step rewrite through the definition of Jpow, integer power zero, and the unit root of J-cost.
Claim. The recognition cost of a zero-rung gap vanishes: $J(\varphi^{0}) = 0$, equivalently $J(1) = 0$, where $J(x) = (x + x^{-1})/2 - 1$ and $\varphi$ is the golden ratio.
background
This module weights the polarized-birth edge ledger by recognition cost. After LatticeBallEdges splits every adjacency into carried (monochromatic) versus interface (bichromatic), the cost posted on an ordered edge whose charges differ by $d$ integer rungs is $J(\varphi^{d})$, written here as Jpow.
The forced cost is $J(x) = (x + x^{-1})/2 - 1$ (unique by the Recognition Composition Law / functional equation). It vanishes at the unit: $J(1) = 0$. The golden ratio $\varphi$ is the self-similar fixed point from the forcing chain (T5–T6). A carried edge has equal charges, so $d = 0$ and the argument collapses to $\varphi^{0} = 1$.
Upstream, Cost.Jcost_unit0 records exactly $J(1) = 0$ by direct simplification of the closed form.
proof idea
Term-mode rewrite in three steps: unfold Jpow to $J(\varphi^{d})$ at $d = 0$; apply zpow_zero so $\varphi^{0} = 1$; finish with Cost.Jcost_unit0, which states $J(1) = 0$. No case splits or arithmetic beyond the power identity.
why it matters
This is the algebraic pin that bulk is free. Downstream, edgeCost_carried_zero rewrites a monochromatic edge's charge difference to zero and applies this lemma, proving carried edges cost exactly 0. GradedRungCost.edgeCost_carried does the same for graded rung fields: equal rungs imply $J(\varphi^{0}) = 0$.
Together with the one-rung fact $J(\varphi^{\pm 1}) = J(\varphi) > 0$, the module obtains the north-star compute-watch law: total recognition cost equals interface count times $J(\varphi)$, with carriedCost identically zero (2D diamond and 3D octahedron formulas in the module doc). That is the cost-unit reading of T5 J-uniqueness and T6 $\varphi$ on the coarsening ledger: cost scales with the codimension-1 interface, not bulk volume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.