SCM.Examples
Worked structural-causal-model examples (instrumental variables and related DAGs) exercising the SCM and identification layers.
BackDoor 8 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 node type consists of the treatment vertex, the outcome vertex, the observed-confounder vertex, the latent root for the confounder, the latent root for treatment, and the latent root for the outcome.
Definition (Lean source)
For each vertex of the backdoor-adjustment DAG and each natural-number precedence level, this method returns a formatted textual rendering of that vertex. There are no additional hypotheses or side conditions.
Definition (Lean source)
The backdoor-edge relation contains exactly the arrow from the observed confounder to treatment, the arrow from the observed confounder to outcome, the arrow from treatment to outcome, the arrow from the first latent root to the confounder, the arrow from the second latent root to treatment, and the arrow from the third latent root to outcome; all other ordered pairs have no edge.
The topological-order label for the backdoor graph assigns label 0 to the first latent root, label 1 to the second latent root, label 2 to the third latent root, label 3 to the observed confounder, label 4 to treatment, and label 5 to 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.
Formal statement
The backdoor-adjustment directed acyclic graph has the specified backdoor edge relation and the displayed topological ordering, and is therefore acyclic.
The pre-intervention SWIG graph for the backdoor example has the backdoor directed acyclic graph, no fixed nodes, treatment, outcome, and confounder as observed random nodes, and the three latent roots as unobserved random nodes.
Definition (Lean source)
The edge-type assignment for the backdoor graph classifies every graph edge as nonparametric.
Definition (Lean source)
4 supporting declarations (lemmas, instances)
-
instDecidableEqBDNodeinstancederiving DecidableEq -
instFintypeBDNodeinstance — A finite enumeration of the backdoor-example node type is provided by the collection of its six named vertices together with the assertion that every backdoor-example vertex belongs to that collection. -
instDecidableRelBDNodeBdEdgeinstance — For every ordered pair of backdoor-example vertices, a decision procedure for whether the pair is a directed edge is provided.instancegiven byby 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 node set of the continuous-backdoor example consists of three positions representing, in order, the confounder, treatment, and outcome.
Definition (Lean source)
The value-space assignment for the continuous-backdoor example gives every node the real-valued state space.
Definition (Lean source)
The confounder node index is the first of the three node positions in the continuous-backdoor example.
Definition (Lean source)
The treatment node index is the second of the three node positions in the continuous-backdoor example.
Definition (Lean source)
The outcome node index is the third of the three node positions in the continuous-backdoor example.
Definition (Lean source)
The Boolean edge indicator is true exactly for an arrow from confounder to treatment, from confounder to outcome, or from treatment to outcome.
The edge relation of the continuous-backdoor graph holds exactly when the Boolean edge indicator is true, namely for arrows from confounder to treatment or outcome and from treatment to outcome.
Definition (Lean source)
The topological-order label of the continuous-backdoor graph is each node's position, so it places the confounder before treatment and treatment before outcome.
Definition (Lean source)
The directed acyclic graph of the continuous backdoor example has the stated three-node edge relation and topological ordering, and is acyclic.
The pre-intervention SWIG graph for the continuous-backdoor example has no fixed or unobserved nodes and has the confounder, treatment, and outcome as observed random nodes.
Definition (Lean source)
The continuous-backdoor structural causal model has the specified real-valued pre-intervention graph, no latent variables, nonparametric edges, and constant-zero structural responses for every observed node.
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 — For every ordered pair of continuous-backdoor vertices, a decision procedure for whether the pair is a directed edge is provided.instancegiven byby intro a b; unfold cbEdge; infer_instance -
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.hypothesesD ∈ ({Xidx} : Finset CBNode) :conclusionSWIGNode.random D ∈ cbSWIGGraph.observed -
cb_Xfixedtheorem — The treatment's fixed node is not already fixed in the computable continuous-backdoor SWIG graph.hypothesesD ∈ ({Xidx} : Finset CBNode) :conclusionSWIGNode.fixed D ∉ cbSWIGGraph.fixedProof (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 node type consists of the latent-confounder vertex, the treatment vertex, the mediator vertex, and the outcome vertex.
Definition (Lean source)
The frontdoor-edge relation contains exactly the arrow from the latent confounder to treatment, the arrow from the latent confounder to outcome, the arrow from treatment to the mediator, and the arrow from the mediator to outcome; all other ordered pairs have no edge.
The topological-order label for the frontdoor graph assigns label 0 to the latent confounder, label 1 to treatment, label 2 to the mediator, and label 3 to 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.
Formal statement
The frontdoor directed acyclic graph has the specified frontdoor edge relation and topological ordering, and is acyclic.
The pre-intervention SWIG graph for the frontdoor example has the frontdoor directed acyclic graph, no fixed nodes, treatment, mediator, and outcome as observed random nodes, and the latent confounder as an unobserved random node.
Definition (Lean source)
4 supporting declarations (lemmas, instances)
-
instDecidableEqFDNodeinstancederiving DecidableEq, Repr -
instReprFDNodeinstancederiving DecidableEq, Repr -
instFintypeFDNodeinstance — A finite enumeration of the frontdoor-example node type is provided by the collection of its four named vertices together with the assertion that every frontdoor-example vertex belongs to that collection. -
instDecidableRelFDNodeFdEdgeinstance — For every ordered pair of frontdoor-example vertices, a decision procedure for whether the pair is a directed edge is provided.instancegiven byby intro a b; cases a <;> cases b <;> simp [fdEdge] <;> infer_instance
IV 11 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.
For the instrumental-variable example, the set of node categories consists of an instrument, a treatment, an outcome, and an unobserved confounder.
Definition (Lean source)
For each vertex of the instrumental-variable DAG and each natural-number precedence level, this method returns a formatted textual rendering of that vertex. There are no additional hypotheses or side conditions.
The instrumental-variable edge relation contains exactly the arrow from instrument to treatment, the arrow from treatment to outcome, the arrow from the latent confounder to treatment, and the arrow from the latent confounder to outcome; all other ordered pairs have no edge.
The topological-order label for the instrumental-variable graph assigns label 0 to the latent confounder, label 1 to the instrument, label 2 to treatment, and label 3 to 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.
Formal statement
The instrumental-variable directed acyclic graph has the stated instrumental-variable edge relation and topological ordering, and is acyclic.
The pre-intervention SWIG graph for the instrumental-variable example has the instrumental-variable directed acyclic graph, no fixed nodes, instrument, treatment, and outcome as observed random nodes, and the latent confounder as an unobserved random node.
Definition (Lean source)
The edge-type assignment for the instrumental-variable graph classifies the instrument-to-treatment edge as strictly increasing and classifies every other ordered pair as nonparametric.
Definition (Lean source)
The value-space assignment for the toy instrumental-variable model gives every node a one-point state space.
The toy instrumental-variable structural causal model has the stated instrumental-variable graph, one-point node value spaces, constant structural functions, and a point-mass distribution for the latent root.
Definition (Lean source)
The intervention graph for treatment in the instrumental-variable example is the single-world intervention graph obtained by fixing treatment in the instrumental-variable directed acyclic graph.
5 supporting declarations (lemmas, instances)
-
instDecidableEqIVNodeinstancederiving DecidableEq -
instFintypeIVNodeinstance — The finite enumeration of instrumental-variable nodes lists the instrument, treatment, outcome, and unobserved confounder, and establishes that every such node occurs in that list. -
instDecidableRelIVNodeIvEdgeinstance — Decidability of the instrumental-variable edge relation determines, for every ordered pair of instrumental-variable nodes, whether that pair is an edge.instancegiven byby intro a b cases a <;> cases b <;> first | exact isTrue trivial | exact isFalse (by simp only [ivEdge]; exact fun h => h) -
ivΩ_measurableinstance — For each node of the toy instrumental-variable model, the measurable structure on its one-point value space is the trivial measurable structure.
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.
For a Boolean value, its real-valued score is one when it is true and zero when it is false.
Definition (Lean source)
For a Boolean-chain structural causal model and a Boolean treatment value, the outcome-parent assignment gives each coordinate corresponding to a parent of the outcome that treatment value when it is the designated treatment parent and false otherwise.
Definition (Lean source)
For each Boolean-chain structural causal model, the monotone response contrast is the real-valued difference between the scored outcome response when the designated treatment parent is true and when it is false, and it is zero whenever the outcome is not observed or the designated treatment parent is absent.
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]