`TimeAsOrbitCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.TimeAsOrbit
domain: Foundation
line: 157 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.TimeAsOrbit on GitHub at line 157.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 154
 155The temporal sequence is canonically the natural-number object forced by
 156recognition. -/
 157structure TimeAsOrbitCert where
 158  tick_is_NNO : IsNaturalNumberObject (N := Tick) tickZero tickSucc
 159  tick_equiv_logicNat : Tick ≃ LogicNat
 160  tick_equiv_logicNat_zero : tick_equiv_logicNat tickZero = LogicNat.identity
 161  tick_equiv_logicNat_succ :
 162    ∀ t : Tick, tick_equiv_logicNat (tickSucc t) =
 163      LogicNat.step (tick_equiv_logicNat t)
 164  recognition_advances_succ :
 165    ∀ step : RecognitionStep, step.output.tick = tickSucc step.input.tick
 166
 167noncomputable def timeAsOrbitCert : TimeAsOrbitCert where
 168  tick_is_NNO := tick_isNNO
 169  tick_equiv_logicNat := tick_orbit_eq_logicNat
 170  tick_equiv_logicNat_zero := tick_orbit_eq_logicNat_zero
 171  tick_equiv_logicNat_succ := tick_orbit_eq_logicNat_succ
 172  recognition_advances_succ := recognitionStep_iterates_succ
 173
 174theorem timeAsOrbitCert_inhabited : Nonempty TimeAsOrbitCert :=
 175  ⟨timeAsOrbitCert⟩
 176
 177/-! ## Summary
 178
 179This module supplies the bridge:
 180
 181```
 182RecognitionStep advances Tick by one
 183       ↓
 184Tick is a natural-number object
 185       ↓
 186Tick ≃ LogicNat (Lawvere universal property)
 187       ↓

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.