Candidate
Candidate is a record bundling an index n, an event e drawn from the enumeration of the event type, and proofs that e lies outside the current picked set while satisfying the eligibility predicate. It supplies the typed payload for the deterministic next-event selector used to build sequential schedules over finite histories. The definition is a direct structure with no computation or auxiliary lemmas.
claimGiven a finite set $S$ of posted events, a candidate consists of a natural number index $n$, an event $e$, together with proofs that $e$ is the image of $n$ under the enumeration of the event type, $e$ does not belong to $S$, and every predecessor of $e$ already lies in $S$.
background
The Atomicity module supplies an axiom-free, constructive serialization of finite recognition histories. Events carry a decidable precedence relation that encodes causal or ledger constraints. The type $E$ is the set of edges of the $D$-cube, so $|E|=D·2^{D-1}$. The noncomputable function enum supplies a surjective listing of all events from the naturals. An event is eligible relative to a picked set $S$ precisely when every predecessor under precedence already belongs to $S$.
proof idea
The declaration is a plain structure definition. Its five fields directly record the index, the event, the equality with the enumerated value, the freshness condition, and the eligibility predicate. No tactics, reductions, or upstream lemmas are invoked inside the definition itself.
why it matters in Recognition Science
Candidate supplies the data type consumed by chooseCandidate, which in turn drives the recursive construction of sequential schedules. Those schedules establish one-per-tick orderings that preserve any conservation predicate, thereby tightening the T2 serialization step of the forcing chain. The same structure appears in downstream statements for continuum-limit convergence and lepton-generation correction formulas.
scope and limits
- Does not assume any cost function or convexity property on events.
- Does not prove existence of a candidate for an arbitrary picked set.
- Does not depend on the J-cost, phi-ladder, or spectral constants.
- Does not treat infinite or non-finite histories.
- Does not encode any metric or ordering beyond precedence.
formal statement (Lean)
315structure Candidate (picked : Finset E.Event) where
316 idx : ℕ
317 event : E.Event
318 event_def : enum (E:=E) idx = event
proof body
Definition body.
319 not_mem : event ∉ picked
320 eligible_event : eligible (ev:=ev) picked event
321