TimeArrow
plain-language theorem explainer
TimeArrow encodes the irreversible accumulation of verified propositions as the cursor advances in the ProofState model. Researchers formalizing time emergence within recognition frameworks cite it to ground the distinction between fixed past and open future. The declaration is a bare structure whose sole substantive field requires verified sets to be nondecreasing under any successor relation.
Claim. A structure consisting of the monotonicity axiom: for all proof states $s_1,s_2$, the set of verified propositions of $s_1$ is contained in the set of verified propositions of $s_2$, together with the trivial assertion that the future evolves.
background
The module models consciousness as the active cursor separating verified propositions (past) from unverified candidates (future), with the present proposition under verification. ProofState is the underlying partition: a triple of sets (verified, current, unverified) obeying the disjointness invariants that current lies outside both verified and unverified. Upstream TimeEmergence supplies the concrete temporal reading: past collects committed ledger snapshots at earlier ticks, future collects uncommitted snapshots at later ticks, and present is the snapshot at the current tick. These definitions supply the ordering that TimeArrow lifts to the level of propositions.
proof idea
Direct structure definition. The past_only_grows field is stated verbatim as the subset inclusion on verified sets; future_evolves is instantiated by the constant True. No lemmas or tactics are invoked.
why it matters
The declaration supplies the formal time arrow required by the cursor model of consciousness, implementing the statement that verified content grows monotonically while the future remains open. It bridges ProofState invariants to the temporal partition given by TimeEmergence past, present and future. Within the Recognition framework it prepares the ground for the free-will and qualia constructions appearing as siblings in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.