tick_orbit_eq_logicNat_zero

formal source

 120  IsNaturalNumberObject.equiv tick_isNNO logicNat_isNNO
 121
 122/-- The Lawvere equivalence sends `tickZero` to `LogicNat.identity`. -/
 123theorem tick_orbit_eq_logicNat_zero :
 124    tick_orbit_eq_logicNat tickZero = LogicNat.identity := by
 125  unfold tick_orbit_eq_logicNat IsNaturalNumberObject.equiv
 126  exact tick_isNNO.recursor_zero LogicNat.identity LogicNat.step
 127
 128/-- The Lawvere equivalence intertwines `tickSucc` with `LogicNat.step`. -/
 129theorem tick_orbit_eq_logicNat_succ (t : Tick) :
 130    tick_orbit_eq_logicNat (tickSucc t) = LogicNat.step (tick_orbit_eq_logicNat t) := by
 131  unfold tick_orbit_eq_logicNat IsNaturalNumberObject.equiv
 132  exact tick_isNNO.recursor_step LogicNat.identity LogicNat.step t
 133
 134/-! ## Recognition steps iterate the tick successor -/
 135
 136/-- A `RecognitionStep` advances the tick by one, equivalently applies
 137`tickSucc` to the input snapshot's tick. This is the bridge from the
 138ledger dynamics of `TimeEmergence` to the abstract natural-number object
 139on `Tick`. -/
 140theorem recognitionStep_iterates_succ (step : RecognitionStep) :
 141    step.output.tick = tickSucc step.input.tick := by
 142  have hadv := step.tick_advance
 143  cases hin : step.input.tick with
 144  | mk i =>
 145    cases hout : step.output.tick with
 146    | mk o =>
 147      rw [hin, hout] at hadv
 148      simp [tickSucc]
 149      exact hadv
 150
 151/-! ## Headline Certificate -/
 152
 153/-- **Time-as-Orbit Certificate.**