eligible_mono
plain-language theorem explainer
The monotonicity lemma establishes that eligibility of an event is preserved when the set of posted events is enlarged by subset inclusion. Researchers constructing sequential schedules for finite recognition histories cite it to extend partial postings while maintaining precedence constraints. The proof is a direct one-line tactic that substitutes the subset relation into the universal quantifier of the eligibility predicate.
Claim. If $picked_1subseteq picked_2$ and every predecessor $v$ of event $e$ (satisfying $Prec v e$) belongs to $picked_1$, then every such predecessor belongs to $picked_2$.
background
The Atomicity module supplies constructive, axiom-free serialization for finite recognition histories over an abstract event type equipped with a precedence relation Prec that encodes ledger and causal constraints. Eligibility of an event $e$ relative to a Finset of posted events is the predicate that all predecessors $v$ with $Prec v e$ already lie in the set. The module deliberately avoids cost or convexity assumptions from T5 and works only with finiteness and decidable precedence.
proof idea
The tactic proof introduces an arbitrary predecessor $v$ together with the hypothesis $Prec v e$, then applies the given subset inclusion directly to the membership fact delivered by the eligibility assumption on the smaller set.
why it matters
This result supports the topological ordering lemmas that tighten T2 by allowing eligibility to survive set extension during schedule construction. It sits inside the forcing chain as a basic preservation property for partial histories and feeds the existence of one-per-tick schedules. No open scaffolding remains, as the lemma is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.