initial_morphism_exists
plain-language theorem explainer
The declaration constructs a morphism in the RecAlg category from the canonical J-cost object to any other object C whose cost function equals J. Algebraists formalizing initiality properties for cost algebras in Recognition Science reference this to confirm the universal mapping property. The construction explicitly supplies the identity map on positive reals and verifies the required axioms by congruence on the cost-equality hypothesis.
Claim. For any cost algebra data bundle $C$ such that the cost function of $C$ equals $J$, there exists a cost morphism from the initial object (the canonical $J$-algebra) to $C$.
background
RecAlgObj stands for cost algebra data bundles that package a cost function with the Recognition Composition Law, normalization at one, symmetry, and non-negativity. RecAlgHom stands for cost morphisms, which are maps between such bundles that preserve the cost function and respect multiplication on positive reals. The initialObject is defined as canonicalCostAlgebra, the structure whose cost component is exactly the function $J$ satisfying the calibrated d'Alembert relation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$.
proof idea
The definition receives an object $C$ and a hypothesis that its cost equals $J$. It assembles a CostMorphism record whose underlying map is the identity on positive reals. Multiplicativity holds by reflexivity; cost preservation is obtained by congruence on the hypothesis followed by simplification against the definitions of initialObject and canonicalCostAlgebra.
why it matters
This definition realizes the initiality of the canonical $J$-cost algebra inside the Recognition Algebra category, directly discharging the universal property recorded in the doc-comment for initialObject. It supports the J-uniqueness step (T5) of the forcing chain by guaranteeing a structure-preserving map from the canonical cost to any other calibrated object. No downstream applications are recorded, so its role in later phi-ladder or octave constructions remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.