SCM.ID.Assumptions
Structural assumptions used by SCM identification results, including monotone Boolean mechanisms and finite Boolean-chain example models.
Monotonicity 15 core · 8 supporting This file defines monotonicity as a restriction on a structural equation itself. ★ monotoneBoolSCM_satisfies★ antitoneBoolSCM_violates
Structural Monotonicity Assumptions
This file defines monotonicity as a restriction on a structural equation itself. The predicate fixes an observed child and one of its parents, then requires the child's structural function to be nondecreasing in that parent coordinate while all other parent coordinates are held fixed.
The file also contains a two-node Boolean SCM used as a sanity check: one model
satisfies the structural restriction and one model violates it. These witnesses
show that the predicate is a genuine constraint on structFun, not a vacuous
edge label.
def MonotoneMechanism reviewed
⚑ flagged
Causalean.SCM.Assumptions
Raising one parent coordinate cannot decrease the child equation.
Definition (Lean source)
def MonotoneMechanism [∀ n, Preorder (Ω n)]
(child parent : SWIGNode N) (M : SCM N Ω) : Prop :=
∃ hchild : child ∈ M.observed,
∃ hparent : parent ∈ M.dag.parents child,
∀ x y : ∀ w : {w // w ∈ M.dag.parents child}, swigΩ Ω w.val,
x ⟨parent, hparent⟩ ≤ y ⟨parent, hparent⟩ →
(∀ w, w.val ≠ parent → x w = y w) →
M.structFun ⟨child, hchild⟩ x ≤ M.structFun ⟨child, hchild⟩ y
inductive BoolChainNode reviewed
⚑ flagged
Causalean.SCM.Assumptions
Two variables for the Boolean monotonicity sanity check.
Definition (Lean source)
def edge reviewed
⚑ flagged
Causalean.SCM.Assumptions.BoolChainNode
The Boolean witness has one directed edge, from treatment d to outcome y.
Definition (Lean source)
def topo reviewed
⚑ flagged
Causalean.SCM.Assumptions.BoolChainNode
The topological order places the parent before the child.
Definition (Lean source)
def topo : BoolChainNode → ℕ
| d => 0
| y => 1
def dag reviewed
⚑ flagged
Causalean.SCM.Assumptions.BoolChainNode
The two-node DAG used by the Boolean monotonicity witnesses.
Definition (Lean source)
def dag : DAG BoolChainNode where
edge := edge
decEdge := edgeDecidable
acyclic := DAG.acyclic_of_topoOrder topo_lt
def boolChainSWIG reviewed
⚑ flagged
Causalean.SCM.Assumptions
The standard SWIG graph for the two-node Boolean witness.
Definition (Lean source)
def boolChainSWIG : SWIGGraph BoolChainNode where
dag := initialSWIG BoolChainNode.dag
fixed := ∅
observed := {SWIGNode.random d, SWIGNode.random y}
unobserved := ∅
fixed_is_fixed := by intro s hs; simp at hs
observed_is_random := by
intro v hv
simp only [Finset.mem_insert, mem_singleton] at hv
rcases hv with rfl | rfl <;> exact ⟨_, rfl⟩
unobserved_is_random := by intro u hu; simp at hu
obs_unobs_disjoint := by
rw [Finset.disjoint_right]
intro x hx
simp at hx
dag_edges_classified := by decide
fixed_image_in_observed := by intro s hs; simp at hs
fixed_are_roots := by intro s hs; simp at hs
unobs_are_roots := by intro u hu; simp at hu
fixed_outside_fixed_isolated := by
intro n _
cases n <;> exact ⟨by decide, by decide⟩
all_children_in_observed := by decide
def boolChainΩ reviewed
⚑ flagged
Causalean.SCM.Assumptions
Every variable in the Boolean witness has Boolean values.
Definition (Lean source)
def boolChainΩ : BoolChainNode → Type := fun _ => Bool
def boolChainDParent reviewed
⚑ flagged
Causalean.SCM.Assumptions
The designated parent coordinate for the Boolean witness outcome.
Definition (Lean source)
def boolChainDParent :
{w // w ∈ boolChainSWIG.dag.parents (SWIGNode.random y)} :=
⟨SWIGNode.random d, by decide⟩
def copyStructFun reviewed
⚑ flagged
Causalean.SCM.Assumptions
The Boolean copying structural equation for the witness SCM.
Definition (Lean source)
def copyStructFun (v : {v // v ∈ boolChainSWIG.observed}) :
(∀ w : {w // w ∈ boolChainSWIG.dag.parents v.val}, swigΩ boolChainΩ w.val) →
swigΩ boolChainΩ v.val := by
rcases v with ⟨n, hn⟩
cases n with
| random n =>
cases n with
| d => exact fun _ => false
| y => exact fun parents => parents boolChainDParent
| fixed n =>
cases n <;> simp [boolChainSWIG] at hn
def flipStructFun reviewed
⚑ flagged
Causalean.SCM.Assumptions
The Boolean reversing structural equation for the witness SCM.
Definition (Lean source)
def flipStructFun (v : {v // v ∈ boolChainSWIG.observed}) :
(∀ w : {w // w ∈ boolChainSWIG.dag.parents v.val}, swigΩ boolChainΩ w.val) →
swigΩ boolChainΩ v.val := by
rcases v with ⟨n, hn⟩
cases n with
| random n =>
cases n with
| d => exact fun _ => false
| y => exact fun parents => !parents boolChainDParent
| fixed n =>
cases n <;> simp [boolChainSWIG] at hn
def monotoneBoolSCM reviewed
⚑ flagged
Causalean.SCM.Assumptions
A Boolean SCM whose outcome equation copies the parent value.
Definition (Lean source)
noncomputable def monotoneBoolSCM : SCM BoolChainNode boolChainΩ where
toSWIGGraph := boolChainSWIG
edgeTypes := EdgeTypeAssignment.allNonparametric boolChainSWIG.dag
iota_valueSpace := by
intro s
exact (notMem_empty s.val s.property).elim
structFun := copyStructFun
structFun_measurable := copyStructFun_measurable
latentDist := fun u => (notMem_empty u.val u.property).elim
isProbability_latent := by
intro u
exact (notMem_empty u.val u.property).elim
def antitoneBoolSCM reviewed
⚑ flagged
Causalean.SCM.Assumptions
A Boolean SCM whose outcome equation reverses the parent value.
Definition (Lean source)
noncomputable def antitoneBoolSCM : SCM BoolChainNode boolChainΩ where
toSWIGGraph := boolChainSWIG
edgeTypes := EdgeTypeAssignment.allNonparametric boolChainSWIG.dag
iota_valueSpace := by
intro s
exact (notMem_empty s.val s.property).elim
structFun := flipStructFun
structFun_measurable := flipStructFun_measurable
latentDist := fun u => (notMem_empty u.val u.property).elim
isProbability_latent := by
intro u
exact (notMem_empty u.val u.property).elim
def boolParentAssignment reviewed
⚑ flagged
Causalean.SCM.Assumptions
The Boolean parent assignment that sets the designated parent to b.
Definition (Lean source)
def boolParentAssignment (b : Bool) :
∀ w : {w // w ∈ boolChainSWIG.dag.parents (SWIGNode.random y)},
swigΩ boolChainΩ w.val := by
intro w
rcases w with ⟨n, _⟩
cases n with
| random n =>
cases n with
| d => exact b
| y => exact false
| fixed n =>
cases n <;> exact false
theorem monotoneBoolSCM_satisfies reviewed
⚑ flagged
Causalean.SCM.Assumptions
The copying Boolean structural causal model satisfies monotonicity of the outcome mechanism in the designated parent coordinate.
Formal statement
conclusion
Proof (Lean source)
theorem monotoneBoolSCM_satisfies :
MonotoneMechanism (Ω := boolChainΩ)
(SWIGNode.random y) (SWIGNode.random d) monotoneBoolSCM := by
refine ⟨by simp [monotoneBoolSCM, boolChainSWIG], boolChainDParent.property, ?_⟩
intro x y hxy _
exact hxy
theorem antitoneBoolSCM_violates reviewed
⚑ flagged
Causalean.SCM.Assumptions
The reversing Boolean structural causal model violates monotonicity of the outcome mechanism in the designated parent coordinate.
Formal statement
conclusion
Proof (Lean source)
theorem antitoneBoolSCM_violates :
¬ MonotoneMechanism (Ω := boolChainΩ)
(SWIGNode.random y) (SWIGNode.random d) antitoneBoolSCM := by
intro hmono
rcases hmono with ⟨hchild, hparent, hmono⟩
have hle :
boolParentAssignment false ⟨SWIGNode.random d, hparent⟩ ≤
boolParentAssignment true ⟨SWIGNode.random d, hparent⟩ := by
change false ≤ true
decide
have hsame :
∀ w, w.val ≠ SWIGNode.random d →
boolParentAssignment false w = boolParentAssignment true w := by
intro w hw
rcases w with ⟨n, hn⟩
cases n with
| random n =>
cases n with
| d => simp at hw
| y => rfl
| fixed n =>
cases n <;> rfl
have hbad := hmono (boolParentAssignment false) (boolParentAssignment true) hle hsame
change not (boolParentAssignment false boolChainDParent) ≤
not (boolParentAssignment true boolChainDParent) at hbad
simp only [boolParentAssignment_boolChainDParent] at hbad
cases hbad rfl
8 supporting declarations (lemmas, instances)
-
instPreorderSwigΩinstance — The SWIG value spaces inherit the base-variable order.instance instPreorderSwigΩ [∀ n, Preorder (Ω n)] : ∀ s : SWIGNode N, Preorder (swigΩ Ω s) | .random _ => inferInstance | .fixed _ => inferInstance -
instDecidableEqBoolChainNodeinstancederiving DecidableEq, Repr -
instReprBoolChainNodeinstancederiving DecidableEq, Repr -
instFintypeinstance — The Boolean witness type has exactly the two elements d and y.instance instFintype : Fintype BoolChainNode where elems := {d, y} complete := by intro x; cases x <;> decide -
edgeDecidableinstanceinstance edgeDecidable : DecidableRel edge := by intro a b cases a <;> cases b · exact isFalse (fun h => h) · exact isTrue trivial · exact isFalse (fun h => h) · exact isFalse (fun h => h) -
boolChainMeasurableSpaceinstanceinstance boolChainMeasurableSpace : ∀ n, MeasurableSpace (boolChainΩ n) | d => ⊤ | y => ⊤ -
boolParentAssignment_boolChainDParenttheorem — Evaluating the Boolean parent assignment at the designated parent returns the assigned value.Proof (Lean source)
@[simp] theorem boolParentAssignment_boolChainDParent (b : Bool) : boolParentAssignment b boolChainDParent = b := by cases b <;> rfl