logicNatPeano
The definition equips the inductive type generated by the Law of Logic with the structure of a Peano algebra by direct field assignment. Researchers in categorical logic and universal forcing cite it as the concrete initial carrier for arithmetic extracted from any LogicRealization. The construction is a direct structure instance that pulls zero and successor directly from the inductive constructors of LogicNat.
claimLet $N$ be the inductive type with constructors $0$ (the zero-cost identity element) and $s : N → N$ (one iteration of the generator). Then $N$ forms a Peano algebra whose carrier is $N$, whose zero element is the identity constructor, and whose successor map is the successor function defined by one application of the step constructor.
background
A Peano algebra is a structure consisting of a carrier type, a zero element, and a successor map. The module extracts arithmetic from an abstract Law-of-Logic realization, where initiality supplies the invariant content: once identity and step data are given, the forced object is the initial Peano algebra generated by that data. As stated upstream, LogicNat is 'the natural numbers as forced by the Law of Logic. identity represents the zero-cost element (the multiplicative identity in the orbit). step represents one more iteration of the generator. The two-constructor structure mirrors the orbit {1, γ, γ², γ³, ...} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1.'
proof idea
The definition is a direct structure instance. It assigns the carrier field to LogicNat, the zero field to LogicNat.zero (the identity constructor), and the step field to LogicNat.succ (defined as one application of the step constructor). No lemmas or tactics are required beyond the inductive definition already established in ArithmeticFromLogic.
why it matters in Recognition Science
This supplies the concrete Peano object used to define the canonical arithmetic for any LogicRealization and to establish initiality in logicNat_initial. Downstream, canonical states that 'the realization supplies the interpretation; initiality supplies the invariant arithmetic content.' The construction realizes the initial Peano algebra forced by the Law of Logic, providing the mechanism behind Universal Forcing and feeding the Lawvere NNO in CategoricalLogicRealization.
scope and limits
- Does not derive the Peano axioms; those are theorems of the inductive structure proved separately.
- Does not depend on a concrete numerical model or physical constants.
- Does not establish uniqueness up to isomorphism; that is supplied by the initiality theorem.
- Does not address higher-order arithmetic or induction principles beyond the basic algebra structure.
formal statement (Lean)
84def logicNatPeano : PeanoObject where
85 carrier := LogicNat
proof body
Definition body.
86 zero := LogicNat.zero
87 step := LogicNat.succ
88
89/-- Fold from `LogicNat` into an arbitrary Peano object. -/