topoSort_perm
plain-language theorem explainer
The lemma shows that the recursive topological sort of any finite event set under a well-founded precedence yields a duplicate-free list whose elements match the input set exactly. Researchers constructing one-per-tick schedules for finite causal histories cite it when serializing recognition events. The argument proceeds by induction on cardinality, prepending a minimal element at each step and verifying distinctness and coverage via set erasure.
Claim. Let $E$ be a type and let $prec$ be a well-founded precedence relation on $E$ (i.e., $e_1$ must precede $e_2$). For any finite set $Hsubseteq E$, the list produced by topological sort under $prec$ is pairwise distinct and has underlying set exactly $H$.
background
Atomicity supplies constructive, axiom-free serialization of finite recognition histories. Events belong to a type $E$ equipped with a precedence relation $prec$, read as $e_1$ must occur before $e_2$. The module works only with finite histories and decidable relations, remaining independent of cost or convexity structures. Precedence is defined as the binary relation $Eto Eto Prop$ encoding ledger or causal constraints. The auxiliary lemma exists_minimal_in guarantees a minimal element in any nonempty finite $H$ under well-founded $prec$.
proof idea
The proof is by classical induction on the cardinality $n$ of $H$. The base case $n=0$ reduces to the empty list, which satisfies both properties by direct simplification. In the step, a minimal element $e$ is obtained from exists_minimal_in, the tail is the inductive result on the erased set, and the full list is $e$ prepended to the tail. Distinctness uses the fact that no tail element equals $e$ (by erasure membership) together with the inductive hypothesis on the tail; coverage follows from the insert-erase identity.
why it matters
This lemma supplies the permutation property required to build sequential schedules. It is used directly by the downstream theorem exists_sequential_schedule, which asserts existence of a one-per-tick ordering for any finite history. Within Recognition Science it tightens T2 by delivering a constructive serialization result for causal constraints. The module deliberately avoids J-cost, phi-ladder, and RCL structures, keeping the result purely order-theoretic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.