Conservative DAG Embedding

Abstract

Conservative DAG embeddings compose and preserve dependency reachability.

Theorem 1.1 (Conservative embeddings preserve reachability).

$$\begin{gathered} \forall edgeV:V\to V\to Prop,edgeW:W\to W\to Prop, \\ embedding:\mathrm{ConservativeEmbedding}\left(edgeV,edgeW\right),first,last:V, \\ \mathrm{ReflTransGen}\left(edgeV,first,last\right)\Rightarrow \\ \mathrm{ReflTransGen}\left(edgeW,\mathrm{toFun}\left(embedding,first\right),\mathrm{toFun}\left(embedding,last\right)\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let an embedding preserve and reflect direct dependency edges. Every reflexive-transitive path in the source maps to a path between the corresponding embedded endpoints.

The conclusion concerns preservation only. Reflection is carried by the structure binder but is not promoted to a stronger path equivalence in this theorem.

Theorem 1.2 (Composition maps paths by successive mapping).

$$\begin{array}{c}\forall edgeV:V\to V\to Prop,edgeW:W\to W\to Prop,\\ edgeZ:Z\to Z\to Prop,\forall firstEmbedding:\mathrm{ConservativeEmbedding}\left(edgeV,edgeW\right),\\ secondEmbedding:\mathrm{ConservativeEmbedding}\left(edgeW,edgeZ\right),source,target:V,\\ path:\mathrm{ReflTransGen}\left(edgeV,source,target\right),\\ (\mathrm{mapReachable}\left(\mathrm{comp}\left(secondEmbedding,firstEmbedding\right),path\right)=\mathrm{mapReachable}\left(secondEmbedding,\mathrm{mapReachable}\left(firstEmbedding,path\right)\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Quantify two composable conservative embeddings and a source path. Mapping through their composite yields the same proof-irrelevant reachability witness as mapping through them successively.

The equality is between path witnesses for the displayed path; it does not identify the two embedding structures themselves.

References

• Truth anchor: D5/S3/ConceptDynamics/DagSemantics/ConservativeDagEmbedding.map_reachable
• Truth anchor: D5/S3/ConceptDynamics/DagSemantics/ConservativeDagEmbedding.map_reachable_comp