isConsistent
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.