initialObject
plain-language theorem explainer
The canonical cost algebra J is defined as the initial object in the RecAlg category whose objects are cost algebra data bundles. Category theorists working on recognition costs cite this to anchor the universal property of J as the starting point for morphisms to any calibrated algebra. The declaration is a direct alias to canonicalCostAlgebra.
Claim. In the category whose objects are cost algebra data bundles, the initial object is the canonical cost algebra whose cost function is $J$.
background
RecAlgObj abbreviates CostAlgebraData, the bundles that pair a cost function with proofs of the Recognition Composition Law, normalization at unity, symmetry under reciprocals, and non-negativity. canonicalCostAlgebra supplies precisely this data for the function J, which arises as the derived cost of multiplicative recognizers and as the J-cost of recognition events in observer forcing. The definition therefore sits inside the RecognitionCategory module that assembles these cost algebras into a category whose morphisms are cost-preserving maps.
proof idea
One-line wrapper that aliases canonicalCostAlgebra.
why it matters
The definition supplies the initial object required by initial_morphism_exists, which then constructs the identity-on-ℝ₊ morphism from J to any C with C.cost = J. It realizes the initial-object claim stated in the module doc-comment and connects directly to the J-uniqueness property (T5) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.