pith. machine review for the scientific record. sign in
lemma proved term proof high

exists_candidate_index

show as:
view Lean formalization →

Given a finite set of posted events and at least one unposted event, there exists a natural-number index into the enumeration such that the corresponding event remains unposted and satisfies the eligibility condition. Atomicity results in Recognition Science cite this lemma to guarantee a deterministic next candidate for sequential schedules over finite histories. The argument obtains a minimal eligible event via well-foundedness of the precedence relation, then recovers its index through surjectivity of the enumeration.

claimLet $P$ be a finite subset of events. If there exists an event outside $P$, then there exists a natural number $n$ such that the $n$th event in the enumeration lies outside $P$ and is eligible relative to $P$ (every predecessor of the event already belongs to $P$).

background

The module Atomicity supplies constructive serialization results for finite recognition histories. It works over an abstract event type $E$ equipped with a precedence relation that encodes ledger and causal constraints, without invoking cost or convexity axioms. An event is eligible once all predecessors have been posted: formally, eligible $P$ $e$ holds when every $v$ with Prec $v$ $e$ satisfies $v$ in $P$. The enumeration is the noncomputable surjection from naturals onto $E$ obtained from countability. The upstream lemma exists_minimal_eligible produces a minimal eligible event outside $P$ by appealing to well-foundedness of the precedence relation on the complement set.

proof idea

The term-mode proof proceeds by classical logic. It invokes exists_minimal_eligible on the given picked set and the non-emptiness hypothesis to obtain a minimal eligible event $e$. It then applies enum_surjective to recover an index $n$ with enum $n$ equal to $e$. The two conjuncts are discharged by simpa after substitution of the equality.

why it matters in Recognition Science

This lemma supplies the index-selection step inside chooseCandidate, which in turn feeds the construction of sequential schedules that respect precedence. It directly supports the module goal of tightening T2 by delivering an axiom-free, constructive one-per-tick ordering for any finite history. The result remains independent of the J-cost and phi-ladder machinery, keeping the serialization layer separate from later spectral and dimensional steps.

scope and limits

Lean usage

let hx := exists_candidate_index (ev:=ev) (E:=E) picked h; let n := Nat.find hx; let hn := Nat.find_spec hx

formal statement (Lean)

 322lemma exists_candidate_index (picked : Finset E.Event)
 323    (h : ∃ e, e ∉ picked) :
 324    ∃ n, enum (E:=E) n ∉ picked ∧ eligible (ev:=ev) picked (enum (E:=E) n) := by

proof body

Term-mode proof.

 325  classical
 326  obtain ⟨e, heNot, helig⟩ := exists_minimal_eligible (ev:=ev) (E:=E) picked h
 327  obtain ⟨n, hn⟩ := enum_surjective (E:=E) e
 328  refine ⟨n, ?_, ?_⟩
 329  · simpa [hn]
 330  · simpa [hn] using helig
 331

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.