`SimpleStructure`

definition

show as: view math explainer →

module: IndisputableMonolith.Recognition.ModelingExamples
domain: Recognition
line: 10 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Recognition.ModelingExamples on GitHub at line 10.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

   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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.