pith. machine review for the scientific record. sign in
def definition def or abbrev

twoStep

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 105def twoStep : Chain M :=

proof body

Definition body.

 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.

depends on (12)

Lean names referenced from this declaration's body.