PeanoObject
plain-language theorem explainer
Peano algebras supply the algebraic carrier for natural-number arithmetic extracted from logic realizations. A mathematician working on initiality or universal forcing would cite this definition when building the initial object in the category of such algebras. The structure is introduced directly as a record type with three fields and no proof obligations.
Claim. A Peano algebra is a triple $(C, 0, s)$ consisting of a type $C$, a distinguished element $0$ in $C$, and a successor map $s: C → C$.
background
The module extracts arithmetic from an abstract Law-of-Logic realization. Once a realization supplies identity and step data, the forced arithmetic object is the initial Peano algebra generated by that data. Initial objects are unique up to unique isomorphism; this supplies the mechanism behind Universal Forcing.
proof idea
The declaration is a structure definition with no proof body. It directly records the three fields required for a Peano algebra and is referenced by sibling definitions of homomorphisms and initiality.
why it matters
This definition is the base type for the ArithmeticOf structure that represents the arithmetic object forced by any Law-of-Logic realization. It feeds the downstream constructions of Hom, id, comp, IsInitial, and equivOfInitial, which establish uniqueness up to isomorphism. In the Recognition framework the construction realizes the passage from logic data to arithmetic on the phi-ladder and supports the eight-tick octave and spatial-dimension forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.