initialObject
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of the initial object up to isomorphism.
- Does not construct explicit morphisms beyond the identity map on positive reals.
- Does not apply to cost algebras that fail calibration to J.
Lean usage
noncomputable def morphismToC (C : RecAlgObj) (hC : C.cost = J) : RecAlgHom initialObject C := initial_morphism_exists C hCformal statement (Lean)
92noncomputable def initialObject : RecAlgObj := canonicalCostAlgebra
proof body
Definition body.
93
94/-- From the initial object to any calibrated object,
95 there exists a morphism (the identity-on-ℝ₊ map, when `C.cost = J`). -/