atomic_tick_countable
plain-language theorem explainer
The theorem establishes existence of a countable schedule over a finite event set that posts exactly one event per tick, covers every event, and admits no duplicates. Workers constructing sequential models of finite recognition histories cite it to guarantee a deterministic enumerative ordering. The proof is a direct term-mode wrapper that instantiates the canonical scheduleByMinIndex and applies its completeness and nodup fields.
Claim. There exists a countable schedule $σ$ for the event type $E$ such that every event $e$ is posted at a unique tick: $∀ e, ∃! n, σ.postAt n = some e$.
background
Atomicity.lean supplies a constructive, axiom-free serialization result for finite recognition histories. It works over an abstract event type $E$ equipped with a precedence relation that encodes ledger and causal constraints. The central object is a CountableSchedule, a map from natural numbers to optional events together with proofs that at most one event is posted per tick and that the assignment is injective on posted events.
proof idea
The proof is a term-mode wrapper. It refines the existential by supplying scheduleByMinIndex (ev:=ev). The first subgoal is discharged by the completeness property of that schedule, which guarantees every event receives a tick. The second subgoal follows from the nodup property of scheduleByMinIndex, which enforces that distinct ticks cannot post the same event.
why it matters
This theorem closes the constructive serialization step required by the atomicity component of the Recognition Science forcing chain (T2). It supplies the enumerative schedule that later stages can use to convert finite event histories into sequential tick sequences while preserving conservation. The construction relies only on minIndex selection and classical choice, remaining fully constructive for any finite history. No downstream theorems are yet recorded, but the result supports the eight-tick octave and dimensional emergence arguments that follow from atomic schedules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.