def
definition
twoStep
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Recognition on GitHub at line 105.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
102
103def L : Ledger M := { debit := fun _ => 1, credit := fun _ => 1 }
104
105def twoStep : Chain M :=
106 { n := 1
107 , f := fun _ => ⟨()⟩
108 , ok := by intro i; trivial }
109
110example : chainFlux L twoStep = 0 := by
111 have hbal : ∀ u, L.debit u = L.credit u := by intro _; rfl
112 simpa [chainFlux_zero_of_balanced (M:=M) L twoStep hbal]
113
114end Demo
115
116-- Moved advanced Recognition sections (ClassicalBridge, Potential uniqueness) to Recognition/WIP.lean during modularization.