Jpow_of_abs_one
plain-language theorem explainer
If two cells differ by exactly one phi-rung (up or down), the adjacency costs exactly J(φ). Cosmology proofs of interface edge costs cite this to collapse the ±1 cases. The proof is a two-branch case split that applies the one-rung-up and one-rung-down lemmas.
Claim. For any integer $d$, if $d = 1$ or $d = -1$, then $J(\varphi^d) = J(\varphi)$, 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. Carried (monochromatic) edges span zero phi-rungs and cost $J(\varphi^0) = J(1) = 0$; interface (bichromatic) edges span exactly one rung and should cost $J(\varphi)$.
Jpow d is defined as $J(\varphi^d)$, the cost of an ordered adjacency whose charges differ by $d$ rungs. The forced cost is $J(x) = (x + x^{-1})/2 - 1$ (Cost.Jcost), unique by the Recognition Composition Law functional equation; $\varphi$ is the golden ratio fixed by the T5–T6 forcing chain.
Upstream, Jpow_one gives $J(\varphi^1) = J(\varphi)$ by simplifying the power, and Jpow_neg_one gives $J(\varphi^{-1}) = J(\varphi)$ via reciprocal symmetry $J(x^{-1}) = J(x)$ for $x > 0$.
proof idea
Term-mode case split on the disjunction $d = 1 \lor d = -1$. After substituting each equality, the goal is exactly Jpow_one in the first branch and Jpow_neg_one in the second. No further algebra is needed.
why it matters
Pins the unit interface cost used throughout the coarsening ledger: every forced bichromatic edge costs exactly $J(\varphi) = (\sqrt{5}-2)/2 > 0$, so total field cost is interface count times $J(\varphi)$ (bulk carried free). Downstream, edgeCost_interface in this module applies it after level_diff shows charges differ by $\pm 1$; GradedRungCost.edgeCost_interface reuses the same identity under the unit-step law. This is the cost-unit form of the compute-watch law: cost scales with the codimension-1 interface, not bulk volume. Lands in the cosmology side of the T5 J-uniqueness and T6 phi-forcing story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.