Graph.Markov­Equiv

Markov equivalence of DAGs (Verma–Pearl) — umbrella

Entry point for the formalization of the Verma–Pearl characterization of Markov equivalence (Verma & Pearl, Equivalence and synthesis of causal models, 1990): two directed acyclic graphs declare the same conditional-independence constraints exactly when they have the same skeleton and the same v-structures. Import this file for the whole development; the headline result is stated here so it is not buried among the supporting files.

Main results

* MarkovEquiv (Defs.lean) — two DAGs declare the same d-separations. * markovEquiv_iff_sameSkeleton_sameImmoralities (this file) — the flagship. Two DAGs are Markov equivalent iff they have the same skeleton (SameSkeleton, undirected adjacency) and the same v-structures (SameImmoralities, colliders with non-adjacent parents). The constraint-based characterization underlying PC/FCI/GES and the CPDAG. * distMarkovEquiv_of_markovEquiv (Distributional.lean) — graph-level Markov equivalence implies distributional Markov equivalence (same distributions have the two DAGs as I-maps), via the global Markov bridge isGlobalIMap_dag_self. * DAG.dSep_iff_moralSep (Moralization.lean) — the Lauritzen moralization criterion: d-separation in a DAG is equivalent to graph separation in the moral graph of the ancestral closure.

Supporting machinery

Readoff.lean (easy direction — skeleton and v-structures are read off the d-separation relation), Transfer.lean (hard direction — same skeleton + v-structures transfer every d-separation), Distributional.lean (the I-map / faithfulness layer connecting the graph notion to distributions), and Moralization.lean (the ancestral moral graph criterion for d-separation). The development reuses the existing d-separation engine (Causalean.Graph.DSep) and the global Markov property (Causalean.SCM.Do.GlobalMarkov).

Markov equivalence of DAGs — basic definitions

This file introduces the combinatorial vocabulary for the Verma–Pearl characterization of Markov equivalence. Two directed acyclic graphs on the same vertices are Markov equivalent when they encode exactly the same d-separation statements, i.e. the same conditional-independence constraints. The Verma–Pearl theorem (proved in the umbrella file) says this happens precisely when the graphs share a skeleton and the same v-structures (immoralities).

The definitions here are:

* DAG.IsImmorality G a b c — there is a v-structure (immorality) a → b ← c whose two parents a, c are non-adjacent and distinct; * SameSkeleton G₁ G₂ — the two graphs have the same undirected adjacency; * SameImmoralities G₁ G₂ — the two graphs have the same v-structures; * MarkovEquiv G₁ G₂ — the two graphs declare the same d-separations.

All of these are decidable on a finite vertex type. The underlying undirected adjacency is the existing DAG.UAdj (a and b joined by an edge in either direction) and a collider a → b ← c is DAG.IsCollider.

Covered-edge reversal (the Andersson–Madigan–Perlman route)

This file develops the covered-edge reversal route to the hard direction of Verma–Pearl, following Andersson, Madigan and Perlman (1997), A characterization of Markov equivalence classes for acyclic digraphs, Appendix B. The route proves the hard direction through covered-edge reversals rather than through moralization.

A directed edge a → b is covered when a and b have the same parents apart from the edge itself (pa(a) = pa(b) \ {a}); equivalently every other vertex is a parent of a iff it is a parent of b. The three pillars are:

* Reversibility (AMP Lemma 3.1): a covered edge can be reversed and the result is still an acyclic digraph with the same skeleton and the same immoralities (flipEdge_*). * Per-step invariance: reversing one covered edge preserves all d-separations, hence Markov equivalence (markovEquiv_flipEdge). This is the analytic core. * Decomposition (AMP Lemma 3.2): two ADGs with the same skeleton and same immoralities are connected by a finite sequence of single covered-edge reversals (exists_covered_reversed_edge + the assembly).

The flipped graph is materialised with DAG.ofAcyclic (AcyclicConstruct.lean).

Covered-edge decomposition (AMP Lemma 3.2) + Verma–Pearl hard direction

This file assembles the covered-edge route to the hard direction of Verma–Pearl: DAGs with the same skeleton and the same immoralities are Markov equivalent. Following Andersson–Madigan–Perlman (1997) Lemma 3.2, two such DAGs are connected by a finite chain of single covered-edge reversals; markovEquiv_flipEdge (CoveredReversal.lean) handles each step, and MarkovEquiv.trans chains them. The induction is on the number of oppositely oriented edges (edgeDiffCount).

Markov equivalence — the distributional I-map layer

The graph-level MarkovEquiv (same d-separations) is connected here to distributions. A distribution μ is a global I-map of a DAG G when every d-separation of G is a conditional independence of μ; it is faithful to G when, conversely, every such conditional independence reflects an actual d-separation. The global Markov property (full_globalMarkov) says every structural causal model is a global I-map of its own DAG — this is the bridge from graphs to distributions, restated here as isGlobalIMap_dag_self.

The theorem in this file proves the easy direction:

* distMarkovEquiv_of_markovEquiv: graph-level Markov equivalence implies distributional Markov equivalence (the two DAGs are I-maps of exactly the same distributions). This is immediate from the definitions: the I-map condition is the same predicate when the d-separations agree.

The d-separation triples handled here are pairwise disjoint, matching the global Markov property; this is the standard setting for the I-map and faithfulness notions. The file states the I-map direction needed by the public Markov-equivalence API and leaves faithfulness-existence results outside this layer.

Markov equivalence — the moralization criterion

This file develops the moral graph of a DAG and the classical moralization criterion for d-separation. It proves that, for pairwise-disjoint source, target, and conditioning sets, d-separation is equivalent to separation in the moral graph of the ancestral set.

* DAG.MoralAdj G S u v — u and v are adjacent in the moral graph restricted to a ground set S: they are skeleton-adjacent (UAdj) or "married", i.e. they have a common child inside S. * DAG.MoralConn G S Z u v — u reaches v by a moral path inside S all of whose vertices avoid Z. * DAG.MoralSep G X Y Z — no x ∈ X is moral-connected to any y ∈ Y inside the ancestral set An(X ∪ Y ∪ Z) while avoiding Z. * DAG.dSep_iff_moralSep — the criterion: for pairwise-disjoint sets, d-separation is exactly moral separation in the ancestral set.

The file also proves that moral adjacency, moral steps, and moral connectivity are invariants of a graph's skeleton together with its v-structures, for a fixed ground set. The main Verma–Pearl hard direction used by the public umbrella theorem is assembled through the covered-edge route in Transfer.lean and Decompose.lean.

Markov equivalence — the easy direction (reading skeleton and v-structures off d-sep)

If two DAGs are Markov equivalent (declare the same d-separations) then they have the same skeleton and the same v-structures. The point is that both the skeleton and the v-structures are determined by the d-separation relation:

* Skeleton. Two distinct vertices are adjacent iff they cannot be d-separated by any set (adjacent_iff_not_dSeparable): an edge is an always-active path, and conversely two non-adjacent vertices are separated by the parents of the topologically later one. * V-structures. For an unshielded triple a — b — c (with a, c non-adjacent), the middle vertex b is a collider a → b ← c iff b lies in no separating set of a and c (immorality_iff_colliderSep) — the rule the PC algorithm uses to orient colliders.

Both characterizations are phrased purely in terms of dSep, so Markov equivalence transports them, giving sameSkeleton_of_markovEquiv and sameImmoralities_of_markovEquiv, hence the easy direction sameSkeleton_sameImmoralities_of_markovEquiv.