logicNat_isNNO
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not presuppose any external model of the natural numbers.
- Does not compute concrete numerical values or perform arithmetic operations.
- Does not address continuous or physical embeddings beyond orbit equivalence.
- Does not derive spatial dimensions or physical constants.
Lean usage
IsNaturalNumberObject.equiv tick_isNNO logicNat_isNNOformal statement (Lean)
86def logicNat_isNNO :
87 IsNaturalNumberObject (N := LogicNat) LogicNat.identity LogicNat.step where
proof body
Definition body.
88 recursor := fun {X} x f => ArithmeticOf.logicNatFold ⟨X, x, f⟩
89 recursor_zero := fun _ _ => rfl
90 recursor_step := fun _ _ _ => rfl
91 recursor_unique := by
92 intro X x f h hz hs n
93 induction n with
94 | identity => exact hz
95 | step n ih =>
96 calc
97 h (LogicNat.step n) = f (h n) := hs n
98 _ = f (ArithmeticOf.logicNatFold ⟨X, x, f⟩ n) := by rw [ih]
99 _ = ArithmeticOf.logicNatFold ⟨X, x, f⟩ (LogicNat.step n) := rfl
100
101/-! ## Forced arithmetic of every realization is a natural-number object -/
102
103/-- The natural-number object structure on a realization's iteration orbit.
104Provided by transport from `LogicNat` through the realization's certified
105orbit equivalence. The universe of the NNO is the carrier universe of the
106realization. -/
107noncomputable def realizationOrbit_isNNO.{u₁, v₁} (R : LogicRealization.{u₁, v₁}) :
108 IsNaturalNumberObject (N := R.Orbit) R.orbitZero R.orbitStep where
109 recursor := fun {X} x f n =>
110 @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (R.orbitEquivLogicNat n)
111 recursor_zero := fun {X} x f => by
112 show @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (R.orbitEquivLogicNat R.orbitZero) = x
113 rw [R.orbitEquiv_zero]
114 rfl
115 recursor_step := fun {X} x f n => by
116 show @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (R.orbitEquivLogicNat (R.orbitStep n)) =
117 f (@ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (R.orbitEquivLogicNat n))
118 rw [R.orbitEquiv_step]
119 rfl
120 recursor_unique := by
121 intro X x f h hz hs n
122 have hlogic_zero :
123 (h ∘ R.orbitEquivLogicNat.symm) LogicNat.zero = x := by
124 simp only [Function.comp_apply]
125 have hsymm0 : R.orbitEquivLogicNat.symm LogicNat.zero = R.orbitZero := by
126 apply R.orbitEquivLogicNat.injective
127 simp [R.orbitEquiv_zero]
128 rw [hsymm0]
129 exact hz
130 have hlogic_step : ∀ k,
131 (h ∘ R.orbitEquivLogicNat.symm) (LogicNat.step k) =
132 f ((h ∘ R.orbitEquivLogicNat.symm) k) := by
133 intro k
134 simp only [Function.comp_apply]
135 have hsymm_step :
136 R.orbitEquivLogicNat.symm (LogicNat.step k) =
137 R.orbitStep (R.orbitEquivLogicNat.symm k) := by
138 apply R.orbitEquivLogicNat.injective
139 rw [R.orbitEquiv_step]
140 simp
141 rw [hsymm_step]
142 exact hs (R.orbitEquivLogicNat.symm k)
143 have huniq :
144 ∀ k, (h ∘ R.orbitEquivLogicNat.symm) k =
145 @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ k := by
146 intro k
147 induction k with
148 | identity => exact hlogic_zero
149 | step k ih =>
150 calc
151 (h ∘ R.orbitEquivLogicNat.symm) (LogicNat.step k)
152 = f ((h ∘ R.orbitEquivLogicNat.symm) k) := hlogic_step k
153 _ = f (@ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ k) := by rw [ih]
154 _ = @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (LogicNat.step k) := rfl
155 have hh : h n = (h ∘ R.orbitEquivLogicNat.symm) (R.orbitEquivLogicNat n) := by
156 simp [Function.comp_apply]
157 rw [hh, huniq]
158
159/-- Convenience alias: the forced arithmetic of every realization is a Lawvere
160natural-number object. The forced arithmetic is by definition the realization
161orbit, so this is the same statement as `realizationOrbit_isNNO`. -/
162noncomputable def forcedArithmetic_isNNO.{u₁, v₁} (R : LogicRealization.{u₁, v₁}) :
163 IsNaturalNumberObject
164 (N := (arithmeticOf R).peano.carrier)
165 (arithmeticOf R).peano.zero
166 (arithmeticOf R).peano.step :=
167 realizationOrbit_isNNO R
168-- ... 53 more lines elided ...