logicNat_isNNO
plain-language theorem explainer
LogicNat equipped with identity and step satisfies the Lawvere natural-number object universal property for pointed endomaps. Categorical foundations researchers and Recognition Science workers cite it to show that the Law of Logic forces an initial iteration object without external number presuppositions. The definition supplies the recursor directly from logicNatFold and discharges the zero, step, and uniqueness axioms by reflexivity plus induction on the inductive constructors.
Claim. The inductive type LogicNat with constructors identity (zero element) and step (successor) forms a Lawvere natural-number object: for any type X, element x : X and endomorphism f : X → X there exists a unique map h : LogicNat → X such that h(identity) = x and h(step(n)) = f(h(n)) for all n.
background
The module NaturalNumberObject characterizes the forced arithmetic via the Lawvere natural-number object: a triple (N, z, s) is an NNO precisely when every pointed endomap (X, x, f) admits a unique mediating map h satisfying the two recursion equations. This is the categorical statement that N is the initial algebra for the endofunctor X ↦ X with a chosen point. LogicNat is the inductive type whose constructors identity and step mirror the orbit {1, γ, γ², …} generated by the multiplicative generator of the Law of Logic, as introduced in ArithmeticFromLogic. The structure IsNaturalNumberObject encodes the recursor together with its zero, step and uniqueness axioms. Upstream, ArithmeticOf.logicNatFold implements the recursor by folding the supplied algebra over the LogicNat constructors.
proof idea
The definition populates the four fields of IsNaturalNumberObject. The recursor is set to ArithmeticOf.logicNatFold applied to the triple (X, x, f). The recursor_zero and recursor_step cases hold by reflexivity. The recursor_unique case proceeds by induction on n: the identity constructor case applies the supplied zero hypothesis directly, while the step constructor case rewrites via the step hypothesis, substitutes the inductive hypothesis, and closes by the definition of logicNatFold.
why it matters
This supplies the base NNO instance that downstream results transport to every realization orbit (realizationOrbit_equiv_logicNat) and to the Tick type (tick_orbit_eq_logicNat). It completes the Lawvere characterization step inside the Universal Forcing chain, establishing that every Law-of-Logic realization carries the identical iteration object up to unique isomorphism, including the discrete Boolean realization whose carrier collapses. The result anchors the claim that time-as-orbit is independent of the particular realization chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.