SCM.Examples
Worked structural-causal-model examples (instrumental variables and related DAGs) exercising the SCM and identification layers.
BackDoor 7 core · 4 supporting This file constructs the canonical directed acyclic graph for backdoor adjustment, with a treatment, an outcome, an observed confounder, and latent root noise variables. ★ bdTopo_lt
Backdoor Adjustment Example
This file constructs the canonical directed acyclic graph for backdoor
adjustment, with a treatment, an outcome, an observed confounder, and latent root
noise variables. The declarations BDNode, bdEdge, bdDAG, and bdSWIG
define the graph and its standard SWIG representation. The examples check
parents, roots, c-components, ID reachability, and the split-graph
d-separation condition behind the graphical backdoor criterion; the final
backdoor-criterion example verifies that the observed confounder is a valid
adjustment set for the treatment-outcome effect.
The backdoor example has treatment, outcome, observed-confounder, and three latent-root vertices.
Definition (Lean source)
The backdoor graph has confounding paths through the observed confounder, a direct treatment-outcome edge, and one latent root for each observed node.
The backdoor graph orders latent roots first, then confounder, treatment, and outcome.
Definition (Lean source)
Every edge of the backdoor-example graph connects a node with a strictly smaller assigned order label to one with a strictly larger label — the chosen ordering is a valid topological order for the graph.
This directed acyclic graph formalizes the canonical backdoor-adjustment example.
This SWIG graph represents the backdoor example before any intervention.
Definition (Lean source)
The backdoor example treats every graph edge as nonparametric.
Definition (Lean source)
4 supporting declarations (lemmas, instances)
-
instDecidableEqBDNodeinstancederiving DecidableEq -
instDecidableRelBDNodeBdEdgeinstance — Whether a proposed backdoor-example edge is present is decidable by case analysis on the endpoints.instance : DecidableRel bdEdge := by intro a b; cases a <;> cases b <;> simp [bdEdge] <;> infer_instance
ContinuousBackdoor 13 core · 10 supporting This file gives a real-valued backdoor example in which the confounder, treatment, and outcome all take values in ℝ. ★ cb_backdoor_criterion★ cb_backdoor_identified
Real-Valued Backdoor Example
This file gives a real-valued backdoor example in which the confounder,
treatment, and outcome all take values in ℝ. The declarations CBNode,
CBΩ, cbDAG, cbSWIGGraph, and continuousBackdoorSCM build a degenerate
constant structural model whose purpose is to exercise the real-valued graph and
kernel interfaces. The theorem cb_backdoor_criterion verifies the graphical
backdoor criterion by computation, and cb_backdoor_identified applies the
kernel-based backdoor pipeline once the required overlap and positivity
conditions are supplied as hypotheses.
The continuous-backdoor example has three nodes: confounder, treatment, and outcome.
Definition (Lean source)
Every node in the continuous-backdoor example takes real values.
Definition (Lean source)
This node index denotes the confounder in the continuous-backdoor example.
Definition (Lean source)
This node index denotes the treatment in the continuous-backdoor example.
Definition (Lean source)
This node index denotes the outcome in the continuous-backdoor example.
Definition (Lean source)
The edge indicator records confounder-to-treatment, confounder-to-outcome, and treatment-to-outcome arrows.
The edge relation says exactly that the confounder points to treatment and outcome, and treatment points to outcome.
Definition (Lean source)
The continuous-backdoor graph orders confounder before treatment before outcome.
Definition (Lean source)
This directed acyclic graph formalizes the three-node continuous backdoor example.
This computable SWIG graph represents the continuous-backdoor example before any intervention.
Definition (Lean source)
This real-valued backdoor structural model has observed nodes for a confounder, treatment, and outcome, with no latent variables.
Definition (Lean source)
The observed confounder satisfies the graphical backdoor criterion relative to the treatment and outcome nodes in the continuous-backdoor example graph.
Formal statement
Proof (Lean source)
Backdoor adjustment identity on the continuous-backdoor example. Fix an assignment s0 of values to the model's fixed background variables. If for every post-intervention background assignment, the do(X)-intervened marginal law of Z is absolutely continuous with respect to its purely observational marginal law — the Rule-2 joint overlap condition, and the product of the observational marginal laws of the treatment's random image and of Z is absolutely continuous with respect to their joint observational law — the joint positivity condition, then almost everywhere under that product measure, the conditional law of the outcome Y given Z under the intervention that fixes the treatment equals the purely observational conditional law of Y given both the treatment and Z — the backdoor Rule-2 adjustment identity.
Formal statement
Proof (Lean source)
10 supporting declarations (lemmas, instances)
-
instDecidableRelCBNodeCbEdgeinstance — Whether a proposed continuous-backdoor edge is present is decidable by evaluating the edge indicator. -
cbTopo_lttheorem — Every edge in the continuous-backdoor graph points from an earlier to a later node in the chosen topological order. -
cb_Xrand_obstheorem — The treatment's observed random node belongs to the computable continuous-backdoor SWIG graph. -
cb_Xfixedtheorem — The treatment's fixed node is not already fixed in the computable continuous-backdoor SWIG graph.Proof (Lean source)
theorem cb_Xfixed : ∀ D ∈ ({Xidx} : Finset CBNode), SWIGNode.fixed D ∉ cbSWIGGraph.fixed := by intro D _ hmem simp [cbSWIGGraph] at hmem -
cb_Yobstheorem — {random Y} is an observed node set.Proof (Lean source)
-
cb_Zobstheorem — {random Z} (the adjustment set) is an observed node set.Proof (Lean source)
-
cb_Xr_obstheorem — The treatment random-image is observed.Proof (Lean source)
theorem cb_Xr_obs : (({Xidx} : Finset CBNode).image SWIGNode.random) ⊆ continuousBackdoorSCM.observed := by rw [Finset.image_singleton] intro v hv; rw [mem_singleton] at hv; subst hv change SWIGNode.random Xidx ∈ ({SWIGNode.random Zidx, SWIGNode.random Xidx, SWIGNode.random Yidx} : Finset (SWIGNode CBNode)); simp -
cb_XrZ_obstheorem — Treatment random-image together with the adjustment set is observed. -
cb_disj_YXrtheorem — The outcome is disjoint from the treatment random-image. -
cb_disj_XrZtheorem — The treatment random-image is disjoint from the adjustment set.
Frontdoor 6 core · 4 supporting This file constructs the canonical frontdoor graph with one latent confounder between treatment and outcome, an observed mediator, and no intervention fixed at the initial graph. ★ fdTopo_lt
Frontdoor Example
This file constructs the canonical frontdoor graph with one latent confounder
between treatment and outcome, an observed mediator, and no intervention fixed
at the initial graph. The declarations FDNode, fdEdge, fdDAG, and fdSWIG
define the graph and standard SWIG representation. The examples verify the
c-components, show that the recursive ID certificate idSucceedsRec succeeds
for P(Y | do(X)), show that the simpler no-fixing reachability certificate
does not apply to the same outcome district, and check that the executable
idAlgorithm returns true on the concrete graph.
The frontdoor example has latent confounder, treatment, mediator, and outcome vertices.
Definition (Lean source)
The frontdoor graph has latent confounding of X and Y, and the directed path X → M → Y.
The frontdoor graph orders latent confounder, treatment, mediator, then outcome.
Definition (Lean source)
Every edge of the frontdoor-example graph connects a node with a smaller assigned order label to one with a larger label, so the chosen ordering is a valid topological order.
This directed acyclic graph formalizes the canonical frontdoor example.
This SWIG graph represents the frontdoor example before any intervention.
Definition (Lean source)
4 supporting declarations (lemmas, instances)
-
instDecidableEqFDNodeinstancederiving DecidableEq, Repr -
instReprFDNodeinstancederiving DecidableEq, Repr -
instDecidableRelFDNodeFdEdgeinstance — Whether a proposed frontdoor-example edge is present is decidable by endpoint cases.instance : DecidableRel fdEdge := by intro a b; cases a <;> cases b <;> simp [fdEdge] <;> infer_instance
IV 10 core · 5 supporting This file constructs the standard instrumental-variable graph with an instrument, a treatment, an outcome, and an unobserved confounder of the treatment-outcome relationship. ★ ivTopo_lt
Instrumental Variable Example
This file constructs the standard instrumental-variable graph with an instrument, a treatment, an outcome, and an unobserved confounder of the treatment-outcome relationship. It exercises the graphical, component, edge-type, and structural-model interfaces used by instrumental-variable examples elsewhere in the library.
The instrumental-variable example has instrument, treatment, outcome, and unobserved-confounder vertices.
Definition (Lean source)
The instrumental-variable graph has instrument-to-treatment, treatment-to-outcome, and latent-confounder-to-treatment/outcome edges.
The instrumental-variable graph orders the unobserved confounder and instrument before treatment and outcome.
Definition (Lean source)
Every edge of the instrumental-variable example graph connects a node with a smaller assigned order label to one with a larger label, so the chosen ordering is a valid topological order.
This directed acyclic graph formalizes the standard instrumental-variable example.
This SWIG graph represents the instrumental-variable example before any intervention.
Definition (Lean source)
The instrumental-variable edge assignment makes the instrument's effect on treatment strictly increasing and leaves all other edges nonparametric.
Definition (Lean source)
This toy instrumental-variable model uses a one-point value space for every node.
This concrete instrumental-variable structural model realizes the example with one-point value spaces.
Definition (Lean source)
This graph is the SWIG obtained by intervening on the treatment in the instrumental-variable DAG.
5 supporting declarations (lemmas, instances)
-
instDecidableEqIVNodeinstancederiving DecidableEq -
instDecidableRelIVNodeIvEdgeinstance — A proposed instrumental-variable edge is decidable by case analysis on its endpoints.instance : DecidableRel ivEdge := by intro a b cases a <;> cases b <;> first | exact isTrue trivial | exact isFalse (by simp only [ivEdge]; exact fun h => h) -
ivΩ_measurableinstance — Every one-point value space in the toy instrumental-variable model carries the trivial measurable structure.instance ivΩ_measurable : ∀ n, MeasurableSpace (ivΩ n) := fun _ => ⊤
MonotoneCounterfactualBound 6 core · 3 supporting This file gives a worked example of structural monotonicity in a two-node Boolean SCM. ★ monotoneCounterfactualBound★ monotoneCounterfactualBound_assumption_satisfiable★ monotoneCounterfactualBound_fails_without_monotonicity
Monotone Counterfactual Bound Example
This file gives a worked example of structural monotonicity in a two-node
Boolean SCM. The target is the unit-level response contrast of the outcome
equation when the parent coordinate is changed from false to true.
Without any structural restriction that contrast has logical range [-1, 1].
Under the monotone-mechanism assumption it must lie in [0, 1]. The companion
counterexample below uses the reversing Boolean SCM as the reference model to
show that graph and observational compatibility alone do not generally imply a
[0, 1] response-contrast bound.
A Boolean value is scored as one for true and zero for false.
A parent assignment inside an arbitrary Boolean-chain SCM.
Definition (Lean source)
The real-valued response contrast of the Boolean outcome equation.
Definition (Lean source)
Structural monotonicity of the outcome mechanism in the treatment parent forces every response contrast in the compatible class to lie in the valid [0, 1] partial-identification interval.
Formal statement
Proof (Lean source)
The class of structural causal models compatible with the Boolean-chain graph and monotone in the outcome's treatment parent, evaluated against the copying model as reference, is nonempty.
Formal statement
Proof (Lean source)
Without the monotonicity restriction, the unconstrained compatible class's response contrast need not lie in [0, 1].
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
boolParentAssignmentIn_parenttheorem — The designated parent coordinate receives the assigned Boolean value.hypotheseshparent :SWIGNode.random d ∈ M.dag.parents (SWIGNode.random y)b :conclusionboolParentAssignmentIn M b ⟨SWIGNode.random d, hparent⟩ = bProof (Lean source)
@[simp] theorem boolParentAssignmentIn_parent (M : SCM BoolChainNode boolChainΩ) (hparent : SWIGNode.random d ∈ M.dag.parents (SWIGNode.random y)) (b : Bool) : boolParentAssignmentIn M b ⟨SWIGNode.random d, hparent⟩ = b := by cases b <;> rfl -
monotoneResponseContrast_monotoneBoolSCMtheorem — The copying Boolean SCM has response contrast one.conclusionProof (Lean source)
theorem monotoneResponseContrast_monotoneBoolSCM : monotoneResponseContrast monotoneBoolSCM = 1 := by have hchild : SWIGNode.random y ∈ monotoneBoolSCM.observed := by simp [monotoneBoolSCM, boolChainSWIG] have hparent : SWIGNode.random d ∈ monotoneBoolSCM.dag.parents (SWIGNode.random y) := boolChainDParent.property rw [responseContrast_eq_of_present monotoneBoolSCM hchild hparent] change boolScore (boolParentAssignmentIn monotoneBoolSCM true boolChainDParent) - boolScore (boolParentAssignmentIn monotoneBoolSCM false boolChainDParent) = 1 simp [boolScore] -
monotoneResponseContrast_antitoneBoolSCMtheorem — The reversing Boolean SCM has response contrast minus one.conclusionProof (Lean source)
theorem monotoneResponseContrast_antitoneBoolSCM : monotoneResponseContrast antitoneBoolSCM = -1 := by have hchild : SWIGNode.random y ∈ antitoneBoolSCM.observed := by simp [antitoneBoolSCM, boolChainSWIG] have hparent : SWIGNode.random d ∈ antitoneBoolSCM.dag.parents (SWIGNode.random y) := boolChainDParent.property rw [responseContrast_eq_of_present antitoneBoolSCM hchild hparent] change boolScore (not (boolParentAssignmentIn antitoneBoolSCM true boolChainDParent)) - boolScore (not (boolParentAssignmentIn antitoneBoolSCM false boolChainDParent)) = -1 simp [boolScore]