Hom
plain-language theorem explainer
This structure defines homomorphisms of Peano algebras: maps between carriers that send zero to zero and commute with the step operation. Workers on initiality of arithmetic objects or uniqueness of LogicRealization embeddings cite it when constructing the category whose initial object yields forced natural numbers. The definition consists of a carrier map plus the two preservation axioms; no further proof is required.
Claim. A homomorphism $f: A.carrier → B.carrier$ between Peano algebras $A$ and $B$ satisfies $f(A.zero) = B.zero$ and $f(A.step(x)) = B.step(f(x))$ for every $x$.
background
PeanoObject is the structure consisting of a carrier type together with a distinguished zero element and a successor map step. The module ArithmeticOf extracts concrete arithmetic from any LogicRealization by taking the initial Peano algebra generated by that realization's identity and step data. Upstream, LogicAsFunctionalEquation.Identity encodes the zero-cost self-comparison that seeds the functional equation whose solutions force the Peano structure.
proof idea
Structure definition; the three fields toFun, map_zero and map_step are introduced directly with no tactics or lemmas applied.
why it matters
Hom supplies the morphisms for the category of Peano algebras whose initial objects are shown unique up to unique isomorphism in IsInitial and equivOfInitial. This uniqueness is the mechanism that converts any LogicRealization into a single arithmetic object, closing the step from LogicAsFunctionalEquation to the forced natural numbers used downstream in logicNatLift and realizationLift. It therefore sits inside the initiality argument that realizes T0–T8 forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.