pith. sign in
theorem

exists_sequential_schedule

proved
show as:
module
IndisputableMonolith.Foundation.Atomicity
domain
Foundation
line
217 · github
papers citing
4 papers (below)

plain-language theorem explainer

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.

Claim. Let $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

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.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 4 of 4)