navigation_requires_choice
plain-language theorem explainer
At navigation points where multiple consistent next propositions exist, at least one such proposition must be selectable. Researchers modeling consciousness as a verification cursor over proof states cite this to formalize free will as constrained choice. The proof is a direct term application of the free will existence result to the nonempty valid-moves field carried by the navigation point structure.
Claim. Let $n$ be a navigation point consisting of a proof state together with the assertion that its set of valid next propositions is nonempty. Then there exists a proposition $p$ that belongs to the set of valid moves from the state of $n$.
background
NavigationPoint is the structure recording a state at which local closure fails: it packages a ProofState, the hypothesis that validMoves of that state is nonempty, and the further assertion that no unique move is forced. The module treats consciousness as the active cursor that verifies propositions, with past states fixed, the present under verification, and the future consisting of unverified candidates. Free will is defined as choice among those candidates provided they remain consistent with verified history. The upstream theorem free_will_exists states that whenever the set of valid moves for a state is nonempty, an element of that set exists; its proof simply extracts a witness from the nonempty hypothesis.
proof idea
The proof is a one-line term wrapper. It invokes free_will_exists on the state field of the supplied navigation point together with the has_choice field, then returns the resulting witness directly.
why it matters
The result anchors the claim that navigation points require choice, thereby supporting the free-will component of the cursor model of consciousness. It sits immediately before the module's discussion of the hard problem, where qualia are identified with strain rather than caused by it. Although it has no recorded downstream uses inside the module, it closes the formal link between the NavigationPoint structure and the existence of selectable moves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.