def CordialMiners.topoSources {H : Type u_1} [LinearOrder H] (deps : H → Finset H) (remaining : Finset H) : Finset H

The sources of the dependency graph restricted to the still-unemitted set: items whose dependencies all lie outside remaining (already emitted, or never in the graph).

Equations

• CordialMiners.topoSources deps remaining = {x ∈ remaining | deps x ∩ remaining = ∅}

theorem CordialMiners.topoSources_subset {H : Type u_1} [LinearOrder H] (deps : H → Finset H) (remaining : Finset H) : topoSources deps remaining ⊆ remaining

A source is one of the unemitted items.

theorem CordialMiners.topoSources_dep {H : Type u_1} [LinearOrder H] {deps : H → Finset H} {remaining : Finset H} {x : H} (hx : x ∈ topoSources deps remaining) : deps x ∩ remaining = ∅

A source has no dependency left in the unemitted set.

def CordialMiners.topoAux {H : Type u_1} [LinearOrder H] (deps : H → Finset H) : ℕ → Finset H → List H

One round of Kahn's algorithm, driven by a fuel counter. With fuel left and a source available, emit the least source and recurse on the rest; otherwise stop.

Equations

• One or more equations did not get rendered due to their size.
• CordialMiners.topoAux deps 0 x✝ = []

def CordialMiners.topoSort {H : Type u_1} [LinearOrder H] (V : Finset H) (deps : H → Finset H) : List H

The concrete ordering: run the topological sort with fuel equal to the vertex count.

Equations

• CordialMiners.topoSort V deps = CordialMiners.topoAux deps V.card V

def CordialMiners.TopoSorted {H : Type u_1} (deps : H → Finset H) (L : List H) : Prop

A list is topologically sorted for deps when no item's dependency appears after it: for every way of splitting the list at an item y, none of y's dependencies sit in the tail.

Equations

• CordialMiners.TopoSorted deps L = ∀ (l₁ : List H) (y : H) (l₂ : List H), L = l₁ ++ y :: l₂ → ∀ p ∈ deps y, p ∉ l₂

theorem CordialMiners.topoAux_mem {H : Type u_1} [LinearOrder H] (deps : H → Finset H) (n : ℕ) (remaining : Finset H) {y : H} : y ∈ topoAux deps n remaining → y ∈ remaining

Every emitted item was in the working set it was drawn from.

theorem CordialMiners.topoAux_nodup {H : Type u_1} [LinearOrder H] (deps : H → Finset H) (n : ℕ) (remaining : Finset H) : (topoAux deps n remaining).Nodup

The output has no duplicates: each emitted item is erased from the working set, so it can never be picked again.

theorem CordialMiners.topoAux_topoSorted {H : Type u_1} [LinearOrder H] (deps : H → Finset H) (n : ℕ) (remaining : Finset H) : TopoSorted deps (topoAux deps n remaining)

The output respects dependencies: an item is emitted only when all its remaining dependencies are gone, so no dependency of an item ever appears after it.

theorem CordialMiners.topoSort_deterministic {H : Type u_1} [LinearOrder H] (V₁ V₂ : Finset H) (deps : H → Finset H) (h : V₁ = V₂) : topoSort V₁ deps = topoSort V₂ deps

TAU-04 realized concretely: the ordering is a pure function, so equal inputs give equal outputs.

theorem CordialMiners.topoSort_subset {H : Type u_1} [LinearOrder H] (V : Finset H) (deps : H → Finset H) {y : H} (hy : y ∈ topoSort V deps) : y ∈ V

Output-validity: every hash in the ordered output came from the input vertex set.

theorem CordialMiners.topoSort_nodup {H : Type u_1} [LinearOrder H] (V : Finset H) (deps : H → Finset H) : (topoSort V deps).Nodup

The ordered output has no duplicate positions.

theorem CordialMiners.topoSort_topoSorted {H : Type u_1} [LinearOrder H] (V : Finset H) (deps : H → Finset H) : TopoSorted deps (topoSort V deps)

The ordered output is topologically sorted: no dependency is ever placed after the item that depends on it. This is the causal-consistency guarantee of the deterministic ordering.

theorem CordialMiners.topoSources_nonempty_of_rank {H : Type u_1} [LinearOrder H] (deps : H → Finset H) {rank : H → ℕ} (hrank : ∀ (x p : H), p ∈ deps x → rank p < rank x) {remaining : Finset H} (hne : remaining.Nonempty) : (topoSources deps remaining).Nonempty

Under a strict rank (every dependency has smaller rank, so the graph is acyclic) a nonempty working set always has a source: the element of least rank, whose dependencies all rank below it and so cannot still be in the working set.

theorem CordialMiners.topoAux_complete {H : Type u_1} [LinearOrder H] (deps : H → Finset H) {rank : H → ℕ} (hrank : ∀ (x p : H), p ∈ deps x → rank p < rank x) (n : ℕ) (remaining : Finset H) : remaining.card ≤ n → ∀ {y : H}, y ∈ remaining → y ∈ topoAux deps n remaining

Completeness under a strict rank: with fuel at least the working-set size, every item is emitted. Acyclicity gives a source at every nonempty round, so the fuel is never exhausted early.

theorem CordialMiners.topoSort_complete {H : Type u_1} [LinearOrder H] (V : Finset H) (deps : H → Finset H) {rank : H → ℕ} (hrank : ∀ (x p : H), p ∈ deps x → rank p < rank x) {y : H} (hy : y ∈ V) : y ∈ topoSort V deps

TAU completeness: every input vertex appears in the ordered output (under acyclicity). Together with topoSort_subset and topoSort_nodup, the output lists exactly the input vertices, once each.