powerMap_pos
plain-language theorem explainer
The power map on positive reals, defined by raising to any real exponent α, preserves positivity. Algebraists constructing morphisms in the CostAlg and CostAlg⁺ categories cite this to keep images inside the positive cone. The proof is a one-line wrapper that unfolds the definition and applies the standard real exponentiation positivity lemma.
Claim. For every real number α and every x > 0, the power map satisfies 0 < x^α.
background
In the RecognitionCategory module the power map is the order-preserving map x ↦ x^α on positive reals and serves as the generator for morphisms between cost algebras. The definition is the standard real exponentiation. The module imports CostAlgebra, whose multiplicative theorem states that J-automorphisms preserve multiplication on PosReal, and PhiRing together with OctaveAlgebra to supply the algebraic scaffolding for recognition structures. The local setting is the category whose objects are cost algebras equipped with a κ parameter and whose morphisms are classified by exponents satisfying linear relations on those parameters.
proof idea
The proof is a one-line wrapper: it unfolds the definition of powerMap to ordinary real exponentiation and invokes the library lemma Real.rpow_pos_of_pos on the hypothesis 0 < x.
why it matters
This result supplies the positivity needed to define the structures CostAlgHomKappa and CostAlgPlusHom, which classify morphisms in the paper-facing CostAlg category as power maps with α κ₂ = ± κ₁ (or the positive-exponent variant). It therefore anchors the order-preserving part of the Recognition algebra and connects to the J-cost and phi-ladder constructions imported from CostAlgebra and PhiRing. No open scaffolding questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.