free_will_exists
plain-language theorem explainer
If a proof state has at least one valid move, then there exists a proposition among those valid moves. Researchers modeling consciousness as a recognition cursor cite this to establish choice points in the verification process. The proof is a direct extraction from the nonempty hypothesis using obtain and exact.
Claim. Let $s$ be a proof state. If the set of valid moves from $s$ is nonempty, then there exists a proposition $p$ such that $p$ belongs to the valid moves from $s$.
background
ProofState is a structure with three disjoint components: verified propositions (the past), the current proposition under verification (the present), and unverified candidates (the future). validMoves returns the subset of unverified propositions that satisfy isConsistent with the verified history. recognize advances the state by verifying the current proposition and selecting a next candidate from unverified, provided consistency and distinctness hold.
proof idea
The proof is a term-mode extraction. It obtains a witness p together with membership hp directly from the nonempty hypothesis h on validMoves s, then returns the pair as the existential witness.
why it matters
This theorem is invoked by navigation_requires_choice to show that consciousness must choose at navigation points. It formalizes the module statement that free will equals constrained choice among valid moves, where valid moves are those consistent with prior recognition steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.