phi_rpow_eq_one_iff
plain-language theorem explainer
The golden ratio raised to a real power equals 1 if and only if the exponent is zero. Cosmology and ladder arguments cite this to convert ratio-one statements into level equality. The proof rewrites the real power as an exponential, reduces to a product vanishing, and uses log phi ≠ 0 from phi > 1.
Claim. For every real $t$, $\varphi^t = 1$ if and only if $t = 0$, where $\varphi > 1$ is the golden ratio.
background
The module formalizes Phase-7 forward dynamics on recognition levels $x : \mathrm{Fin}, n \to \mathbb{R}$: each tick resolves a coupled pair to its mean (the $\sigma=0$, $J$-minimal move). The forced ratio between two regions is $\varphi^{x_i - x_j}$. Recognition cost $J$ vanishes only at ratio one, so identifying when $\varphi^t = 1$ is the bridge from cost-zero to equal levels.
Here $\varphi$ is the RS constant from Constants, with $\varphi > 1$ (one_lt_phi) and $\varphi > 0$. Real powers are defined via $\varphi^t = \exp(t \log \varphi)$ for positive base. The lemma is pure real analysis on that definition; it does not itself mention $J$ or the graph dynamics.
proof idea
Rewrite $\varphi^t$ by Real.rpow_def_of_pos (using positivity of $\varphi$) as $\exp(t \log \varphi)$, and rewrite $1$ as $\exp 0$. Injectivity of $\exp$ yields $t \log \varphi = 0$. From $\varphi > 1$ one has $\log \varphi > 0$, hence $\log \varphi \neq 0$. The product-zero lemma then forces $t = 0$ in one direction; the converse is $0 \cdot \log \varphi = 0$.
why it matters
Immediate parent is cost_phi_eq_zero_iff: two regions carry no forced distinction exactly when their levels are equal, proved by chaining $J(r)=0 \Leftrightarrow r=1$ with this lemma on $r = \varphi^{a-b}$. That zero-cost characterization feeds the module's total-cost vanishing criterion (consensus on every edge) and the Lyapunov story that variance descent reaches the $J$-ground state.
In the RS ladder, ratios are pure powers of $\varphi$ (T6 fixed point). Without $\varphi^t=1 \Leftrightarrow t=0$, equal cost would not pin equal rungs. The result is elementary but load-bearing for the equilibrium package: closed-system descent to consensus and the interpretation of births that keep $\sigma=0$ while structure persists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.