Graph.Markov­Equiv

Markov equivalence of DAGs (Verma–Pearl)

The Verma–Pearl characterization of Markov equivalence (Verma & Pearl, Equivalence and synthesis of causal models, 1990): two directed acyclic graphs on the same finite vertex set imply exactly the same d-separation statements, and hence the same conditional-independence constraints, if and only if they have the same skeleton (the same adjacent pairs) and the same v-structures (colliders a → b ← c with a and c non-adjacent). The forward direction reads the skeleton and v-structures off the d-separation relation; the converse shows that two such graphs are linked by reversals of covered edges, each of which preserves every d-separation. The development also proves the moralization criterion: for pairwise-disjoint sets, d-separation is the same as separation in the moral graph of the ancestral set.

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. * 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), and Moralization.lean (the ancestral moral graph criterion for d-separation). The development reuses the existing d-separation engine (Causalean.Graph.DSep).

The higher-layer companion Causalean.SCM.Do.MarkovEquivDistributional connects this graph notion to distributions and proves SCM.distMarkovEquiv_of_markovEquiv; it is not imported by this file.

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 Causalean.Graph.MarkovEquiv) 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.

The first three relations have decidable instances on a finite vertex type. MarkovEquiv is instead the semantic relation quantified over all finite vertex sets. 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 induction for the 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. The public helper exists_covered_reversed_edge gives the key one-step progress result underlying Andersson–Madigan–Perlman (1997), Lemma 3.2. A private strong induction on the number of oppositely oriented edges (edgeDiffCount) combines each step with markovEquiv_flipEdge and MarkovEquiv.trans to prove the semantic-equivalence theorem. This module does not expose a finite reversal sequence or a finite-chain certificate.

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 Verma–Pearl equivalence 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 walk, 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.