LedgerConstraint

formal source

  72end StrainFunctional
  73
  74/-- A ledger constraint: the sum of debits equals the sum of credits. -/
  75structure LedgerConstraint (State : Type*) where
  76  /-- Total debit for a state. -/
  77  debit : State → ℤ
  78  /-- Total credit for a state. -/
  79  credit : State → ℤ
  80
  81namespace LedgerConstraint
  82
  83variable {State : Type*}
  84
  85/-- A state satisfies the ledger constraint if debit = credit. -/
  86def isClosed (L : LedgerConstraint State) (x : State) : Prop :=
  87  L.debit x = L.credit x
  88
  89/-- The net balance (should be zero for closed ledgers). -/
  90def net (L : LedgerConstraint State) (x : State) : ℤ :=
  91  L.debit x - L.credit x
  92
  93theorem closed_iff_net_zero (L : LedgerConstraint State) (x : State) :
  94    L.isClosed x ↔ L.net x = 0 := by
  95  simp [isClosed, net, sub_eq_zero]
  96
  97end LedgerConstraint
  98
  99/-- Combined strain and ledger: the full RRF state evaluation. -/
 100structure StrainLedger (State : Type*) where
 101  strain : StrainFunctional State
 102  ledger : LedgerConstraint State
 103
 104namespace StrainLedger
 105