GradedLedger
The structure for a conserved integer flow on a finite directed graph with n vertices assigns edge weights such that inflow equals outflow at each vertex. Researchers building algebraic models in Recognition Science cite this when deriving cycle sums or potential functions from balanced ledgers. The definition encodes conservation directly in the structure, and the associated net flux theorem follows from unfolding and integer arithmetic simplification.
claimA structure consisting of a natural number $n$, an integer-valued function on directed edges between $n$ vertices, and the axiom that the sum of incoming weights equals the sum of outgoing weights at every vertex.
background
In the LedgerAlgebra module a graded ledger formalizes conserved flows on a finite directed graph with integer labels. The structure requires a natural number n for the number of vertices, an edges function from pairs of Fin n to integers, and a conservation predicate ensuring balance at each vertex. This sits downstream of the Chain structure, which provides minimal axioms for sequences satisfying a relation, and LedgerFactorization which calibrates the J function on positive reals. It precedes the definition of cycles as closed paths in the ledger and the double-entry algebra that adds pairing of edges. The local setting is the algebraic preparation for the closed-chain theorem T3, where conservation implies that cycle sums vanish.
proof idea
The structure is introduced by direct definition of its three fields. The netFlux operation is defined by subtracting the outgoing sum from the incoming sum at a vertex. The theorem that net flux vanishes everywhere unfolds the definition and invokes the conservation field, which is discharged by the omega tactic for integer arithmetic.
why it matters in Recognition Science
This declaration supplies the conserved ledger for Cycle and DoubleEntryAlgebra constructions in the same module. It fills the algebraic step toward the closed-chain theorem T3 by guaranteeing that net flux is zero, which is a prerequisite for showing that cycle sums are zero in the potential function setting. In the Recognition framework it encodes the local conservation law that follows from the J-uniqueness in T5 and supports the eight-tick octave periodicity in T7.
scope and limits
- Does not assume the graph is strongly connected.
- Does not bound the integer weights.
- Does not include dynamics or time evolution.
- Does not enforce global balance beyond local conservation.
formal statement (Lean)
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) : ℤ :=
proof body
Definition body.
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. -/