Well-Founded Frontier

Abstract

Every nonempty pending set has an executable node under a well-founded prerequisite relation.

Theorem 1.1 (A well-founded nonempty pending set has a frontier node).

$$\begin{gathered} \forall edge:V\to V\to Prop,pending:\mathrm{Set}\left(V\right), \\ (\mathrm{WellFounded}\left(edge\right)\wedge \mathrm{Nonempty}\left(pending\right))\Rightarrow \\ \mathrm{Nonempty}\left(\mathrm{executableFrontier}\left(edge,\mathrm{complement}\left(pending\right),pending\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DagCompletion/WellFoundedFrontier.complement_frontier_nonempty_of_wellFounded (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume the prerequisite relation is well-founded and the pending set is nonempty. A minimal pending element has no pending prerequisite.

That element witnesses nonemptiness of the executable frontier over the pending complement. No finiteness or linear order is assumed.

References

• Truth anchor: D5/S3/ConceptDynamics/DagCompletion/WellFoundedFrontier.complement_frontier_nonempty_of_wellFounded
• Dependency: D5/S3/ConceptDynamics/DagSemantics/ExecutableFrontier