module module high

`IndisputableMonolith.Foundation.ArithmeticOf`

The module defines a Peano algebra as a type equipped with a zero element and a successor map. It supplies the common arithmetic target into which distinct Law-of-Logic realizations are mapped. Researchers working on the Universal Forcing theorem cite the module to establish that forced arithmetic objects are initial in this category. The module organizes its content around the algebra object, its homomorphisms, and initiality without containing proofs.

claimA Peano algebra is a type $P$ together with a distinguished element $0_P : P$ and a successor function $s_P : P : P$.

background

Recognition Science derives arithmetic from logic by mapping realizations into initial Peano algebras. The upstream LogicRealization module creates a setting-independent interface that accepts continuous positive ratios, discrete propositions, or categorical settings and produces a common object. ArithmeticFromLogic supplies the logical grounding that lets these mappings land in arithmetic. The present module therefore defines the arithmetic side of the interface.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Peano algebra structure required by the Universal Forcing theorem. That downstream result states that any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. The module therefore completes the arithmetic half of the first formal statement of the forcing theorem.

scope and limits

Does not realize arithmetic inside any concrete logic setting.
Does not prove existence of an initial Peano algebra.
Does not introduce induction or recursion principles.
Does not connect the algebra to the phi-ladder or physical constants.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.UniversalForcing module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.ArithmeticFromLogic module_import
IndisputableMonolith.Foundation.LogicRealization module_import

declarations in this module (22)

structure PeanoObject L23
structure Hom L31
def id L42
def comp L48
structure IsInitial L58
structure ArithmeticOf L65
structure PeanoSurface L72
def logicNatPeano L84
def logicNatFold L90
def logicNatLift L95
theorem logicNatLift_unique_fun L102
def logicNat_initial L116
def realizationPeano L123
def realizationFold L130
def realizationLift L134
theorem realizationLift_unique_fun L150
def realization_initial L189
def extracted L197
theorem extracted_peanoSurface L202
def equivOfInitial L209
def canonical L237
theorem canonical_peanoSurface L242