tick_isNNO

formal source

  90/-- **Tick is a Lawvere natural-number object.** Together with `tickZero`
  91and `tickSucc`, the `Tick` type satisfies the universal property of the
  92natural-number object: primitive recursion exists and is unique. -/
  93def tick_isNNO :
  94    IsNaturalNumberObject (N := Tick) tickZero tickSucc where
  95  recursor := fun {X} x f => tickRecursor x f
  96  recursor_zero := fun {X} x f => tickRecursor_zero x f
  97  recursor_step := fun {X} x f t => tickRecursor_succ x f t
  98  recursor_unique := by
  99    intro X x f h hz hs t
 100    -- Reduce to induction on t.index.
 101    suffices hgen : ∀ n : Nat, h ⟨n⟩ = tickRecursor x f ⟨n⟩ by
 102      have := hgen t.index
 103      cases t
 104      exact this
 105    intro n
 106    induction n with
 107    | zero => exact hz
 108    | succ n ih =>
 109        have hstep : h ⟨n + 1⟩ = h (tickSucc ⟨n⟩) := rfl
 110        rw [hstep, hs ⟨n⟩, ih]
 111        rfl
 112
 113/-! ## Time IS the orbit (Lawvere identification) -/
 114
 115/-- **Time is the orbit.** The `Tick` type is canonically equivalent, as a
 116natural-number object, to `LogicNat`. The temporal iteration of recognition
 117and the orbit construction in `ArithmeticFromLogic` deliver the same
 118iteration object up to unique isomorphism. -/
 119noncomputable def tick_orbit_eq_logicNat : Tick ≃ LogicNat :=
 120  IsNaturalNumberObject.equiv tick_isNNO logicNat_isNNO
 121
 122/-- The Lawvere equivalence sends `tickZero` to `LogicNat.identity`. -/
 123theorem tick_orbit_eq_logicNat_zero :