Epoch

formal source

  44instance : DecidableRel (· < · : Tick → Tick → Prop) := fun a b => Nat.decLt a.index b.index
  45
  46/-- A ledger epoch: one complete 8-tick cycle. -/
  47structure Epoch where
  48  start : Tick
  49  deriving DecidableEq
  50
  51/-- The duration of one epoch is exactly 8 ticks (2^D for D = 3). -/
  52def epoch_length : ℕ := DimensionForcing.eight_tick
  53
  54theorem epoch_length_eq : epoch_length = 8 := rfl
  55
  56/-- The tick within an epoch (0 through 7). -/
  57def tick_within_epoch (t : Tick) : Fin 8 :=
  58  ⟨t.index % 8, Nat.mod_lt _ (by norm_num)⟩
  59
  60/-! ## Ledger State and Temporal Progression -/
  61
  62/-- A ledger state at a given tick. The state space is indexed by ticks,
  63    not by a continuous time parameter. -/
  64structure LedgerSnapshot where
  65  tick : Tick
  66  defect : ℝ
  67  defect_nonneg : 0 ≤ defect
  68
  69/-- Temporal ordering: snapshot A is before snapshot B iff its tick index is smaller. -/
  70def before (a b : LedgerSnapshot) : Prop := a.tick.index < b.tick.index
  71
  72instance : DecidableRel before := fun a b => Nat.decLt a.tick.index b.tick.index
  73
  74/-! ## Arrow of Time: Defect Monotonicity -/
  75
  76/-- **Core Principle**: Within a single epoch, the defect is non-increasing.
  77    Recognition events reduce defect (move toward the cost minimum).