DoubleEntryAlgebra
DoubleEntryAlgebra packages a graded ledger with antisymmetric edge pairings and a global sum-zero condition. It is referenced by moral ledger constructions and DREAM theorem statements in the algebra layer. The declaration is a direct structure definition encoding the algebraic consequences of the J-involution J(x) = J(1/x).
claimA double-entry algebra consists of a graded ledger with $n$ vertices and integer edge weights $E(u,v)$ satisfying inflow equals outflow at each vertex, together with the antisymmetry condition $E(u,v) = -E(v,u)$ for all $u,v$ and the global balance condition that the sum of all edge values is zero.
background
A graded ledger is a finite directed graph with integer edge weights where local conservation holds: for each vertex the sum of incoming edges equals the sum of outgoing edges. This supplies the base structure for DoubleEntryAlgebra. The module LedgerAlgebra imports Mathlib for finite-set summation and the Cost module that defines the J-cost function. The added paired and global_balance fields encode the global consequences of the Recognition Composition Law under the involution J(x) = J(1/x).
proof idea
This is a pure structure definition with an empty proof body. It asserts the three fields ledger, paired, and global_balance directly on top of the GradedLedger structure. No lemmas or tactics are applied.
why it matters in Recognition Science
MoralLedger extends DoubleEntryAlgebra to model agent skew transfers while preserving balance zero. The structure supplies the algebraic substrate for the DREAM theorem, which proves that fourteen virtues generate all sigma-preserving maps on this ledger. It realizes the closed-system requirement forced by J-uniqueness in the T5 step of the unified forcing chain.
scope and limits
- Does not specify vertex count or explicit edge values.
- Does not derive global balance from antisymmetry inside the definition.
- Does not embed the J-cost function or phi-ladder.
- Does not assign physical or agent interpretations to vertices.
formal statement (Lean)
215structure DoubleEntryAlgebra where
216 /-- The underlying graded ledger -/
217 ledger : GradedLedger
218 /-- Every edge has a reverse edge (pairing) -/
219 paired : ∀ u v : Fin ledger.n, ledger.edges u v = -(ledger.edges v u)
220 /-- Global balance: total of all edges is zero -/
221 global_balance : (Finset.univ.sum fun u => Finset.univ.sum fun v => ledger.edges u v) = 0
222
223/-- **PROVED: Antisymmetric edges automatically give global balance.** -/