Finite Ready Existence

Abstract

Every nonempty finite pending set has a ready minimum under a topological linear order.

Theorem 1.1 (A nonempty finite pending set has an executable node).

$$\begin{gathered} \forall edge:V\to V\to Prop,pending:\mathrm{Finset}\left(V\right), \\ [\mathrm{LinearOrder}\left(V\right)], \\ (\mathrm{StrictDependencyCoordinate}\left(edge,id\right)\wedge \mathrm{Nonempty}\left(pending\right))\Rightarrow \\ \mathrm{Nonempty}\left(\mathrm{executableFrontier}\left(edge,\mathrm{complement}\left(\mathrm{coeSet}\left(pending\right)\right),\mathrm{coeSet}\left(pending\right)\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DagSemantics/FiniteReadyExistence.complement_frontier_nonempty (✓ std3). ∎

Source. Repository-derived.

Commentary.

On a linearly ordered carrier, assume every dependency edge strictly increases the identity coordinate. A nonempty finite pending set then has a minimum with no pending prerequisite.

That minimum witnesses nonemptiness of the executable frontier over the pending complement. Finiteness is carried by the Finset binder and the linear order remains an instance binder.

References

• Truth anchor: D5/S3/ConceptDynamics/DagSemantics/FiniteReadyExistence.complement_frontier_nonempty
• Dependency: D5/S3/ConceptDynamics/DagSemantics/ExecutableFrontier
• Dependency: D5/S3/ConceptDynamics/DagSemantics/StrictDependencyCoordinate