Schedule
plain-language theorem explainer
A Schedule over event type E is an ordered list of distinct events that serves as a one-per-tick serialization of a finite recognition history. Researchers formalizing atomic timelines in Recognition Science cite this structure when constructing explicit causal orderings from precedence graphs. It is introduced directly as a structure with a list field and a pairwise distinctness predicate, acting as the carrier type for existence and preservation results.
Claim. A schedule over an event type $E$ is a list $s : List E$ equipped with a proof that its entries are pairwise distinct: $s.Pairwise (· ≠ ·)$.
background
The Atomicity module supplies constructive, axiom-free serialization for finite recognition histories. It works abstractly over an event type E equipped with a precedence relation that encodes ledger and causal constraints, assuming only finiteness and decidable equality. The module deliberately avoids cost or convexity assumptions from T5 and relies on topological ordering via minimal-element recursion.
proof idea
The declaration is a structure definition that directly introduces the two fields order and nodup. No lemmas or tactics are applied; the structure serves as the inductive carrier for downstream results on sequential schedules.
why it matters
This definition supplies the data type used by atomic_tick to assert existence of a precedence-respecting one-per-tick ordering for any finite history, and by exists_sequential_schedule and sequential_preserves_conservation. It supports Flight subtheories including eightGateNeutral_shift_invariance and PulseCoherence, which enforce 8-tick neutrality. The construction tightens T2 of the forcing chain by providing explicit serialization aligned with the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.