enum_surjective
plain-language theorem explainer
The map from naturals to events is surjective for any countable event type. Researchers building sequential schedules for finite causal histories cite it to guarantee every event receives an index under the fixed ordering. The proof is a direct one-line appeal to the specification of classical choice applied to the standard existence of a surjection from naturals onto a countable set.
Claim. Let $E$ be a countable event type. The enumeration map $f : {N} {to} E$ is surjective.
background
The Atomicity module supplies serialization tools for finite recognition histories over an abstract event type $E$ equipped with a precedence relation that encodes causal ledger constraints. The enumeration map is the non-computable function obtained by classical choice from the theorem asserting a surjection from naturals onto any countable type. Eligibility of an event is the predicate that all its predecessors have already been posted. The module deliberately avoids cost or convexity assumptions and works only with finiteness and decidable precedence.
proof idea
One-line term proof that invokes the specification of the classical choice operator on the existence theorem for a surjection from the naturals to a countable type.
why it matters
This surjectivity result is required to define minimal indices in the enumeration and to select candidate events during construction of sequential schedules. It is used directly by exists_candidate_index, minIndex, minIndex_min, and minIndex_spec. In the Recognition framework it supplies the covering property needed for the deterministic pick-minimal recursion that realizes one-per-tick atomic schedules, thereby tightening the T2 serialization step in an axiom-free manner.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.