exists_sequential_schedule
Any finite set of events equipped with a decidable well-founded precedence relation admits a linear ordering that posts exactly one event per tick while respecting all precedence constraints. Researchers formalizing atomicity in Recognition Science cite this when serializing finite histories without extra axioms. The proof is a direct wrapper that invokes the topoSort recursion and delegates the distinctness, coverage, and order-preservation properties to the supporting lemmas topoSort_perm and topoSort_respects.
claimLet $E$ be a type and let $prec$ be a decidable well-founded precedence relation on $E$ (i.e., $prec(e_1,e_2)$ asserts that $e_1$ must precede $e_2$). For any finite subset $H$ of $E$ there exists a list $σ$ of distinct elements from $H$ whose underlying set equals $H$ such that $e_1 ∈ H$, $e_2 ∈ H$ and $prec(e_1,e_2)$ together imply that the index of $e_1$ in $σ$ is strictly smaller than the index of $e_2$.
background
Precedence is the abstract relation on events defined by the abbrev Precedence (E : Type _) := E → E → Prop; the notation prec e₁ e₂ is read “e₁ must occur before e₂”. Schedule is the structure whose order field is a list of distinct events representing a one-per-tick serialization of a finite history H. The module works entirely inside the finite-history fragment of Recognition Science, deliberately independent of cost functionals or convexity, and assumes only finiteness together with decidable precedence. It supplies the constructive half of the atomicity requirement that tightens T2 in the forcing chain.
proof idea
The tactic proof opens with classical, then refines the existential witness to the pair consisting of the topoSort recursion applied to prec, wf and H together with three subgoals. The first two subgoals are discharged by the two projections of topoSort_perm; the third subgoal is discharged by a direct application of topoSort_respects to the membership and precedence hypotheses.
why it matters in Recognition Science
The theorem supplies the existence direction used verbatim by the downstream atomic_tick theorem in the same module. It therefore completes the constructive serialization step required to tighten T2 for finite recognition histories. The result stays axiom-free and independent of the J-cost, phi-ladder and eight-tick octave structures that appear later in the framework; it therefore serves as a stable interface for any later conservation or mass-formula arguments that need a well-ordered posting sequence.
scope and limits
- Does not assert existence for infinite event collections.
- Does not incorporate any conservation predicate or cost functional.
- Does not assume any algebraic structure on the event type beyond decidable precedence.
- Does not claim uniqueness of the resulting schedule.
formal statement (Lean)
217theorem exists_sequential_schedule
218 (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
219 (wf : WellFounded prec) (H : Finset E) :
220 ∃ σ : Schedule E,
221 σ.order.Pairwise (· ≠ ·) ∧
222 σ.order.toFinset = H ∧
223 (∀ {e₁ e₂}, e₁ ∈ H → e₂ ∈ H → prec e₁ e₂ →
224 σ.order.indexOf e₁ < σ.order.indexOf e₂) := by
proof body
Tactic-mode proof.
225 classical
226 refine ⟨⟨topoSort (E:=E) prec wf H, ?_⟩, ?_, ?_, ?_⟩
227 · exact (topoSort_perm (E:=E) prec wf H).1
228 · exact (topoSort_perm (E:=E) prec wf H).2
229 · intro e₁ e₂ h₁ h₂ h12; exact topoSort_respects (E:=E) prec wf H h₁ h₂ h12
230
231/-- Generic preservation: if conservation holds initially and is preserved
232 by single postings, then conservation holds along any sequential schedule
233 for a finite history. -/