initialObject
plain-language theorem explainer
The canonical cost algebra J is defined as the initial object in the RecAlg category of cost algebras. Researchers formalizing Recognition Science algebraic structures cite this to fix the universal source for morphisms to any calibrated cost algebra C. The declaration is a direct one-line alias to the pre-built canonicalCostAlgebra bundle.
Claim. The initial object of the category of recognition algebras is the canonical cost algebra $J$.
background
Objects in RecAlg are cost algebra data bundles (RecAlgObj := CostAlgebraData). Each bundle packages a cost function with proofs that the function obeys the Recognition Composition Law, equals zero at unity, is symmetric under reciprocals, and is non-negative. The upstream canonicalCostAlgebra constructs exactly this bundle by setting cost := J together with rcl := RCL_holds, normalized := J_at_one, symmetric := J_reciprocal, and nonneg := J_nonneg. This supplies the local setting in which J functions as the universal initial object.
proof idea
One-line definition that aliases initialObject directly to canonicalCostAlgebra.
why it matters
This definition supplies the initial object referenced by the downstream initial_morphism_exists, which produces the unique morphism from J to any C satisfying C.cost = J. It realizes the initial-object property for the canonical cost algebra inside the Recognition Science framework and connects to J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.