IndisputableMonolith.Recognition.ModelingExamples

   1import Mathlib
   2import IndisputableMonolith.Recognition
   3
   4namespace IndisputableMonolith
   5namespace ModelingExamples
   6
   7open Recognition
   8
   9/-- A simple 2-vertex recognition structure with bidirectional relation. -/
  10def SimpleStructure : RecognitionStructure := {
  11  U := Bool,
  12  R := fun a b => a ≠ b
  13}
  14
  15/-- A balanced ledger on the simple structure. -/
  16def SimpleLedger : Ledger SimpleStructure := {
  17  debit := fun _ => 1,
  18  credit := fun _ => 0
  19}
  20
  21/-- The simple structure satisfies conservation on closed chains. -/
  22instance : Conserves SimpleLedger := {
  23  conserve := by
  24    intro ch hclosed
  25    simp [chainFlux, phi]
  26    -- For any closed chain, head = last, so flux = 0
  27    rw [hclosed]
  28    ring
  29}
  30
  31/-- A simple tick schedule alternating between the two vertices. -/
  32def SimpleTicks : Nat → Bool → Prop := fun t v => v = (t % 2 == 1)
  33
  34instance : AtomicTick SimpleStructure := {
  35  postedAt := SimpleTicks,
  36  unique_post := by
  37    intro t
  38    use (t % 2 == 1)
  39    constructor
  40    · rfl
  41    · intro u hu
  42      simp [SimpleTicks] at hu
  43      exact hu
  44}
  45
  46/-- Example of BoundedStep on Bool with degree 1. -/
  47instance : BoundedStep Bool 1 := {
  48  step := SimpleStructure.R,
  49  neighbors := fun b => if b then {false} else {true},
  50  step_iff_mem := by
  51    intro a b
  52    simp [SimpleStructure]
  53    cases a <;> cases b <;> simp
  54}
  55
  56end ModelingExamples
  57end IndisputableMonolith
  58