chooseCandidate_none_iff
The lemma states that the candidate selection function on a finite set of picked events returns none exactly when no events remain unpicked. Workers on constructive serialization of finite recognition histories cite it to certify termination of the minimal-pick recursion. The proof unfolds the definition, performs case split on the existence hypothesis, and simplifies both branches.
claimLet $S$ be a finite subset of events. The candidate selection function satisfies $C(S) = none$ if and only if there is no event $e$ with $e$ outside $S$.
background
The Atomicity module supplies a constructive, axiom-free serialization for finite recognition histories over an abstract event type equipped with a decidable precedence relation. The central object is the noncomputable chooseCandidate function: given a picked Finset it returns Some candidate (via Nat.find on the existence witness) precisely when an unpicked event exists, and none otherwise. The module works independently of cost or convexity assumptions and only requires finiteness plus decidable precedence. The upstream E definition supplies the concrete event cardinality $D times 2^{D-1}$ for the D-cube edges, but the lemma itself remains parametric.
proof idea
The tactic proof opens with classical, unfolds chooseCandidate, then splits on the if-condition that encodes existence of an unpicked event. In the true branch it simplifies using the witness; in the false branch it simplifies directly to the negated existence statement. Both cases collapse by the definition of the if-then-else.
why it matters in Recognition Science
The result closes the termination case for the deterministic minimal-pick recursion that produces one-per-tick schedules, thereby supporting the existence of sequential schedules that respect precedence. It sits inside the Atomicity module whose purpose is to tighten T2 of the forcing chain without invoking J-cost or the phi-ladder. No downstream uses are recorded yet, so the lemma currently serves as an internal interface for later conservation-preservation arguments.
scope and limits
- Does not assume any cost function or convexity properties.
- Does not extend to infinite event histories.
- Does not itself prove conservation preservation under scheduling.
- Does not supply an explicit algorithm for the precedence relation.
formal statement (Lean)
348lemma chooseCandidate_none_iff (picked : Finset E.Event) :
349 chooseCandidate (ev:=ev) (E:=E) picked = none ↔
proof body
Tactic-mode proof.
350 ¬∃ e, e ∉ picked := by
351 classical
352 unfold chooseCandidate
353 split_ifs with h
354 · simp [h]
355 · simp [h]
356