theorem
proved
recognitionStep_iterates_succ
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.TimeAsOrbit on GitHub at line 140.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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.**
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