171structure Cycle (L : GradedLedger) where 172 /-- Length of the cycle -/ 173 len : ℕ 174 /-- The vertices visited -/ 175 vertices : Fin (len + 1) → Fin L.n 176 /-- Returns to start -/ 177 closed : vertices ⟨0, Nat.zero_lt_succ _⟩ = vertices ⟨len, Nat.lt_succ_self _⟩ 178 179/-- The **chain sum** along a cycle: Σᵢ edge(vᵢ, vᵢ₊₁). -/ 180def Cycle.chainSum {L : GradedLedger} (c : LedgerAlgebra.Cycle L) : ℤ :=
proof body
Definition body.
181 Finset.univ.sum fun i : Fin c.len => 182 L.edges 183 (c.vertices ⟨i.1, Nat.lt_trans i.2 (Nat.lt_succ_self c.len)⟩) 184 (c.vertices ⟨i.1 + 1, Nat.succ_lt_succ i.2⟩) 185 186/-! ## §6. The Potential Theorem (T4) -/ 187 188/-- **T4: Discrete Exactness** — If all cycle sums are zero, then the edge 189 weights are gradients of a potential function. 190 191 This is the algebraic statement: w = ∇φ, where φ : V → ℤ is unique 192 up to an additive constant on each connected component. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.