logicNat_isNNO

formal source

  83/-! ## `LogicNat` is a natural-number object -/
  84
  85/-- `LogicNat` with `identity` and `step` is a Lawvere natural-number object. -/
  86def logicNat_isNNO :
  87    IsNaturalNumberObject (N := LogicNat) LogicNat.identity LogicNat.step where
  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)) =