GradedLedger
plain-language theorem explainer
A graded ledger is a finite directed graph on n vertices carrying integer edge weights that obey inflow-equals-outflow conservation at every vertex. Ledger-algebra constructions in Recognition Science cite this structure when assembling double-entry bookkeeping and proving that cycle sums vanish. The declaration is a plain structure definition that packages the three fields n, edges and conservation with no further proof obligations.
Claim. A graded ledger consists of a natural number $n$, an integer-valued map $e : [n]×[n]→ℤ$ on directed edges, and the axiom that for every vertex $v$ the sum of incoming weights equals the sum of outgoing weights.
background
The LedgerAlgebra module assembles the algebraic layer that sits above the J-cost functional equation imported from Cost. The graded ledger encodes the discrete conservation law that follows from the involution property J(x)=J(1/x). Upstream, the Chain structure supplies the minimal relation axioms used to close loops, while LedgerFactorization calibrates the same J on the multiplicative group of positive reals. The conservation field is the direct translation of Kirchhoff current balance into the integer lattice.
proof idea
This is a structure definition. The auxiliary netFlux function subtracts the two vertex sums; the companion theorem netFlux_zero unfolds the definition and invokes the conservation field, after which omega closes the equality.
why it matters
GradedLedger is the base type for Cycle, DoubleEntryAlgebra, PotentialFunction and the ledger_algebra_certificate that lists the six verified properties of the Recognition ledger. It supplies the conservation axiom required by the Closed-Chain Theorem (T3) section that immediately follows in the same module. The structure therefore sits between the J-uniqueness axiom (T5) and the exactness statements that feed the eight-tick octave and D=3 results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.