Graph
Causal graphs: DAGs, d-separation via Bayes-Ball, SWIGs and their splits, and c-components.
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)
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)
For a finite directed acyclic graph on a vertex population and a vertex, the parent set is the finite set of all vertices having a directed edge into that vertex.
For a finite directed acyclic graph on a vertex population and a vertex, the child set is the finite set of all vertices to which that vertex has a directed edge.
For a finite vertex population with decidable equality and a directed acyclic graph on that population, the ancestor relation holds from one vertex to another exactly when there is a directed path from the former to the latter. It is established either by a directed edge from the former vertex to the latter or by an existing ancestor path followed by a directed edge.
Definition (Lean source)
For a finite directed acyclic graph on a vertex population and two vertices, the first and the second, the descendant relation holds precisely when there is a directed path from the second vertex to the first.
Definition (Lean source)
For a finite directed acyclic graph on a vertex population and a finite vertex set, one backward ancestor-expansion step returns that set together with every parent of every member of the set.
For a finite directed acyclic graph on a vertex population and a vertex, the strict-ancestor set is obtained by starting with the vertex’s parents and applying backward ancestor expansion once for each vertex in the population.
For a finite directed acyclic graph on a vertex population and a vertex, the ancestor set is the finite set of all vertices from which a directed path reaches that vertex.
For a finite directed acyclic graph on a vertex population and a vertex, the descendant set is the finite set of all vertices reachable from that vertex by a directed path.
For a finite directed acyclic graph on a vertex population and a finite vertex set, the set of its strict ancestors contains exactly the vertices from which a directed path reaches at least one member of the given set.
For a finite directed acyclic graph on a vertex population and a finite vertex set, its ancestral closure is that set together with every vertex from which a directed path reaches one of its members.
For a finite directed acyclic graph on a vertex population and a finite vertex set, the set of its strict descendants contains exactly the vertices reachable by a directed path from at least one member of the given set.
For a finite directed acyclic graph on a vertex population and a vertex, the non-descendant set contains exactly the vertices other than that vertex which cannot be reached from it by a directed path.
For a finite directed acyclic graph on a vertex population and a vertex, its ancestor rank is the number of that vertex’s strict ancestors.
Definition (Lean source)
For a finite directed acyclic graph on a vertex population and a vertex, the derived topological number is its number of strict ancestors times the population size, plus a fixed tie-breaking enumeration number. This number is injective across vertices and strictly increases along every directed edge.
For a finite directed acyclic graph on a vertex population and a vertex, the root condition holds exactly when no directed edge enters that vertex.
Definition (Lean source)
For a finite directed acyclic graph on a vertex population, the root set is the finite set of all vertices with no incoming directed edge.
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)
24 supporting declarations (lemmas, instances)
-
mem_parentstheorem — Membership characterization for parents: u ∈ G.parents v ↔ G.edge u v.Proof (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.Proof (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.hypothesesconclusionG.isAncestor u v ↔ TransGen G.edge u vProof (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 -
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). -
isAncestor_irrefltheorem — Ancestor relation is irreflexive: no vertex is its own ancestor (this is acyclicity, restated for the inductive ancestor relation).Proof (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.hypothesesconclusionG.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.hypothesesconclusionG.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.hypothesesV :sharedType u_2S₀ :Finset Vk :ℕhstrict :∀ jifj < kthen(f^[j] S₀).card < (f^[j + 1] S₀).cardconclusion(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.hypothesesconclusionG.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.hypothesesconclusionu ∈ 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.hypothesesconclusionu ∈ 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 — For a finite vertex population with decidable equality and a directed acyclic graph on that population, the decision procedure for the ancestor relation determines, for every ordered pair of vertices, whether the first is an ancestor of the second.parametersV :sharedType u_2instancegiven byfun 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.hypothesesconclusionu ∈ 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.hypothesesconclusionw ∈ 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.Proof (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.Proof (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.hypothesesconclusionG.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.Proof (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.hypothesesconclusionG.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.hypothesesconclusionG.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) -
decIsRootinstance — For a finite vertex population with decidable equality, a directed acyclic graph on that population, and a vertex, the decision procedure for the root condition determines whether no directed edge enters that vertex. -
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.
For a collection of base variables, the population of nodes in a single-world intervention graph consists of a random-node constructor that assigns each base variable its natural random copy and a fixed-node constructor that assigns each base variable its intervention copy. Thus it is the disjoint union of two copies of the base-variable population.
The split-node equivalence bijects each random copy of a base variable with the first copy of that variable and each fixed copy with the second copy.
For a family of value spaces indexed by base variables, the single-world-intervention value-space family assigns to each random copy its base variable's value space and to each fixed copy that same base variable's value space.
Definition (Lean source)
For a finite directed acyclic graph and a set of intervention targets, the single-world-intervention edge relation declares that a random copy points to a random copy precisely when the corresponding original edge starts outside the targets, that a fixed copy points to a random copy precisely when its base variable is targeted and has the corresponding original outgoing edge, and that every other ordered pair has no edge.
For a finite directed acyclic graph, the interleaved topological order of its split nodes assigns each random copy one plus twice its base variable's topological position and each fixed copy twice that position.
For a finite directed acyclic graph and a set of intervention targets, the single-world intervention graph as a directed acyclic graph is obtained by replacing every outgoing edge of a targeted variable by an edge from its fixed copy while retaining all incoming edges to its random copy.
Definition (Lean source)
The link map on split nodes sends every fixed copy of a base variable to its random copy and leaves every random copy at that random copy.
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
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)
For a finite directed acyclic graph, the initial single-world intervention graph is its split-node graph with no intervention targets, so every original edge joins random copies and every fixed copy is isolated.
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)
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)
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)
For a single-world intervention graph and a fixed intervention node in that graph, the canonical link map returns its random counterpart, together with the fact that this counterpart is observed.
Definition (Lean source)
For a single-world intervention graph and a fixed intervention node in that graph, the node-level canonical link is that node's random counterpart, with the membership certification omitted.
For a single-world intervention graph and a base variable whose fixed copy belongs to its fixed nodes, the base-variable link map returns the same base variable together with the fact that its random copy is observed.
For a single-world intervention graph, the standard-graph property holds exactly when it contains no fixed intervention nodes.
Definition (Lean source)
For two single-world intervention graphs, graph equivalence ignoring topological order holds exactly when they have the same directed edges, the same fixed nodes, the same observed nodes, and the same unobserved nodes.
Definition (Lean source)
21 supporting declarations (lemmas, instances)
-
instDecidableEqSWIGNodeinstancederiving DecidableEq, Repr -
instReprSWIGNodeinstancederiving DecidableEq, Repr -
random_injectivetheorem — The random-node constructor is injective: equal random SWIG nodes come from the same base variable. -
fixed_injectivetheorem — The fixed-node constructor is injective: equal fixed SWIG nodes come from the same base variable. -
instFintypeinstance — For a finite collection of base variables, the finite enumeration of its split SWIG nodes contains exactly the random and fixed copy of every base variable. -
instMeasurableSpaceSwigΩinstance — For a collection of base variables, a family of base-variable value spaces, each equipped with a σ-algebra, and any split node, the σ-algebra on that node's SWIG value space is the σ-algebra of the corresponding base-variable value space.parametersinstance -
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)
@[fun_prop] 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)
@[fun_prop] 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 — For a collection of base variables, a family of value spaces each equipped with a σ-algebra and forming a standard Borel space, and any split node, the standard Borel-space structure on that node's SWIG value space is inherited from the corresponding base-variable value space.parametersinstance -
instNonemptySwigΩinstance — For a collection of base variables, a family of nonempty base-variable value spaces, and any split node, the nonemptiness guarantee for that node's SWIG value space is inherited from the corresponding base-variable value space.parametersN :Type*Ω :N → Type*∀ n, Nonempty (Ω n)sn :instance -
swigEdge_decidableinstance — For a finite collection of base variables with decidable equality, a directed acyclic graph on those variables, and a finite set of intervention targets, the decision procedure for the single-world-intervention edge relation determines, for every ordered pair of split nodes, whether the pair is joined by a SWIG edge.parametersinstancegiven byby 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.hypothesesconclusionG.iotaNode s = iotaMap sProof (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.
For a single-world intervention graph, a set of active split nodes, and two split nodes, the induced edge relation holds exactly when the original graph has the directed edge, the first endpoint belongs to the active set, and the second endpoint belongs to the active set.
For a single-world intervention graph and a set of active split nodes, the induced directed acyclic graph retains exactly the original directed edges whose two endpoints are active.
Definition (Lean source)
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)
For a single-world intervention graph and a retained set of split nodes, the induced single-world intervention graph has as its observed nodes the retained observed nodes, fixed nodes precisely those original fixed nodes whose random counterparts remain observed, unobserved nodes precisely those original unobserved nodes with an edge into the retained observed nodes, and directed edges precisely the original edges with both endpoints among these retained nodes.
Definition (Lean source)
5 supporting declarations (lemmas, instances)
-
inducedEdge_decidableinstance — For a finite collection of base variables with decidable equality, a single-world intervention graph, and a set of active split nodes, the decision procedure for the induced edge relation determines, for every ordered pair of split nodes, whether the original graph joins them by an edge and both endpoints are active. -
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.hypothesesconclusionconclusion 1u ∈ activeconclusion 2v ∈ 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.
Given an edge relation on a finite vertex set for which no vertex can return to itself by a nonempty directed path, the directed acyclic graph constructed from that relation has precisely that edge relation.
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)
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.
For a single-world intervention graph and two split nodes, the direct-confounding relation holds exactly when the nodes are distinct and some unobserved node has a directed edge to each of them.
For a single-world intervention graph and a split node, the bidirected-neighbor set consists exactly of the graph's observed nodes that are directly confounded with that node.
For a finite collection of base variables with decidable equality and a single-world intervention graph, the bidirected-reachability relation on split nodes is generated by relating each observed split node to itself and by extending any such relation across a direct-confounding link from its current endpoint. Two observed nodes are therefore related exactly through a finite chain of direct-confounding links.
Definition (Lean source)
For a single-world intervention graph and a starting split node, the breadth-first bidirected-reachability set is the set reached by repeatedly adding observed nodes directly confounded with the current frontier, starting from the given node when it is observed and otherwise returning the empty set.
Definition (Lean source)
For a single-world intervention graph and a split node, the c-component associated with that node is its breadth-first bidirected-reachability set.
For a single-world intervention graph, the array of c-components is formed by scanning its observed nodes and appending a node's c-component exactly when that node is not already contained in a previously appended component.
For a single-world intervention graph, the canonical set of c-components is the set of c-components associated with its observed nodes, with duplicate components identified.
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
Proof (Lean source)
The c-components cover exactly the observed nodes: their union recovers the set of observed nodes exactly.
Formal statement
Proof (Lean source)
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
Proof (Lean source)
Distinct c-components are pairwise disjoint: no observed node belongs to two different c-components.
Formal statement
Proof (Lean source)
22 supporting declarations (lemmas, instances)
-
decDirectlyConfoundedinstance — For a finite collection of base variables with decidable equality, a single-world intervention graph, and two split nodes, the decision procedure for direct confounding determines whether the nodes are distinct and have a common unobserved parent in the graph. -
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).hypothesesconclusionG.directlyConfounded v₂ v₁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).hypothesesconclusionu ∈ G.observedProof (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).hypothesesconclusionv ∈ G.observedProof (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.hypothesesN :sharedType u_1u v w :SWIGNode Nhuv :G.directlyConfounded u vhvw :G.bidirectedReachable v wconclusionG.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.hypothesesconclusionG.bidirectedReachable v uProof (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.hypothesesN :sharedType u_1u v w :SWIGNode Nhuv :G.bidirectedReachable u vhvw :G.bidirectedReachable v wconclusionG.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.hypothesesconclusionG.bidirectedNeighbors v ⊆ G.observedProof (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.hypothesesN :sharedType u_1fuel :ℕhvis :visited ⊆ G.observedconclusionbidirectedBFS.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.hypothesesconclusionG.bidirectedBFS start ⊆ G.observedProof (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).hypothesesconclusionstart ∈ G.bidirectedBFS startProof (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.hypothesesN :sharedType u_1start :SWIGNode Nfuel :ℕ(∀ y ∈ visited, G.bidirectedReachable start y)(∀ y ∈ frontier, G.bidirectedReachable start y)z ∈ bidirectedBFS.go G frontier visited fuel :conclusionG.bidirectedReachable start zProof (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.hypothesesN :sharedType u_1fuel :sharedℕfuel :ℕ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 bconclusionb ∈ 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.hypothesesconclusionG.cComponentOf v ⊆ G.observedProof (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.hypothesesconclusionv ∈ G.cComponentOf vProof (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.hypothesesconclusionC ⊆ 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.hypothesesconclusionG.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.
For a finite vertex set with decidable equality, a directed-edge relation on its random and fixed copies, and a finite set of vertices selected for splitting, the monolithic split edge relation removes every edge leaving the random copy of a selected vertex and otherwise retains the corresponding original edge, while each fixed copy of a selected vertex inherits the outgoing edges of its random copy and every other fixed copy retains its original outgoing edges.
Definition (Lean source)
For a finite vertex set with decidable equality, a SWIG graph, and a finite set of vertices selected for splitting, the topological-order assignment for the monolithically split graph assigns each random copy twice its original topological rank plus one, and assigns each selected fixed copy twice the original rank of its random copy, while assigning each unselected fixed copy twice its own original rank plus one.
Definition (Lean source)
For a finite vertex set with decidable equality, a SWIG graph, and a finite set of vertices selected for splitting, the monolithically split directed acyclic graph is the directed acyclic graph obtained by rerouting, in one operation, every edge from the random copy of a selected vertex to instead leave that vertex's fixed copy.
Definition (Lean source)
For a finite vertex set with decidable equality, a SWIG graph, and a finite set of vertices selected for splitting, provided that the random copy of every selected vertex is an observed vertex of the graph and the fixed copy of every selected vertex is not already among the graph's fixed vertices, the monolithic multi-target split SWIG graph is obtained by rerouting every outgoing edge of each selected random copy to leave the corresponding fixed copy, while adding those fixed copies to the fixed vertices and retaining the observed and unobserved vertices.
Definition (Lean source)
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
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
splitMonoEdgeRel_decidableinstance — For a collection of base variables with decidable equality, a directed-edge relation on split nodes for which every proposed edge can be decided, and a finite set of vertices selected for splitting, the decision procedure for the monolithic split edge relation determines, for every ordered pair of split nodes, whether that pair is joined after the split.parametersinstancegiven byby 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.hypothesesN :sharedType u_1G :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.hypothesesN :sharedType u_1G :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.hypothesesN :sharedType u_1G :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.hypothesesN :sharedType u_1G :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.hypothesesh :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