CostAlgPlusObj
plain-language theorem explainer
Objects of the positive cost algebra are pairs consisting of a positive real parameter κ together with the associated cost function F_κ(x) = (x^κ + x^{-κ})/2 - 1. Category theorists and Recognition Science researchers cite this when building the order-preserving morphisms of CostAlg⁺. The definition is a direct one-line wrapper around the costFamily construction that excludes the negative branch to preserve monotonicity.
Claim. An object of the positive cost algebra consists of a real number κ > 0 equipped with the cost function F_κ(x) = ½(x^κ + x^{-κ}) - 1 for x > 0.
background
The Recognition Science framework derives costs from the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The costFamily supplies the explicit one-parameter family F_κ(x) = ½(x^κ + x^{-κ}) - 1 that solves the calibrated d'Alembert law on positive reals before imposing κ = 1. CostAlg⁺ restricts to the positive-κ branch because the negative branch reverses order, as stated in the module documentation.
proof idea
The structure is defined by a one-line wrapper that applies the costFamily function to the supplied positive parameter κ.
why it matters
This definition supplies the objects of CostAlg⁺ whose morphisms are the positive exponents α satisfying α κ₂ = κ₁. It implements the paper's order-preserving morphism classification for the cost category and feeds directly into CostAlgPlusHom. The construction aligns with T5 J-uniqueness and the calibrated d'Alembert law before the canonical κ = 1 case recovers the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.