proofstate_has_boundary
plain-language theorem explainer
Every ProofState satisfies the boundary condition that its current proposition lies outside both the verified past and unverified future sets. Researchers modeling consciousness as a verification cursor in the Recognition framework cite this to enforce the disjointness invariant. The proof is a direct term construction unpacking the two field projections from the ProofState structure.
Claim. For any proof state $s$, the present proposition is neither in the verified set nor in the unverified set: $s.current ∉ s.verified ∧ s.current ∉ s.unverified$.
background
ProofState is a structure with three components: a set of verified propositions (past), a single current proposition (present), and a set of unverified propositions (future). The structure carries two explicit invariants ensuring the current proposition is absent from both sets. The predicate present_is_boundary is defined exactly as the conjunction of those two absences, making the present the boundary between fixed past and open future. This lives inside the RRF cursor model where consciousness is identified with the verification step itself.
proof idea
The proof is a term-mode construction that directly supplies the two conjuncts of present_is_boundary by projecting the current_not_in_past and current_not_in_future fields from the input ProofState.
why it matters
This theorem locks in the core invariant of the cursor model inside the Consciousness module. It supplies the boundary condition required for any subsequent reasoning about free will as constrained choice among valid moves and about qualia as strain measures. The result sits at the base of the RRF treatment of the present as the active edge of recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.