rpow_one_base'
plain-language theorem explainer
The identity that one raised to any real power equals one is a standard algebraic fact. It supports the coordinate rescaling argument that reduces the general alpha case to the base J function in the WLOG proposition. The argument consists of a direct call to the one_rpow lemma.
Claim. For every real number $α$, $1^α = 1$.
background
The WLOGAlphaOne module shows that the calibrated solution family takes the form $F_α(x) = (1/α²)(cosh(α ln x) − 1)$ for $α ≥ 1$. This expression equals $(1/α²) J(x^α)$ where $J(x) = (x + x^{-1})/2 − 1$. The reparametrization uses that the map $x ↦ x^α$ is a group automorphism of the positive reals under multiplication, so the unit-curvature condition holds uniformly and α may be set to one without loss of generality.
proof idea
The proof is a one-line wrapper that applies the one_rpow lemma from the standard library.
why it matters
This supplies the trivial base case needed for the rpow operations that appear in the coordinate-rescaling step of the WLOG alpha equals one proposition. The step aligns with the J-uniqueness result (T5) and the Recognition Composition Law that underpins the forcing chain. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.