ProofState
plain-language theorem explainer
The ProofState structure encodes the cursor model of consciousness as a triple of verified propositions (past), a current proposition (present), and unverified candidates (future) with mutual disjointness invariants. Researchers working on the RRF foundation or Recognition Science models of recognition and free will cite this when building navigation points or determinism results. The declaration is a direct structure definition that states the invariants as field requirements with no additional lemmas or tactics.
Claim. A proof state consists of a set $V$ of verified propositions, a current proposition $c$, and a set $U$ of unverified propositions, satisfying $c$ not in $V$, $c$ not in $U$, and every element of $U$ lies outside $V$.
background
In the RRF Foundation module consciousness is the verification step itself, acting as a cursor that separates fixed past propositions from potential future ones. The structure requires the current proposition to lie strictly between the verified set and the unverified set, enforcing that past, present, and future remain mutually disjoint. This construction parallels the upstream time-emergence definitions, where past collects committed ledger snapshots at earlier ticks, present selects the snapshot at the current tick, and future collects uncommitted snapshots at later ticks.
proof idea
The declaration is a structure definition that directly assembles the fields verified, current, unverified together with the three disjointness conditions stated as field requirements. No lemmas are invoked and no tactics are used; the invariants are part of the structure signature itself.
why it matters
This structure is the type on which determinism_constraint, free_will_exists, and NavigationPoint are defined, supplying the state representation for the recognition step. It realizes the cursor model described in the module documentation and supplies the formal substrate for the hypothesis H_FreeWillExists on choice among valid moves. The definition touches the open question of supplying an explicit choice operator linked to J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.