Pith. sign in
module module high

IndisputableMonolith.Foundation.ArithmeticOf

show as:
view Lean formalization →

Defines Peano algebras (a carrier with zero and successor) and the ArithmeticOf package used throughout Universal Forcing. Establishes the initial-object interface: morphisms, identity, composition, and uniqueness of the fold out of the logic-native naturals. Downstream forcing theorems cite this module as the common arithmetic target that any Law-of-Logic realization must hit.

claimA Peano algebra is a triple $(A, 0_A, S_A)$ with $0_A \in A$ and $S_A : A \to A$. Morphisms preserve zero and successor. $\mathrm{ArithmeticOf}$ packages such an algebra together with the initiality data: the unique fold $F : \mathbb{N}_{\mathrm{logic}} \to A$ from the logic-native naturals, uniqueness of that fold, and the surface presentation used by Universal Forcing.

background

Universal Forcing claims that every realization of the Law of Logic forces the same arithmetic object up to unique isomorphism. The common target is a Peano algebra: a type equipped with a distinguished zero and a step (successor) map. Morphisms are zero-and-successor-preserving maps; initiality means there is a unique morphism out of a designated source into any other Peano algebra.

LogicRealization supplies the setting-independent interface into which continuous, discrete, or categorical Law-of-Logic presentations are mapped. ArithmeticFromLogic builds the arithmetic side of that interface. This module names the Peano surface itself: the carrier, the hom-sets, identity and composition, the IsInitial predicate, and the concrete logic-native natural object together with its fold and uniqueness lemmas.

The sibling surface includes PeanoObject, hom-sets, identity and composition, IsInitial, the ArithmeticOf package, a PeanoSurface presentation, and the logic-native natural with its fold, lift, uniqueness, and initiality facts.

proof idea

Definition and interface module rather than a single deep theorem. It introduces the Peano-algebra structure, the category-like data (identity, composition), and the initiality predicate. The logic-native natural is exhibited as a Peano object; fold and lift maps are constructed; uniqueness of the mediating map is recorded; initiality of that object is stated. Downstream modules import this surface and apply the initiality package rather than re-proving Peano recursion.

why it matters in Recognition Science

This is the named arithmetic target of the Universal Forcing program. UniversalForcing states that any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects precisely because those objects are initial Peano algebras in the sense fixed here. DistinctionToArithmetic welds distinction-side analysis to this package: it maps a distinction to its forced ArithmeticOf and proves canonicity, matching the program register entry on unification from distinction. CanonicalForcing likewise imports the surface as the forced object. Without a single Peano/ArithmeticOf interface, the equivalence-of-realizations claim would have no common codomain.

scope and limits

used by (3)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (22)