pith. machine review for the scientific record. sign in
theorem proved term proof

antisymmetric_implies_balance

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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. -/

depends on (9)

Lean names referenced from this declaration's body.