exists_minimal_eligible
In a finite collection of events under a well-founded precedence relation, if any events remain unpicked then at least one unpicked event has all its predecessors already posted. Atomicity arguments in Recognition Science invoke this to start building a sequential posting order. The proof extracts a minimal unpicked event via the ledger well-ordering and shows eligibility by contradiction on any missing predecessor.
claimLet $P$ be a finite set of posted events. If there exists at least one event outside $P$, then there exists an event $e$ outside $P$ such that every predecessor $v$ of $e$ under the precedence relation lies in $P$.
background
The Atomicity module supplies serialization results that tighten the T2 axiom of discrete causal structure in Recognition Science. It works over an abstract event type equipped with a precedence relation encoding ledger and causal constraints, assuming only finiteness and decidable precedence on finite histories. The central auxiliary definition states that an event is eligible with respect to the posted set once every predecessor under the precedence relation has already been posted.
proof idea
The argument begins by invoking classical logic to access the well-founded ledger precedence relation. It forms the nonempty set of unpicked events and applies the has_min property to extract a minimal element m. Eligibility of m follows by supposing a predecessor v is unpicked, placing v in the unpicked set, and invoking minimality to obtain a contradiction.
why it matters in Recognition Science
This lemma initiates the inductive construction of sequential schedules over finite histories and is invoked directly by the exists_candidate_index lemma to locate the next event via enumeration. It realizes the constructive serialization step described in the Atomicity module documentation for tightening T2. Within the Recognition framework it supports gap-free causal posting that underpins the eight-tick octave and three spatial dimensions.
scope and limits
- Does not guarantee uniqueness of the minimal eligible event.
- Does not extend to infinite event collections.
- Does not depend on the J-cost function or Recognition Composition Law.
- Does not incorporate spatial dimension or the fine-structure constant band.
Lean usage
obtain ⟨e, heNot, helig⟩ := exists_minimal_eligible (ev:=ev) (E:=E) picked hformal statement (Lean)
299lemma exists_minimal_eligible (picked : Finset E.Event)
300 (h : ∃ e, e ∉ picked) :
301 ∃ e, e ∉ picked ∧ eligible (ev:=ev) picked e := by
proof body
Tactic-mode proof.
302 classical
303 have wf := ledger_prec_wf (ev:=ev)
304 let S : Set E.Event := {x | x ∉ picked}
305 have hS : S.Nonempty := by
306 rcases h with ⟨e, he⟩
307 exact ⟨e, he⟩
308 obtain ⟨m, hmS, hmin⟩ := wf.has_min S hS
309 refine ⟨m, hmS, ?_⟩
310 intro v hv
311 by_contra hvPicked
312 have hvS : v ∈ S := hvPicked
313 exact (hmin v hvS hv)
314