theorem
proved
nothing_cannot_recognize_itself
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Core.Recognition on GitHub at line 37.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
34/-- Re-export: Nothing cannot recognize itself. -/
35abbrev NothingCannotRecognizeItself := Recognition.NothingCannotRecognizeItself
36
37theorem nothing_cannot_recognize_itself : NothingCannotRecognizeItself :=
38 Recognition.nothing_cannot_recognize_itself
39
40/-- Re-export: Recognition structure. -/
41abbrev RecognitionStructure := Recognition.RecognitionStructure
42
43/-- Re-export: Chain of recognition steps. -/
44abbrev Chain := Recognition.Chain
45
46/-- Re-export: Ledger for double-entry. -/
47abbrev RecogLedger := Recognition.Ledger
48
49/-- Re-export: Phi (net balance) function. -/
50def phi {M : RecognitionStructure} (L : Recognition.Ledger M) : M.U → ℤ :=
51 Recognition.phi L
52
53/-- Re-export: Chain flux. -/
54def chainFlux {M : RecognitionStructure} (L : Recognition.Ledger M) (ch : Recognition.Chain M) : ℤ :=
55 Recognition.chainFlux L ch
56
57/-- Re-export: Atomic tick class. -/
58abbrev AtomicTick := Recognition.AtomicTick
59
60/-- Re-export: Atomicity theorem (T2). -/
61theorem T2_atomicity {M : RecognitionStructure} [Recognition.AtomicTick M] :
62 ∀ t u v, Recognition.AtomicTick.postedAt (M:=M) t u → Recognition.AtomicTick.postedAt (M:=M) t v → u = v :=
63 Recognition.T2_atomicity
64
65/-- The bridge theorem: chainFlux is zero for balanced ledgers. -/
66theorem chainFlux_zero_of_balanced {M : RecognitionStructure} (L : Recognition.Ledger M)
67 (ch : Recognition.Chain M) (hbal : ∀ u, L.debit u = L.credit u) :