costFamily_comp_powerMap
plain-language theorem explainer
The theorem states that the cost family F_κ composed with the power map x^α equals the cost family with scaled parameter ακ evaluated at x, for positive x. Algebraists working on RecognitionCategory morphisms would cite this when verifying composition in the CostAlg category. The proof is a short term-mode reduction that unfolds the explicit formulas and applies the real exponent multiplication identity twice.
Claim. For real numbers $κ, α$ and positive real $x > 0$, $F_κ(x^α) = F_{α κ}(x)$, where $F_κ(y) := (y^κ + y^{-κ})/2 - 1$.
background
The RecognitionCategory module builds the algebraic structure for cost functions in Recognition Science. costFamily supplies the explicit one-parameter family $F_κ(x) = ½(x^κ + x^{-κ}) - 1$ on positive reals, the full continuous solution family to the calibrated d'Alembert law before fixing κ = 1. powerMap is the order-preserving map $x ↦ x^α$ on positive reals.
proof idea
The proof unfolds costFamily and powerMap to expose the real-power expressions. It rewrites using the real exponent multiplication rule (x^α)^κ = x^(α κ) and (x^α)^{-κ} = x^(-α κ), then applies mul_neg to align the signs.
why it matters
This result supplies the composition rule used to define morphisms in CostAlgHomKappa (where α κ₂ = ± κ₁) and CostAlgPlusHom (where α κ₂ = κ₁). It fills the algebraic step required to classify order-preserving morphisms in the cost category, consistent with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.