enum
plain-language theorem explainer
The noncomputable map from naturals to events in E is obtained by classical choice from the countability of the event set. Atomicity results on serialization of finite recognition histories cite this map to index events for minimal-eligible selection under precedence. The definition is a one-line wrapper invoking Classical.choose on the existence of a surjection from ℕ.
Claim. Let $E$ be the event type. There exists a surjective function $f : ℕ → E$ defined by classical choice applied to the theorem that every countable type admits a surjection from the naturals.
background
The Atomicity module supplies serialization results for finite recognition histories over an event type equipped with a precedence relation that encodes ledger and causal constraints. The module works independently of cost or convexity and assumes only finiteness and decidable precedence on the history. Upstream, the event type E arises in SpectralEmergence as the edges of the D-cube with cardinality $D × 2^{D-1}$.
proof idea
The definition is a one-line wrapper that applies Classical.choose to Countable.exists_surjective_nat on the countability of E.
why it matters
This definition supplies the indexing map used by Candidate, chooseCandidate, exists_candidate_index, and enum_surjective to build minimal eligible events and sequential schedules. It directly supports the constructive one-per-tick ordering required to tighten T2 while remaining independent of the J-cost function and the phi-ladder. The map feeds the preservation lemma for conservation predicates under any finite sequential schedule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.