def
definition
LedgerClosure
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Core.Glossary on GitHub at line 62.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
59 ∃ x, S.isBalanced x
60
61/-- Ledger closure: the double-entry constraint holds. -/
62def LedgerClosure {State : Type*} (L : LedgerConstraint State) (x : State) : Prop :=
63 L.isClosed x
64
65/-- Channel equivalence: two channels induce the same state ordering. -/
66abbrev ChannelEquiv {State Obs₁ Obs₂ : Type*} :=
67 QualityEquiv (State := State) (Obs₁ := Obs₁) (Obs₂ := Obs₂)
68
69/-! ## RRF Consistency Conditions
70
71For a state to be "real" (recognized), it must satisfy:
721. Strain minimization (or at least local minimum)
732. Ledger closure
743. Consistent observation across channels
75-/
76
77/-- A state is RRF-consistent if it has low strain and closed ledger. -/
78def isConsistent {State : Type*}
79 (SL : StrainLedger State) (x : State) : Prop :=
80 SL.strain.isBalanced x ∧ SL.ledger.isClosed x
81
82/-- The set of RRF-consistent states. -/
83def consistentStates {State : Type*} (SL : StrainLedger State) : Set State :=
84 { x | isConsistent SL x }
85
86end RRF.Core
87end IndisputableMonolith