potential_implies_exact
plain-language theorem explainer
If a potential function exists on a graded ledger then the chain sum along any cycle vanishes. Algebraists formalizing discrete conservation would cite the result when confirming that gradient data forces exactness on closed paths. The proof is a term-mode reduction that records the gradient axiom from the potential structure and concludes immediately from the supplied hypothesis on the cycle sum.
Claim. Let $L$ be a finite directed graph with integer edge weights satisfying inflow equals outflow at every vertex. Let $P$ assign an integer to each vertex such that the weight on every edge equals the difference of the values at its endpoints. Then the sum of weights around any closed path is zero.
background
A graded ledger consists of a finite set of vertices, integer weights on directed edges, and a conservation law requiring that the sum of weights into each vertex equals the sum out of it. A potential function on the ledger supplies an integer at each vertex together with the gradient relation that every edge weight equals the difference of potentials at its target and source. A cycle is a finite sequence of vertices that returns to its starting point; its chain sum is the sum of the edge weights traversed along the sequence.
proof idea
The proof is a term-mode script. It first invokes the gradient property supplied by the potential function structure. It then applies exact to the hypothesis that the chain sum equals zero.
why it matters
The result supplies one direction of discrete exactness inside the double-entry algebra section of LedgerAlgebra. That section encodes the global balance and closed-chain cancellation forced by the recognition composition law and the involution J(x) = J(1/x). It aligns with the T4 step of the forcing chain and supports the claim that closed chains sum to zero. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.