comp
plain-language theorem explainer
Composition of homomorphisms between Peano algebras is defined by composing their underlying functions while preserving zero and successor maps. Researchers formalizing initiality or Universal Forcing in Recognition Science cite this when building the category of Peano objects. The definition is a direct record construction that verifies the homomorphism conditions by rewriting with the component maps and function composition.
Claim. Let $A$, $B$, $C$ be Peano algebras. Given homomorphisms $g: B → C$ and $f: A → B$, the composite $g ∘ f: A → C$ is the homomorphism whose underlying function is the ordinary composition of the underlying functions of $g$ and $f$.
background
PeanoObject is a structure consisting of a carrier type together with a distinguished zero element and a successor map. Hom is the structure of maps between two PeanoObjects that send zero to zero and commute with successor. The module extracts arithmetic from an abstract Law-of-Logic realization by exhibiting the initial Peano algebra generated by any such data; initiality supplies uniqueness up to unique isomorphism and thereby the mechanism of Universal Forcing.
proof idea
The definition builds a Hom record whose toFun field is ordinary function composition. The map_zero and map_step fields are filled by rewriting with the corresponding preservation properties of the two input homomorphisms together with the definition of function composition.
why it matters
The definition equips the collection of PeanoObjects with categorical composition, which is required for the initiality argument that drives Universal Forcing. It is invoked downstream in proofs of J-action convexity on admissible paths and of energy conservation along Newtonian trajectories. The construction is the direct analogue of the composition operation already defined for J-automorphisms in CostAlgebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.