IndisputableMonolith.Foundation.TimeAsOrbit

   1import Mathlib
   2import IndisputableMonolith.Foundation.TimeEmergence
   3import IndisputableMonolith.Foundation.ArithmeticFromLogic
   4import IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject
   5
   6/-!
   7# Time as Forced Orbit
   8
   9This module makes the explicit claim:
  10
  11> The temporal sequence (`Tick`) is canonically the natural-number object
  12> forced by recognition.
  13
  14Concretely, `Tick` is a Lawvere natural-number object under successor
  15`fun t => ⟨t.index + 1⟩`. By the universal property of natural-number
  16objects (proved in `UniversalForcing.NaturalNumberObject`), `Tick` is
  17canonically equivalent to `LogicNat`, the orbit construction of
  18`ArithmeticFromLogic`. The orbit of recognition and the tick count of
  19the ledger are the same iteration object up to canonical isomorphism.
  20
  21This closes the time-as-orbit frontier: time is not added to physics; it
  22is the canonical iteration object of recognition.
  23
  24## Honest scope
  25
  26This module proves time as a *combinatorial* iteration object. It does
  27not derive metric time, the 8-tick cycle's `D=3` origin (already in
  28`Foundation.DimensionForcing`), or the arrow of time as Berry-phase
  29monotonicity (Layer 8 of the cosmological forcing chain, separate work).
  30What is proved here is the structural identification: recognition steps
  31generate the natural-number object, and that object is `Tick`.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Foundation
  36namespace TimeAsOrbit
  37
  38open TimeEmergence
  39open ArithmeticFromLogic
  40open UniversalForcing
  41
  42universe u
  43
  44/-! ## The Tick Successor -/
  45
  46/-- The canonical successor on `Tick`: advance the index by one. -/
  47def tickSucc (t : Tick) : Tick := ⟨t.index + 1⟩
  48
  49@[simp] theorem tickSucc_index (t : Tick) : (tickSucc t).index = t.index + 1 := rfl
  50
  51/-- The canonical zero tick. -/
  52def tickZero : Tick := ⟨0⟩
  53
  54@[simp] theorem tickZero_index : tickZero.index = 0 := rfl
  55
  56/-! ## Tick is canonically the natural numbers -/
  57
  58/-- The canonical equivalence between `Tick` and `Nat` via the index. -/
  59def tickEquivNat : Tick ≃ Nat where
  60  toFun t := t.index
  61  invFun n := ⟨n⟩
  62  left_inv := by intro t; cases t; rfl
  63  right_inv := by intro n; rfl
  64
  65@[simp] theorem tickEquivNat_apply (t : Tick) : tickEquivNat t = t.index := rfl
  66@[simp] theorem tickEquivNat_symm_apply (n : Nat) :
  67    tickEquivNat.symm n = ⟨n⟩ := rfl
  68
  69@[simp] theorem tickEquivNat_zero : tickEquivNat tickZero = 0 := rfl
  70
  71@[simp] theorem tickEquivNat_succ (t : Tick) :
  72    tickEquivNat (tickSucc t) = (tickEquivNat t) + 1 := rfl
  73
  74/-- The canonical equivalence `Tick ≃ LogicNat` via `Nat`. -/
  75def tickEquivLogicNat : Tick ≃ LogicNat :=
  76  tickEquivNat.trans LogicNat.equivNat.symm
  77
  78/-! ## Tick is a natural-number object -/
  79
  80/-- Recursor on `Tick`: iterate `f` from `x` exactly `t.index` times. -/
  81def tickRecursor {X : Type u} (x : X) (f : X → X) (t : Tick) : X :=
  82  Nat.rec x (fun _ acc => f acc) t.index
  83
  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
 118iteration object up to unique isomorphism. -/
 119noncomputable def tick_orbit_eq_logicNat : Tick ≃ LogicNat :=
 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.**
 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       ↓
 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
 198end IndisputableMonolith
 199