SCM.ID.Assumptions

Structural assumptions used by SCM identification results, including monotone Boolean mechanisms and finite Boolean-chain example models.

Monotonicity 15 core · 10 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

Causalean.SCM.Assumptions

For a finite population of nodes with measurable ordered value spaces, a child node, a parent node, and a structural causal model, the monotone-mechanism condition holds precisely when the child is observed, the parent is a parent of that child, and for every two parent-value assignments that agree at all other parent coordinates and are ordered at the designated parent coordinate, the child's structural-function value is ordered in the same direction.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

∀ n, Preorder (Ω n)

child parent :

SWIGNode N

M :

SCM N Ω

def

MonotoneMechanism child parent M :

Prop

given by

∃ 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

Causalean.SCM.Assumptions.MonotoneMechanism · Causalean/SCM/ID/Assumptions/Monotonicity.lean:38 · uses SCM , SWIGNode

inductive BoolChainNode reviewed

Causalean.SCM.Assumptions

The Boolean-chain node type consists of the treatment node and the outcome node.

Definition (Lean source)

inductive

BoolChainNode :

Type

constructors

d :

y :

deriving DecidableEq, Repr

Causalean.SCM.Assumptions.BoolChainNode · Causalean/SCM/ID/Assumptions/Monotonicity.lean:61

def edge reviewed

Causalean.SCM.Assumptions.BoolChainNode

The Boolean-chain edge relation holds for the ordered pair consisting of treatment $d$ and outcome $y$ , and holds for no other ordered pair of Boolean-chain nodes.

Definition (Lean source)

def

edge :

BoolChainNode → BoolChainNode → Prop

given by

clause 1

| d, y => True

clause 2

| _, _ => False

Causalean.SCM.Assumptions.BoolChainNode.edge · Causalean/SCM/ID/Assumptions/Monotonicity.lean:79 · uses BoolChainNode

def topo reviewed

Causalean.SCM.Assumptions.BoolChainNode

The Boolean-chain topological ranking assigns rank zero to treatment $d$ and rank one to outcome $y$ .

Definition (Lean source)

def

topo :

BoolChainNode → ℕ

given by

clause 1

| d => 0

clause 2

| y => 1

Causalean.SCM.Assumptions.BoolChainNode.topo · Causalean/SCM/ID/Assumptions/Monotonicity.lean:94 · uses BoolChainNode

def dag reviewed

Causalean.SCM.Assumptions.BoolChainNode

The Boolean-chain directed acyclic graph is the two-node graph whose only directed edge is from treatment $d$ to outcome $y$ .

Definition (Lean source)

def

dag :

DAG BoolChainNode

given by

clause 1

edge := edge

clause 2

decEdge := edgeDecidable

clause 3

acyclic := DAG.acyclic_of_topoOrder topo_lt

Causalean.SCM.Assumptions.BoolChainNode.dag · Causalean/SCM/ID/Assumptions/Monotonicity.lean:108 · uses DAG , BoolChainNode , instFintype , instDecidableEqBoolChainNode

def boolChainSWIG reviewed

Causalean.SCM.Assumptions

The Boolean-chain single-world intervention graph has random observed treatment $d$ and outcome $y$ , no fixed nodes, and no unobserved nodes, with the Boolean-chain directed graph.

Definition (Lean source)

def

boolChainSWIG :

SWIGGraph BoolChainNode

given by

clause 1

dag := initialSWIG BoolChainNode.dag

clause 2

fixed := ∅

clause 3

observed := {SWIGNode.random d, SWIGNode.random y}

clause 4

unobserved := ∅

clause 5

fixed_is_fixed := by intro s hs; simp at hs

clause 6

observed_is_random := by intro v hv simp only [Finset.mem_insert, mem_singleton] at hv rcases hv with rfl | rfl <;> exact ⟨_, rfl⟩

clause 7

unobserved_is_random := by intro u hu; simp at hu

clause 8

obs_unobs_disjoint := by rw [Finset.disjoint_right] intro x hx simp at hx

clause 9

dag_edges_classified := by decide

clause 10

fixed_image_in_observed := by intro s hs; simp at hs

clause 11

fixed_are_roots := by intro s hs; simp at hs

clause 12

unobs_are_roots := by intro u hu; simp at hu

clause 13

fixed_outside_fixed_isolated := by intro n _ cases n <;> exact ⟨by decide, by decide⟩

clause 14

all_children_in_observed := by decide

Causalean.SCM.Assumptions.boolChainSWIG · Causalean/SCM/ID/Assumptions/Monotonicity.lean:119 · uses BoolChainNode , instFintype , instDecidableEqBoolChainNode , SWIGGraph

def boolChainΩ reviewed

Causalean.SCM.Assumptions

The Boolean-chain value-space assignment gives both treatment $d$ and outcome $y$ the two-point Boolean value space.

Definition (Lean source)

def

boolChainΩ :

BoolChainNode → Type

given by

fun _ => Bool

Causalean.SCM.Assumptions.boolChainΩ · Causalean/SCM/ID/Assumptions/Monotonicity.lean:146 · uses BoolChainNode

def boolChainDParent reviewed

Causalean.SCM.Assumptions

The designated Boolean-chain outcome-parent coordinate is the random treatment node $d$ , the sole parent of the random outcome node $y$ .

Definition (Lean source)

def

boolChainDParent :

{w // w ∈ boolChainSWIG.dag.parents (SWIGNode.random y)}

given by

⟨SWIGNode.random d, by decide⟩

Causalean.SCM.Assumptions.boolChainDParent · Causalean/SCM/ID/Assumptions/Monotonicity.lean:160 · uses parents , BoolChainNode , instFintype , boolChainSWIG , instDecidableEqBoolChainNode , SWIGNode , instFintype , instDecidableEqSWIGNode

def copyStructFun reviewed

Causalean.SCM.Assumptions

For an observed node of the Boolean-chain graph, the Boolean copying structural equation returns false at treatment $d$ and, at outcome $y$ , returns the value assigned to the treatment-parent coordinate.

Definition (Lean source)

parameters

v :

{v // v ∈ boolChainSWIG.observed}

def

copyStructFun v :

(∀ w : {w // w ∈ boolChainSWIG.dag.parents v.val}, swigΩ boolChainΩ w.val) → swigΩ boolChainΩ v.val

given by

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

Causalean.SCM.Assumptions.copyStructFun · Causalean/SCM/ID/Assumptions/Monotonicity.lean:166 · uses parents , BoolChainNode , instFintype , boolChainSWIG , boolChainΩ , instDecidableEqBoolChainNode , SWIGNode , instFintype , instDecidableEqSWIGNode , swigΩ

def flipStructFun reviewed

Causalean.SCM.Assumptions

For an observed node of the Boolean-chain graph, the Boolean reversing structural equation returns false at treatment $d$ and, at outcome $y$ , returns the Boolean negation of the value assigned to the treatment-parent coordinate.

Definition (Lean source)

parameters

v :

{v // v ∈ boolChainSWIG.observed}

def

flipStructFun v :

(∀ w : {w // w ∈ boolChainSWIG.dag.parents v.val}, swigΩ boolChainΩ w.val) → swigΩ boolChainΩ v.val

given by

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

Causalean.SCM.Assumptions.flipStructFun · Causalean/SCM/ID/Assumptions/Monotonicity.lean:184 · uses parents , BoolChainNode , instFintype , boolChainSWIG , boolChainΩ , instDecidableEqBoolChainNode , SWIGNode , instFintype , instDecidableEqSWIGNode , swigΩ

def monotoneBoolSCM reviewed

Causalean.SCM.Assumptions

The monotone Boolean structural causal model is the Boolean-chain model with no fixed or latent nodes, nonparametric edge labels, and the copying structural equation.

Definition (Lean source)

def

monotoneBoolSCM :

SCM BoolChainNode boolChainΩ

given by

clause 1

toSWIGGraph := boolChainSWIG

clause 2

edgeTypes := EdgeTypeAssignment.allNonparametric boolChainSWIG.dag

clause 3

iota_valueSpace := by intro s exact (notMem_empty s.val s.property).elim

clause 4

structFun := copyStructFun

clause 5

structFun_measurable := copyStructFun_measurable

clause 6

latentDist := fun u => (notMem_empty u.val u.property).elim

clause 7

isProbability_latent := by intro u exact (notMem_empty u.val u.property).elim

Causalean.SCM.Assumptions.monotoneBoolSCM · Causalean/SCM/ID/Assumptions/Monotonicity.lean:232 · uses SCM , BoolChainNode , instFintype , boolChainMeasurableSpace , boolChainΩ , instDecidableEqBoolChainNode

def antitoneBoolSCM reviewed

Causalean.SCM.Assumptions

The antitone Boolean structural causal model is the Boolean-chain model with no fixed or latent nodes, nonparametric edge labels, and the reversing structural equation.

Definition (Lean source)

def

antitoneBoolSCM :

SCM BoolChainNode boolChainΩ

given by

clause 1

toSWIGGraph := boolChainSWIG

clause 2

edgeTypes := EdgeTypeAssignment.allNonparametric boolChainSWIG.dag

clause 3

iota_valueSpace := by intro s exact (notMem_empty s.val s.property).elim

clause 4

structFun := flipStructFun

clause 5

structFun_measurable := flipStructFun_measurable

clause 6

latentDist := fun u => (notMem_empty u.val u.property).elim

clause 7

isProbability_latent := by intro u exact (notMem_empty u.val u.property).elim

Causalean.SCM.Assumptions.antitoneBoolSCM · Causalean/SCM/ID/Assumptions/Monotonicity.lean:250 · uses SCM , BoolChainNode , instFintype , boolChainMeasurableSpace , boolChainΩ , instDecidableEqBoolChainNode

def boolParentAssignment reviewed

Causalean.SCM.Assumptions

For a Boolean value, the Boolean-chain outcome-parent assignment assigns that value to the designated treatment-parent coordinate and false to every other parent coordinate.

Definition (Lean source)

parameters

b :

Bool

w :

{w // w ∈ boolChainSWIG.dag.parents (SWIGNode.random y)}

def

boolParentAssignment b w :

swigΩ boolChainΩ w.val

given by

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

Causalean.SCM.Assumptions.boolParentAssignment · Causalean/SCM/ID/Assumptions/Monotonicity.lean:268 · uses parents , BoolChainNode , instFintype , boolChainSWIG , boolChainΩ , instDecidableEqBoolChainNode , SWIGNode , instFintype , instDecidableEqSWIGNode , swigΩ

theorem monotoneBoolSCM_satisfies reviewed

Causalean.SCM.Assumptions

The copying Boolean structural causal model satisfies monotonicity of the outcome mechanism in the designated parent coordinate.

Formal statement

conclusion

MonotoneMechanism (Ω := boolChainΩ) (SWIGNode.random y) (SWIGNode.random d) monotoneBoolSCM

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

Causalean.SCM.Assumptions.monotoneBoolSCM_satisfies · Causalean/SCM/ID/Assumptions/Monotonicity.lean:293 · uses BoolChainNode , instFintype , MonotoneMechanism , boolChainMeasurableSpace , boolChainPreorder , boolChainΩ , instDecidableEqBoolChainNode , monotoneBoolSCM

theorem antitoneBoolSCM_violates reviewed

Causalean.SCM.Assumptions

The reversing Boolean structural causal model violates monotonicity of the outcome mechanism in the designated parent coordinate.

Formal statement

conclusion

¬ MonotoneMechanism (Ω := boolChainΩ) (SWIGNode.random y) (SWIGNode.random d) antitoneBoolSCM

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

Causalean.SCM.Assumptions.antitoneBoolSCM_violates · Causalean/SCM/ID/Assumptions/Monotonicity.lean:305 · uses BoolChainNode , instFintype , MonotoneMechanism , antitoneBoolSCM , boolChainMeasurableSpace , boolChainPreorder , boolChainΩ , instDecidableEqBoolChainNode

10 supporting declarations (lemmas, instances)

instPreorderSwigΩ instance — For a finite collection of variables whose members can be compared for equality and that have measurable ordered value spaces and each random or fixed copy of a variable, an order on that copy's value space is provided by the order on the corresponding base-variable value space, with the random-copy case and the fixed-copy case treated identically.

parameters

N :

Type u_1
N → Type u_2
shared

∀ n, Preorder (Ω n)

s :

SWIGNode N

instance

instPreorderSwigΩ s :
Preorder (swigΩ Ω s)

given by

clause 1
| .random _ => inferInstance
clause 2
| .fixed _ => inferInstance

Causalean.SCM.Assumptions.instPreorderSwigΩ · Causalean/SCM/ID/Assumptions/Monotonicity.lean:29
instDecidableEqBoolChainNode instance

deriving DecidableEq, Repr

Causalean.SCM.Assumptions.instDecidableEqBoolChainNode · Causalean/SCM/ID/Assumptions/Monotonicity.lean:65
instReprBoolChainNode instance

deriving DecidableEq, Repr

Causalean.SCM.Assumptions.instReprBoolChainNode · Causalean/SCM/ID/Assumptions/Monotonicity.lean:65
instFintype instance — A finite enumeration of the Boolean-chain node type is provided by the two-element collection containing treatment and outcome together with the assertion that every Boolean-chain node belongs to that collection.

instance

instFintype :
Fintype BoolChainNode

given by

clause 1
elems := {d, y}
clause 2
complete := by intro x; cases x <;> decide

Causalean.SCM.Assumptions.BoolChainNode.instFintype · Causalean/SCM/ID/Assumptions/Monotonicity.lean:69
edgeDecidable instance — For every ordered pair of Boolean-chain nodes, a decision procedure for whether the pair is a directed edge is provided.

instance

edgeDecidable :
DecidableRel edge

given by

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)

Causalean.SCM.Assumptions.BoolChainNode.edgeDecidable · Causalean/SCM/ID/Assumptions/Monotonicity.lean:85
boolChainMeasurableSpace instance — For each Boolean-chain node, the measurable-space structure on its Boolean value space is the discrete measurable space, with the treatment case and the outcome case specified separately.

parameters

n :

instance

boolChainMeasurableSpace n :
MeasurableSpace (boolChainΩ n)

given by

clause 1
| d => ⊤
clause 2
| y => ⊤

Causalean.SCM.Assumptions.boolChainMeasurableSpace · Causalean/SCM/ID/Assumptions/Monotonicity.lean:150
boolChainPreorder instance — For each Boolean-chain node, the preorder on its Boolean value space is the usual Boolean preorder, with the treatment case and the outcome case specified separately.

parameters

n :

instance

boolChainPreorder n :
Preorder (boolChainΩ n)

given by

clause 1
| d => inferInstanceAs (Preorder Bool)
clause 2
| y => inferInstanceAs (Preorder Bool)

Causalean.SCM.Assumptions.boolChainPreorder · Causalean/SCM/ID/Assumptions/Monotonicity.lean:155
copyStructFun_measurable theorem — Each structural function of the copy mechanism on the Boolean chain example is measurable.

hypotheses

v :

{v // v ∈ boolChainSWIG.observed}

conclusion

Measurable (copyStructFun v)

Proof (Lean source)

@[fun_prop] theorem copyStructFun_measurable (v : {v // v ∈ boolChainSWIG.observed}) : Measurable (copyStructFun v) := by rcases v with ⟨n, hn⟩ cases n with | random n => cases n with | d => exact measurable_const | y => exact measurable_pi_apply boolChainDParent | fixed n => cases n <;> simp [boolChainSWIG] at hn

Causalean.SCM.Assumptions.copyStructFun_measurable · Causalean/SCM/ID/Assumptions/Monotonicity.lean:202
flipStructFun_measurable theorem — Each structural function of the flip mechanism on the Boolean chain example is measurable.

hypotheses

v :

{v // v ∈ boolChainSWIG.observed}

conclusion

Measurable (flipStructFun v)

Proof (Lean source)

@[fun_prop] theorem flipStructFun_measurable (v : {v // v ∈ boolChainSWIG.observed}) : Measurable (flipStructFun v) := by rcases v with ⟨n, hn⟩ cases n with | random n => cases n with | d => exact measurable_const | y => exact (measurable_of_finite (fun b : Bool => !b)).comp (measurable_pi_apply boolChainDParent) | fixed n => cases n <;> simp [boolChainSWIG] at hn

Causalean.SCM.Assumptions.flipStructFun_measurable · Causalean/SCM/ID/Assumptions/Monotonicity.lean:216
boolParentAssignment_boolChainDParent theorem — Evaluating the Boolean parent assignment at the designated parent returns the assigned value.

hypotheses

b :

Bool

conclusion

boolParentAssignment b boolChainDParent = b

Proof (Lean source)

@[simp] theorem boolParentAssignment_boolChainDParent (b : Bool) : boolParentAssignment b boolChainDParent = b := by cases b <;> rfl

Causalean.SCM.Assumptions.boolParentAssignment_boolChainDParent · Causalean/SCM/ID/Assumptions/Monotonicity.lean:287