chooseCandidate_some_spec
The lemma states that whenever the candidate selection function returns a concrete candidate c for a finite set of picked events, that c is absent from the picked set and its event satisfies the eligibility condition under the precedence relation. Workers constructing deterministic topological schedules for finite recognition histories cite it to certify that each selected event meets the minimal-index and predecessor constraints. The proof proceeds by classical unfolding of the selection definition followed by case analysis on the existence of
claimLet $S$ be a finite set of events and let $c$ be a candidate structure for $S$. If the selection function returns $c$, then the event of $c$ does not belong to $S$ and every predecessor of that event already lies in $S$.
background
The Atomicity module supplies a constructive serialization of finite event histories that respects a decidable precedence relation, independent of cost or convexity. A Candidate for a picked set $S$ is a structure carrying an index $n$, an event $e$ such that $e$ equals the $n$th term of the fixed enumeration of the event type, a proof that $e$ is absent from $S$, and a proof that $e$ is eligible. The function chooseCandidate returns some such structure precisely when an event outside $S$ exists; it selects the minimal index via Nat.find. An event is eligible for $S$ precisely when every predecessor under the precedence relation already belongs to $S$. The module works over an abstract event type $E$ equipped with a countable enumeration and a precedence predicate, aiming at one-per-tick schedules that preserve conservation properties.
proof idea
The tactic proof opens classical logic, unfolds the definition of chooseCandidate inside the hypothesis, and splits on the if-condition that decides existence of an event outside the picked set. In the branch where the condition holds, the returned value is the some case whose fields directly supply not_mem and eligible; the contradictory branch is discharged by cases on the equality hypothesis.
why it matters in Recognition Science
The lemma certifies the output of the minimal-index selector used to build sequential schedules in the Atomicity module. That module tightens T2 by delivering an axiom-free topological ordering for any finite history, which in turn supports the existence of one-per-tick schedules and the preservation of conservation predicates under sequential posting. It therefore supplies a concrete, constructive step toward the serialization result that precedes later cost-based arguments in the forcing chain.
scope and limits
- Does not prove existence of any candidate.
- Does not treat infinite event sets.
- Does not incorporate the J-cost or convexity axioms.
- Does not address conservation preservation directly.
formal statement (Lean)
357lemma chooseCandidate_some_spec {picked : Finset E.Event}
358 {c : Candidate (ev:=ev) (E:=E) picked}
proof body
Tactic-mode proof.
359 (h : chooseCandidate (ev:=ev) (E:=E) picked = some c) :
360 c.not_mem ∧ eligible (ev:=ev) picked c.event := by
361 classical
362 unfold chooseCandidate at h
363 split_ifs at h with hExists
364 · rcases h with ⟨⟩
365 simp
366 · cases h
367
368/-- Minimal index (in the fixed enumeration `enum`) where an event appears. -/