RecAlgObj
plain-language theorem explainer
RecAlgObj aliases the CostAlgebraData structure to serve as the object type in the recognition algebra category. Category theorists in Recognition Science cite it when building morphisms or initial objects from cost bundles. The declaration is a direct one-line abbreviation with no added proof obligations.
Claim. Objects of the recognition algebra category are cost algebra data structures, each consisting of a cost function $c : (0,∞) → ℝ$ on positive reals that satisfies the recognition composition law together with normalization $c(1) = 0$ and an involution preserving the cost.
background
CostAlgebraData is the fundamental algebraic object of Recognition Science: its carrier is the positive reals under multiplication, equipped with a cost function satisfying the recognition composition law, identity element 1 with cost zero, and involution $x ↦ 1/x$ that preserves cost. Upstream definitions supply concrete cost functions, including the one induced by a multiplicative recognizer via its comparator and the J-cost of a recognition event. The module Algebra.RecognitionCategory uses this structure to define a category whose objects are precisely these bundles, with morphisms given by cost-preserving maps.
proof idea
This declaration is a one-line abbreviation that directly aliases CostAlgebraData.
why it matters
RecAlgObj supplies the objects for the recognition category certificate, which confirms that the category laws hold, that an initial object exists (the canonical J), and that morphisms from the initial object reach any calibrated cost algebra. It feeds directly into initialObject, initial_morphism_exists, LayerSysPlusObj, and the composition operations recAlg_comp and recAlg_comp_assoc, anchoring the algebraic layer of Recognition Science to the J-uniqueness and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.