theorem
proved
closed_iff_net_zero
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Core.Strain on GitHub at line 93.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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