Reachability Projection Invariance

Abstract

Prerequisite and consequence closures depend only on reachability, not the chosen direct-edge presentation.

Theorem 1.1 (Reachability-equivalent graphs have equal prerequisite closures).

$$\begin{gathered} \forall firstEdge,secondEdge:V\to V\to Prop,targets:\mathrm{Set}\left(V\right), \\ \mathrm{SameReachability}\left(firstEdge,secondEdge\right)\Rightarrow \\ \mathrm{prerequisiteClosure}\left(firstEdge,targets\right)=\mathrm{prerequisiteClosure}\left(secondEdge,targets\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

If two direct-edge relations induce the same reflexive-transitive reachability relation, they generate identical prerequisite closures of every displayed target set.

The SameReachability hypothesis is explicit; equality of direct edge relations is neither assumed nor concluded.

Theorem 1.2 (Reachability-equivalent graphs have equal consequence closures).

$$\begin{gathered} \forall firstEdge,secondEdge:V\to V\to Prop,sources:\mathrm{Set}\left(V\right), \\ \mathrm{SameReachability}\left(firstEdge,secondEdge\right)\Rightarrow \\ \mathrm{consequenceClosure}\left(firstEdge,sources\right)=\mathrm{consequenceClosure}\left(secondEdge,sources\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

For the same pair of reachability-equivalent presentations, consequence closures of a displayed source set are equal.

The theorem changes only the edge presentation and holds the source set fixed on both sides.

References

• Truth anchor: D5/S3/ConceptDynamics/DagCompletion/ReachabilityProjectionInvariance.consequenceClosure_eq
• Truth anchor: D5/S3/ConceptDynamics/DagCompletion/ReachabilityProjectionInvariance.prerequisiteClosure_eq
• Dependency: D5/S3/ConceptDynamics/DagCompletion/ConsequenceClosure
• Dependency: D5/S3/ConceptDynamics/DependencyTopology/DependencyReachabilityOrder