present_is_boundary
plain-language theorem explainer
The definition asserts that in any ProofState the current proposition lies outside both the verified set and the unverified set. Researchers working on the cursor model of consciousness in Recognition Science cite it to mark the present as the active boundary between fixed past and open future. The definition is a direct conjunction of the two disjointness invariants supplied by the ProofState structure.
Claim. Let $s$ be a proof state with verified propositions $V$, current proposition $c$, and unverified propositions $U$. The present is the boundary precisely when $c$ belongs to neither $V$ nor $U$.
background
The RRF Foundation module models consciousness as the verification cursor. Past propositions are those already verified and therefore fixed; the present is the single proposition under active verification; future propositions remain unverified candidates. The ProofState structure records these three components as sets and a singleton, together with the two invariants that the current proposition lies outside both the verified set and the unverified set.
proof idea
The definition is a one-line wrapper that returns the conjunction of the two disjointness conditions already present in the ProofState invariants.
why it matters
The definition is used directly by the theorem proofstate_has_boundary, which states that every valid ProofState satisfies the boundary condition. It supplies the formal link between the cursor model of consciousness and the present-as-current-tick construction in TimeEmergence, placing the verification step at the active edge of recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.