chooseCandidate_none_iff
plain-language theorem explainer
The lemma states that the minimal unpicked-event selector returns none precisely when the picked Finset already contains every event in the finite history. Serialization constructions in Atomicity cite the equivalence to confirm recursion termination. The tactic proof unfolds the selector definition and splits cases on its internal existence test.
Claim. Let $P$ be a finite set of events drawn from the event type. Let $C(P)$ be the function that returns a candidate minimal unpicked event when one exists. Then $C(P)= exttt{none}$ if and only if no event lies outside $P$.
background
Atomicity constructs axiom-free one-per-tick schedules for any finite recognition history by recursive minimal selection that respects a precedence relation on events. The module assumes only finiteness and decidable precedence; it deliberately omits cost or convexity structure. chooseCandidate is the noncomputable selector that, given an existence witness for an unpicked event, returns the index found by Nat.find on that witness.
proof idea
The tactic proof invokes classical logic, unfolds chooseCandidate, then splits on the if-condition that tests existence of an event outside the picked set. Each branch applies simp to obtain the matching side of the biconditional.
why it matters
The result supplies the termination condition for the recursive schedule construction that tightens T2. It belongs to the Atomicity module whose outcomes include existence of sequential schedules and preservation of conservation predicates under any such schedule. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.