exists_minimal_in
plain-language theorem explainer
The lemma establishes that any nonempty finite set of events admits a minimal element under a well-founded precedence relation. Researchers constructing topological orders for finite causal histories cite this when building sequential schedules. The argument applies well-founded recursion to descend the relation until a minimal element is located, using a by-cases check at each step.
Claim. Let $E$ be a type of events and let $prec$ be a well-founded precedence relation on $E$ (with decidable relation and equality). For any nonempty finite subset $H$ of $E$, there exists an element $e$ in $H$ such that no $e'$ in $H$ satisfies $prec$ $e'$ $e$.
background
The Atomicity module works abstractly over an event type $E$ equipped with a precedence relation $prec$, where $prec$ $e_1$ $e_2$ means $e_1$ must occur before $e_2$ in any valid ledger history. Precedence is introduced as the simple abbreviation $E → E → Prop$. The module derives constructive, axiom-free serialization results for finite histories, deliberately avoiding cost or convexity assumptions from T5. Upstream results include the definition of $H$ as the shifted cost $J(x) + 1$ in CostAlgebra, though the present lemma uses only the well-foundedness of $prec$ itself.
proof idea
The tactic proof opens with classical reasoning and eliminates the nonempty hypothesis to select an arbitrary element $a$ in $H$. It then applies well-founded induction on $prec$ to the predicate that every $x$ in $H$ admits a minimal element $m$ in $H$. Inside the induction step a by-cases check decides whether $x$ is already minimal; if not, negation is pushed to extract a predecessor $y$ with $prec$ $y$ $x$, and the induction hypothesis is invoked on $y$.
why it matters
This lemma supplies the existence step required by the downstream definitions topoSort, topoSort_perm and topoSort_respects, which iteratively extract minimal elements to produce a total order on finite histories. It directly implements the constructive serialization promised in the module doc-comment for tightening T2. The result remains independent of the J-cost functional equation, the phi-ladder and the eight-tick octave, focusing solely on well-founded relations over finite sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.