cost_phi_eq_zero_iff
plain-language theorem explainer
Two recognition levels induce zero J-cost on the forced phi-ratio exactly when the levels are equal. Cosmology and forward-dynamics arguments cite this to equate zero edge demand with level equality. The proof is a three-step rewrite: J vanishes only at ratio one, phi to a real power equals one only at exponent zero, and a difference vanishes iff the endpoints match.
Claim. For real levels $a$ and $b$, $J(\varphi^{a-b}) = 0$ if and only if $a = b$, where $J(x) = \frac{x+x^{-1}}{2}-1$ is the recognition cost and $\varphi$ is the golden ratio.
background
The Recognition Equilibrium module formalizes Phase-7 forward dynamics on a coupling graph: a field of recognition levels evolves by resolving each coupled pair to its mean (the sigma-conserving, J-minimal move). The forced ratio between two regions at levels $a$ and $b$ is $\varphi^{a-b}$. The recognition cost of a positive ratio is the J-cost $J(x)=(x+x^{-1})/2-1$, the unique cost forced by the Recognition Composition Law (T5).
Upstream, the local fact that $J(x)=0$ iff $x=1$ (for $x>0$) is already proved from strict positivity of $J$ off ratio one. Separately, $\varphi^t=1$ iff $t=0$, using positivity of $\varphi$ and $\log\varphi\neq 0$ from $1<\varphi$. This lemma packages those two facts for the phi-ladder ratio that appears on every edge.
proof idea
Pure term-mode rewrite. Apply the local zero-cost characterization at the positive base $\varphi^{a-b}$ (positivity from $\varphi>0$ and real power positivity), reducing the goal to $\varphi^{a-b}=1$. Rewrite by the phi-power identity to obtain $a-b=0$, then close with the standard fact that a difference vanishes iff the two reals are equal.
why it matters
Per-edge kernel of the ground-state theorem: total recognition cost over the coupling graph vanishes iff the level field is constant on every edge (consensus). That parent applies this lemma edgewise after a sum-of-nonnegatives argument, so the zero-cost configuration the variance descent converges to is exactly graph consensus.
In the framework this ties the T5 J-cost and the phi-ladder comparison of levels to the cosmogenesis claim that closed-system recognition dynamics relaxes to homogenization, while conjugate births keep sigma conserved in the open extension. No new axioms; it closes a documented Python check as a theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.