logicNat_isNNO

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 ...