H_FreeWillExists
plain-language theorem explainer
H_FreeWillExists encodes free will as the existence of at least one valid move whenever the set of consistent unverified propositions is nonempty. Researchers modeling consciousness via the cursor in the RRF framework cite it to separate verified history from future candidates. The definition is a direct encoding of the nonempty-set property, left as a scaffold pending an explicit choice operator.
Claim. For a proof state $s$, if the set of propositions consistent with verified history is nonempty, then there exists a proposition $p$ in that set.
background
The RRF Foundation module treats consciousness as the verification cursor: past propositions are fixed and verified, the present is the proposition under verification, and the future consists of unverified candidates. ProofState is the structure holding these three components as sets with the invariants that the current proposition lies outside both the verified set and the unverified set.
proof idea
One-line definition that applies the standard set-theoretic fact that a nonempty set contains an element. The body simply unfolds the Nonempty predicate into an existential quantifier over the output of validMoves.
why it matters
The declaration supplies the hypothesis interface for free will inside the cursor model, where free will is defined as constrained choice among paths that preserve ledger balance. Module documentation states that qualia arise as the internal view of strain, with this scaffold marking the missing formal link to a choice operator and J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.