structure
definition
Ledger
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Chain on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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)
42
43class Conserves {M} (L : Ledger M) : Prop where
44 conserve : ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0
45
46/-- ## T2 (Atomicity): unique posting per tick implies no collision at a tick. -/
47theorem T2_atomicity {M} [AtomicTick M] :
48 ∀ t u v, AtomicTick.postedAt (M:=M) t u → AtomicTick.postedAt (M:=M) t v → u = v := by
49 intro t u v hu hv
50 rcases (AtomicTick.unique_post (M:=M) t) with ⟨w, hw, huniq⟩
51 have hu' : u = w := huniq u hu
52 have hv' : v = w := huniq v hv
53 exact hu'.trans hv'.symm
54
55theorem T3_continuity {M} (L : Ledger M) [Conserves L] :
56 ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0 := Conserves.conserve
57
58end IndisputableMonolith