consistentStates
plain-language theorem explainer
consistentStates defines the set of states satisfying the RRF consistency predicate for a given StrainLedger. Researchers modeling recognition processes or strain minimization cite it to restrict attention to valid configurations. The definition is a direct set comprehension over the isConsistent predicate that checks balanced strain and closed ledger.
Claim. Let $SL$ be a StrainLedger on a state space. The set of RRF-consistent states is the collection of all $x$ such that the strain component of $SL$ is balanced at $x$ and the ledger component of $SL$ is closed at $x$.
background
The RRF.Core.Glossary module supplies the single source of truth for Reality Recognition Framework vocabulary, including Strain as deviation from balance with J approaching zero, Ledger as double-entry conservation, and Octave as a scale of manifestation. StrainLedger is the structure that pairs a StrainFunctional with a LedgerConstraint to evaluate full RRF states. isConsistent is the predicate requiring both balanced strain and closed ledger on a state.
proof idea
This is a definition. It constructs the set by direct comprehension over the isConsistent predicate defined in the same module.
why it matters
The declaration supplies the canonical collection of consistent states used throughout RRF constructions. It anchors the framework's requirement that valid states obey both strain balance and ledger closure, consistent with the Recognition Composition Law and the T5 J-uniqueness step of the forcing chain. As a glossary entry it enforces uniform terminology across modules that import RRF, Strain, and Ledger types.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.