costAlgPlus_initiality
plain-language theorem explainer
The calibrated object with parameter κ=1 is initial in the category CostAlg⁺ of positive-parameter cost families. Researchers formalizing the Recognition Science cost structures would cite this result to fix the base case for all order-preserving cost morphisms. The proof is a term-mode construction that directly supplies the canonical morphism and invokes its uniqueness lemma.
Claim. In the category whose objects are pairs $(κ, F_κ)$ with $κ > 0$ and $F_κ$ the cost family, and whose morphisms from $(κ_1, F_{κ_1})$ to $(κ_2, F_{κ_2})$ are positive reals $α > 0$ satisfying $α κ_2 = κ_1$, the object with $κ = 1$ is initial: for every object $C$ there exists a unique morphism from the $κ=1$ object to $C$.
background
Objects of CostAlg⁺ are positive reals κ > 0 equipped with the cost function costFamily κ. Morphisms are positive exponents α satisfying the intertwining relation α κ₂ = κ₁, which encodes the order-preserving branch of cost algebras. The initial object is the calibrated case κ = 1. This construction sits inside the RecognitionCategory module and rests on the upstream definition that fixes κ = 1 together with the positivity constraints in the object and morphism structures.
proof idea
The proof is a term-mode one-line wrapper. It refines the pair consisting of the canonical morphism supplied by CostAlgPlusHom.fromInitial C and the uniqueness statement CostAlgPlusHom.fromInitial_unique C g, then discharges the universal quantifier by exact application of that uniqueness lemma.
why it matters
This declaration is the paper's crown-jewel theorem that the calibrated κ=1 object is initial in CostAlg⁺. It anchors the cost-algebra layer of the Recognition Science framework and supplies the unique base case needed for the forcing chain and the J-cost constructions. No downstream uses are recorded in the current graph, leaving open how this initiality will be invoked in later layer-category or linked-system results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.