DoubleEntryAlgebra
plain-language theorem explainer
The DoubleEntryAlgebra structure packages a graded ledger with antisymmetric integer edge weights and global sum zero. It encodes the algebraic consequences of the recognition cost symmetry J(x) = J(1/x). MoralLedger constructions extend this structure to model agent skew and admissibility constraints. The definition assembles the three required fields directly from the GradedLedger base without further derivation.
Claim. A double-entry algebra consists of a graded ledger $(n, e, c)$ together with the conditions that $e(u,v) = -e(v,u)$ for all vertices $u,v$ and that the double sum of all edge values equals zero.
background
A graded ledger assigns integer events to directed edges of a complete graph on $n$ vertices while enforcing local conservation: inflow equals outflow at every vertex. The double-entry algebra augments this base with the global antisymmetry condition on edges and the requirement that the total sum of all edge values vanishes. The module doc-comment states that this structure is the algebraic foundation forced by the recognition cost symmetry J(x) = J(1/x), which requires every flow to possess a paired counterflow and closed chains to sum to zero.
proof idea
The declaration is a structure definition that directly records the three components: the underlying graded ledger, the universal quantification expressing antisymmetry of edges, and the explicit summation expressing global balance. No lemmas are applied; the fields are stated verbatim from the GradedLedger signature and the two additional axioms listed in the doc-comment.
why it matters
MoralLedger extends DoubleEntryAlgebra by adding agentSkew and skew_from_edges fields, thereby interpreting vertices as agents and applying the DREAM theorem to generate all sigma-preserving transformations. The structure supplies the ledger carrier required for the Recognition Composition Law and the eight-tick octave bookkeeping. It closes the algebraic interface between the J-cost symmetry and downstream moral and kinship models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.