rpow_mul_hom'
plain-language theorem explainer
The real power function satisfies the homomorphism property (xy)^α = x^α y^α for α real and x, y positive. This identity is invoked to confirm that the rescaling φ_α preserves multiplication in the positive reals, which is required for the WLOG reduction to α = 1 in the cost function family. The proof is a short term-mode calculation that substitutes the exponential definition of rpow and uses the additivity of the logarithm on products.
Claim. For every real number $α$ and all positive real numbers $x, y > 0$, one has $(xy)^α = x^α · y^α$.
background
The module develops the coordinate rescaling that reduces the general calibrated cost to the canonical J-cost. CostAlpha α x is defined via CostAlphaLog α (log x), which equals (1/α²)(cosh(α ln x) - 1). The rescaling identity states that this equals (1/α²) J(x^α).
proof idea
The proof applies a sequence of rewrites: it replaces each occurrence of real power with its definition exp(α log ·) using rpow_def_of_pos, converts the product inside the logarithm to a sum via log_mul, distributes the multiplication by α, and reassembles the result as a product of exponentials via exp_add.
why it matters
This result is used directly in the proof of wlog_alpha_eq_one, the central theorem asserting that F_α(x) = (1/α²) J(x^α) together with the recovery at α=1 and the automorphism property. It completes the group-automorphism component of the WLOG α=1 proposition. Within Recognition Science, the identity confirms that the parameter α does not alter the underlying structure, aligning with the forcing chain from T5 J-uniqueness through T6 phi fixed point to the calibrated costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.