powerMap
plain-language theorem explainer
The power map is the function sending each real x to x raised to alpha. Researchers formalizing morphisms in the CostAlg category cite this definition when classifying order-preserving maps that scale the kappa parameter. The definition is a direct noncomputable abbreviation of real exponentiation.
Claim. The map $xmapsto x^alpha$ for real numbers $alpha$ and $x$, used on positive $x$ to preserve order and positivity.
background
The RecognitionCategory module defines a category whose objects are cost algebras parameterized by a real kappa and whose morphisms are power maps. This definition supplies the concrete map used to construct CostAlgHomKappa and CostAlgPlusHom structures.
proof idea
This is a one-line definition that directly applies the real exponentiation operator from Mathlib.
why it matters
This definition supplies the maps for CostAlgHomKappa, where alpha satisfies alpha times kappa2 equals plus or minus kappa1, and for CostAlgPlusHom with positive alpha. It enables costFamily_comp_powerMap showing that composition multiplies the parameter and powerMap_mul establishing multiplicativity on positive reals. The construction advances the algebraic layer supporting the Recognition Composition Law and the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.