Cycle
plain-language theorem explainer
A cycle on a graded ledger is a finite sequence of vertices that returns to its starting point, equipped with an integer chain sum obtained by adding the directed edge weights along consecutive pairs. Researchers formalizing discrete conservation or potential theory in ledger models cite this structure when relating cycle conditions to exactness of edge weights. The definition is a direct record of length, vertex map, closure equality, and an explicit finite summation for the chain sum.
Claim. Let $L$ be a graded ledger with $n$ vertices and integer edge weights $w$. A cycle of length $k$ consists of a map $v : [0..k] → [0..n-1]$ satisfying $v(0) = v(k)$, together with the chain sum $∑_{i=0}^{k-1} w(v(i), v(i+1))$.
background
A graded ledger is a finite directed graph whose vertices carry integer edge weights obeying inflow equals outflow at every vertex; this is the algebraic transcription of local conservation. The LedgerAlgebra module introduces the Cycle structure immediately before the statement of discrete exactness (T4), which asserts that vanishing cycle sums are equivalent to the weights being the gradient of an integer-valued potential on the vertices. Upstream results supply the graded ledger itself and the surrounding algebraic scaffolding for conservation laws.
proof idea
The structure is assembled from three fields: a natural-number length, a function from Fin (len+1) into the vertex set, and the equality that identifies the initial and terminal vertices. The chain sum is obtained by direct summation of the ledger's edge function over the consecutive pairs indexed by Fin len, using the standard Finset.univ.sum combinator.
why it matters
Cycle supplies the algebraic object needed for the potential theorem (T4) and is invoked in the downstream result potential_implies_exact, which records that a potential function forces every cycle sum to zero. The same object appears in recognition-loop surjectivity theorems and in derivations of mixing angles, thereby linking ledger algebra to the eight-tick octave and to the broader forcing chain that yields three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.