timeAsOrbitCert

formal source

 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       ↓
 188Time is the canonical orbit of recognition
 189```
 190
 191The temporal iteration of the ledger and the orbit construction of
 192`ArithmeticFromLogic` are the same mathematical object up to unique
 193isomorphism. Time is not background; time is what recognition forces.
 194-/
 195
 196end TimeAsOrbit
 197end Foundation