Hom
plain-language theorem explainer
The Hom structure encodes maps between Peano algebras that send zero to zero and commute with the successor operation. Researchers deriving arithmetic from logic realizations or proving uniqueness of initial objects in Recognition Science cite it when constructing lifts. It is introduced as a plain record with three fields and no proof obligations.
Claim. A homomorphism between Peano algebras $A$ and $B$ is a function $f: A.carrier → B.carrier$ satisfying $f(A.zero) = B.zero$ and $f(A.step(x)) = B.step(f(x))$ for all $x$.
background
PeanoObject is the structure with a carrier type, zero element, and successor map step; this module extracts arithmetic from an abstract Law-of-Logic realization. The local setting emphasizes initiality: once a realization supplies identity and step data, the generated Peano algebra is initial, yielding unique isomorphisms. Upstream, the Identity definition from LogicAsFunctionalEquation enforces zero comparison cost for self-equality, while the step operation from CellularAutomata supplies the successor rule used in the preservation axioms.
proof idea
Direct record definition declaring the three fields toFun, map_zero, and map_step. No lemmas or tactics are invoked; the structure simply packages the carrier map together with the two preservation conditions.
why it matters
Hom supplies the morphisms required to formulate IsInitial and the unique lift in equivOfInitial and logicNatLift. It implements the initiality mechanism behind Universal Forcing, where arithmetic is extracted from the logic functional equation. The definition feeds composition and identity homomorphisms that close the category of Peano objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.