recAlg_id
plain-language theorem explainer
The definition supplies the identity morphism for each object in the recognition algebra category, where objects are cost algebra data bundles and morphisms are multiplicative positivity-preserving maps on positive reals. Modelers building categorical structures for recognition science cite it when verifying that composition admits neutral elements. The definition is realized as a direct one-line wrapper that reuses the identity map already constructed in the cost morphism layer.
Claim. For every cost algebra data bundle $C$, there is an identity morphism $id_C : C → C$ given by the map $x ↦ x$ on the underlying positive reals, which preserves multiplication and positivity.
background
Objects in the recognition algebra category are cost algebra data bundles. Morphisms are cost morphisms: functions $f : ℝ₊ → ℝ₊$ that satisfy $f(xy) = f(x)f(y)$ for all positive $x,y$ and map positive inputs to positive outputs. The local setting is the construction of a category whose morphisms encode cost-preserving transformations compatible with the recognition composition law. Upstream, the cost morphism structure is defined with an explicit map field together with positivity and multiplicativity conditions, and its identity is the map that sends every positive real to itself while satisfying the two preservation axioms.
proof idea
One-line wrapper that applies the identity constructor from the cost morphism definition directly to the input object.
why it matters
This definition is invoked by the category certificate theorem to confirm that identity morphisms act as neutral elements under composition, completing the verification that the recognition algebra forms a category. It also feeds the left-neutral and right-neutral identity lemmas. In the framework it supplies the neutral element required for the recognition composition law and supports the passage from cost algebra data to the full categorical structure used in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.