logicNatPeano
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
XOR-and-shift over GF(2) meets Marcus's three cognitive pillars
"treelet as an algebraic register set indexed by a primitive generator polynomial"