Prerequisite Closure

Abstract

Reachability generates the least predecessor-closed set containing a target set.

Theorem 1.1 (Prerequisite closure is the least closed superset).

$$\begin{gathered} \forall edge:V\to V\to Prop,targets,closed:\mathrm{Set}\left(V\right), \\ (targets\subseteq closed\wedge \mathrm{PredecessorClosed}\left(edge,closed\right))\Rightarrow \\ \mathrm{prerequisiteClosure}\left(edge,targets\right)\subseteq closed. \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Fix target and closed sets. If the closed set contains every target and is closed under direct prerequisites, it contains the full prerequisite closure generated by reachability.

Both containment and predecessor closure are explicit antecedents. The conclusion is only the resulting subset relation.

References

• Truth anchor: D5/S3/ConceptDynamics/DagSemantics/PrerequisiteClosure.prerequisiteClosure_least
• Dependency: D5/S3/ConceptDynamics/DependencyTopology/DependencyReachabilityOrder