pith. machine review for the scientific record. sign in
theorem proved term proof

chainFlux_zero_of_balanced

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)

  66theorem chainFlux_zero_of_balanced {M : RecognitionStructure} (L : Recognition.Ledger M)
  67    (ch : Recognition.Chain M) (hbal : ∀ u, L.debit u = L.credit u) :
  68    Recognition.chainFlux L ch = 0 :=

proof body

Term-mode proof.

  69  Recognition.chainFlux_zero_of_balanced L ch hbal
  70
  71end RRF.Core
  72end IndisputableMonolith

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.