MoralLedger
plain-language theorem explainer
MoralLedger augments the double-entry algebra by adding an integer agentSkew map on vertices together with the axiom that this map equals net flux at each vertex. Researchers extending ledger models to ethics or narrative structures cite it when they need a carrier that already enforces sigma equals zero. The declaration is a direct structure extension of DoubleEntryAlgebra with one compatibility field.
Claim. A moral ledger consists of a double-entry algebra together with a map $agentSkew : Fin(n) → ℤ$ such that $agentSkew(v) = netFlux(v)$ for every vertex $v$.
background
DoubleEntryAlgebra packages a graded ledger with an antisymmetry condition on edges and a global-balance sum that totals zero. This algebra is the direct consequence of the J-cost functional obeying J(x) = J(1/x), which forces every flow to possess a paired counterflow and closed chains to cancel. The moral ledger sits inside the same module and simply adjoins an integer-valued skew function on agents while requiring that skew coincide with the ledger's net-flux computation.
proof idea
The declaration is a structure definition that extends DoubleEntryAlgebra and adds the two fields agentSkew and skew_from_edges. No tactics or lemmas are applied; the object is assembled by direct field declaration.
why it matters
MoralLedger supplies the algebraic carrier required by the DREAM theorem, which asserts that fourteen virtues generate all sigma-preserving transformations on this structure. It completes the ledger-algebra layer that links the double-entry axioms to the narrative and kinship modules imported by the same file. The construction directly supports the summary certificate that lists eight ledger properties ending with the ethics connection sigma equals zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.