id_comp
plain-language theorem explainer
The left unit law holds for composition in the monoid of J-automorphisms of the positive reals equipped with the cost function J. Algebraists formalizing the multiplicative structure of the Recognition Science cost algebra cite this result when reducing expressions that involve the identity element. The proof reduces the claim to a pointwise equality via the JAut extensionality principle and concludes by reflexivity.
Claim. Let JAut be the type of maps $f : (0,∞) → (0,∞)$ that are multiplicative, $f(xy) = f(x)f(y)$, and preserve the cost function, $J(f(x)) = J(x)$. For every such $f$, the composition of $f$ with the identity map equals $f$.
background
JAut is the subtype of maps on positive reals that are multiplicative with respect to the positive multiplication operation and satisfy the J-preservation condition. The comp operation on JAut is the pointwise composition of two such maps, which inherits multiplicativity from each factor. The id element is the identity map on positive reals, which satisfies both the multiplicative and J-preservation axioms by direct verification.
proof idea
The proof is a one-line wrapper that applies the JAut.ext lemma to convert the equality of automorphisms into a pointwise statement on positive reals. For arbitrary x the definition of comp yields (comp f id) x = f (id x). The right-hand side equals f x by the definition of id, and this identity is immediate by reflexivity.
why it matters
The result supplies the left unit law needed to treat JAut as a monoid under composition. It is invoked by the downstream theorems idAutomorphism_comp_left_toFun and idSymmetry_comp_left in the RecogGeom.Symmetry module, which lift the same neutrality statement to the larger categories of recognition automorphisms and symmetry maps. The lemma therefore closes a basic algebraic prerequisite for any further development of automorphism groups inside the cost algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.