postAtTick
plain-language theorem explainer
The postAtTick definition retrieves the event at a given index n from the order list of a finite sequential schedule. Atomicity researchers cite it when inspecting one-per-tick postings or verifying topological orderings that respect precedence on finite histories. It is realized as a direct list lookup via get? on the schedule's order field.
Claim. For a schedule $σ$ whose order is a list of distinct events and a natural number $n$, postAtTick($σ$, $n$) returns the event at position $n$ in the list if it exists and none otherwise.
background
The Atomicity module supplies a constructive serialization for finite recognition histories. A Schedule is a structure holding an ordered list of events together with a pairwise distinctness property; it encodes a one-per-tick topological ordering that respects a decidable precedence relation on the event type E. The module deliberately avoids cost or convexity assumptions and works only with finiteness and decidable relations.
proof idea
The definition is a one-line wrapper that applies get? directly to the order list of the input schedule at index n.
why it matters
postAtTick supplies the basic accessor used by the module's existence and preservation results for sequential schedules. These results tighten T2 by delivering an axiom-free serialization step that feeds the broader forcing chain. The definition itself touches no open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.