topoSort
The topoSort definition constructs a linear extension of any well-founded precedence on a finite event set by recursively extracting minimal elements until the set empties. Researchers proving existence of one-per-tick schedules for finite recognition histories cite it as the constructive ordering primitive. The recursion matches on set emptiness, invokes the minimal-element existence result, and terminates by strict cardinality decrease.
claimLet $E$ be a type of events and let $e_1 prec e_2$ be a well-founded precedence relation on $E$. For any finite subset $H subset E$, the ordering $sigma(H)$ is the list obtained by repeatedly selecting a minimal element $e$ of the current set under $prec$ and removing it until the set is empty.
background
The Atomicity module supplies an axiom-free serialization result for finite recognition histories. A Precedence on events $E$ is the binary relation where $prec e_1 e_2$ asserts that $e_1$ must occur before $e_2$. The supporting lemma exists_minimal_in guarantees that every nonempty finite set possesses a minimal element under a well-founded precedence, allowing deterministic extraction of sequential schedules.
proof idea
The definition is a recursive function on Finset $H$. When $H$ is nonempty it extracts a minimal element via exists_minimal_in, prepends it to the result on the erased set, and otherwise returns the empty list. Termination is declared by $H.card$ and discharged by the fact that erasing a member strictly lowers cardinality.
why it matters in Recognition Science
topoSort supplies the ordering primitive used by exists_sequential_schedule to assert a one-per-tick schedule for any finite history. It thereby tightens T2 by delivering a constructive, decidable serialization that respects ledger constraints without cost or convexity assumptions. The construction feeds directly into the preservation lemmas that close the atomicity argument.
scope and limits
- Does not extend to infinite event collections.
- Does not incorporate cost functionals or J-cost minimization.
- Does not itself prove conservation preservation under the schedule.
- Does not assume any structure beyond finiteness and decidable precedence.
formal statement (Lean)
72def topoSort
73 (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
74 (wf : WellFounded prec) :
75 ∀ H : Finset E, List E
76 | H =>
77 if h : H.Nonempty then
78 let ⟨e, heH, hmin⟩ := exists_minimal_in (E:=E) prec wf h
proof body
Definition body.
79 e :: topoSort prec wf (H.erase e)
80 else []
81 termination_by H => H.card
82 decreasing_by
83 classical
84 simp_wf
85 have : (H.erase _) .card < H.card := by
86 simpa [Nat.lt_iff_add_one_le, Nat.succ_le_succ_iff] using
87 Finset.card_erase_lt_of_mem heH
88 simpa using this
89
90/-- `topoSort` covers exactly the elements of `H` with no duplicates. -/