`L`

definition

show as: view math explainer →

module: IndisputableMonolith.Recognition.Cycle3
domain: Recognition
line: 15 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Recognition.Cycle3 on GitHub at line 15.

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

  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

papers checked against this theorem

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