past_is_fixed
plain-language theorem explainer
The theorem states that any ledger snapshot belonging to the past of a given tick count must appear at some strictly earlier index in the state sequence. Researchers deriving the arrow of time from irreversible ledger updates cite it to enforce immutability of committed history. The proof is a direct term that applies the membership hypothesis without further reduction.
Claim. Let $(states_n)_{n∈ℕ}$ be a sequence of ledger snapshots and let $now∈ℕ$. If a snapshot $s$ belongs to the past of $states$ at tick $now$, then there exists $n<now$ such that $states_n=s$.
background
Time in this module is identified with the discrete tick counter of ledger updates; no background continuum parameter exists. A LedgerSnapshot is a structure carrying a tick index together with a non-negative real defect that quantifies distance from the cost minimum. The local setting establishes that past entries are committed and therefore fixed once the tick advances, while future entries remain uncommitted.
proof idea
The proof is a one-line term that directly invokes the hypothesis hs asserting membership of s in the past set. No lemmas are applied and no tactics are used; the existential witness is supplied immediately by the definition of the past predicate.
why it matters
The result secures the immutability of the past inside the time-emergence construction, feeding the arrow-of-time statements that follow in the same module. It fills the F-004 claim that time is defined by tick count rather than presupposed, and aligns with the eight-tick octave and monotonic defect decrease under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.