NavigationPoint
plain-language theorem explainer
A NavigationPoint packages a ProofState together with the assertions that its validMoves set is nonempty and contains no unique element. Researchers working on the cursor model of recognition would cite the structure when formalizing free will as constrained choice among ledger-consistent extensions. The definition is assembled directly from the ProofState record and the two predicates on validMoves without invoking external lemmas.
Claim. A navigation point consists of a proof state $s$ together with proofs that the set of valid moves from $s$ is nonempty and that no proposition is the unique member of that set.
background
In the RRF cursor model a ProofState partitions propositions into verified (past), current (present) and unverified (future) sets, subject to the invariants that the current proposition lies outside both the verified and unverified collections. The function validMoves returns the subset of unverified propositions that remain consistent with the verified history. NavigationPoint records a ProofState together with the two predicates that this subset is nonempty yet fails to be a singleton.
proof idea
The declaration is a structure definition that directly records the three fields: the underlying ProofState, the Nonempty predicate on validMoves, and the negation of unique existence inside that set. No lemmas or tactics are applied.
why it matters
NavigationPoint supplies the local non-closure hypothesis required by the free-will clause of the cursor model. It is used directly by the theorem navigation_requires_choice, which extracts an explicit move from any such point. Within the Recognition framework the structure implements the statement that free will equals constrained choice among valid ledger extensions, linking the eight-tick octave to the possibility of multiple consistent future states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.