rpow_inv_hom'
plain-language theorem explainer
The identity states that for real α and positive real x, (x^{-1})^α equals the reciprocal of x^α. It is cited in arguments that normalize the curvature parameter α to 1 inside the calibrated cost family F_α. The proof is a direct term reduction that substitutes the exponential definition of real powers, applies the log-of-inverse rule, and cancels the resulting negation.
Claim. For any real number α and any x > 0, (x^{-1})^α = (x^α)^{-1}.
background
The module establishes the WLOG α = 1 proposition for the cost functional. After the Calibration axiom forces c = 2α², the family is written F_α(x) = (1/α²)(cosh(α ln x) − 1), which is equivalently (1/α²) J(x^α) with J(y) = (y + y^{-1})/2 − 1. The map x ↦ x^α is a group automorphism of the positive reals under multiplication, so α merely reparametrizes the coordinate while preserving the unit-curvature condition G''(0) = 1. The upstream Calibration axiom from CostAxioms states that the second derivative at the origin in log coordinates equals 1, normalizing the curvature of any admissible cost functional.
proof idea
The term proof substitutes the exponential definition of real exponentiation twice (once for the base x^{-1} and once for the base x), replaces log(x^{-1}) by its negation, distributes the outer negation through the product, and recognizes that exp(−z) is the reciprocal of exp(z).
why it matters
The lemma confirms that the rescaling automorphism φ_α preserves inverses, which is required to transport the J-cost expression back to itself after the coordinate change. It therefore closes one algebraic step in the module's argument that the calibrated family reduces to the standard J without loss of generality. The result sits inside the forcing chain that isolates a unique cost functional once the curvature is fixed at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.