`GradedLedger`

definition

show as: view math explainer →

module: IndisputableMonolith.Algebra.LedgerAlgebra
domain: Algebra
line: 145 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.LedgerAlgebra on GitHub at line 145.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 142/-- A **graded ledger** assigns events to vertices of a graph.
 143    The grading ensures conservation at each node:
 144    inflow = outflow at every vertex. -/
 145structure GradedLedger where
 146  /-- Number of vertices -/
 147  n : ℕ
 148  /-- Events on edges (indexed by source, target) -/
 149  edges : Fin n → Fin n → ℤ
 150  /-- Conservation at each vertex: inflow = outflow -/
 151  conservation : ∀ v : Fin n,
 152    (Finset.univ.sum fun u => edges u v) =
 153    (Finset.univ.sum fun w => edges v w)
 154
 155/-- The **net flux** through a vertex. -/
 156def GradedLedger.netFlux (L : GradedLedger) (v : Fin L.n) : ℤ :=
 157  (Finset.univ.sum fun u => L.edges u v) -
 158  (Finset.univ.sum fun w => L.edges v w)
 159
 160/-- **PROVED: Net flux is zero at every vertex (conservation).** -/
 161theorem GradedLedger.netFlux_zero (L : GradedLedger) (v : Fin L.n) :
 162    L.netFlux v = 0 := by
 163  unfold netFlux
 164  have h := L.conservation v
 165  omega
 166
 167/-! ## §5. The Closed-Chain Theorem (T3) -/
 168
 169/-- A **cycle** in the graded ledger is a sequence of vertices that returns
 170    to the start. -/
 171structure Cycle (L : GradedLedger) where
 172  /-- Length of the cycle -/
 173  len : ℕ
 174  /-- The vertices visited -/
 175  vertices : Fin (len + 1) → Fin L.n

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.