`Chain`

definition

show as: view math explainer →

module: IndisputableMonolith.Chain
domain: Chain
line: 11 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Chain on GitHub at line 11.

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

   8  R : U → U → Prop
   9
  10/-- Chain structure with minimal axioms for standalone compilation -/
  11structure Chain (M : RecognitionStructure) where
  12  n : Nat
  13  f : Fin (n+1) → M.U
  14  ok : ∀ i : Fin n, M.R (f i.castSucc) (f i.succ)
  15
  16namespace Chain
  17
  18variable {M : RecognitionStructure} (ch : Chain M)
  19
  20def head : M.U := by
  21  have hpos : 0 < ch.n + 1 := Nat.succ_pos _
  22  exact ch.f ⟨0, hpos⟩
  23
  24def last : M.U := by
  25  have hlt : ch.n < ch.n + 1 := Nat.lt_succ_self _
  26  exact ch.f ⟨ch.n, hlt⟩
  27
  28end Chain
  29
  30class AtomicTick (M : RecognitionStructure) where
  31  postedAt : Nat → M.U → Prop
  32  unique_post : ∀ t : Nat, ∃! u : M.U, postedAt t u
  33
  34structure Ledger (M : RecognitionStructure) where
  35  debit : M.U → ℤ
  36  credit : M.U → ℤ
  37
  38def phi {M} (L : Ledger M) : M.U → ℤ := fun u => L.debit u - L.credit u
  39
  40def chainFlux {M} (L : Ledger M) (ch : Chain M) : ℤ :=
  41  phi L (ch.last) - phi L (ch.head)

papers checked against this theorem

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