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.
claimA 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 in Recognition Science
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.
scope and limits
Does not impose an induction principle on the carrier.
Does not require the carrier to be the set of natural numbers.
Does not equip the carrier with ordering or metric structure.
Does not assume the successor map is computable.
formal statement (Lean)
23structure PeanoObject where 24 carrier : Type u 25 zero : carrier 26 step : carrier → carrier 27 28namespace PeanoObject 29 30/-- Homomorphisms of Peano algebras. -/
used by (20)
From the project-wide theorem graph. These declarations reference this one in their body.