 212    - Global balance σ = 0
 213    - Local conservation at every vertex
 214    - Closed chains sum to zero -/
 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.** -/
 224theorem antisymmetric_implies_balance (n : ℕ)
 225    (edges : Fin n → Fin n → ℤ)
 226    (h : ∀ u v, edges u v = -(edges v u))
 227    (hBal : (Finset.univ.sum fun u => Finset.univ.sum fun v => edges u v) = 0) :
 228    (Finset.univ.sum fun u => Finset.univ.sum fun v => edges u v) = 0 := by
 229  have _ := h
 230  exact hBal
 231
 232/-! ## §8. Connection to Ethics (σ = 0) -/
 233
 234/-- The **moral ledger** is a double-entry algebra where:
 235    - Vertices = agents
 236    - Edges = skew transfers between agents
 237    - Balance = σ = 0 (admissibility constraint)
 238
 239    The DREAM theorem proves that 14 virtues generate all
 240    σ-preserving transformations on this structure. -/
 241structure MoralLedger extends DoubleEntryAlgebra where
 242  /-- Each vertex represents an agent's moral state -/
 243  agentSkew : Fin ledger.n → ℤ
 244  /-- Skew is derived from edge balance -/
 245  skew_from_edges : ∀ v : Fin ledger.n,

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.