powerMap_mul
plain-language theorem explainer
The power map x ↦ x^α on positive reals satisfies (xy)^α = x^α y^α for x, y > 0. Category theorists building CostAlg morphisms in Recognition Science cite this to confirm power maps act as structure-preserving homomorphisms. The proof is a direct term reduction that unfolds the definition and applies the standard real multiplication rule for exponents.
Claim. For any real number α and positive reals x, y, the map z ↦ z^α obeys (x y)^α = x^α y^α.
background
In RecognitionCategory the power map is defined by powerMap α x := x^α. It supplies the concrete morphisms for the CostAlg category whose objects carry a real parameter κ and whose arrows are power maps obeying the intertwining condition α κ₂ = κ₁ (or its negative). The module sits atop CostAlgebra and PhiRing, supplying the algebraic layer that lets recognition costs compose under the Recognition Composition Law.
proof idea
Term-mode proof: unfold powerMap to obtain the raw exponentiation, then rewrite with Real.mul_rpow using the two positivity hypotheses to justify the product rule for real powers.
why it matters
The result is required by the downstream structures CostAlgHomKappa and CostAlgPlusHom, which classify all morphisms in the category exactly as power maps satisfying the κ-intertwining relation. It therefore supplies the algebraic closure needed for the Recognition Science category that encodes the J-cost and phi-ladder constructions. No open scaffolding remains; the property is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.