eligible_mono
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not prove existence of minimal eligible events or full schedules.
- Does not incorporate conservation predicates or tick-level dynamics.
- Does not depend on cost functions, convexity, or the phi-ladder.
- Does not extend to infinite histories or non-finite event sets.
formal statement (Lean)
292lemma eligible_mono {picked₁ picked₂ : Finset E.Event}
293 (hsubset : picked₁ ⊆ picked₂) {e : E.Event}
294 (helig : eligible (ev:=ev) picked₁ e) :
proof body
Tactic-mode proof.
295 eligible (ev:=ev) picked₂ e := by
296 intro v hv
297 exact hsubset (helig hv)
298