tickRecursor_succ

formal source

  84@[simp] theorem tickRecursor_zero {X : Type u} (x : X) (f : X → X) :
  85    tickRecursor x f tickZero = x := rfl
  86
  87@[simp] theorem tickRecursor_succ {X : Type u} (x : X) (f : X → X) (t : Tick) :
  88    tickRecursor x f (tickSucc t) = f (tickRecursor x f t) := rfl
  89
  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