topoSort_respects
plain-language theorem explainer
The lemma shows that a deterministic topological sort on a finite event set respects a well-founded precedence relation by placing any predecessor strictly earlier in the output sequence. Workers constructing one-per-tick schedules for finite recognition histories cite it to guarantee causal order preservation. The argument proceeds by induction on set cardinality, extracting a minimal element at each step via exists_minimal_in and shifting indices on the recursive tail.
Claim. Let $E$ be a type of events and let $e_1,e_2$ belong to a finite subset $H$. If $e_1$ must precede $e_2$ under a well-founded precedence relation, then the position of $e_1$ in the topological sort of $H$ is strictly smaller than the position of $e_2$.
background
The Atomicity module supplies a constructive serialization of finite recognition histories into sequential schedules. A Precedence relation on events is simply a binary predicate declaring that one event must occur before another. The function topoSort is defined by repeated selection of a minimal element (an event with no predecessors inside the current set) followed by recursion on the remainder; the supporting lemma exists_minimal_in guarantees such an element exists for every nonempty finite set under a well-founded relation. The module works only with finiteness and decidability, deliberately avoiding cost or convexity assumptions from T5.
proof idea
An auxiliary statement is proved by recursion on the cardinality $n$ of $H$. The base case $n=0$ is vacuous. In the successor step a minimal element $e$ is obtained from exists_minimal_in, the tail is formed by erasing $e$, and the inductive hypothesis is applied to the smaller set. Separate cases on whether $e_1$ or $e_2$ equals $e$ produce the required index inequality after accounting for the one-position shift induced by prepending $e$.
why it matters
The lemma supplies the ordering property required by the downstream theorem exists_sequential_schedule, which asserts existence of a one-per-tick schedule for any finite history. It thereby completes the constructive half of the T2 serialization result inside the Recognition Science framework, ensuring the pick-minimal recursion yields a valid topological order without extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Coherent rules fix deferral contradictions in medical taxonomies
"On a tree, (6) is solved by dynamic programming... F_v(i) = max_{j∈Γ_SE(i)} [log η_v(j|x) + Σ_{u∈C(v)} F_u(j)]. A single decode costs O(|V||A|^2), effectively linear since |A|=3."
-
Non-monotone triangular models identify all counterfactuals
"Theorem 1 proof: triangular induction along the causal order; injectivity/surjectivity of Γ_M by recursive inversion"