chooseCandidate
plain-language theorem explainer
The definition supplies a deterministic selector for the next eligible event in a finite recognition history by returning the minimal-index Candidate record when unpicked events remain. Researchers proving constructive sequential schedules over causal precedence relations cite it to build topological orderings without axioms. The implementation branches on existence, applies Nat.find to the witness from exists_candidate_index, and assembles the record via the surjective enumeration.
Claim. Let $P$ be a finite set of events. Define chooseCandidate$(P)$ to equal some$(C)$ where $C$ records the smallest $n$ such that enum$(n)notin P$ and enum$(n)$ is eligible relative to $P$, if such an $n$ exists; otherwise it equals none.
background
The Atomicity module tightens T2 by supplying constructive, axiom-free serialization for finite recognition histories over an event type equipped with a precedence relation. Events are taken from the edge set $E$ of the $D$-cube, satisfying $|E|=D times 2^{D-1}$. The Candidate structure packages an index, the corresponding event obtained from the surjective enumeration enum, a non-membership proof, and an eligibility proof. The upstream lemma exists_candidate_index guarantees a suitable index exists whenever an unpicked event is present, by combining a minimal-eligible witness with surjectivity of enum.
proof idea
The definition splits on whether an unpicked event exists. In the positive case it invokes exists_candidate_index to obtain a witness, extracts the minimal index via Nat.find together with its specification, retrieves the event via enum, and constructs the Candidate record with reflexivity for the event definition and the extracted non-membership and eligibility facts. In the negative case it returns none.
why it matters
This definition supplies the deterministic pick used by the downstream lemmas chooseCandidate_none_iff and chooseCandidate_some_spec, which establish the equivalence for termination and the specification of the returned candidate. It fills the constructive serialization step required for the existence of sequential schedules and conservation preservation in the Atomicity module. The construction connects directly to the forcing chain at T2 by enabling one-per-tick ordering over finite histories while remaining independent of J-cost and convexity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.