enum
plain-language theorem explainer
The definition supplies a surjective map from the natural numbers onto the event set of any countable recognition history. Atomicity constructions in Recognition Science cite it to index events for one-per-tick serialization under precedence constraints. The construction is a direct one-line wrapper that selects a surjection via the axiom of choice applied to countability.
Claim. Let $E$ be a countable type of events. Then there exists a surjective function $enum : ℕ → E$ obtained by choice from the theorem that every countable set admits a surjection from the naturals.
background
The Atomicity module tightens T2 by supplying a serialization result for finite recognition histories. It works abstractly over an event type $E$ equipped with a precedence relation that encodes causal and ledger constraints, assuming only finiteness and decidable precedence. The module remains independent of cost or convexity axioms from T5 onward.
proof idea
The definition is a one-line wrapper that applies Classical.choose to Countable.exists_surjective_nat (E.countable).
why it matters
This definition feeds the Candidate structure and chooseCandidate function, which select minimal eligible events for sequential schedules. It supports downstream lemmas such as exists_sequential_schedule and sequential_preserves_conservation. In the Recognition framework it supplies the indexing map required for the T2 serialization result on finite histories.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.