isConsistent
A definition that declares a proposition p consistent with verified history V precisely when p is not the negation of any q in V. Researchers modeling consciousness as the verification cursor in the RRF framework cite this when constructing valid next states for free-will hypotheses. The definition is realized directly as a universal check over the verified set for negation mismatch.
claimA proposition $p$ is consistent with a verified history $V$ if and only if $p$ is not the negation of any proposition in $V$, i.e., $p$ does not contradict any element of the fixed past.
background
The RRF module models consciousness as the active cursor advancing through propositions: verified propositions form the immutable past, the current proposition is the present, and unverified candidates are the future. Free will is then constrained choice among valid moves that balance the ledger. This local definition of consistency operates at the level of propositional history without yet invoking strain or J-cost.
proof idea
The definition is a direct one-line abbreviation: it expands to the universal quantification over the verified set that excludes any q where p equals the negation of q. No lemmas are applied; the body is the predicate itself.
why it matters in Recognition Science
This definition is used by validMoves to filter unverified propositions and by consistentStates in the Glossary to collect RRF-consistent states. It supplies the consistency predicate required for the free-will hypothesis (currently scaffolded) and connects to the cursor model in the module doc. It inherits the semantic consistency notion from the SAT.Backprop consistent predicate and the eight-tick phase structure from upstream.
scope and limits
- Does not incorporate strain balance or ledger closure from the RRF Glossary isConsistent.
- Does not reference J-cost, phi-ladder, or Recognition Composition Law.
- Does not guarantee that p is verifiable or true, only that it avoids direct negation.
- Does not handle consistency across multiple steps or higher-order propositions.
Lean usage
def validMoves (s : ProofState) : Set Prop := { p ∈ s.unverified | isConsistent s.verified p }formal statement (Lean)
88def isConsistent (verified : Set Prop) (p : Prop) : Prop :=
proof body
Definition body.
89 -- Simplified: just check p isn't ¬q for some q ∈ verified
90 ∀ q ∈ verified, ¬(p = ¬q)
91
92/-- Valid next moves: consistent with history. -/