enum
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not construct an explicit enumeration without the axiom of choice.
- Does not incorporate precedence relations or eligibility predicates.
- Does not depend on the J-cost function or the phi-ladder.
- Does not address infinite or uncountable histories.
Lean usage
lemma example_surjective (E : Type) [Countable E] : Function.Surjective (enum (E:=E)) := enum_surjectiveformal statement (Lean)
282noncomputable def enum : ℕ → E.Event :=
proof body
Definition body.
283 Classical.choose (Countable.exists_surjective_nat (E.countable))
284