SCM.Do.Rule2Kernel.Structural
Structural helpers for Rule 2 kernels: cross-SCM compatibility and pointwise structural identities behind the kernel-level argument.
StructCrossSCM 1 core · 1 supporting Cross-SCM pointwise bridge for the Rule 2 kernel proof. ★ evalMap_overrideC_fixSet_compat_on_fillZrW
Cross-SCM pointwise bridge for the Rule 2 kernel proof.
This module compares the original SCM with the SCM after intervening on Z.
The public unfold lemma evalMap_overrideC_observed_unfold rewrites the
evalMap_overrideC map in struct-function form, exposing the override
short-circuit and the recursive observed-parent calls. The main theorem
evalMap_overrideC_fixSet_compat_on_fillZrW then proves that, at the filled
assignment produced by fillZrW, the original and post-intervention overridden
evaluations agree on every observed coordinate.
theorem evalMap_overrideC_fixSet_compat_on_fillZrW reviewed
⚑ flagged
Causalean.SCM
Original and post-intervention override evaluations agree at fillZrW. For the intervention on names Z, whose random copies are observed in the base model and whose fixed copies are not yet part of the base model's fixed coordinates, with the union of the random copies of Z and a set W contained in the intervened model's observed variables, fix an intervened fixed assignment s, a conditioning value w on W, and a latent draw ℓ. Then at any observed node v of the intervened model, the base model's override-evaluation at the projected fixed assignment and the filled point built from s and w, applied to the reindexed latent draw, equals the intervened model's override-evaluation at s, the same filled point, and ℓ, evaluated at v.
Formal statement
hypotheses
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
hZrW_M2 :
Z.image SWIGNode.random ∪ W ⊆ (M'.fixSet Z hZ_obs hZ_fixed).observed
s :
(M'.fixSet Z hZ_obs hZ_fixed).FixedValues
ℓ :
(M'.fixSet Z hZ_obs hZ_fixed).LatentValues
v :
SWIGNode N
hv :
v ∈ (M'.fixSet Z hZ_obs hZ_fixed).observed
conclusion
M'.evalMap_overrideC (refl _) ((fixSet_observed M' Z hZ_obs hZ_fixed) ▸ hZrW_M2) (M'.fixSetProj Z hZ_obs hZ_fixed s) (M'.fillZrW Z hZ_obs hZ_fixed W s w) (valuesProjection (le_of_eq (fixSet_unobserved M' Z hZ_obs hZ_fixed).symm) ℓ) ⟨v, hv⟩
= (M'.fixSet Z hZ_obs hZ_fixed).evalMap_overrideC (refl _) hZrW_M2 s (M'.fillZrW Z hZ_obs hZ_fixed W s w) ℓ ⟨v, hv⟩
Proof (Lean source)
theorem evalMap_overrideC_fixSet_compat_on_fillZrW
(M' : SCM N Ω) (Z : Finset N)
(hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed)
(hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed)
(W : Finset (SWIGNode N))
(hZrW_M2 : Z.image SWIGNode.random ∪ W ⊆
(M'.fixSet Z hZ_obs hZ_fixed).observed)
(s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues)
(w : ValuesOn W (swigΩ Ω))
(ℓ : (M'.fixSet Z hZ_obs hZ_fixed).LatentValues)
{v : SWIGNode N}
(hv : v ∈ (M'.fixSet Z hZ_obs hZ_fixed).observed) :
M'.evalMap_overrideC (refl _)
((fixSet_observed M' Z hZ_obs hZ_fixed) ▸ hZrW_M2)
(M'.fixSetProj Z hZ_obs hZ_fixed s)
(M'.fillZrW Z hZ_obs hZ_fixed W s w)
(valuesProjection
(le_of_eq (fixSet_unobserved M' Z hZ_obs hZ_fixed).symm) ℓ)
⟨v, hv⟩
= (M'.fixSet Z hZ_obs hZ_fixed).evalMap_overrideC
(refl _) hZrW_M2 s
(M'.fillZrW Z hZ_obs hZ_fixed W s w) ℓ
⟨v, hv⟩ := by
classical
let M1 := M'
let M2 := M1.fixSet Z hZ_obs hZ_fixed
have h_obs_eq : M2.observed = M1.observed := rfl
let hZrW_M1 : Z.image SWIGNode.random ∪ W ⊆ M'.observed :=
(fixSet_observed M' Z hZ_obs hZ_fixed) ▸ hZrW_M2
have h_unobs : M2.unobserved = M1.unobserved := rfl
let s_M1 : M1.FixedValues := M1.fixSetProj Z hZ_obs hZ_fixed s
let ℓ_M1 : M1.LatentValues := valuesProjection (le_of_eq h_unobs.symm) ℓ
let Fw : ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω) :=
M'.fillZrW Z hZ_obs hZ_fixed W s w
-- Strong recursion on `M1.observedIndex ⟨v, hv⟩`.
suffices h_obs : ∀ (n : ℕ) (w' : SWIGNode N) (hw' : w' ∈ M2.observed),
(M1.observedIndex ⟨w', hw'⟩).val = n →
M1.evalMap_overrideC (refl _) hZrW_M1 s_M1 Fw ℓ_M1
⟨w', hw'⟩
= M2.evalMap_overrideC (refl _) hZrW_M2 s Fw ℓ
⟨w', hw'⟩ by
exact h_obs _ v hv rfl
intro n
induction n using Nat.strongRecOn with
| _ n ih =>
intro v hv hidx
have hv_M1 : v ∈ M1.observed := hv
-- Use the structFun-form unfold on both sides.
rw [evalMap_overrideC_observed_unfold M1 hZrW_M1 s_M1 Fw ℓ_M1 ⟨v, hv_M1⟩,
evalMap_overrideC_observed_unfold M2 hZrW_M2 s Fw ℓ ⟨v, hv⟩]
-- Case split on v ∈ C.
by_cases hvC : v ∈ Z.image SWIGNode.random ∪ W
· simp only [dif_pos hvC]
· simp only [dif_neg hvC]
-- Both sides are `structFun ⟨v, _⟩ (parentDispatchOverride ...)`.
-- M2.structFun ⟨v, _⟩ = M1.structFun ⟨v, _⟩ ∘ fixMonoParentMap.
-- Flip to M2 = M1 orientation to mirror fixSet_evalMap_levelset_compat_M2.
symm
change M1.structFun ⟨v, hv_M1⟩
(fixMonoParentMap M1.toSWIGGraph Z hZ_obs hZ_fixed v
(fun w' : {w' // w' ∈ (M1.splitMono Z hZ_obs hZ_fixed).dag.parents v} =>
parentDispatchOverride M2 hZrW_M2 s Fw ℓ ⟨v, hv⟩ w'))
= M1.structFun ⟨v, hv_M1⟩
(parentDispatchOverride M1 hZrW_M1 s_M1 Fw ℓ_M1 ⟨v, hv_M1⟩)
congr 1
funext wp
rcases wp with ⟨wpVal, hwpVal_M1⟩
cases wpVal with
| random u =>
by_cases hu_Z : u ∈ Z
· -- u ∈ Z: fixMonoParentMap routes M2-side to `.fixed u`.
rw [fixMonoParentMap_apply_random M1.toSWIGGraph Z hZ_obs hZ_fixed v u hu_Z _
hwpVal_M1]
-- M2-side: parentDispatchOverride at `⟨.fixed u, _⟩`.
have huo_M2 : (SWIGNode.fixed u : SWIGNode N) ∉ M2.unobserved := by
intro h
rcases M2.unobserved_is_random _ h with ⟨_, hEq⟩; cases hEq
have hfix_M2 : (SWIGNode.fixed u : SWIGNode N) ∈ M2.fixed :=
SCM.fixed_mem_fixSet M1 Z hZ_obs hZ_fixed hu_Z
unfold parentDispatchOverride
rw [dif_neg huo_M2, dif_pos hfix_M2]
-- M1-side: parentDispatchOverride at `⟨.random u, _⟩`.
have hobs_M1_u : (SWIGNode.random u : SWIGNode N) ∈ M1.observed :=
hZ_obs u hu_Z
have huo_M1 : (SWIGNode.random u : SWIGNode N) ∉ M1.unobserved :=
Finset.disjoint_left.mp M1.obs_unobs_disjoint hobs_M1_u
have hfix_M1 : (SWIGNode.random u : SWIGNode N) ∉ M1.fixed := by
intro h
rcases M1.fixed_is_fixed _ h with ⟨_, hEq⟩; cases hEq
rw [dif_neg huo_M1, dif_neg hfix_M1]
have hcW : (SWIGNode.random u : SWIGNode N) ∈ Z.image SWIGNode.random ∪ W :=
mem_union_left _ (Finset.mem_image.mpr ⟨u, hu_Z, rfl⟩)
rw [dif_pos hcW]
-- Goal: s ⟨.fixed u, hfix_M2⟩ = Fw ⟨.random u, hcW⟩.
exact (fillZrW_random_eq_fixed M' Z hZ_obs hZ_fixed W s w hu_Z hcW).symm
· -- u ∉ Z: fixMonoParentMap leaves alone.
rw [fixMonoParentMap_apply_random_notMem M1.toSWIGGraph Z hZ_obs hZ_fixed v _ u
hu_Z hwpVal_M1]
unfold parentDispatchOverride
by_cases huo : (SWIGNode.random u : SWIGNode N) ∈ M1.unobserved
· have huo_M2 : (SWIGNode.random u : SWIGNode N) ∈ M2.unobserved := huo
rw [dif_pos huo, dif_pos huo_M2]; rfl
· have huo_M2 : (SWIGNode.random u : SWIGNode N) ∉ M2.unobserved := huo
rw [dif_neg huo, dif_neg huo_M2]
by_cases hfix : (SWIGNode.random u : SWIGNode N) ∈ M1.fixed
· exfalso
rcases M1.fixed_is_fixed _ hfix with ⟨_, hEq⟩; cases hEq
· have hfix_M2 : (SWIGNode.random u : SWIGNode N) ∉ M2.fixed := by
intro h
rcases Finset.mem_union.mp
(show _ ∈ M1.fixed ∪ Z.image SWIGNode.fixed from h) with h1 | h2
· exact hfix h1
· rcases Finset.mem_image.mp h2 with ⟨_, _, hEq⟩; cases hEq
rw [dif_neg hfix, dif_neg hfix_M2]
-- Observed parent. Classify on C-membership.
by_cases hcW : (SWIGNode.random u : SWIGNode N) ∈ Z.image SWIGNode.random ∪ W
· simp only [dif_pos hcW]
· simp only [dif_neg hcW]
-- Recurse via IH at `.random u`.
have hobs_M1 : (SWIGNode.random u : SWIGNode N) ∈ M1.observed := by
have hedge_M1 : M1.dag.edge (SWIGNode.random u) v :=
M1.dag.mem_parents.mp hwpVal_M1
rcases Finset.mem_union.mp (M1.dag_edges_classified _ _ hedge_M1).1
with h1 | h2
· rcases Finset.mem_union.mp h1 with hfx | hob
· exact absurd hfx hfix
· exact hob
· exact absurd h2 huo
have hobs_M2 : (SWIGNode.random u : SWIGNode N) ∈ M2.observed := hobs_M1
have hidx_w : (M1.observedIndex ⟨SWIGNode.random u, hobs_M1⟩).val
< (M1.observedIndex ⟨v, hv_M1⟩).val := by
have hedge_M1 : M1.dag.edge (SWIGNode.random u) v :=
M1.dag.mem_parents.mp hwpVal_M1
have hv_eq : (M1.observedAt
⟨(M1.observedIndex ⟨v, hv_M1⟩).val,
(M1.observedIndex ⟨v, hv_M1⟩).isLt⟩).val = v := by
have := M1.observedAt_observedIndex ⟨v, hv_M1⟩
convert this
have hedge_M1' : M1.dag.edge (SWIGNode.random u)
(M1.observedAt
⟨(M1.observedIndex ⟨v, hv_M1⟩).val,
(M1.observedIndex ⟨v, hv_M1⟩).isLt⟩).val := by
rw [hv_eq]; exact hedge_M1
exact M1.observed_parent_index_lt
(M1.observedIndex ⟨v, hv_M1⟩).isLt hedge_M1' hobs_M1
rw [hidx] at hidx_w
exact (ih _ hidx_w (SWIGNode.random u) hobs_M2 rfl).symm
| fixed d =>
rw [fixMonoParentMap_apply_fixed M1.toSWIGGraph Z hZ_obs hZ_fixed v _ d hwpVal_M1]
unfold parentDispatchOverride
have huo : (SWIGNode.fixed d : SWIGNode N) ∉ M1.unobserved := by
intro h
rcases M1.unobserved_is_random _ h with ⟨_, hEq⟩; cases hEq
have huo_M2 : (SWIGNode.fixed d : SWIGNode N) ∉ M2.unobserved := huo
rw [dif_neg huo, dif_neg huo_M2]
by_cases hfix_M1 : (SWIGNode.fixed d : SWIGNode N) ∈ M1.fixed
· have hfix_M2 : (SWIGNode.fixed d : SWIGNode N) ∈ M2.fixed := by
change _ ∈ M1.fixed ∪ Z.image SWIGNode.fixed
exact mem_union_left _ hfix_M1
rw [dif_pos hfix_M1, dif_pos hfix_M2]
rfl
· by_cases hd_Z : d ∈ Z
· exfalso
have := M1.fixed_outside_fixed_isolated d hfix_M1
have hCh : v ∈ M1.dag.children (SWIGNode.fixed d) :=
M1.dag.mem_children.mpr (M1.dag.mem_parents.mp hwpVal_M1)
simpa [this.2] using hCh
· have hfix_M2 : (SWIGNode.fixed d : SWIGNode N) ∉ M2.fixed := by
intro h
rcases Finset.mem_union.mp
(show _ ∈ M1.fixed ∪ Z.image SWIGNode.fixed from h) with h1 | h2
· exact hfix_M1 h1
· rcases Finset.mem_image.mp h2 with ⟨d', hd'Z, hEq⟩
have : d = d' := SWIGNode.fixed.inj hEq.symm
exact hd_Z (this ▸ hd'Z)
rw [dif_neg hfix_M1, dif_neg hfix_M2]
-- `.fixed d` cannot be observed.
exfalso
have hobs : (SWIGNode.fixed d : SWIGNode N) ∈ M1.observed := by
have hedge_M1 : M1.dag.edge (SWIGNode.fixed d) v :=
M1.dag.mem_parents.mp hwpVal_M1
rcases Finset.mem_union.mp (M1.dag_edges_classified _ _ hedge_M1).1
with h1 | h2
· rcases Finset.mem_union.mp h1 with hfx | hob
· exact absurd hfx hfix_M1
· exact hob
· exact absurd h2 huo
rcases M1.observed_is_random _ hobs with ⟨_, hEq⟩; cases hEq
1 supporting declaration (lemmas, instances)
-
evalMap_overrideC_observed_unfoldlemma — Cast-free observed unfold for evalMap_overrideC (Y = M.observed case).hypothesesconclusionM.evalMap_overrideC (refl _) hC s c ℓ ⟨v.val, v.property⟩= if hvC : v.val ∈ C then c ⟨v.val, hvC⟩ else M.structFun v (parentDispatchOverride M hC s c ℓ v)Proof (Lean source)
lemma evalMap_overrideC_observed_unfold (M : SCM N Ω) {C : Finset (SWIGNode N)} (hC : C ⊆ M.observed) (s : FixedValues M) (c : ValuesOn C (swigΩ Ω)) (ℓ : LatentValues M) (v : {v // v ∈ M.observed}) : M.evalMap_overrideC (refl _) hC s c ℓ ⟨v.val, v.property⟩ = if hvC : v.val ∈ C then c ⟨v.val, hvC⟩ else M.structFun v (parentDispatchOverride M hC s c ℓ v) := by -- Use the suffices + subst trick (mirror of evalMap_observed_unfold). suffices h : ∀ (j : Fin M.observed.card) (w : {v // v ∈ M.observed}) (_ : M.observedAt j = w), M.evalMap_overrideC (refl _) hC s c ℓ ⟨w.val, w.property⟩ = if hwC : w.val ∈ C then c ⟨w.val, hwC⟩ else M.structFun w (parentDispatchOverride M hC s c ℓ w) by have key := h (M.observedIndex ⟨v.val, v.property⟩) v (Subtype.ext (M.observedAt_observedIndex ⟨v.val, v.property⟩)) exact key intro j w hw subst hw -- `w` eliminated; goal mentions `M.observedAt j` only. rw [evalMap_overrideC_eq M (refl _) hC s c ℓ ⟨(M.observedAt j).val, (M.observedAt j).property⟩] -- Apply the cast helper at k := M.observedIndex ⟨(observedAt j).val, _⟩, -- which equals j by `observedIndex_observedAt`. exact evalObservedAuxOverride_cast_eq_structFunAt M hC s c ℓ (M.observedIndex_observedAt j) (M.observedAt_observedIndex ⟨(M.observedAt j).val, (M.observedAt j).property⟩)
StructPointwise 1 core · 5 supporting Pointwise structural identities for the Rule 2 kernel proof. ★ fixSet_random_no_children
Pointwise structural identities for the Rule 2 kernel proof.
This module proves the graph and evaluation facts that make filled treatment
coordinates inert in the post-intervention model. The graph lemmas
fixSet_random_no_children and fixSet_random_not_isAncestor show that random
copies of intervened nodes cannot affect downstream evaluation after fixSet Z.
The main theorem evalMap_overrideC_dropZr_on_fillZrW uses those facts to show
that overriding on Z.image .random ∪ W at fillZrW s w has the same effect on
Y as overriding only on W at w; fillZrW_random_eq_fixed records the
coordinate identity used by the cross-model bridge.
lemma fixSet_random_no_children reviewed
⚑ flagged
Causalean.SCM
In the intervened model, consider a name D belonging to the intervention set Z, where random copies of names in Z are observed in the base model and their fixed copies are not yet part of the base model's fixed coordinates. Then the random copy of D has no outgoing edge, in the post-intervention DAG, to any node v.
Formal statement
Proof (Lean source)
lemma fixSet_random_no_children (M : SCM N Ω) (Z : Finset N)
(hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M.observed)
(hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M.fixed)
{D : N} (hD : D ∈ Z) (v : SWIGNode N) :
¬ (M.fixSet Z hZ_obs hZ_fixed).dag.edge (SWIGNode.random D) v := by
intro hEdge
-- (M.fixSet Z _ _).dag.edge = splitMonoEdgeRel M.toSWIGGraph.dag.edge Z.
have h_eqrel : (M.fixSet Z hZ_obs hZ_fixed).dag.edge (SWIGNode.random D) v ↔
SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge Z (SWIGNode.random D) v := by
simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG]
rw [h_eqrel] at hEdge
simp only [SWIGGraph.splitMonoEdgeRel, if_pos hD] at hEdge
5 supporting declarations (lemmas, instances)
-
fixSet_random_not_isAncestorlemma — In M.fixSet Z _ _, every .random D (D ∈ Z) is not a proper ancestor of any node. Direct consequence of fixSet_random_no_children via isAncestor_child.hypothesesM :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M.fixedD :NhD :D ∈ Zv :SWIGNode Nconclusion¬ (M.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.random D) vProof (Lean source)
lemma fixSet_random_not_isAncestor (M : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M.fixed) {D : N} (hD : D ∈ Z) (v : SWIGNode N) : ¬ (M.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.random D) v := by intro hAnc rcases (M.fixSet Z hZ_obs hZ_fixed).dag.isAncestor_child hAnc with hE | ⟨c, hE, _⟩ · exact fixSet_random_no_children M Z hZ_obs hZ_fixed hD v hE · exact fixSet_random_no_children M Z hZ_obs hZ_fixed hD c hE -
evalObservedAuxOverride_agree_anclemma — If two overrides use the same values on every observed ancestor of a target set, their recursive structural evaluations agree at every such ancestor and target.hypothesesM :SCM N ΩhC₁ :C₁ ⊆ M.observedhC₂ :C₂ ⊆ M.observeds :ℓ :hAgree :∀ (x : SWIGNode N)if(∃ t ∈ T, x = t ∨ M.dag.isAncestor x t)then((x ∈ C₁ ↔ x ∈ C₂) ∧ (∀ (h₁ : x ∈ C₁) (h₂ : x ∈ C₂), c₁ ⟨x, h₁⟩ = c₂ ⟨x, h₂⟩))conclusion∀ (n : ℕ) (hn : n < M.observed.card) (_ : ∃ t ∈ T, (M.observedAt ⟨n, hn⟩).val = t ∨ M.dag.isAncestor (M.observedAt ⟨n, hn⟩).val t),evalObservedAuxOverride M hC₁ s c₁ ℓ n hn = evalObservedAuxOverride M hC₂ s c₂ ℓ n hnProof (Lean source)
lemma evalObservedAuxOverride_agree_anc (M : SCM N Ω) (T : Finset (SWIGNode N)) {C₁ C₂ : Finset (SWIGNode N)} (hC₁ : C₁ ⊆ M.observed) (hC₂ : C₂ ⊆ M.observed) (s : FixedValues M) (ℓ : LatentValues M) (c₁ : ValuesOn C₁ (swigΩ Ω)) (c₂ : ValuesOn C₂ (swigΩ Ω)) (hAgree : ∀ (x : SWIGNode N), (∃ t ∈ T, x = t ∨ M.dag.isAncestor x t) → ((x ∈ C₁ ↔ x ∈ C₂) ∧ (∀ (h₁ : x ∈ C₁) (h₂ : x ∈ C₂), c₁ ⟨x, h₁⟩ = c₂ ⟨x, h₂⟩))) : ∀ (n : ℕ) (hn : n < M.observed.card) (_ : ∃ t ∈ T, (M.observedAt ⟨n, hn⟩).val = t ∨ M.dag.isAncestor (M.observedAt ⟨n, hn⟩).val t), evalObservedAuxOverride M hC₁ s c₁ ℓ n hn = evalObservedAuxOverride M hC₂ s c₂ ℓ n hn := by intro n induction n using Nat.strongRecOn with | _ n ih => intro hn hAnc rw [evalObservedAuxOverride_eq M hC₁ s c₁ ℓ n hn, evalObservedAuxOverride_eq M hC₂ s c₂ ℓ n hn] -- Agreement at the node itself. have hSelfAgree := hAgree (M.observedAt ⟨n, hn⟩).val hAnc by_cases h1 : (M.observedAt ⟨n, hn⟩).val ∈ C₁ · have h2 : (M.observedAt ⟨n, hn⟩).val ∈ C₂ := hSelfAgree.1.mp h1 rw [dif_pos h1, dif_pos h2] exact hSelfAgree.2 h1 h2 · have h2 : (M.observedAt ⟨n, hn⟩).val ∉ C₂ := fun h => h1 (hSelfAgree.1.mpr h) rw [dif_neg h1, dif_neg h2] congr 1 funext w -- Parent recursion: classify w identically on both sides. have hedge : M.dag.edge w.val (M.observedAt ⟨n, hn⟩).val := M.dag.mem_parents.mp w.property have hw_anc_obs : M.dag.isAncestor w.val (M.observedAt ⟨n, hn⟩).val := DAG.isAncestor.edge hedge -- Chain the ancestor witness from `observedAt n` through `w`. have hAncW : ∃ t ∈ T, w.val = t ∨ M.dag.isAncestor w.val t := by rcases hAnc with ⟨t, ht, hOrAnc⟩ refine ⟨t, ht, ?_⟩ rcases hOrAnc with hEq | hAncToT · exact inr (hEq ▸ hw_anc_obs) · exact inr (M.dag.isAncestor_trans hw_anc_obs hAncToT) have hWAgree := hAgree w.val hAncW by_cases huo : w.val ∈ M.unobserved · rw [parentMapOverride_unobserved M hC₁ s c₁ ℓ hn _ w huo, parentMapOverride_unobserved M hC₂ s c₂ ℓ hn _ w huo] · by_cases hfix : w.val ∈ M.fixed · rw [parentMapOverride_fixed M hC₁ s c₁ ℓ hn _ w hfix, parentMapOverride_fixed M hC₂ s c₂ ℓ hn _ w hfix] · -- Observed (non-fixed, non-latent) parent: either in C or recurse. have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1' | h2' · rcases Finset.mem_union.mp h1' with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2' huo by_cases hcW1 : w.val ∈ C₁ · have hcW2 : w.val ∈ C₂ := hWAgree.1.mp hcW1 rw [parentMapOverride_C M hC₁ s c₁ ℓ hn _ w hcW1, parentMapOverride_C M hC₂ s c₂ ℓ hn _ w hcW2] exact hWAgree.2 hcW1 hcW2 · have hcW2 : w.val ∉ C₂ := fun h => hcW1 (hWAgree.1.mpr h) rw [parentMapOverride_observed M hC₁ s c₁ ℓ hn _ w hobs hcW1, parentMapOverride_observed M hC₂ s c₂ ℓ hn _ w hobs hcW2] -- Recursion at w's smaller topological index. have hj : (M.observedIndex ⟨w.val, hobs⟩).val < n := M.observed_parent_index_lt hn hedge hobs congr 1 apply ih _ hj rcases hAncW with ⟨t, ht, hwt⟩ refine ⟨t, ht, ?_⟩ have h_at : (M.observedAt ⟨(M.observedIndex ⟨w.val, hobs⟩).val, (M.observedIndex ⟨w.val, hobs⟩).isLt⟩).val = w.val := M.observedAt_observedIndex ⟨w.val, hobs⟩ rw [h_at] exact hwt -
evalMap_overrideC_agree_anclemma — Two assignments that override observed variables give the same evaluated values at every target variable when they agree on which relevant ancestors are overridden and on the values assigned there.hypothesesM :SCM N ΩhY :Y ⊆ M.observedhC₁ :C₁ ⊆ M.observedhC₂ :C₂ ⊆ M.observeds :ℓ :hAgree :∀ (x : SWIGNode N)if(∃ y ∈ Y, x = y ∨ M.dag.isAncestor x y)then((x ∈ C₁ ↔ x ∈ C₂) ∧ (∀ (h₁ : x ∈ C₁) (h₂ : x ∈ C₂), c₁ ⟨x, h₁⟩ = c₂ ⟨x, h₂⟩))conclusionM.evalMap_overrideC hY hC₁ s c₁ ℓ = M.evalMap_overrideC hY hC₂ s c₂ ℓProof (Lean source)
lemma evalMap_overrideC_agree_anc (M : SCM N Ω) {Y C₁ C₂ : Finset (SWIGNode N)} (hY : Y ⊆ M.observed) (hC₁ : C₁ ⊆ M.observed) (hC₂ : C₂ ⊆ M.observed) (s : FixedValues M) (ℓ : LatentValues M) (c₁ : ValuesOn C₁ (swigΩ Ω)) (c₂ : ValuesOn C₂ (swigΩ Ω)) (hAgree : ∀ (x : SWIGNode N), (∃ y ∈ Y, x = y ∨ M.dag.isAncestor x y) → ((x ∈ C₁ ↔ x ∈ C₂) ∧ (∀ (h₁ : x ∈ C₁) (h₂ : x ∈ C₂), c₁ ⟨x, h₁⟩ = c₂ ⟨x, h₂⟩))) : M.evalMap_overrideC hY hC₁ s c₁ ℓ = M.evalMap_overrideC hY hC₂ s c₂ ℓ := by funext v rw [evalMap_overrideC_eq M hY hC₁ s c₁ ℓ v, evalMap_overrideC_eq M hY hC₂ s c₂ ℓ v] congr 1 apply evalObservedAuxOverride_agree_anc M Y hC₁ hC₂ s ℓ c₁ c₂ hAgree refine ⟨v.val, v.property, inl ?_⟩ exact M.observedAt_observedIndex ⟨v.val, hY v.property⟩ -
evalMap_overrideC_dropZr_on_fillZrWtheorem — Filled intervention coordinates do not affect the post-intervention override on Y.hypothesesM' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixedhY_M2 :Y ⊆ (M'.fixSet Z hZ_obs hZ_fixed).observedhZrW :Z.image SWIGNode.random ∪ W ⊆ (M'.fixSet Z hZ_obs hZ_fixed).observedhDisj_YZr :Disjoint Y (Z.image SWIGNode.random)s :(M'.fixSet Z hZ_obs hZ_fixed).FixedValuesℓ :(M'.fixSet Z hZ_obs hZ_fixed).LatentValuesconclusion(M'.fixSet Z hZ_obs hZ_fixed).evalMap_overrideC hY_M2 hZrW s (M'.fillZrW Z hZ_obs hZ_fixed W s w) ℓ= (M'.fixSet Z hZ_obs hZ_fixed).evalMap_overrideC hY_M2 (Finset.subset_union_right.trans hZrW) s w ℓProof (Lean source)
theorem evalMap_overrideC_dropZr_on_fillZrW (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (Y W : Finset (SWIGNode N)) (hY_M2 : Y ⊆ (M'.fixSet Z hZ_obs hZ_fixed).observed) (hZrW : Z.image SWIGNode.random ∪ W ⊆ (M'.fixSet Z hZ_obs hZ_fixed).observed) (hDisj_YZr : Disjoint Y (Z.image SWIGNode.random)) (s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) (ℓ : (M'.fixSet Z hZ_obs hZ_fixed).LatentValues) (w : ValuesOn W (swigΩ Ω)) : (M'.fixSet Z hZ_obs hZ_fixed).evalMap_overrideC hY_M2 hZrW s (M'.fillZrW Z hZ_obs hZ_fixed W s w) ℓ = (M'.fixSet Z hZ_obs hZ_fixed).evalMap_overrideC hY_M2 (Finset.subset_union_right.trans hZrW) s w ℓ := by let hW_M2 : W ⊆ (M'.fixSet Z hZ_obs hZ_fixed).observed := Finset.subset_union_right.trans hZrW classical let M2 := M'.fixSet Z hZ_obs hZ_fixed -- Apply the override-agreement helper with C₁ := Zr ∪ W, C₂ := W. apply evalMap_overrideC_agree_anc M2 hY_M2 hZrW hW_M2 s ℓ _ _ intro x hAnc -- For x in (ancestors-or-eq of some y ∈ Y) in M2: -- We must show x ∈ Zr ∪ W ↔ x ∈ W, and the values agree on the -- intersection W. -- The key fact: x cannot be a `.random D` (D ∈ Z), since: -- (1) if `x = y` with `y ∈ Y`, then x ∉ Zr by hDisj_YZr; -- (2) if `x` is a proper M2-ancestor of `y ∈ Y`, then x ≠ .random D -- for any D ∈ Z (by fixSet_random_not_isAncestor). have hxNotZr : x ∉ Z.image SWIGNode.random := by intro hxZr rcases Finset.mem_image.mp hxZr with ⟨D, hD, rfl⟩ rcases hAnc with ⟨y, hy, hOrAnc⟩ rcases hOrAnc with hEq | hAncToY · -- x = .random D = y ∈ Y, contradicting Y disjoint Zr. have : SWIGNode.random D ∈ Y := hEq ▸ hy exact Finset.disjoint_left.mp hDisj_YZr this (Finset.mem_image.mpr ⟨D, hD, rfl⟩) · -- .random D is a proper M2-ancestor of y, contradicting -- fixSet_random_not_isAncestor. exact fixSet_random_not_isAncestor M' Z hZ_obs hZ_fixed hD y hAncToY refine ⟨?_, ?_⟩ · -- x ∈ Zr ∪ W ↔ x ∈ W (given x ∉ Zr). constructor · intro hxZrW rcases Finset.mem_union.mp hxZrW with hxZr | hxW · exact absurd hxZr hxNotZr · exact hxW · intro hxW exact mem_union_right _ hxW · -- Values agree on W: fillZrW W s w at x = w at x. intro h₁ h₂ -- h₁ : x ∈ Zr ∪ W, h₂ : x ∈ W. show M'.fillZrW Z hZ_obs hZ_fixed W s w ⟨x, h₁⟩ = w ⟨x, h₂⟩ unfold fillZrW rw [valuesUnionMk_apply_right _ _ h₁ hxNotZr] -
fillZrW_random_eq_fixedlemma — The filled assignment pins intervention values on the random copies of Z.hypothesesM' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixeds :(M'.fixSet Z hZ_obs hZ_fixed).FixedValuesD :NhD :D ∈ ZhRD :SWIGNode.random D ∈ Z.image SWIGNode.random ∪ WconclusionM'.fillZrW Z hZ_obs hZ_fixed W s w ⟨SWIGNode.random D, hRD⟩= s ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M' Z hZ_obs hZ_fixed hD⟩Proof (Lean source)
lemma fillZrW_random_eq_fixed (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (W : Finset (SWIGNode N)) (s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) (w : ValuesOn W (swigΩ Ω)) {D : N} (hD : D ∈ Z) (hRD : SWIGNode.random D ∈ Z.image SWIGNode.random ∪ W) : M'.fillZrW Z hZ_obs hZ_fixed W s w ⟨SWIGNode.random D, hRD⟩ = s ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M' Z hZ_obs hZ_fixed hD⟩ := by unfold fillZrW rw [valuesUnionMk_apply_left _ _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)] rfl