structure
definition
Cycle
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Algebra.LedgerAlgebra on GitHub at line 171.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
all -
GradedLedger -
GradedLedger -
all -
of -
of -
Length -
V -
all -
lt_trans -
zero_lt_succ -
of -
of -
is -
of -
of -
is -
of -
of -
V -
is -
of -
of -
is -
all -
L -
L -
L -
L -
constant -
V -
LedgerAlgebra
used by
formal source
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
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) : ℤ :=
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. -/
193structure PotentialFunction (L : GradedLedger) where
194 /-- The potential at each vertex -/
195 potential : Fin L.n → ℤ
196 /-- Edge weight = potential difference -/
197 gradient : ∀ u v : Fin L.n,
198 L.edges u v = potential v - potential u
199
200/-- **PROVED: If a potential exists, then all cycle sums are zero.** -/
201theorem potential_implies_exact {L : GradedLedger} (P : PotentialFunction L)