costFamily_neg_param
plain-language theorem explainer
The cost family satisfies F_{-κ}(x) = F_κ(x) for every real κ and x. Modelers of the CostAlg category cite this when constructing morphisms that flip the sign of the parameter via power maps. The proof is a direct unfolding of the explicit definition followed by commutativity of addition.
Claim. Let $F(κ, x) = (x^κ + x^{-κ})/2 - 1$. Then $F(-κ, x) = F(κ, x)$ for all real $κ, x$.
background
In RecognitionCategory the costFamily is the explicit one-parameter family $F_κ(x) = (x^κ + x^{-κ})/2 - 1$ that solves the calibrated d'Alembert law on positive reals before κ is fixed to 1. Objects of the CostAlg category are these families restricted to κ > 0. The module imports CostAlgebra, PhiRing, LedgerAlgebra and OctaveAlgebra to embed the family inside the larger Recognition algebra.
proof idea
Unfolds the definition of costFamily to expose the symmetric sum, then applies add_comm to interchange the two powered terms after κ is replaced by -κ.
why it matters
The result is invoked by CostAlgHomKappa, whose morphisms are power maps satisfying α κ₂ = ± κ₁. It supplies the evenness needed to represent every morphism with a positive representative of κ, closing the sign ambiguity in the category. This property is required for the Recognition Composition Law to act consistently on the full continuous solution family before reduction to the J-cost at κ = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.