Graph
Causal graphs: DAGs, d-separation via Bayes-Ball, SWIGs and their splits, and c-components.
DSep 24 core · 58 supporting · 7 submodules d-separation on directed acyclic graphs: the Bayes-Ball characterization, ancestral closures, moralization bridges, and equivalences between the criteria. MarkovEquiv 28 core · 55 supporting · 6 submodules 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-in
DAG 18 core · 24 supporting This file provides finite directed acyclic graphs. ★ DAG★ acyclic_of_topoOrder
Directed Acyclic Graphs
This file provides finite directed acyclic graphs. A DAG is represented by a
decidable edge relation together with the standard acyclicity condition: no
vertex reaches itself along a directed path (∀ v, ¬ Relation.TransGen edge v v).
This is the textbook definition, and it is the entire data of the structure — a
DAG is determined by its edge relation.
A topological numbering is not part of the definition; it is derived. The
strict ancestors of a vertex are computed by a finite backward-reachability
fixpoint (ancClosure), which yields both a decidable ancestor relation
(decIsAncestor, order-free and computable) and a canonical strict-ancestor count
(ancestorRank, computable). The topological order
topoOrder v = rank v * |V| + enum v is built on the rank; it satisfies
injectivity (topoOrder_injective) and edge-consistency (topoOrder_lt), so
downstream constructions that need a topological order use it exactly as before.
topoOrder is noncomputable because the tie-breaking enumeration of a bare
finite type needs a choice of ordering; it is used purely for its ordering
properties, never reduced on concrete values (decidable ancestry goes through
ancClosure).
This file also defines immediate neighborhoods (parents, children), strict
reachability (isAncestor, isDescendant), finite ancestor/descendant sets,
set-level ancestry operations (ancestralSet, descendantsSet), non-descendants,
and roots.
References
- Basic Concepts.tex, Definition 1 (Directed Acyclic Graph)
structure DAG reviewed
⚑ flagged
Causalean
A Directed Acyclic Graph on a finite vertex type: a decidable edge relation together with the condition that no vertex is connected to itself by a directed path — the transitive closure of the edge relation is irreflexive. Irreflexivity of the transitive closure is exactly the statement that the graph has no directed cycle.
Definition (Lean source)
parameters
V :
fields
The edge relation: `edge u v` means there is a directed edge from `u` to `v`.
edge :
V → V → Prop
Decidability of the edge relation.
decEdge :
DecidableRel edge
**Acyclicity.** No vertex reaches itself along a directed path: the
transitive closure of `edge` is irreflexive. Equivalently, the graph has no
directed cycle. This is the defining property of a DAG.
acyclic :
∀ v, ¬ TransGen edge v v
def parents reviewed
⚑ flagged
Causalean.DAG
The parents of v in G: all vertices u such that (u, v) ∈ E.
def children reviewed
⚑ flagged
Causalean.DAG
The children of v in G: all vertices w such that (v, w) ∈ E.
inductive isAncestor reviewed
⚑ flagged
Causalean.DAG
isAncestor G u v means u is an ancestor of v: there is a directed path from u to v. Defined inductively as the transitive closure of the edge relation.
Definition (Lean source)
inductive isAncestor : V → V → Prop
| edge {u v : V} : G.edge u v → isAncestor u v
| trans {u w v : V} : isAncestor u w → G.edge w v → isAncestor u v
def isDescendant reviewed
⚑ flagged
Causalean.DAG
u is a descendant of v in the DAG exactly when there is a directed path from v to u, equivalently when v is an ancestor of u.
Definition (Lean source)
def isDescendant (u v : V) : Prop := G.isAncestor v u
def ancStep reviewed
⚑ flagged
Causalean.DAG
One backward reachability step: enlarge S by the parents of every vertex in S. Iterating this from G.parents v accumulates all strict ancestors of v.
def ancClosure reviewed
⚑ flagged
Causalean.DAG
The strict ancestors of v: all vertices u with a directed path u ⇝ v, computed by iterating the backward-parent step |V| times starting from v's parents. |V| iterations suffice because the accumulating set is an increasing chain of subsets of a |V|-element type, hence reaches its fixpoint.
Definition (Lean source)
def ancestors reviewed
⚑ flagged
Causalean.DAG
The ancestors of v in G: all vertices u such that u is an ancestor of v.
def descendants reviewed
⚑ flagged
Causalean.DAG
The descendants of v in G: all vertices w such that v is an ancestor of w.
Definition (Lean source)
def descendants (v : V) : Finset V :=
Finset.univ.filter (fun w => G.isAncestor v w)
def ancestorsSet reviewed
⚑ flagged
Causalean.DAG
The ancestors of a set S: all vertices that are ancestors of some vertex in S.
Definition (Lean source)
def ancestorsSet (S : Finset V) : Finset V :=
Finset.univ.filter (fun u => ∃ v ∈ S, G.isAncestor u v)
def ancestralSet reviewed
⚑ flagged
Causalean.DAG
The ancestral set of S: the set S together with all its ancestors (S ∪ G.ancestorsSet S).
Definition (Lean source)
def descendantsSet reviewed
⚑ flagged
Causalean.DAG
The descendants of a set S: all vertices that are descendants of some vertex in S.
Definition (Lean source)
def descendantsSet (S : Finset V) : Finset V :=
Finset.univ.filter (fun w => ∃ v ∈ S, G.isAncestor v w)
def nonDescendants reviewed
⚑ flagged
Causalean.DAG
The non-descendants of v: all vertices that are NOT descendants of v (and not v itself).
Definition (Lean source)
def nonDescendants (v : V) : Finset V :=
Finset.univ.filter (fun w => ¬G.isAncestor v w ∧ w ≠ v)
def ancestorRank reviewed
⚑ flagged
Causalean.DAG
The rank of v: the number of strict ancestors of v. Along an edge the strict-ancestor set strictly grows, so the rank strictly increases; this makes it the basis of a topological numbering.
Definition (Lean source)
def ancestorRank (v : V) : ℕ := (G.ancClosure v).card
def topoOrder reviewed
⚑ flagged
Causalean.DAG
The topological order derived from the DAG: assign each vertex the value rank v * |V| + enum v, where rank v counts the strict ancestors of v (the computable ancestorRank) and enum : V ↪ Fin |V| breaks ties. The result is a natural number that strictly increases along edges (topoOrder_lt) and is injective (topoOrder_injective).
def isRoot reviewed
⚑ flagged
Causalean.DAG
A vertex is a root if it has no parents (G.parents v = ∅).
Definition (Lean source)
def isRoot (v : V) : Prop := G.parents v = ∅
def roots reviewed
⚑ flagged
Causalean.DAG
The set of all root nodes.
Definition (Lean source)
def roots : Finset V :=
Finset.univ.filter (fun v => G.isRoot v)
theorem acyclic_of_topoOrder reviewed
⚑ flagged
Causalean.DAG
Acyclicity from a topological ranking. Given an edge relation e on V and a ranking function τ into a type equipped with a transitive, irreflexive relation r, if τ strictly increases (with respect to r) along every edge of e, then e has no directed cycle: no vertex is reachable from itself via the transitive closure of e.
Formal statement
Proof (Lean source)
theorem acyclic_of_topoOrder {W : Type*} {r : W → W → Prop} [IsTrans W r] [Irrefl r]
{e : V → V → Prop} {τ : V → W}
(hτ : ∀ u v, e u v → r (τ u) (τ v)) : ∀ v, ¬ TransGen e v v := by
have key : ∀ {a b : V}, TransGen e a b → r (τ a) (τ b) := by
intro a b h
induction h with
| single hab => exact hτ _ _ hab
| tail _ hbc ih => exact IsTrans.trans _ _ _ ih (hτ _ _ hbc)
intro v hv
exact absurd (key hv) (Std.Irrefl.irrefl _)
24 supporting declarations (lemmas, instances)
-
mem_parentstheorem — Membership characterization for parents: u ∈ G.parents v ↔ G.edge u v.hypothesesv u :Vconclusionu ∈ G.parents v ↔ G.edge u vProof (Lean source)
theorem mem_parents {v u : V} : u ∈ G.parents v ↔ G.edge u v := by simp [parents] -
mem_childrentheorem — Membership characterization for children: w ∈ G.children v ↔ G.edge v w.hypothesesv w :Vconclusionw ∈ G.children v ↔ G.edge v wProof (Lean source)
theorem mem_children {v w : V} : w ∈ G.children v ↔ G.edge v w := by simp [children] -
isAncestor_iff_transGentheorem — The inductive ancestor relation coincides with Relation.TransGen of the edge relation: both are the transitive closure of the edge relation.Proof (Lean source)
theorem isAncestor_iff_transGen {u v : V} : G.isAncestor u v ↔ TransGen G.edge u v := by constructor · intro h induction h with | edge he => exact Relation.TransGen.single he | trans _ he ih => exact ih.tail he · intro h induction h with | single he => exact isAncestor.edge he | tail _ he ih => exact isAncestor.trans ih he -
irrefltheorem — No vertex has an edge to itself (a directed self-loop would be a length-one cycle).hypothesesv :Vconclusion¬G.edge v vProof (Lean source)
theorem irrefl (v : V) : ¬G.edge v v := by intro h exact G.acyclic v (Relation.TransGen.single h) -
asymmtheorem — If there is an edge from u to v, then there is no edge from v to u (a two-cycle is forbidden by acyclicity).hypothesesu v :Vh :G.edge u vconclusion¬G.edge v u -
isAncestor_irrefltheorem — Ancestor relation is irreflexive: no vertex is its own ancestor (this is acyclicity, restated for the inductive ancestor relation).hypothesesv :Vconclusion¬G.isAncestor v vProof (Lean source)
theorem isAncestor_irrefl (v : V) : ¬G.isAncestor v v := by intro h exact G.acyclic v (G.isAncestor_iff_transGen.mp h) -
isAncestor_transtheorem — Ancestor relation is transitive.hypothesesu v w :Vh1 :G.isAncestor u vh2 :G.isAncestor v wconclusionG.isAncestor u wProof (Lean source)
theorem isAncestor_trans {u v w : V} (h1 : G.isAncestor u v) (h2 : G.isAncestor v w) : G.isAncestor u w := by induction h2 with | edge he => exact isAncestor.trans h1 he | trans _ he ih => exact isAncestor.trans ih he -
isAncestor_childtheorem — First-step decomposition: if u is an ancestor of v, then either edge u v or there exists a child c of u such that c is an ancestor of v.hypothesesu v :Vh :G.isAncestor u vconclusionG.edge u v ∨ ∃ c, G.edge u c ∧ G.isAncestor c vProof (Lean source)
theorem isAncestor_child {u v : V} (h : G.isAncestor u v) : G.edge u v ∨ ∃ c, G.edge u c ∧ G.isAncestor c v := by induction h with | edge he => exact inl he | trans _ he' ih => rcases ih with he | ⟨c, huc, hcw⟩ · exact inr ⟨_, he, isAncestor.edge he'⟩ · exact inr ⟨c, huc, isAncestor.trans hcw he'⟩ -
subset_iterate_ancSteptheorem — Any finite set of graph nodes remains contained after applying the graph's ancestor-step operation any number of times.Proof (Lean source)
theorem subset_iterate_ancStep (S : Finset V) (k : ℕ) : S ⊆ (G.ancStep)^[k] S := by induction k with | zero => simp | succ k ih => rw [Function.iterate_succ_apply'] exact ih.trans (G.subset_ancStep _) -
le_card_iteratetheorem — If each of a specified number of successive applications of a function on finite sets strictly increases cardinality, the final set has grown by at least that number.hypothesesconclusion(f^[0] S₀).card + k ≤ (f^[k] S₀).cardProof (Lean source)
theorem le_card_iterate (f : Finset V → Finset V) (S₀ : Finset V) (k : ℕ) (hstrict : ∀ j, j < k → (f^[j] S₀).card < (f^[j + 1] S₀).card) : (f^[0] S₀).card + k ≤ (f^[k] S₀).card := by induction k with | zero => simp | succ k ih => have ihk := ih (fun j hj => hstrict j (Nat.lt_succ_of_lt hj)) have hlast := hstrict k (Nat.lt_succ_self k) omega -
ancClosure_closedtheorem — Every parent of a vertex in its computed ancestor set also belongs to that ancestor set.hypothesesv :Vx :Vhx :x ∈ G.ancClosure vconclusionG.parents x ⊆ G.ancClosure vProof (Lean source)
theorem ancClosure_closed (v : V) {x : V} (hx : x ∈ G.ancClosure v) : G.parents x ⊆ G.ancClosure v := by intro p hp have hbu : p ∈ (G.ancClosure v).biUnion G.parents := Finset.mem_biUnion.mpr ⟨x, hx, hp⟩ have hstep : p ∈ G.ancStep (G.ancClosure v) := by rw [ancStep, mem_union]; exact inr hbu rwa [G.ancStep_ancClosure v] at hstep -
isAncestor_mem_of_closedtheorem — A finite set that contains every parent of each of its vertices contains every ancestor of each vertex it contains.hypothesesconclusionw ∈ T → u ∈ TProof (Lean source)
theorem isAncestor_mem_of_closed {T : Finset V} (hT : ∀ x ∈ T, G.parents x ⊆ T) {u w : V} (h : G.isAncestor u w) : w ∈ T → u ∈ T := by induction h with | edge e => intro hw; exact hT _ hw (G.mem_parents.mpr e) | trans _ e ih => intro hw; exact ih (hT _ hw (G.mem_parents.mpr e)) -
mem_ancClosuretheorem — Membership in the backward-reachability fixpoint is exactly ancestry: a vertex lies in G.ancClosure v iff it is an ancestor of v. This makes the ancestor relation decidable using only the (decidable) edge relation, with no reference to any topological order.hypothesesu v :Vconclusionu ∈ G.ancClosure v ↔ G.isAncestor u vProof (Lean source)
theorem mem_ancClosure {u v : V} : u ∈ G.ancClosure v ↔ G.isAncestor u v := by constructor · intro hu have hbase : ∀ x ∈ G.parents v, G.isAncestor x v := fun x hx => isAncestor.edge (G.mem_parents.mp hx) exact G.iterate_ancStep_sound hbase (card V) u hu · intro h have hclosed : ∀ x ∈ G.ancClosure v, G.parents x ⊆ G.ancClosure v := fun x hx => G.ancClosure_closed v hx have hpar : G.parents v ⊆ G.ancClosure v := G.subset_iterate_ancStep (G.parents v) (card V) cases h with | edge e => exact hpar (G.mem_parents.mpr e) | trans h' e => exact G.isAncestor_mem_of_closed hclosed h' (hpar (G.mem_parents.mpr e)) -
decIsAncestorinstance — Decidability of the ancestor relation, computed from the edge relation alone via the backward-reachability fixpoint ancClosure.instance decIsAncestor : DecidableRel G.isAncestor := fun u v => decidable_of_iff _ (G.mem_ancClosure (u := u) (v := v)) -
mem_ancestorstheorem — Membership characterization for ancestors: u ∈ G.ancestors v ↔ G.isAncestor u v.hypothesesv u :Vconclusionu ∈ G.ancestors v ↔ G.isAncestor u vProof (Lean source)
theorem mem_ancestors {v u : V} : u ∈ G.ancestors v ↔ G.isAncestor u v := by simp [ancestors] -
mem_descendantstheorem — Membership characterization for descendants: w ∈ G.descendants v ↔ G.isAncestor v w.hypothesesv w :Vconclusionw ∈ G.descendants v ↔ G.isAncestor v wProof (Lean source)
theorem mem_descendants {v w : V} : w ∈ G.descendants v ↔ G.isAncestor v w := by simp [descendants] -
parents_subset_ancestorstheorem — Parents are a subset of ancestors.hypothesesv :VconclusionG.parents v ⊆ G.ancestors vProof (Lean source)
theorem parents_subset_ancestors (v : V) : G.parents v ⊆ G.ancestors v := by intro u hu rw [mem_ancestors] exact isAncestor.edge (G.mem_parents.mp hu) -
children_subset_descendantstheorem — Children are a subset of descendants.hypothesesv :VconclusionG.children v ⊆ G.descendants vProof (Lean source)
theorem children_subset_descendants (v : V) : G.children v ⊆ G.descendants v := by intro w hw rw [mem_descendants] exact isAncestor.edge (G.mem_children.mp hw) -
ancestorRank_lt_of_edgetheorem — Along an edge the strict-ancestor count strictly increases.hypothesesa b :Vhab :G.edge a bconclusionG.ancestorRank a < G.ancestorRank bProof (Lean source)
theorem ancestorRank_lt_of_edge {a b : V} (hab : G.edge a b) : G.ancestorRank a < G.ancestorRank b := by unfold ancestorRank apply Finset.card_lt_card rw [Finset.ssubset_iff_of_subset] · refine ⟨a, ?_, ?_⟩ · rw [mem_ancClosure]; exact isAncestor.edge hab · rw [mem_ancClosure]; exact G.isAncestor_irrefl a · intro w hw rw [mem_ancClosure] at hw ⊢ exact G.isAncestor_trans hw (isAncestor.edge hab) -
topoOrder_injectivetheorem — The derived topological order is injective, so it provides a canonical total order on the finite vertex type.conclusionInjective G.topoOrderProof (Lean source)
theorem topoOrder_injective : Injective G.topoOrder := by intro u v huv unfold topoOrder at huv have hu : (Fintype.equivFin V u).val < card V := (Fintype.equivFin V u).isLt have hv : (Fintype.equivFin V v).val < card V := (Fintype.equivFin V v).isLt have hmod : (Fintype.equivFin V u).val = (Fintype.equivFin V v).val := by have := congrArg (· % card V) huv simpa [Nat.mul_add_mod, Nat.mod_eq_of_lt hu, Nat.mod_eq_of_lt hv] using this have : (Fintype.equivFin V u) = (Fintype.equivFin V v) := Fin.ext hmod exact (Fintype.equivFin V).injective this -
topoOrder_lttheorem — The derived topological order is edge-consistent: if there is an edge from u to v, then topoOrder u < topoOrder v. This witnesses acyclicity.conclusion∀ u vifG.edge u vthenG.topoOrder u < G.topoOrder vProof (Lean source)
theorem topoOrder_lt : ∀ u v, G.edge u v → G.topoOrder u < G.topoOrder v := by intro u v huv unfold topoOrder have hrank : G.ancestorRank u < G.ancestorRank v := G.ancestorRank_lt_of_edge huv have hv : (Fintype.equivFin V v).val < card V := (Fintype.equivFin V v).isLt have hu : (Fintype.equivFin V u).val < card V := (Fintype.equivFin V u).isLt have hle : G.ancestorRank u + 1 ≤ G.ancestorRank v := by omega have key : (G.ancestorRank u + 1) * card V ≤ G.ancestorRank v * card V := Nat.mul_le_mul hle (le_refl (card V)) have expand : (G.ancestorRank u + 1) * card V = G.ancestorRank u * card V + card V := by rw [Nat.add_mul, Nat.one_mul] omega -
isAncestor_topoOrder_lttheorem — Ancestors respect the topological order: if u is an ancestor of v then G.topoOrder u < G.topoOrder v, so ancestor pairs are strictly ordered by topoOrder.hypothesesu v :Vh :G.isAncestor u vconclusionG.topoOrder u < G.topoOrder vProof (Lean source)
theorem isAncestor_topoOrder_lt {u v : V} (h : G.isAncestor u v) : G.topoOrder u < G.topoOrder v := by induction h with | edge he => exact G.topoOrder_lt _ _ he | trans _ he ih => exact Nat.lt_trans ih (G.topoOrder_lt _ _ he) -
isAncestor_has_parenttheorem — Every vertex reached by a nonempty directed path has an incoming edge, namely the final edge of that path.Proof (Lean source)
theorem isAncestor_has_parent (G : DAG V) {u v : V} (h : G.isAncestor u v) : G.parents v ≠ ∅ := by intro hempty have hmem : ∀ w, w ∉ G.parents v := fun w => (Finset.eq_empty_iff_forall_notMem.mp hempty) w induction h with | edge he => exact hmem u (G.mem_parents.mpr he) | trans _ he _ => exact hmem _ (G.mem_parents.mpr he)
SWIG 18 core · 21 supporting This file defines the graph-theoretic structure of a Single World Intervention Graph (SWIG). ★ SWIGNode★ swig_fixed_are_roots★ swig_target_parents★ initialSWIG_random_edge★ initialSWIG_fixed_isolated★ SWIGGraph
Single World Intervention Graphs
This file defines the graph-theoretic structure of a Single World Intervention
Graph (SWIG). A base variable n : N has two SWIG nodes: .random n, used for
the natural random variable, and .fixed n, used for intervention values. The
shared value-space family swigΩ gives both copies the same measurable value
space as the base variable.
The core construction is swigDAG G targets. It keeps incoming edges into
targeted random nodes, reroutes outgoing edges from each targeted random node to
the corresponding fixed node, and leaves fixed nodes for non-targets isolated.
The interleaved order swigTopo proves that this edge relation is acyclic, and
the basic lemmas describe roots, target parents, and the initial no-intervention
SWIG.
The structure SWIGGraph packages a DAG on SWIG nodes together with the fixed,
observed, and unobserved node sets, the link map ι from fixed nodes to their
random counterparts, and root/classification invariants used by structural
causal models. The namespace also provides graph equivalence up to edge and
partition equality, plus parent/child classification lemmas. The monolithic
multi-target split operation is defined in Causalean.Graph.SWIGSplitMono.
inductive SWIGNode reviewed
⚑ flagged
Causalean
A node of a SWIG (Single World Intervention Graph) is either the random version of a base variable or its fixed intervention version, so the SWIG node set is the disjoint union of two copies of the base variable set.
Definition (Lean source)
inductive SWIGNode (N : Type*)
| random : N → SWIGNode N
| fixed : N → SWIGNode N
deriving DecidableEq, Repr
def equiv reviewed
⚑ flagged
Causalean.SWIGNode
Equivalence between SWIGNode N and N ⊕ N.
abbrev swigΩ reviewed
⚑ flagged
Causalean
Value-space family for the SWIG model. Both random and fixed versions of a node share the same value space as the original node: swigΩ(.random n) = Ω n and swigΩ(.fixed n) = Ω n. This matches the tex requirement X_d = X_{ι(d)}. Declared as abbrev so that swigΩ Ω (.random n) reduces to Ω n during type class synthesis.
def swigEdge reviewed
⚑ flagged
Causalean
The edge relation in a SWIG.
def swigTopo reviewed
⚑ flagged
Causalean
Topological order for the SWIG.
def swigDAG reviewed
⚑ flagged
Causalean
The SWIG DAG: the DAG on SWIGNode N constructed by node-splitting.
Definition (Lean source)
def swigDAG (G : DAG N) (targets : Finset N) : DAG (SWIGNode N) where
edge := swigEdge G targets
decEdge := swigEdge_decidable G targets
acyclic := DAG.acyclic_of_topoOrder (swigTopo_lt G targets)
def iotaMap reviewed
⚑ flagged
Causalean
The injection ι mapping each fixed intervention parameter to its random counterpart. In the SWIG, ι(fixed d) = random d.
theorem swig_fixed_are_roots reviewed
⚑ flagged
Causalean
For any base DAG G, any set of intervention targets, and any node n, the fixed copy of n has no parents in the single-world intervention graph built from G and targets.
Formal statement
theorem swig_target_parents reviewed
⚑ flagged
Causalean
For any base DAG G, any set of intervention targets, and any node d, the parents of the random copy of d in the single-world intervention graph are exactly the copies of d's original parents in G, each represented by its random version if it is not a target and by its fixed version if it is.
Formal statement
Proof (Lean source)
theorem swig_target_parents (G : DAG N) (targets : Finset N) (d : N) :
∀ x : SWIGNode N, x ∈ (swigDAG G targets).parents (.random d) ↔
∃ p, G.edge p d ∧ x = .random p ∧ p ∉ targets ∨
G.edge p d ∧ x = .fixed p ∧ p ∈ targets := by
intro x
rw [DAG.mem_parents]
show swigEdge G targets x (.random d) ↔ _
constructor
· intro hedge
cases x with
| random u =>
simp only [swigEdge] at hedge
exact ⟨u, inl ⟨hedge.1, rfl, hedge.2⟩⟩
| fixed f =>
simp only [swigEdge] at hedge
exact ⟨f, inr ⟨hedge.2, rfl, hedge.1⟩⟩
· intro ⟨p, hp⟩
rcases hp with ⟨hedge, rfl, hnt⟩ | ⟨hedge, rfl, ht⟩
· simp only [swigEdge]; exact ⟨hedge, hnt⟩
· simp only [swigEdge]; exact ⟨ht, hedge⟩
def initialSWIG reviewed
⚑ flagged
Causalean
The initial SWIG DAG with no intervention targets. All edges stay between random nodes; all fixed nodes are isolated. This is the DAG used by a standard causal model.
Definition (Lean source)
theorem initialSWIG_random_edge reviewed
⚑ flagged
Causalean
For any base DAG G and any nodes u, v, in the initial SWIG of G (the SWIG with no intervention targets), the random copies of u and v are joined by an edge exactly when u and v are joined by an edge in G.
Formal statement
Proof (Lean source)
theorem initialSWIG_random_edge (G : DAG N) (u v : N) :
(initialSWIG G).edge (.random u) (.random v) ↔ G.edge u v := by
simp [initialSWIG, swigDAG, swigEdge]
theorem initialSWIG_fixed_isolated reviewed
⚑ flagged
Causalean
For any base DAG G and any node n, the fixed copy of n has no parents in the initial SWIG of G (the SWIG with no intervention targets).
Formal statement
Proof (Lean source)
theorem initialSWIG_fixed_isolated (G : DAG N) (n : N) :
(initialSWIG G).parents (.fixed n) = ∅ :=
swig_fixed_are_roots G ∅ n
structure SWIGGraph reviewed
⚑ flagged
Causalean
A Single-World Intervention Graph (SWIG), G = (S, V, U, E, ι) (Definition 4 from Basic Concepts.tex): a directed acyclic graph on the SWIG nodes whose vertices are partitioned into fixed intervention nodes, observed random nodes, and unobserved random nodes, where every fixed node is genuinely of fixed form, every observed node is of random form, every unobserved node is of random form, and the observed and unobserved sets are disjoint. Every edge of the graph has both endpoints classified as fixed, observed, or unobserved; the map sending each fixed intervention node to its random counterpart lands inside the observed nodes; fixed nodes and unobserved nodes have no parents; a fixed-form node absent from the fixed set is isolated, with neither parents nor children; and every child of a classified node is observed.
Definition (Lean source)
parameters
N :
fields
The underlying DAG on SWIG nodes.
Fixed (intervention) nodes `S` as fixed SWIG nodes.
Observed/endogenous random nodes `V` as random SWIG nodes.
Unobserved/exogenous random nodes `U` as random SWIG nodes.
All elements of `fixed` are of the form `.fixed n`.
fixed_is_fixed :
∀ s ∈ fixed, ∃ n : N, s = SWIGNode.fixed n
All elements of `observed` are of the form `.random n`.
observed_is_random :
∀ v ∈ observed, ∃ n : N, v = SWIGNode.random n
All elements of `unobserved` are of the form `.random n`.
unobserved_is_random :
∀ u ∈ unobserved, ∃ n : N, u = SWIGNode.random n
`observed` and `unobserved` are disjoint.
obs_unobs_disjoint :
Disjoint observed unobserved
Every vertex participating in any edge of `dag` is classified as
fixed, observed, or unobserved. Trivially preserved under edge
removal, which is why it replaces the older `obs_unobs_cover_random`
that did not survive the `induce` operation.
dag_edges_classified :
∀ u v
if
dag.edge u v
then
u ∈ fixed ∪ observed ∪ unobserved ∧ v ∈ fixed ∪ observed ∪ unobserved
The image of `fixed` under `iotaMap` lies in `observed`.
fixed_image_in_observed :
∀ s ∈ fixed, iotaMap s ∈ observed
Fixed nodes are roots in `dag`.
fixed_are_roots :
∀ s ∈ fixed, dag.parents s = ∅
Unobserved nodes are roots in `dag`.
unobs_are_roots :
∀ u ∈ unobserved, dag.parents u = ∅
Any fixed-form node not listed in `fixed` is isolated in `dag`.
fixed_outside_fixed_isolated :
∀ n : N
if
SWIGNode.fixed n ∉ fixed
then
dag.parents (SWIGNode.fixed n) = ∅ ∧ dag.children (SWIGNode.fixed n) = ∅
Every child of any classified node is observed. This global
child-classification invariant is used to rule out outgoing edges into
fixed or latent-root nodes.
all_children_in_observed :
∀ u ∈ unobserved ∪ fixed ∪ observed, dag.children u ⊆ observed
def iota reviewed
⚑ flagged
Causalean.SWIGGraph
The canonical map ι : S → V sending each fixed intervention parameter to its random counterpart in observed, via iotaMap.
def iotaNode reviewed
⚑ flagged
Causalean.SWIGGraph
Evaluate ι as a SWIGNode (forgetting membership).
def iotaN reviewed
⚑ flagged
Causalean.SWIGGraph
ι at the level of original nodes N, using the fact that every s ∈ fixed is of the form .fixed n.
def isStandard reviewed
⚑ flagged
Causalean.SWIGGraph
A standard SWIG graph has no fixed (intervention) variables: S = ∅.
Definition (Lean source)
def isStandard (G : SWIGGraph N) : Prop := G.fixed = ∅
def Equivalent reviewed
⚑ flagged
Causalean.SWIGGraph
Equivalence of SWIG graphs, ignoring the particular topological order.
Definition (Lean source)
def Equivalent (G H : SWIGGraph N) : Prop :=
(∀ u v, G.dag.edge u v ↔ H.dag.edge u v) ∧
G.fixed = H.fixed ∧
G.observed = H.observed ∧
G.unobserved = H.unobserved
21 supporting declarations (lemmas, instances)
-
instDecidableEqSWIGNodeinstancederiving DecidableEq, Repr -
instReprSWIGNodeinstancederiving DecidableEq, Repr -
instMeasurableSpaceSwigΩinstance — The shared SWIG value-space family inherits measurable spaces from the base variables.instance instMeasurableSpaceSwigΩ {N : Type*} (Ω : N → Type*) [∀ n, MeasurableSpace (Ω n)] : ∀ sn, MeasurableSpace (swigΩ Ω sn) | .random _ => inferInstance | .fixed _ => inferInstance -
measurable_cast_familytheorem — Transporting a value along an equality of indices is measurable.hypothesesconclusionMeasurable (cast (congrArg X hab) : X a → X b)Proof (Lean source)
theorem measurable_cast_family {I : Type*} {X : I → Type*} [∀ i, MeasurableSpace (X i)] {a b : I} (hab : a = b) : Measurable (cast (congrArg X hab) : X a → X b) := by subst hab exact measurable_id -
measurable_family_casttheorem — A measurable function remains measurable after transporting its codomain index.hypothesesconclusionMeasurable (fun x => (h ▸ f x : X w))Proof (Lean source)
theorem measurable_family_cast {I γ : Type*} {X : I → Type*} [∀ i, MeasurableSpace (X i)] [MeasurableSpace γ] {v w : I} (h : v = w) {f : γ → X v} (hf : Measurable f) : Measurable (fun x => (h ▸ f x : X w)) := by subst h exact hf -
instStandardBorelSpaceSwigΩinstance — The shared SWIG value-space family inherits standard Borel spaces from the base variables.instance instStandardBorelSpaceSwigΩ {N : Type*} (Ω : N → Type*) [∀ n, MeasurableSpace (Ω n)] [∀ n, StandardBorelSpace (Ω n)] : ∀ sn, StandardBorelSpace (swigΩ Ω sn) | .random _ => inferInstance | .fixed _ => inferInstance -
instNonemptySwigΩinstance — The shared SWIG value-space family is nonempty whenever each base value space is nonempty.instance instNonemptySwigΩ {N : Type*} (Ω : N → Type*) [∀ n, Nonempty (Ω n)] : ∀ sn, Nonempty (swigΩ Ω sn) | .random _ => inferInstance | .fixed _ => inferInstance -
swigEdge_decidableinstance — The SWIG edge relation is decidable whenever the base variables and target set are finite.instance swigEdge_decidable (G : DAG N) (targets : Finset N) : DecidableRel (swigEdge G targets) := by intro a b cases a <;> cases b <;> simp only [swigEdge] <;> infer_instance -
swigTopo_lttheorem — Every SWIG edge points from a lower to a higher position in the interleaved topological order.hypothesesProof (Lean source)
theorem swigTopo_lt (G : DAG N) (targets : Finset N) : ∀ u v, swigEdge G targets u v → swigTopo G u < swigTopo G v := by intro u v h cases u with | random u => cases v with | random v => simp only [swigEdge] at h simp only [swigTopo] have := G.topoOrder_lt u v h.1 omega | fixed _ => exact absurd h (by simp [swigEdge]) | fixed d => cases v with | random v => simp only [swigEdge] at h simp only [swigTopo] have := G.topoOrder_lt d v h.2 omega | fixed _ => exact absurd h (by simp [swigEdge]) -
swig_random_root_of_roottheorem — If n is a root in G, then random n is a root in the SWIG.hypothesesProof (Lean source)
theorem swig_random_root_of_root (G : DAG N) (targets : Finset N) (n : N) (hroot : G.parents n = ∅) : (swigDAG G targets).parents (.random n) = ∅ := by rw [Finset.eq_empty_iff_forall_notMem] intro x hx rw [DAG.mem_parents] at hx replace hx : swigEdge G targets x (.random n) := hx cases x with | random u => obtain ⟨hedge, _⟩ := hx have : u ∈ G.parents n := G.mem_parents.mpr hedge simp [hroot] at this | fixed d => obtain ⟨_, hedge⟩ := hx have : d ∈ G.parents n := G.mem_parents.mpr hedge simp [hroot] at this -
iotaNode_eq_iotaMaptheorem — Forgetting the membership proof in the graph-level link map gives the node-level link map.Proof (Lean source)
@[simp] theorem iotaNode_eq_iotaMap (G : SWIGGraph N) (s : {s // s ∈ G.fixed}) : G.iotaNode s = iotaMap s := rfl -
refltheorem — SWIG graph equivalence is reflexive.Proof (Lean source)
@[refl] theorem Equivalent.refl (G : SWIGGraph N) : Equivalent G G := by unfold Equivalent refine intro ?hedge ?hfix · intro u v; exact Iff.rfl · exact intro rfl (intro rfl rfl) -
symmtheorem — SWIG graph equivalence is symmetric.Proof (Lean source)
@[symm] theorem Equivalent.symm {G H : SWIGGraph N} : Equivalent G H → Equivalent H G := by intro h rcases h with ⟨hedge, hfix, hobs, hunobs⟩ refine intro ?hedge' ?rest · intro u v have := hedge u v exact this.symm · refine intro ?hfix' ?hobs_unobs' · simp [hfix] · refine intro ?hobs' ?hunobs' · simp [hobs] · simp [hunobs] -
transtheorem — SWIG graph equivalence is transitive.Proof (Lean source)
@[trans] theorem Equivalent.trans {G H K : SWIGGraph N} : Equivalent G H → Equivalent H K → Equivalent G K := by intro hGH hHK rcases hGH with ⟨hedgeGH, hfixGH, hobsGH, hunobsGH⟩ rcases hHK with ⟨hedgeHK, hfixHK, hobsHK, hunobsHK⟩ refine intro ?hedge ?rest · intro u v exact Iff.trans (hedgeGH u v) (hedgeHK u v) · refine intro ?hfix ?hobs_unobs · -- fixed sets simp [hfixGH, hfixHK] · refine intro ?hobs ?hunobs · -- observed sets simp [hobsGH, hobsHK] · -- unobserved sets simp [hunobsGH, hunobsHK] -
parents_eqtheorem — Equivalent SWIGGraphs have the same parents Finset at every node.hypothesesconclusionG.dag.parents v = H.dag.parents v -
parent_classifiedtheorem — If u is a parent of v in G, then u is classified (fixed, observed, or unobserved).hypothesesconclusionu ∈ G.fixed ∪ G.observed ∪ G.unobservedProof (Lean source)
theorem parent_classified (G : SWIGGraph N) {u v : SWIGNode N} (h : u ∈ G.dag.parents v) : u ∈ G.fixed ∪ G.observed ∪ G.unobserved := (G.dag_edges_classified u v (G.dag.mem_parents.mp h)).1 -
child_classifiedtheorem — If w is a child of u in G, then w is classified (fixed, observed, or unobserved).hypothesesconclusionw ∈ G.fixed ∪ G.observed ∪ G.unobservedProof (Lean source)
theorem child_classified (G : SWIGGraph N) {u w : SWIGNode N} (h : w ∈ G.dag.children u) : w ∈ G.fixed ∪ G.observed ∪ G.unobserved := (G.dag_edges_classified u w (G.dag.mem_children.mp h)).2
Induce 4 core · 5 supporting This file defines graph-level restriction of a Single World Intervention Graph to an observed subset. ★ inducedDag_edge_iff★ induce
Induced SWIG Subgraphs
This file defines graph-level restriction of a Single World Intervention Graph to an observed subset. The construction keeps the relevant observed nodes, retains only fixed nodes whose random counterparts remain observed, retains only latent roots that feed those observed nodes, and filters edges to the resulting active vertex set.
The auxiliary inducedEdge and inducedDag restrict the ambient DAG while
preserving its topological order. The main constructor SWIGGraph.induce builds
the restricted SWIG and proves all structural invariants; inducedDag_edge_iff
and the parent/child subset lemmas expose the relationship with the ambient
graph. The theorem induce_isAncestor_mem_R shows that every nontrivial
descendant in an induced subgraph lies in the retained observed part of R.
def inducedEdge reviewed
⚑ flagged
Causalean.SWIGGraph
The edge relation of G.dag restricted to a given active vertex set: keep an edge iff both endpoints are in active.
Definition (Lean source)
def inducedEdge (active : Finset (SWIGNode N)) (u v : SWIGNode N) : Prop :=
G.dag.edge u v ∧ u ∈ active ∧ v ∈ active
def inducedDag reviewed
⚑ flagged
Causalean.SWIGGraph
The DAG obtained by filtering G.dag's edges to those with both endpoints in active. Acyclicity follows from the parent graph via the parent's topological order (every restricted edge is an original edge).
lemma inducedDag_edge_iff reviewed
⚑ flagged
Causalean.SWIGGraph
For a set of active nodes and vertices u, v, u and v are joined by an edge of the DAG restricted to the active nodes exactly when they are joined by an edge of the original DAG and both are active.
Formal statement
Proof (Lean source)
lemma inducedDag_edge_iff (active : Finset (SWIGNode N)) (u v : SWIGNode N) :
(G.inducedDag active).edge u v ↔
G.dag.edge u v ∧ u ∈ active ∧ v ∈ active := Iff.rfl
def induce reviewed
⚑ flagged
Causalean.SWIGGraph
Induce a sub-SWIG on a subset R. The new observed is R ∩ observed; the new fixed drops any fixed node whose iotaMap image was removed; the new unobserved keeps exactly the original latent roots with an edge into the retained observed set; the DAG keeps only edges with both endpoints in the new active set.
Definition (Lean source)
def induce (R : Finset (SWIGNode N)) : SWIGGraph N :=
let newObserved : Finset (SWIGNode N) := R ∩ G.observed
let newFixed : Finset (SWIGNode N) := G.fixed.filter (fun s => iotaMap s ∈ newObserved)
let newUnobserved : Finset (SWIGNode N) :=
G.unobserved.filter (fun u => ∃ v ∈ newObserved, G.dag.edge u v)
let newActive : Finset (SWIGNode N) := newFixed ∪ newObserved ∪ newUnobserved
{ dag := G.inducedDag newActive
fixed := newFixed
observed := newObserved
unobserved := newUnobserved
fixed_is_fixed := by
intro s hs
exact G.fixed_is_fixed s ((Finset.mem_filter.mp hs).1)
observed_is_random := by
intro v hv
exact G.observed_is_random v (Finset.mem_inter.mp hv).2
unobserved_is_random := by
intro u hu
exact G.unobserved_is_random u (Finset.mem_filter.mp hu).1
obs_unobs_disjoint := by
rw [Finset.disjoint_left]
intro u huObs huUnobs
exact (Finset.disjoint_left.mp G.obs_unobs_disjoint
(inter_subset_right huObs) (Finset.mem_filter.mp huUnobs).1).elim
dag_edges_classified := by
intro u v huv
-- Unfold the induced edge: both endpoints lie in `newActive`.
have hu : u ∈ newActive := huv.2.1
have hv : v ∈ newActive := huv.2.2
-- `newActive = newFixed ∪ newObserved ∪ newUnobserved`, which equals
-- `newFixed ∪ newObserved ∪ unobserved` in the induced graph.
refine ⟨?_, ?_⟩
· -- Rearrange: newFixed ∪ newObserved ∪ unobserved = (newFixed ∪ newObserved) ∪ unobserved
simpa [newActive] using hu
· simpa [newActive] using hv
fixed_image_in_observed := by
intro s hs
exact (Finset.mem_filter.mp hs).2
fixed_are_roots := by
intro s hs
-- parents in the induced DAG ⊆ parents in G.dag = ∅
have hsFixed : s ∈ G.fixed := (Finset.mem_filter.mp hs).1
have hGroot : G.dag.parents s = ∅ := G.fixed_are_roots s hsFixed
have hsub := G.inducedDag_parents_subset newActive s
rw [hGroot] at hsub
exact Finset.subset_empty.mp hsub
unobs_are_roots := by
intro u hu
have hGroot : G.dag.parents u = ∅ := G.unobs_are_roots u (Finset.mem_filter.mp hu).1
have hsub := G.inducedDag_parents_subset newActive u
rw [hGroot] at hsub
exact Finset.subset_empty.mp hsub
fixed_outside_fixed_isolated := by
intro n hnNotFixed
-- Case split: is `.fixed n` in the old `G.fixed`?
by_cases horig : SWIGNode.fixed n ∈ G.fixed
· -- It is in the old fixed set, but dropped by the filter. Show its
-- edges in the induced DAG are empty because `.fixed n ∉ newActive`.
have hnotActive : SWIGNode.fixed n ∉ newActive := by
intro hin
rcases Finset.mem_union.mp hin with hin | hin
· rcases Finset.mem_union.mp hin with hin | hin
· exact hnNotFixed hin
· -- .fixed n ∈ newObserved ⊆ G.observed, but observed nodes
-- are `.random _`, contradicting .fixed form.
have hinObs : SWIGNode.fixed n ∈ G.observed :=
(Finset.mem_inter.mp hin).2
obtain ⟨_, hm⟩ := G.observed_is_random _ hinObs
cases hm
· -- .fixed n ∈ G.unobserved — contradiction (unobserved are random)
obtain ⟨_, hm⟩ := G.unobserved_is_random _ (Finset.mem_filter.mp hin).1
cases hm
refine ⟨?_, ?_⟩
· -- No parents: any parent would come with an edge, requiring
-- `.fixed n ∈ newActive`.
rw [Finset.eq_empty_iff_forall_notMem]
intro w hw
have hedge := ((G.inducedDag newActive).mem_parents.mp hw)
exact hnotActive hedge.2.2
· rw [Finset.eq_empty_iff_forall_notMem]
intro w hw
have hedge := ((G.inducedDag newActive).mem_children.mp hw)
exact hnotActive hedge.2.1
· -- `.fixed n` was never in G.fixed: use G.fixed_outside_fixed_isolated.
have hGiso := G.fixed_outside_fixed_isolated n horig
refine ⟨?_, ?_⟩
· have hsub := G.inducedDag_parents_subset newActive (SWIGNode.fixed n)
rw [hGiso.1] at hsub
exact Finset.subset_empty.mp hsub
· have hsub := G.inducedDag_children_subset newActive (SWIGNode.fixed n)
rw [hGiso.2] at hsub
exact Finset.subset_empty.mp hsub
all_children_in_observed := by
-- hu : u ∈ newUnobserved ∪ newFixed ∪ newObserved (the struct invariant's
-- old-to-new field substitution), which parses as
-- (G.unobserved ∪ newFixed) ∪ newObserved.
intro u hu v hv
have hedge := (G.inducedDag newActive).mem_children.mp hv
have hvActive : v ∈ newActive := hedge.2.2
have hvChildOrig : v ∈ G.dag.children u := G.dag.mem_children.mpr hedge.1
-- Lift u into the old classified set.
have huOld : u ∈ G.unobserved ∪ G.fixed ∪ G.observed := by
rcases Finset.mem_union.mp hu with hu' | hu'
· rcases Finset.mem_union.mp hu' with hu' | hu'
· -- u ∈ G.unobserved
exact mem_union_left _ (mem_union_left _ (Finset.mem_filter.mp hu').1)
· -- u ∈ newFixed ⊆ G.fixed
have : u ∈ G.fixed := (Finset.mem_filter.mp hu').1
exact mem_union_left _ (Finset.mem_union_right _ this)
· -- u ∈ newObserved ⊆ G.observed
have : u ∈ G.observed := (Finset.mem_inter.mp hu').2
exact Finset.mem_union_right _ this
have hvOldObs : v ∈ G.observed := G.all_children_in_observed u huOld hvChildOrig
-- Combine: v ∈ newActive and v ∈ G.observed. Rule out newFixed and
-- G.unobserved to land in newObserved.
-- newActive parses as (newFixed ∪ newObserved) ∪ G.unobserved.
rcases Finset.mem_union.mp hvActive with hv' | hv'
· rcases Finset.mem_union.mp hv' with hv' | hv'
· -- v ∈ newFixed → v is `.fixed _`, but v ∈ G.observed → v is `.random _`.
have hvFixed : v ∈ G.fixed := (Finset.mem_filter.mp hv').1
obtain ⟨m, hm⟩ := G.fixed_is_fixed _ hvFixed
obtain ⟨k, hk⟩ := G.observed_is_random _ hvOldObs
rw [hm] at hk
cases hk
· -- v ∈ newObserved — done.
exact hv'
· -- v ∈ G.unobserved contradicts v ∈ G.observed via disjointness.
exact (Finset.disjoint_left.mp G.obs_unobs_disjoint hvOldObs
(Finset.mem_filter.mp hv').1).elim }
5 supporting declarations (lemmas, instances)
-
inducedEdge_decidableinstance — Whether an edge remains after restricting to an active vertex set is decidable.instance inducedEdge_decidable (active : Finset (SWIGNode N)) : DecidableRel (G.inducedEdge active) := by intro u v unfold inducedEdge infer_instance -
inducedDag_parents_subsetlemma — Every parent in the restricted DAG is also a parent in the original graph.hypothesesconclusion(G.inducedDag active).parents v ⊆ G.dag.parents vProof (Lean source)
lemma inducedDag_parents_subset (active : Finset (SWIGNode N)) (v : SWIGNode N) : (G.inducedDag active).parents v ⊆ G.dag.parents v := by intro u hu have h := (G.inducedDag active).mem_parents.mp hu exact G.dag.mem_parents.mpr h.1 -
inducedDag_children_subsetlemma — Every child in the restricted DAG is also a child in the original graph.hypothesesconclusion(G.inducedDag active).children u ⊆ G.dag.children uProof (Lean source)
lemma inducedDag_children_subset (active : Finset (SWIGNode N)) (u : SWIGNode N) : (G.inducedDag active).children u ⊆ G.dag.children u := by intro v hv have h := (G.inducedDag active).mem_children.mp hv exact G.dag.mem_children.mpr h.1 -
inducedDag_isAncestor_mem_activelemma — If (G.inducedDag active).isAncestor u v, then both endpoints belong to active.hypothesesconclusionu ∈ active ∧ v ∈ activeProof (Lean source)
lemma inducedDag_isAncestor_mem_active (active : Finset (SWIGNode N)) {u v : SWIGNode N} (h : (G.inducedDag active).isAncestor u v) : u ∈ active ∧ v ∈ active := by induction h with | edge he => exact ⟨((G.inducedDag_edge_iff active _ _).mp he).2.1, ((G.inducedDag_edge_iff active _ _).mp he).2.2⟩ | trans _ he ih => exact ⟨ih.1, ((G.inducedDag_edge_iff active _ _).mp he).2.2⟩ -
induce_isAncestor_mem_Rlemma — In the induced subgraph, every vertex with a proper ancestor lies in the retained observed support.hypothesesconclusionv ∈ R ∩ G.observedProof (Lean source)
lemma induce_isAncestor_mem_R (R : Finset (SWIGNode N)) {u v : SWIGNode N} (h : (G.induce R).dag.isAncestor u v) : v ∈ R ∩ G.observed := by -- v has at least one parent in the induced DAG have hpar : (G.induce R).dag.parents v ≠ ∅ := (G.induce R).dag.isAncestor_has_parent h -- v is in the active set of the induced DAG have hactive : v ∈ (G.fixed.filter (fun s => iotaMap s ∈ R ∩ G.observed)) ∪ (R ∩ G.observed) ∪ (G.unobserved.filter (fun u => ∃ w ∈ R ∩ G.observed, G.dag.edge u w)) := (G.inducedDag_isAncestor_mem_active _ h).2 -- v is not fixed (fixed nodes are roots, but v has a parent) have hnotFixed : v ∉ G.fixed.filter (fun s => iotaMap s ∈ R ∩ G.observed) := by intro hv have := (G.induce R).fixed_are_roots v hv exact hpar this -- v is not unobserved (unobserved nodes are roots, but v has a parent) have hnotUnobs : v ∉ G.unobserved.filter (fun u => ∃ w ∈ R ∩ G.observed, G.dag.edge u w) := by intro hv have := (G.induce R).unobs_are_roots v hv exact hpar this -- So v ∈ R ∩ G.observed. rcases Finset.mem_union.mp hactive with hv | hv · rcases Finset.mem_union.mp hv with hv | hv · exact absurd hv hnotFixed · exact hv · exact absurd hv hnotUnobs
AcyclicConstruct 2 core · 0 supporting Since DAG stores acyclicity directly (acyclic : ∀ v, ¬ Relation.TransGen edge v v), building one only requires exhibiting the edge relation, its decidability, and a proof that it has no directed cycle. ★ ofAcyclic★ ofAcyclic_edge
Constructing a DAG from a raw acyclic edge relation
Since DAG stores acyclicity directly (acyclic : ∀ v, ¬ Relation.TransGen edge v v),
building one only requires exhibiting the edge relation, its decidability, and a
proof that it has no directed cycle. This file provides:
* DAG.ofAcyclic e hac — from an edge relation e whose transitive closure is
irreflexive (hac). Materialises the graph directly. (Used e.g. for the
Verma–Pearl covered-edge reversal, where acyclicity of the modified relation is
known before any topological numbering.)
For constructions that already carry a topological numbering, build the DAG
structure directly and discharge its acyclic field with
DAG.acyclic_of_topoOrder (in Causalean.Graph.DAG), which keeps the edge
relation definitionally transparent.
def ofAcyclic reviewed
⚑ flagged
Causalean.DAG
Build a DAG from an acyclic edge relation. Given e : V → V → Prop whose transitive closure is irreflexive (hac, i.e. e has no directed cycle), this is the directed acyclic graph with edge relation e.
theorem ofAcyclic_edge reviewed
⚑ flagged
Causalean.DAG
The directed acyclic graph ofAcyclic e hac, built from an edge relation e together with a proof that e has no directed cycle, has exactly e as its edge relation.
Formal statement
Proof (Lean source)
@[simp] theorem ofAcyclic_edge (e : V → V → Prop)
(hac : ∀ v, ¬ TransGen e v v) :
(ofAcyclic e hac).edge = e := rfl
CComponents 11 core · 22 supporting This file defines c-components for a Single World Intervention Graph. ★ cComponentSet★ mem_bidirectedBFS_iff_reachable★ cComponentSet_biUnion★ mem_cComponentOf_iff_reachable★ cComponentSet_pairwise_disjoint
C-Components
This file defines c-components for a Single World Intervention Graph. Two observed variables are directly confounded when they share an unobserved parent, and c-components are the connected components generated by that bidirected confounding relation.
The executable side is bidirectedBFS, cComponentOf, cComponents, and the
canonical order-independent cComponentSet. The main correctness theorem
mem_bidirectedBFS_iff_reachable identifies the BFS output with
bidirectedReachable; the partition lemmas cComponentSet_biUnion and
cComponentSet_pairwise_disjoint show that cComponentSet covers exactly the
observed variables with disjoint components. The boundary lemmas rule out shared
latent parents across distinct c-components and provide the induced-graph bridge
induce_cComponentOf_eq_of_shared_unobserved_parent.
def directlyConfounded reviewed
⚑ flagged
Causalean.SWIGGraph
Two distinct variables are directly confounded if they share an unobserved parent.
Definition (Lean source)
def directlyConfounded (v₁ v₂ : SWIGNode N) : Prop :=
v₁ ≠ v₂ ∧
∃ u ∈ G.unobserved, G.dag.edge u v₁ ∧ G.dag.edge u v₂
def bidirectedNeighbors reviewed
⚑ flagged
Causalean.SWIGGraph
The bidirected neighbors of an observed variable v: all observed variables that are directly confounded with v.
Definition (Lean source)
def bidirectedNeighbors (v : SWIGNode N) : Finset (SWIGNode N) :=
G.observed.filter (fun w => G.directlyConfounded v w)
inductive bidirectedReachable reviewed
⚑ flagged
Causalean.SWIGGraph
Bidirected reachability: the transitive closure of the directly-confounded relation, restricted to observed variables. Two observed variables are in the same C-component iff they are bidirected-reachable from each other.
def bidirectedBFS reviewed
⚑ flagged
Causalean.SWIGGraph
Compute the bidirected-reachable set from a single vertex via BFS on the bidirected projection graph.
Definition (Lean source)
def bidirectedBFS (start : SWIGNode N) : Finset (SWIGNode N) :=
let rec go (frontier visited : Finset (SWIGNode N)) (fuel : ℕ) :
Finset (SWIGNode N) :=
match fuel with
| 0 => visited
| fuel + 1 =>
let newNeighbors := frontier.biUnion (G.bidirectedNeighbors) \ visited
if newNeighbors = ∅ then visited
else go newNeighbors (visited ∪ newNeighbors) fuel
if start ∈ G.observed then
go {start} {start} (card (SWIGNode N))
else ∅
def cComponentOf reviewed
⚑ flagged
Causalean.SWIGGraph
The C-component of a given observed variable v: the maximal set of observed variables connected to v via chains of directly-confounded pairs.
Definition (Lean source)
def cComponents reviewed
⚑ flagged
Causalean.SWIGGraph
Compute all C-components in the order obtained by scanning the observed variables.
def cComponentSet reviewed
⚑ flagged
Causalean.SWIGGraph
The set of c-components as a Finset of Finsets — the canonical, order-independent index for the c-component factorization. It is the image of the observed nodes under cComponentOf (each observed node maps to its own component; distinct components have distinct images, so duplicates collapse). Used as the index set in c_component_factorization.
theorem mem_bidirectedBFS_iff_reachable reviewed
⚑ flagged
Causalean.SWIGGraph
BFS computes bidirected reachability. Fix a single-world intervention graph G and a node start that is observed in G. Then a node w is found by the breadth-first search from start exactly when w is bidirected-reachable from start — connected to it by a chain of directly-confounded (shared-unobserved-parent) pairs.
Formal statement
hypotheses
start w :
SWIGNode N
hstart :
start ∈ G.observed
conclusion
w ∈ G.bidirectedBFS start ↔ G.bidirectedReachable start w
Proof (Lean source)
theorem mem_bidirectedBFS_iff_reachable {start w : SWIGNode N}
(hstart : start ∈ G.observed) :
w ∈ G.bidirectedBFS start ↔ G.bidirectedReachable start w := by
constructor
· -- Soundness: fully proved.
intro hw
rw [bidirectedBFS] at hw
simp only [hstart, if_true] at hw
refine G.bidirectedBFS_go_reachable _ _ _ ?_ ?_ w hw
· intro y hy
rw [Finset.mem_singleton.mp hy]
exact bidirectedReachable.refl hstart
· intro y hy
rw [Finset.mem_singleton.mp hy]
exact bidirectedReachable.refl hstart
· -- Completeness: the BFS result is confounding-closed (saturation), and it
-- contains `start`; induct on the reachability derivation.
intro hreach
rw [bidirectedBFS]
simp only [hstart, if_true]
-- The initial state satisfies the closure invariant with sufficient fuel.
have hclosed := G.bidirectedBFS_go_closed (card (SWIGNode N))
{start} {start} (by simpa using hstart)
(by intro a ha haf; exact absurd ha haf)
(by
have h1 : G.observed.card ≤ card (SWIGNode N) :=
(Finset.card_le_univ G.observed).trans_eq (Fintype.card_eq.mpr ⟨Equiv.refl _⟩).symm
simp only [Finset.card_singleton]
omega)
have hself : start ∈ bidirectedBFS.go G {start} {start} (card (SWIGNode N)) :=
G.subset_bidirectedBFS_go _ _ _ (mem_singleton_self start)
induction hreach with
| refl _ => exact hself
| step _ hconf ih => exact hclosed _ ih _ hconf
theorem cComponentSet_biUnion reviewed
⚑ flagged
Causalean.SWIGGraph
The c-components cover exactly the observed nodes: their union recovers the set of observed nodes exactly.
Formal statement
conclusion
G.cComponentSet.biUnion id = G.observed
Proof (Lean source)
theorem cComponentSet_biUnion :
G.cComponentSet.biUnion id = G.observed := by
apply Finset.Subset.antisymm
· intro w hw
rw [Finset.mem_biUnion] at hw
obtain ⟨C, hC, hwC⟩ := hw
exact G.cComponentSet_subset_observed C hC (id_eq C ▸ hwC)
· intro v hv
rw [Finset.mem_biUnion]
refine ⟨G.cComponentOf v, ?_, ?_⟩
· rw [cComponentSet, mem_image]
exact ⟨v, hv, rfl⟩
· exact id_eq _ ▸ G.mem_cComponentOf_self hv
theorem mem_cComponentOf_iff_reachable reviewed
⚑ flagged
Causalean.SWIGGraph
Membership in a c-component is exactly bidirected reachability from its seed. For a node v that is observed in G, a node w belongs to the c-component seeded at v exactly when w is bidirected-reachable from v.
Formal statement
hypotheses
v w :
SWIGNode N
hv :
v ∈ G.observed
conclusion
w ∈ G.cComponentOf v ↔ G.bidirectedReachable v w
Proof (Lean source)
theorem mem_cComponentOf_iff_reachable {v w : SWIGNode N} (hv : v ∈ G.observed) :
w ∈ G.cComponentOf v ↔ G.bidirectedReachable v w :=
G.mem_bidirectedBFS_iff_reachable hv
theorem cComponentSet_pairwise_disjoint reviewed
⚑ flagged
Causalean.SWIGGraph
Distinct c-components are pairwise disjoint: no observed node belongs to two different c-components.
Formal statement
conclusion
Proof (Lean source)
theorem cComponentSet_pairwise_disjoint :
(G.cComponentSet : Set (Finset (SWIGNode N))).PairwiseDisjoint id := by
intro C hC D hD hCD
rw [Finset.mem_coe, cComponentSet, mem_image] at hC hD
obtain ⟨v, hv, rfl⟩ := hC
obtain ⟨w, hw, rfl⟩ := hD
-- If the components intersect at some `x`, the seeds are mutually reachable,
-- hence the components are equal — contradicting `hCD`.
rw [onFun, id_eq, id_eq, Finset.disjoint_left]
intro x hxv hxw
apply hCD
rw [G.mem_cComponentOf_iff_reachable hv] at hxv
rw [G.mem_cComponentOf_iff_reachable hw] at hxw
-- `v` reaches `x` and `w` reaches `x`, so `v` reaches `w`.
exact G.cComponentOf_eq_of_reachable
(G.bidirectedReachable_trans hxv (G.bidirectedReachable_symm hxw))
22 supporting declarations (lemmas, instances)
-
decDirectlyConfoundedinstance — Direct confounding can be decided by finite search for a shared unobserved parent.instance decDirectlyConfounded (v₁ v₂ : SWIGNode N) : Decidable (G.directlyConfounded v₁ v₂) := inferInstanceAs (Decidable (_ ∧ ∃ _, _)) -
directlyConfounded_symmtheorem — The directly-confounded relation is symmetric: if v₁ and v₂ share an unobserved parent, then so do v₂ and v₁ (the shared parent and the observed-ness conditions are symmetric in the two arguments).Proof (Lean source)
theorem directlyConfounded_symm {v₁ v₂ : SWIGNode N} (h : G.directlyConfounded v₁ v₂) : G.directlyConfounded v₂ v₁ := by obtain ⟨hne, u, hu, e1, e2⟩ := h exact ⟨hne.symm, u, hu, e2, e1⟩ -
bidirectedReachable_observed_lefttheorem — Both endpoints of a bidirected-reachability derivation are observed (left endpoint).Proof (Lean source)
theorem bidirectedReachable_observed_left {u v : SWIGNode N} (h : G.bidirectedReachable u v) : u ∈ G.observed := by induction h with | refl hv => exact hv | step _ _ ih => exact ih -
bidirectedReachable_observed_righttheorem — Both endpoints of a bidirected-reachability derivation are observed (right endpoint).Proof (Lean source)
theorem bidirectedReachable_observed_right {u v : SWIGNode N} (h : G.bidirectedReachable u v) : v ∈ G.observed := by induction h with | refl hv => exact hv | step _ hconf _ => obtain ⟨_, u, hu, _, huw⟩ := hconf exact G.all_children_in_observed u (mem_union_left _ (mem_union_left _ hu)) (G.dag.mem_children.mpr huw) -
bidirectedReachable_headtheorem — Prepend a directly-confounded step at the head of a reachability chain: if u and v are directly confounded and v reaches w, then u reaches w. Proved by induction on the v-to-w derivation.hypothesesconclusionG.bidirectedReachable u wProof (Lean source)
theorem bidirectedReachable_head {u v w : SWIGNode N} (huv : G.directlyConfounded u v) (hvw : G.bidirectedReachable v w) : G.bidirectedReachable u w := by induction hvw with | refl hv => obtain ⟨hne, x, hx, hux, hxv⟩ := huv have huObs : u ∈ G.observed := G.all_children_in_observed x (mem_union_left _ (mem_union_left _ hx)) (G.dag.mem_children.mpr hux) exact bidirectedReachable.step (bidirectedReachable.refl huObs) ⟨hne, x, hx, hux, hxv⟩ | step _ hconf ih => exact bidirectedReachable.step ih hconf -
bidirectedReachable_symmtheorem — Bidirected reachability is symmetric.Proof (Lean source)
theorem bidirectedReachable_symm {u v : SWIGNode N} (h : G.bidirectedReachable u v) : G.bidirectedReachable v u := by induction h with | refl hv => exact bidirectedReachable.refl hv | step _ hconf ih => exact bidirectedReachable_head G (G.directlyConfounded_symm hconf) ih -
bidirectedReachable_transtheorem — Bidirected reachability is transitive.hypothesesconclusionG.bidirectedReachable u wProof (Lean source)
theorem bidirectedReachable_trans {u v w : SWIGNode N} (huv : G.bidirectedReachable u v) (hvw : G.bidirectedReachable v w) : G.bidirectedReachable u w := by induction hvw with | refl _ => exact huv | step _ hconf ih => exact bidirectedReachable.step ih hconf -
bidirectedNeighbors_subset_observedtheorem — The bidirected neighbors of a node are observed.Proof (Lean source)
theorem bidirectedNeighbors_subset_observed (v : SWIGNode N) : G.bidirectedNeighbors v ⊆ G.observed := by intro w hw exact (Finset.mem_filter.mp hw).1 -
subset_bidirectedBFS_gotheorem — The visited set only grows: it is contained in the result of go.hypothesesconclusionvisited ⊆ bidirectedBFS.go G frontier visited fuelProof (Lean source)
theorem subset_bidirectedBFS_go (frontier visited : Finset (SWIGNode N)) (fuel : ℕ) : visited ⊆ bidirectedBFS.go G frontier visited fuel := by induction fuel generalizing frontier visited with | zero => rw [bidirectedBFS.go] | succ n ih => rw [bidirectedBFS.go] by_cases h : frontier.biUnion (G.bidirectedNeighbors) \ visited = ∅ · simp [h] · simp only [h, if_false] exact (subset_union_left).trans (ih _ _) -
bidirectedBFS_go_subset_observedtheorem — If the visited set and frontier are within observed, so is the result of go.hypothesesconclusionbidirectedBFS.go G frontier visited fuel ⊆ G.observedProof (Lean source)
theorem bidirectedBFS_go_subset_observed (frontier visited : Finset (SWIGNode N)) (fuel : ℕ) (hvis : visited ⊆ G.observed) : bidirectedBFS.go G frontier visited fuel ⊆ G.observed := by induction fuel generalizing frontier visited with | zero => rw [bidirectedBFS.go]; exact hvis | succ n ih => rw [bidirectedBFS.go] by_cases h : frontier.biUnion (G.bidirectedNeighbors) \ visited = ∅ · simpa [h] using hvis · simp only [h, if_false] apply ih apply union_subset hvis intro w hw obtain ⟨hw', _⟩ := Finset.mem_sdiff.mp hw obtain ⟨x, _, hx⟩ := Finset.mem_biUnion.mp hw' exact G.bidirectedNeighbors_subset_observed x hx -
bidirectedBFS_subset_observedtheorem — The bidirected BFS from start is contained in observed.Proof (Lean source)
theorem bidirectedBFS_subset_observed (start : SWIGNode N) : G.bidirectedBFS start ⊆ G.observed := by rw [bidirectedBFS] by_cases h : start ∈ G.observed · simp only [h, if_true] exact G.bidirectedBFS_go_subset_observed _ _ _ (by simpa using h) · simp [h] -
mem_bidirectedBFS_selftheorem — The start node belongs to its own BFS result (when observed).Proof (Lean source)
theorem mem_bidirectedBFS_self {start : SWIGNode N} (h : start ∈ G.observed) : start ∈ G.bidirectedBFS start := by rw [bidirectedBFS] simp only [h, if_true] exact G.subset_bidirectedBFS_go _ _ _ (by simp) -
bidirectedBFS_go_reachabletheorem — Soundness of BFS. Every node produced by bidirectedBFS.go from a frontier and visited set all of whose elements are bidirected-reachable from start is itself bidirected-reachable from start. Fully proved by induction on the fuel.hypothesesstart :SWIGNode NProof (Lean source)
theorem bidirectedBFS_go_reachable {start : SWIGNode N} : ∀ (fuel : ℕ) (frontier visited : Finset (SWIGNode N)), (∀ y ∈ visited, G.bidirectedReachable start y) → (∀ y ∈ frontier, G.bidirectedReachable start y) → ∀ z ∈ bidirectedBFS.go G frontier visited fuel, G.bidirectedReachable start z := by intro fuel induction fuel with | zero => intro frontier visited hv _ z hz rw [bidirectedBFS.go] at hz; exact hv z hz | succ n ih => intro frontier visited hv hf z hz rw [bidirectedBFS.go] at hz by_cases h : frontier.biUnion (G.bidirectedNeighbors) \ visited = ∅ · simp only [h, if_true] at hz; exact hv z hz · simp only [h, if_false] at hz have hnew : ∀ y ∈ frontier.biUnion (G.bidirectedNeighbors) \ visited, G.bidirectedReachable start y := by intro y hy obtain ⟨hy', _⟩ := Finset.mem_sdiff.mp hy obtain ⟨q, hq, hqy⟩ := Finset.mem_biUnion.mp hy' exact bidirectedReachable.step (hf q hq) ((Finset.mem_filter.mp hqy).2) apply ih _ _ _ _ z hz · intro y hy rcases Finset.mem_union.mp hy with hy | hy · exact hv y hy · exact hnew y hy · exact hnew -
bidirectedBFS_go_closedtheorem — Closure at saturation. Under the BFS invariants — the visited set is observed, and every *already-expanded* visited node (one outside the frontier) has all its directly-confounded neighbors in visited — and given enough remaining fuel (card observed - card visited ≤ fuel), the result of go is closed under the directly-confounded relation: every neighbor of a node in the result is again in the result.conclusionvisited ⊆ G.observed → (∀ a ∈ visited, a ∉ frontier → ∀ b, G.directlyConfounded a b → b ∈ visited) → (G.observed.card - visited.card ≤ fuel) → ∀ a ∈ bidirectedBFS.go G frontier visited fuel, ∀ b, G.directlyConfounded a b → b ∈ bidirectedBFS.go G frontier visited fuelProof (Lean source)
theorem bidirectedBFS_go_closed : ∀ (fuel : ℕ) (frontier visited : Finset (SWIGNode N)), visited ⊆ G.observed → (∀ a ∈ visited, a ∉ frontier → ∀ b, G.directlyConfounded a b → b ∈ visited) → (G.observed.card - visited.card ≤ fuel) → ∀ a ∈ bidirectedBFS.go G frontier visited fuel, ∀ b, G.directlyConfounded a b → b ∈ bidirectedBFS.go G frontier visited fuel := by intro fuel induction fuel with | zero => intro frontier visited hvo hexp hbudget a ha b hab rw [bidirectedBFS.go] at ha ⊢ -- fuel = 0: budget forces visited to already cover observed, so frontier -- nodes' neighbors are visited too. have hcard : G.observed.card ≤ visited.card := by omega have hveq : visited = G.observed := Finset.eq_of_subset_of_card_le hvo hcard by_cases haf : a ∈ frontier · -- a ∈ frontier ⊆ visited = observed; b ∈ observed ⊆ visited. obtain ⟨_, u, hu, _, hub⟩ := hab have hbo : b ∈ G.observed := G.all_children_in_observed u (mem_union_left _ (mem_union_left _ hu)) (G.dag.mem_children.mpr hub) rwa [hveq] · exact hexp a ha haf b hab | succ n ih => intro frontier visited hvo hexp hbudget a ha b hab rw [bidirectedBFS.go] at ha ⊢ set newNeighbors := frontier.biUnion (G.bidirectedNeighbors) \ visited with hnn by_cases h : newNeighbors = ∅ · -- Terminating branch: result = visited, which is confounding-closed. simp only [h, if_true] at ha ⊢ by_cases haf : a ∈ frontier · -- a in frontier: its neighbor b is in biUnion; since newNeighbors = ∅, -- b must already be in visited. have hbn : b ∈ G.bidirectedNeighbors a := by rw [bidirectedNeighbors, mem_filter] obtain ⟨hne, u, hu, hua, hub⟩ := hab have hbo : b ∈ G.observed := G.all_children_in_observed u (mem_union_left _ (mem_union_left _ hu)) (G.dag.mem_children.mpr hub) exact ⟨hbo, ⟨hne, u, hu, hua, hub⟩⟩ have hbU : b ∈ frontier.biUnion (G.bidirectedNeighbors) := Finset.mem_biUnion.mpr ⟨a, haf, hbn⟩ by_contra hbv have : b ∈ newNeighbors := Finset.mem_sdiff.mpr ⟨hbU, hbv⟩ rw [h] at this exact absurd this (by simp) · exact hexp a ha haf b hab · -- Recursing branch: apply IH to the grown visited set. simp only [h, if_false] at ha ⊢ have hUobs : ∀ x ∈ frontier.biUnion (G.bidirectedNeighbors), x ∈ G.observed := by intro x hx obtain ⟨q, _, hq⟩ := Finset.mem_biUnion.mp hx exact G.bidirectedNeighbors_subset_observed q hq -- New invariant pieces. have hfv' : newNeighbors ⊆ visited ∪ newNeighbors := Finset.subset_union_right have hvo' : visited ∪ newNeighbors ⊆ G.observed := by apply union_subset hvo intro x hx exact hUobs x (Finset.mem_sdiff.mp hx).1 have hexp' : ∀ x ∈ visited ∪ newNeighbors, x ∉ newNeighbors → ∀ c, G.directlyConfounded x c → c ∈ visited ∪ newNeighbors := by intro x hx hxnn c hxc have hxv : x ∈ visited := by rcases Finset.mem_union.mp hx with hxv | hxnew · exact hxv · exact absurd hxnew hxnn by_cases hxf : x ∈ frontier · -- x ∈ frontier: c is a neighbor, so c ∈ biUnion, hence c ∈ visited or -- c ∈ newNeighbors. have hcn : c ∈ G.bidirectedNeighbors x := by rw [bidirectedNeighbors, mem_filter] obtain ⟨hne, u, hu, hux, huc⟩ := hxc have hco : c ∈ G.observed := G.all_children_in_observed u (mem_union_left _ (mem_union_left _ hu)) (G.dag.mem_children.mpr huc) exact ⟨hco, ⟨hne, u, hu, hux, huc⟩⟩ have hcU : c ∈ frontier.biUnion (G.bidirectedNeighbors) := Finset.mem_biUnion.mpr ⟨x, hxf, hcn⟩ by_cases hcv : c ∈ visited · exact mem_union_left _ hcv · exact mem_union_right _ (Finset.mem_sdiff.mpr ⟨hcU, hcv⟩) · exact mem_union_left _ (hexp x hxv hxf c hxc) -- Budget decreases by at least one because newNeighbors is nonempty and -- disjoint from visited. have hdisj : Disjoint visited newNeighbors := disjoint_sdiff_self_right have hcardU : (visited ∪ newNeighbors).card = visited.card + newNeighbors.card := Finset.card_union_of_disjoint hdisj have hnnpos : 0 < newNeighbors.card := Finset.card_pos.mpr (Finset.nonempty_of_ne_empty h) have hbudget' : G.observed.card - (visited ∪ newNeighbors).card ≤ n := by rw [hcardU]; omega exact ih newNeighbors (visited ∪ newNeighbors) hvo' hexp' hbudget' a ha b hab -
cComponentOf_subset_observedtheorem — The c-component of v is contained in the observed nodes.Proof (Lean source)
theorem cComponentOf_subset_observed (v : SWIGNode N) : G.cComponentOf v ⊆ G.observed := G.bidirectedBFS_subset_observed v -
mem_cComponentOf_selftheorem — An observed node belongs to its own c-component.Proof (Lean source)
theorem mem_cComponentOf_self {v : SWIGNode N} (hv : v ∈ G.observed) : v ∈ G.cComponentOf v := G.mem_bidirectedBFS_self hv -
cComponentSet_subset_observedtheorem — Every c-component (in the canonical set) is contained in the observed nodes.conclusion∀ C ∈ G.cComponentSet, C ⊆ G.observedProof (Lean source)
theorem cComponentSet_subset_observed : ∀ C ∈ G.cComponentSet, C ⊆ G.observed := by intro C hC rw [cComponentSet, mem_image] at hC obtain ⟨v, _, rfl⟩ := hC exact G.cComponentOf_subset_observed v -
cComponentOf_eq_of_reachabletheorem — Two c-components seeded by reachable observed nodes are equal.hypothesesv w :SWIGNode Nh :G.bidirectedReachable v wconclusionG.cComponentOf v = G.cComponentOf wProof (Lean source)
theorem cComponentOf_eq_of_reachable {v w : SWIGNode N} (h : G.bidirectedReachable v w) : G.cComponentOf v = G.cComponentOf w := by have hv := G.bidirectedReachable_observed_left h have hw := G.bidirectedReachable_observed_right h apply Finset.Subset.antisymm · intro x hx rw [G.mem_cComponentOf_iff_reachable hw] rw [G.mem_cComponentOf_iff_reachable hv] at hx exact G.bidirectedReachable_trans (G.bidirectedReachable_symm h) hx · intro x hx rw [G.mem_cComponentOf_iff_reachable hv] rw [G.mem_cComponentOf_iff_reachable hw] at hx exact G.bidirectedReachable_trans h hx -
cComponentOf_eq_of_mem_cComponentSettheorem — A node in a listed c-component has that component as its computed c-component.hypothesesconclusionG.cComponentOf v = CProof (Lean source)
theorem cComponentOf_eq_of_mem_cComponentSet {C : Finset (SWIGNode N)} (hC : C ∈ G.cComponentSet) {v : SWIGNode N} (hvC : v ∈ C) : G.cComponentOf v = C := by classical rw [cComponentSet, mem_image] at hC obtain ⟨s, hsObs, rfl⟩ := hC exact (G.cComponentOf_eq_of_reachable ((G.mem_cComponentOf_iff_reachable hsObs).mp hvC)).symm -
not_directlyConfounded_of_mem_cComponentSet_of_not_memtheorem — A node outside a c-component is not directly confounded with a node inside it.hypothesesconclusion¬ G.directlyConfounded v wProof (Lean source)
theorem not_directlyConfounded_of_mem_cComponentSet_of_not_mem {C : Finset (SWIGNode N)} (hC : C ∈ G.cComponentSet) {v w : SWIGNode N} (hvC : v ∈ C) (hwNotC : w ∉ C) : ¬ G.directlyConfounded v w := by intro hconf rw [cComponentSet, mem_image] at hC obtain ⟨s, hsObs, rfl⟩ := hC have hsv : G.bidirectedReachable s v := (G.mem_cComponentOf_iff_reachable hsObs).mp hvC have hsw : G.bidirectedReachable s w := bidirectedReachable.step hsv hconf exact hwNotC ((G.mem_cComponentOf_iff_reachable hsObs).mpr hsw)
SWIGSplitMono 5 core · 6 supporting This file defines the one-shot split of a Single World Intervention Graph at a finite set of intervention targets. ★ splitMono★ splitMono_parents_char
Monolithic Multi-Target SWIG Split
This file defines the one-shot split of a Single World Intervention Graph at a
finite set of intervention targets. The construction reroutes every outgoing
edge from a targeted random node .random D to its fixed counterpart .fixed D
in one graph transformation, while preserving the observed and unobserved node
sets and adding the fixed copies of the targets to the fixed set.
The main definitions are:
* splitMonoEdgeRel — the edge relation after rerouting all targeted outgoing
edges;
* splitMonoTopo and splitMonoDAG — the topological order and DAG proof for
the rerouted graph;
* SWIGGraph.splitMono — the packaged SWIG graph after the split;
* splitMono_parents_char — an exact parent-set characterization; and
* splitMono_parents_eq_of_no_fixed_parent — the parent-set coincidence lemma
used by the SCM Rule 3 evaluation-map compatibility bridge.
The operation is monolithic rather than an iterated single-target split so that parents at unaffected vertices reduce definitionally in downstream SCM bookkeeping.
def splitMonoEdgeRel reviewed
⚑ flagged
Causalean.SWIGGraph
Edge relation after monolithically splitting every node D ∈ X.
def splitMonoTopo reviewed
⚑ flagged
Causalean.SWIGGraph
Topological order for the monolithically-split DAG.
Definition (Lean source)
noncomputable def splitMonoTopo (G : SWIGGraph N) (X : Finset N) : SWIGNode N → ℕ
| .random u => 2 * G.dag.topoOrder (SWIGNode.random u) + 1
| .fixed d =>
if d ∈ X then 2 * G.dag.topoOrder (SWIGNode.random d)
else 2 * G.dag.topoOrder (SWIGNode.fixed d) + 1
def splitMonoDAG reviewed
⚑ flagged
Causalean.SWIGGraph
The monolithically-split DAG: the DAG on SWIGNode N obtained by rerouting all .random D → w edges (for D ∈ X) to .fixed D → w in a single pass.
Definition (Lean source)
def splitMonoDAG (G : SWIGGraph N) (X : Finset N) :
DAG (SWIGNode N) where
edge := splitMonoEdgeRel G.dag.edge X
decEdge := splitMonoEdgeRel_decidable G.dag.edge X
acyclic := DAG.acyclic_of_topoOrder (τ := splitMonoTopo G X) (by
intro u v h
cases u with
| random u =>
simp only [splitMonoEdgeRel] at h
by_cases hu : u ∈ X
· simp [hu] at h
· have hOld : G.dag.edge (SWIGNode.random u) v := by simpa [hu] using h
have hltOld := G.dag.topoOrder_lt _ _ hOld
-- v is not a .fixed node with d ∈ X, because in G.dag there are no
-- edges into .fixed d (by fixed_are_roots / fixed_outside_fixed_isolated).
cases v with
| random v =>
exact Nat.add_lt_add_right
((Nat.mul_lt_mul_left (by omega : 0 < 2)).mpr hltOld) 1
| fixed d =>
-- edge .random u → .fixed d in G.dag: impossible since
-- .fixed d has no parents in G.dag (root/isolated)
exfalso
by_cases hd_in_fix : SWIGNode.fixed d ∈ G.fixed
· have hroot : G.dag.parents (SWIGNode.fixed d) = ∅ :=
G.fixed_are_roots _ hd_in_fix
have : SWIGNode.random u ∈ G.dag.parents (SWIGNode.fixed d) :=
G.dag.mem_parents.mpr hOld
simp [hroot] at this
· have hiso := G.fixed_outside_fixed_isolated d hd_in_fix
have : SWIGNode.random u ∈ G.dag.parents (SWIGNode.fixed d) :=
G.dag.mem_parents.mpr hOld
simp [hiso.1] at this
| fixed d =>
simp only [splitMonoEdgeRel] at h
by_cases hd : d ∈ X
· have hOld : G.dag.edge (SWIGNode.random d) v := by simpa [hd] using h
have hltOld := G.dag.topoOrder_lt _ _ hOld
cases v with
| random v =>
simp only [splitMonoTopo, if_pos hd]
exact Nat.lt_succ_of_le (Nat.mul_le_mul_left 2 (le_of_lt hltOld))
| fixed d' =>
exfalso
by_cases hd'_in_fix : SWIGNode.fixed d' ∈ G.fixed
· have hroot : G.dag.parents (SWIGNode.fixed d') = ∅ :=
G.fixed_are_roots _ hd'_in_fix
have : SWIGNode.random d ∈ G.dag.parents (SWIGNode.fixed d') :=
G.dag.mem_parents.mpr hOld
simp [hroot] at this
· have hiso := G.fixed_outside_fixed_isolated d' hd'_in_fix
have : SWIGNode.random d ∈ G.dag.parents (SWIGNode.fixed d') :=
G.dag.mem_parents.mpr hOld
simp [hiso.1] at this
· have hOld : G.dag.edge (SWIGNode.fixed d) v := by simpa [hd] using h
have hltOld := G.dag.topoOrder_lt _ _ hOld
cases v with
| random v =>
simp only [splitMonoTopo, if_neg hd]
exact Nat.add_lt_add_right
((Nat.mul_lt_mul_left (by omega : 0 < 2)).mpr hltOld) 1
| fixed d' =>
exfalso
by_cases hd'_in_fix : SWIGNode.fixed d' ∈ G.fixed
· have hroot : G.dag.parents (SWIGNode.fixed d') = ∅ :=
G.fixed_are_roots _ hd'_in_fix
have : SWIGNode.fixed d ∈ G.dag.parents (SWIGNode.fixed d') :=
G.dag.mem_parents.mpr hOld
simp [hroot] at this
· have hiso := G.fixed_outside_fixed_isolated d' hd'_in_fix
have : SWIGNode.fixed d ∈ G.dag.parents (SWIGNode.fixed d') :=
G.dag.mem_parents.mpr hOld
simp [hiso.1] at this)
def splitMono reviewed
⚑ flagged
Causalean.SWIGGraph
Monolithic multi-target split. (Definition 8, one-shot form.)
Definition (Lean source)
def splitMono (G : SWIGGraph N) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) :
SWIGGraph N where
dag := G.splitMonoDAG X
fixed := G.fixed ∪ X.image SWIGNode.fixed
observed := G.observed
unobserved := G.unobserved
fixed_is_fixed := by
intro s hs
rcases Finset.mem_union.mp hs with hs_old | hs_new
· exact G.fixed_is_fixed s hs_old
· rcases Finset.mem_image.mp hs_new with ⟨d, _, rfl⟩
exact ⟨d, rfl⟩
observed_is_random := G.observed_is_random
unobserved_is_random := G.unobserved_is_random
obs_unobs_disjoint := G.obs_unobs_disjoint
dag_edges_classified := by
intro u v huv
-- huv : splitMonoEdgeRel G.dag.edge X u v
change splitMonoEdgeRel G.dag.edge X u v at huv
have hsplit : splitMonoEdgeRel G.dag.edge X u v := huv
cases u with
| random a =>
by_cases ha : a ∈ X
· -- random a loses outgoing edges
exfalso
simp [splitMonoEdgeRel, ha] at hsplit
· have hold : G.dag.edge (SWIGNode.random a) v := by
simpa [splitMonoEdgeRel, ha] using hsplit
have hcls := G.dag_edges_classified _ _ hold
refine ⟨?_, ?_⟩
· rcases Finset.mem_union.mp hcls.1 with h | h
· rcases Finset.mem_union.mp h with h | h
· exact mem_union_left _ (mem_union_left _
(mem_union_left _ h))
· exact mem_union_left _ (mem_union_right _ h)
· exact mem_union_right _ h
· rcases Finset.mem_union.mp hcls.2 with h | h
· rcases Finset.mem_union.mp h with h | h
· exact mem_union_left _ (mem_union_left _
(mem_union_left _ h))
· exact mem_union_left _ (mem_union_right _ h)
· exact mem_union_right _ h
| fixed d =>
by_cases hd : d ∈ X
· -- Moved edge: .fixed d → v originates from .random d → v in G.dag.
have hold : G.dag.edge (SWIGNode.random d) v := by
simpa [splitMonoEdgeRel, hd] using hsplit
have hd_obs : SWIGNode.random d ∈ G.observed := hObs d hd
have hvObs : v ∈ G.observed :=
G.all_children_in_observed (SWIGNode.random d)
(mem_union_right _ hd_obs)
(G.dag.mem_children.mpr hold)
refine ⟨?_, ?_⟩
· -- .fixed d ∈ new fixed via X.image
have : SWIGNode.fixed d ∈ X.image SWIGNode.fixed :=
Finset.mem_image.mpr ⟨d, hd, rfl⟩
exact mem_union_left _ (mem_union_left _
(mem_union_right _ this))
· exact mem_union_left _ (mem_union_right _ hvObs)
· have hold : G.dag.edge (SWIGNode.fixed d) v := by
simpa [splitMonoEdgeRel, hd] using hsplit
have hcls := G.dag_edges_classified _ _ hold
refine ⟨?_, ?_⟩
· rcases Finset.mem_union.mp hcls.1 with h | h
· rcases Finset.mem_union.mp h with h | h
· exact mem_union_left _ (mem_union_left _
(mem_union_left _ h))
· exact mem_union_left _ (mem_union_right _ h)
· exact mem_union_right _ h
· rcases Finset.mem_union.mp hcls.2 with h | h
· rcases Finset.mem_union.mp h with h | h
· exact mem_union_left _ (mem_union_left _
(mem_union_left _ h))
· exact mem_union_left _ (mem_union_right _ h)
· exact mem_union_right _ h
fixed_image_in_observed := by
intro s hs
rcases Finset.mem_union.mp hs with hs_old | hs_new
· exact G.fixed_image_in_observed s hs_old
· rcases Finset.mem_image.mp hs_new with ⟨d, hd, rfl⟩
simpa [iotaMap] using hObs d hd
fixed_are_roots := by
intro s hs
-- No parents of s in the split DAG: every edge x → s in splitMonoEdgeRel
-- reduces to an edge into s in G.dag, which is empty (by root/isolation).
have hNoG : ∀ x : SWIGNode N, ¬ G.dag.edge x s := by
intro x hxE
rcases Finset.mem_union.mp hs with hs_old | hs_new
· have hroot : G.dag.parents s = ∅ := G.fixed_are_roots s hs_old
have : x ∈ G.dag.parents s := G.dag.mem_parents.mpr hxE
simp [hroot] at this
· rcases Finset.mem_image.mp hs_new with ⟨D, hD, rfl⟩
have hroot : G.dag.parents (SWIGNode.fixed D) = ∅ :=
(G.fixed_outside_fixed_isolated D (hFix D hD)).1
have : x ∈ G.dag.parents (SWIGNode.fixed D) := G.dag.mem_parents.mpr hxE
simp [hroot] at this
ext x
constructor
· intro hxPar
have hxEdge := (G.splitMonoDAG X).mem_parents.mp hxPar
change splitMonoEdgeRel G.dag.edge X x s at hxEdge
exfalso
cases x with
| random u =>
by_cases hu : u ∈ X
· simp [splitMonoEdgeRel, hu] at hxEdge
· have : G.dag.edge (SWIGNode.random u) s := by
simpa [splitMonoEdgeRel, hu] using hxEdge
exact hNoG _ this
| fixed d =>
by_cases hd : d ∈ X
· have : G.dag.edge (SWIGNode.random d) s := by
simpa [splitMonoEdgeRel, hd] using hxEdge
exact hNoG _ this
· have : G.dag.edge (SWIGNode.fixed d) s := by
simpa [splitMonoEdgeRel, hd] using hxEdge
exact hNoG _ this
· intro hxPar
simp at hxPar
unobs_are_roots := by
intro u hu
have hrootOld : G.dag.parents u = ∅ := G.unobs_are_roots u hu
ext x
constructor
· intro hxPar
have hxEdge := (G.splitMonoDAG X).mem_parents.mp hxPar
change splitMonoEdgeRel G.dag.edge X x u at hxEdge
exfalso
cases x with
| random n =>
by_cases hn : n ∈ X
· simp [splitMonoEdgeRel, hn] at hxEdge
· have : G.dag.edge (SWIGNode.random n) u := by
simpa [splitMonoEdgeRel, hn] using hxEdge
have : SWIGNode.random n ∈ G.dag.parents u := G.dag.mem_parents.mpr this
simp [hrootOld] at this
| fixed d =>
by_cases hd : d ∈ X
· have : G.dag.edge (SWIGNode.random d) u := by
simpa [splitMonoEdgeRel, hd] using hxEdge
have : SWIGNode.random d ∈ G.dag.parents u := G.dag.mem_parents.mpr this
simp [hrootOld] at this
· have : G.dag.edge (SWIGNode.fixed d) u := by
simpa [splitMonoEdgeRel, hd] using hxEdge
have : SWIGNode.fixed d ∈ G.dag.parents u := G.dag.mem_parents.mpr this
simp [hrootOld] at this
· intro hxPar
simp at hxPar
fixed_outside_fixed_isolated := by
intro n hn
-- hn : .fixed n ∉ G.fixed ∪ X.image .fixed, so .fixed n ∉ G.fixed AND n ∉ X
have hn_old : SWIGNode.fixed n ∉ G.fixed := by
intro hmem
exact hn (mem_union_left _ hmem)
have hn_notX : n ∉ X := by
intro hmem
exact hn (mem_union_right _ (Finset.mem_image.mpr ⟨n, hmem, rfl⟩))
have hIsoOld := G.fixed_outside_fixed_isolated n hn_old
refine ⟨?_, ?_⟩
· -- parents ∅
ext x
constructor
· intro hxPar
have hxEdge := (G.splitMonoDAG X).mem_parents.mp hxPar
change splitMonoEdgeRel G.dag.edge X x (SWIGNode.fixed n) at hxEdge
exfalso
cases x with
| random u =>
by_cases hu : u ∈ X
· simp [splitMonoEdgeRel, hu] at hxEdge
· have : G.dag.edge (SWIGNode.random u) (SWIGNode.fixed n) := by
simpa [splitMonoEdgeRel, hu] using hxEdge
have : SWIGNode.random u ∈ G.dag.parents (SWIGNode.fixed n) :=
G.dag.mem_parents.mpr this
simp [hIsoOld.1] at this
| fixed d =>
by_cases hd : d ∈ X
· have : G.dag.edge (SWIGNode.random d) (SWIGNode.fixed n) := by
simpa [splitMonoEdgeRel, hd] using hxEdge
have : SWIGNode.random d ∈ G.dag.parents (SWIGNode.fixed n) :=
G.dag.mem_parents.mpr this
simp [hIsoOld.1] at this
· have : G.dag.edge (SWIGNode.fixed d) (SWIGNode.fixed n) := by
simpa [splitMonoEdgeRel, hd] using hxEdge
have : SWIGNode.fixed d ∈ G.dag.parents (SWIGNode.fixed n) :=
G.dag.mem_parents.mpr this
simp [hIsoOld.1] at this
· intro hxPar
simp at hxPar
· -- children ∅
ext x
constructor
· intro hxCh
have hxEdge := (G.splitMonoDAG X).mem_children.mp hxCh
change splitMonoEdgeRel G.dag.edge X (SWIGNode.fixed n) x at hxEdge
have : G.dag.edge (SWIGNode.fixed n) x := by
simpa [splitMonoEdgeRel, hn_notX] using hxEdge
have : x ∈ G.dag.children (SWIGNode.fixed n) := G.dag.mem_children.mpr this
simp [hIsoOld.2] at this
· intro hxCh
simp at hxCh
all_children_in_observed := by
intro u hu w hw
have hwEdge := (G.splitMonoDAG X).mem_children.mp hw
change splitMonoEdgeRel G.dag.edge X u w at hwEdge
-- In every branch the new edge reduces to a G-edge whose target `w` is in observed.
cases u with
| random a =>
by_cases ha : a ∈ X
· exfalso
simp [splitMonoEdgeRel, ha] at hwEdge
· have hold : G.dag.edge (SWIGNode.random a) w := by
simpa [splitMonoEdgeRel, ha] using hwEdge
-- `.random a` is observed or unobserved in G; apply G's closure.
have hu_old : SWIGNode.random a ∈ G.unobserved ∪ G.fixed ∪ G.observed := by
rcases Finset.mem_union.mp hu with hu' | huObs
· rcases Finset.mem_union.mp hu' with huUnobs | huFixNew
· exact mem_union_left _ (mem_union_left _ huUnobs)
· -- huFixNew : .random a ∈ G.fixed ∪ X.image .fixed
rcases Finset.mem_union.mp huFixNew with huFix | huImg
· exact mem_union_left _ (mem_union_right _ huFix)
· exfalso
rcases Finset.mem_image.mp huImg with ⟨d, _, hfix_eq⟩
cases hfix_eq
· exact mem_union_right _ huObs
have := G.all_children_in_observed _ hu_old (G.dag.mem_children.mpr hold)
exact this
| fixed d =>
by_cases hd : d ∈ X
· have hold : G.dag.edge (SWIGNode.random d) w := by
simpa [splitMonoEdgeRel, hd] using hwEdge
have hd_obs : SWIGNode.random d ∈ G.observed := hObs d hd
exact G.all_children_in_observed (SWIGNode.random d)
(mem_union_right _ hd_obs) (G.dag.mem_children.mpr hold)
· have hold : G.dag.edge (SWIGNode.fixed d) w := by
simpa [splitMonoEdgeRel, hd] using hwEdge
-- .fixed d is in new fixed iff in G.fixed (since d ∉ X rules out the image branch).
have hu_old : SWIGNode.fixed d ∈ G.unobserved ∪ G.fixed ∪ G.observed := by
-- … truncated; follow the source link for the rest …
theorem splitMono_parents_char reviewed
⚑ flagged
Causalean.SWIGGraph
Characterization of parents in splitMono. Fix a SWIG G and a set X of variables to split, where the random copy of every variable in X is observed in G and the fixed copy of every variable in X is not already among G's fixed nodes. Then, for any node v, a node x is a parent of v in the graph obtained by monolithically splitting X exactly when either x is a parent of v in the original graph and is not the random copy of any variable in X, or x is the fixed copy of some variable D ∈ X whose random copy is a parent of v in the original graph.
Formal statement
hypotheses
G :
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ G.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed
v :
SWIGNode N
conclusion
∀ x : SWIGNode N,
x ∈ (G.splitMono X hObs hFix).dag.parents v
↔ (x ∈ G.dag.parents v ∧ ∀ D ∈ X, x ≠ SWIGNode.random D) ∨ (∃ D ∈ X, x = SWIGNode.fixed D ∧ SWIGNode.random D ∈ G.dag.parents v)
Proof (Lean source)
theorem splitMono_parents_char (G : SWIGGraph N) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed)
(v : SWIGNode N) :
∀ x : SWIGNode N,
x ∈ (G.splitMono X hObs hFix).dag.parents v ↔
(x ∈ G.dag.parents v ∧ ∀ D ∈ X, x ≠ SWIGNode.random D) ∨
(∃ D ∈ X, x = SWIGNode.fixed D ∧ SWIGNode.random D ∈ G.dag.parents v) := by
intro x
-- Bridge to edge relation.
have hiff : x ∈ (G.splitMono X hObs hFix).dag.parents v ↔
splitMonoEdgeRel G.dag.edge X x v := by
change x ∈ (G.splitMonoDAG X).parents v ↔ splitMonoEdgeRel G.dag.edge X x v
rw [DAG.mem_parents]
rfl
rw [hiff]
cases x with
| random u =>
simp only [splitMonoEdgeRel]
by_cases hu : u ∈ X
· constructor
· intro h; simp [hu] at h
· rintro (⟨hPar, hNoRand⟩ | ⟨D, hD, hEq, _⟩)
· exact absurd rfl (hNoRand u hu)
· exact absurd hEq (by intro h; cases h)
· constructor
· intro hEdge
have hEdgeG : G.dag.edge (SWIGNode.random u) v := by
rw [if_neg hu] at hEdge; exact hEdge
refine inl ⟨G.dag.mem_parents.mpr hEdgeG, ?_⟩
intro D hD heq
have : u = D := SWIGNode.random.inj heq
exact hu (this ▸ hD)
· rintro (⟨hPar, _⟩ | ⟨D, _, hEq, _⟩)
· rw [if_neg hu]; exact G.dag.mem_parents.mp hPar
· exact absurd hEq (by intro h; cases h)
| fixed d =>
simp only [splitMonoEdgeRel]
by_cases hd : d ∈ X
· constructor
· intro hEdge
have hEdgeG : G.dag.edge (SWIGNode.random d) v := by
rw [if_pos hd] at hEdge; exact hEdge
exact inr ⟨d, hd, rfl, G.dag.mem_parents.mpr hEdgeG⟩
· rintro (⟨hPar, _⟩ | ⟨D, hD, hEq, hRD⟩)
· exfalso
have hfix_notin : SWIGNode.fixed d ∉ G.fixed := hFix d hd
have hiso := (G.fixed_outside_fixed_isolated d hfix_notin).2
have hch : v ∈ G.dag.children (SWIGNode.fixed d) :=
G.dag.mem_children.mpr (G.dag.mem_parents.mp hPar)
simp [hiso] at hch
· have : d = D := SWIGNode.fixed.inj hEq
subst this
rw [if_pos hd]; exact G.dag.mem_parents.mp hRD
· constructor
· intro hEdge
have hEdgeG : G.dag.edge (SWIGNode.fixed d) v := by
rw [if_neg hd] at hEdge; exact hEdge
refine inl ⟨G.dag.mem_parents.mpr hEdgeG, ?_⟩
intro D hD heq
exact absurd heq (by intro h; cases h)
· rintro (⟨hPar, _⟩ | ⟨D, hD, hEq, _⟩)
· rw [if_neg hd]; exact G.dag.mem_parents.mp hPar
· have : d = D := SWIGNode.fixed.inj hEq
exact absurd (this ▸ hD) hd
6 supporting declarations (lemmas, instances)
-
splitMonoEdgeRel_decidableinstance — The monolithic split edge relation is decidable whenever the original edge relation is decidable.instance splitMonoEdgeRel_decidable (dagEdge : SWIGNode N → SWIGNode N → Prop) [DecidableRel dagEdge] (X : Finset N) : DecidableRel (splitMonoEdgeRel dagEdge X) := by intro a b cases a with | random u => simp only [splitMonoEdgeRel] by_cases h : u ∈ X · rw [if_pos h] exact instDecidableFalse · rw [if_neg h] infer_instance | fixed d => simp only [splitMonoEdgeRel] by_cases h : d ∈ X · rw [if_pos h] infer_instance · rw [if_neg h] infer_instance -
splitMono_observedlemma — Monolithic splitting preserves the observed node set.hypothesesG :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedconclusion(G.splitMono X hObs hFix).observed = G.observedProof (Lean source)
@[simp] lemma splitMono_observed (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) : (G.splitMono X hObs hFix).observed = G.observed := rfl -
splitMono_unobservedlemma — Monolithic splitting preserves the unobserved node set.hypothesesG :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedconclusion(G.splitMono X hObs hFix).unobserved = G.unobservedProof (Lean source)
@[simp] lemma splitMono_unobserved (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) : (G.splitMono X hObs hFix).unobserved = G.unobserved := rfl -
splitMono_fixedlemma — Monolithic splitting adds the fixed copies of the target variables to the fixed node set.hypothesesG :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedconclusion(G.splitMono X hObs hFix).fixed = G.fixed ∪ X.image SWIGNode.fixedProof (Lean source)
@[simp] lemma splitMono_fixed (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) : (G.splitMono X hObs hFix).fixed = G.fixed ∪ X.image SWIGNode.fixed := rfl -
splitMono_parents_eq_of_no_fixed_parenttheorem — Parent-set coincidence at non-.fixed-targeted vertices.hypothesesG :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedv :SWIGNode NhNoFP :∀ D ∈ X, SWIGNode.fixed D ∉ (G.splitMono X hObs hFix).dag.parents vconclusion(G.splitMono X hObs hFix).dag.parents v = G.dag.parents vProof (Lean source)
theorem splitMono_parents_eq_of_no_fixed_parent (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) (v : SWIGNode N) (hNoFP : ∀ D ∈ X, SWIGNode.fixed D ∉ (G.splitMono X hObs hFix).dag.parents v) : (G.splitMono X hObs hFix).dag.parents v = G.dag.parents v := by -- Under hNoFP, no .random D (D ∈ X) can be a parent of v in G.dag either, -- because if it were, splitMono_parents_char would place .fixed D in parents — contradiction. have hNoRD : ∀ D ∈ X, SWIGNode.random D ∉ G.dag.parents v := by intro D hD hRD apply hNoFP D hD exact (splitMono_parents_char G X hObs hFix v (SWIGNode.fixed D)).mpr (inr ⟨D, hD, rfl, hRD⟩) ext x rw [splitMono_parents_char G X hObs hFix v x] constructor · rintro (⟨hP, _⟩ | ⟨D, hD, rfl, hRD⟩) · exact hP · exact absurd hRD (hNoRD D hD) · intro hP left refine ⟨hP, ?_⟩ intro D hD heq subst heq exact hNoRD D hD hP -
splitMono_congrtheorem — Congruence of splitMono under SWIGGraph.Equivalent.hypothesesG₁ G₂ :h :Equivalent G₁ G₂X :Finset NhObs₁ :∀ D ∈ X, SWIGNode.random D ∈ G₁.observedhFix₁ :∀ D ∈ X, SWIGNode.fixed D ∉ G₁.fixedhObs₂ :∀ D ∈ X, SWIGNode.random D ∈ G₂.observedhFix₂ :∀ D ∈ X, SWIGNode.fixed D ∉ G₂.fixedconclusionEquivalent (G₁.splitMono X hObs₁ hFix₁) (G₂.splitMono X hObs₂ hFix₂)Proof (Lean source)
theorem Equivalent.splitMono_congr {G₁ G₂ : SWIGGraph N} (h : Equivalent G₁ G₂) (X : Finset N) (hObs₁ : ∀ D ∈ X, SWIGNode.random D ∈ G₁.observed) (hFix₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ G₁.fixed) (hObs₂ : ∀ D ∈ X, SWIGNode.random D ∈ G₂.observed) (hFix₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ G₂.fixed) : Equivalent (G₁.splitMono X hObs₁ hFix₁) (G₂.splitMono X hObs₂ hFix₂) := by obtain ⟨hEdge, hFix_eq, hObs_eq, hUnobs_eq⟩ := h refine ⟨?_, ?_, ?_, ?_⟩ · -- (1) Edge iff: 4-way case split on (random/fixed) × (∈ X / ∉ X). intro u v cases u with | random u => change (if u ∈ X then False else G₁.dag.edge (.random u) v) ↔ (if u ∈ X then False else G₂.dag.edge (.random u) v) by_cases hu : u ∈ X · simp [hu] · simp [hu] exact hEdge _ _ | fixed d => change (if d ∈ X then G₁.dag.edge (.random d) v else G₁.dag.edge (.fixed d) v) ↔ (if d ∈ X then G₂.dag.edge (.random d) v else G₂.dag.edge (.fixed d) v) by_cases hd : d ∈ X · simp [hd] exact hEdge _ _ · simp [hd] exact hEdge _ _ · -- (2) Fixed sets: G.fixed ∪ X.image .fixed = G₂.fixed ∪ X.image .fixed simp only [splitMono_fixed] rw [hFix_eq] · -- (3) Observed: preserved by rfl. simp only [splitMono_observed] exact hObs_eq · -- (4) Unobserved: preserved by rfl. simp only [splitMono_unobserved] exact hUnobs_eq