IndisputableMonolith.Recognition.Cycle3

   1import Mathlib
   2import IndisputableMonolith.Recognition
   3
   4namespace IndisputableMonolith
   5namespace Cycle3
   6
   7open Recognition
   8
   9def M : RecognitionStructure :=
  10  { U := Fin 3
  11  , R := fun i j => j = ⟨(i.val + 1) % 3, by
  12      have h : (i.val + 1) % 3 < 3 := Nat.mod_lt _ (by decide : 0 < 3)
  13      simpa using h⟩ }
  14
  15def L : Ledger M :=
  16  { debit := fun _ => 0
  17  , credit := fun _ => 0 }
  18
  19instance : Conserves L :=
  20  { conserve := by
  21      intro ch hclosed
  22      -- phi is identically 0, so flux is 0
  23      simp [chainFlux, phi, hclosed] }
  24
  25def postedAt : Nat → M.U → Prop := fun t v =>
  26  v = ⟨t % 3, by
  27    have : t % 3 < 3 := Nat.mod_lt _ (by decide : 0 < 3)
  28    simpa using this⟩
  29
  30instance : AtomicTick M :=
  31  { postedAt := postedAt
  32  , unique_post := by
  33      intro t
  34      refine ⟨⟨t % 3, ?_⟩, ?_, ?_⟩
  35      · have : t % 3 < 3 := Nat.mod_lt _ (by decide : 0 < 3)
  36        simpa using this
  37      · rfl
  38      · intro u hu
  39        simpa [postedAt] using hu }
  40
  41end Cycle3
  42end IndisputableMonolith
  43