`net`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Core.Strain
domain: RRF
line: 90 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Core.Strain on GitHub at line 90.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
 106variable {State : Type*}
 107
 108/-- A state is valid if it has zero strain and closed ledger. -/
 109def isValid (SL : StrainLedger State) (x : State) : Prop :=
 110  SL.strain.isBalanced x ∧ SL.ledger.isClosed x
 111
 112/-- The set of valid states. -/
 113def validStates (SL : StrainLedger State) : Set State :=
 114  { x | SL.isValid x }
 115
 116end StrainLedger
 117
 118end RRF.Core
 119end IndisputableMonolith

papers checked against this theorem

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