SCM.Do.Rule2­Kernel.Witness­Bridge

theorem cutset_condIndep_condDistrib (M : SCM N Ω) [StandardBorelSpace M.RandomValues] [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] [∀ s : M.FixedValues, IsFiniteMeasure (M.jointKernel s)] (Y W : Finset (SWIGNode N)) (Z : Finset N) [StandardBorelSpace (ValuesOn (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] [Nonempty (ValuesOn (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] (hZr : Z.image SWIGNode.random ⊆ M.observed) (hW : W ⊆ M.observed) (hdSepCW : M.dag.dSep (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (Z.image SWIGNode.random) (W ∪ M.fixed)) (s : M.FixedValues) : (fun p : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω) => condDistrib (valuesProjection (M.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) (fun ℓ : M.LatentValues => (valuesProjection hZr (M.randomToObserved (M.evalMap s ℓ)), valuesProjection hW (M.randomToObserved (M.evalMap s ℓ)))) M.latentProduct p) =ᵐ[M.latentProduct.map (fun ℓ : M.LatentValues => (valuesProjection hZr (M.randomToObserved (M.evalMap s ℓ)), valuesProjection hW (M.randomToObserved (M.evalMap s ℓ))))] (fun p => condDistrib (valuesProjection (M.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) (fun ℓ : M.LatentValues => valuesProjection hW (M.randomToObserved (M.evalMap s ℓ))) M.latentProduct p.2) := by classical set Zr := Z.image SWIGNode.random with hZr_def set CW := M.cutsetLatent Y (Zr ∪ W) with hCW_def have hCWsub : CW ⊆ M.unobserved := M.cutsetLatent_subset Y (Zr ∪ W) -- Subset facts into `randomVars`. have hobs_rv : M.observed ⊆ M.randomVars := by intro v hv; exact Finset.mem_union_left _ hv have hunobs_rv : M.unobserved ⊆ M.randomVars := by intro v hv; exact Finset.mem_union_right _ hv have hZr_rv : Zr ⊆ M.randomVars := hZr.trans hobs_rv have hW_rv : W ⊆ M.randomVars := hW.trans hobs_rv have hCW_rv : CW ⊆ M.randomVars := hCWsub.trans hunobs_rv -- Bridge: for an observed set `D`, projecting `randomToObserved (evalMap s ℓ)` -- equals projecting `evalMap s ℓ` directly (same underlying values). have hbridge_obs : ∀ {D : Finset (SWIGNode N)} (hD : D ⊆ M.observed) (hD_rv : D ⊆ M.randomVars) (ℓ : M.LatentValues), valuesProjection hD (M.randomToObserved (M.evalMap s ℓ)) = valuesProjection hD_rv (M.evalMap s ℓ) := by intro D hD hD_rv ℓ; funext v; rfl -- Bridge: for the latent cutset, projecting `evalMap s ℓ` equals projecting `ℓ`. have hbridge_lat : ∀ ℓ : M.LatentValues, valuesProjection hCW_rv (M.evalMap s ℓ) = valuesProjection hCWsub ℓ := by intro ℓ; funext v change M.evalMap s ℓ ⟨v.val, hCW_rv v.property⟩ = ℓ ⟨v.val, hCWsub v.property⟩ rw [M.evalMap_unobserved s ℓ _ (hCWsub v.property)] -- Measurability of the pulled-back coordinate maps (as compositions with evalMap s). have hev : Measurable (fun ℓ : M.LatentValues => M.evalMap s ℓ) := by fun_prop -- Abbreviations for the pulled-back coordinate maps. set Xmap : M.LatentValues → ValuesOn Zr (swigΩ Ω) := fun ℓ => valuesProjection hZr (M.randomToObserved (M.evalMap s ℓ)) with hX_def set Zmap : M.LatentValues → ValuesOn W (swigΩ Ω) := fun ℓ => valuesProjection hW (M.randomToObserved (M.evalMap s ℓ)) with hZmap_def set Cmap : M.LatentValues → ValuesOn CW (swigΩ Ω) := valuesProjection hCWsub with hC_def have hXmeas : Measurable Xmap := by fun_prop have hZmeas : Measurable Zmap := by fun_prop have hCmeas : Measurable Cmap := by fun_prop -- Step 1: cutset graph d-sep is now a direct hypothesis; global Markov -- (FullCondIndep under jointKernel) follows. (Previously derived internally -- via `cutsetLatent_dSep_of_dSep` from `dSep Y Zr`, which is FALSE at M1; the -- cutset d-sep `dSep C_W Zr` is the satisfiable input and is threaded directly.) have hdSepCW : M.dag.dSep CW Zr (W ∪ M.fixed) := hdSepCW have hDisj_CWZr : Disjoint CW Zr := by rw [Finset.disjoint_left]; intro a haCW haZr exact not_obs_of_unobs M.toSWIGGraph (hCWsub haCW) (hZr haZr) have hDisj_CWW : Disjoint CW W := by rw [Finset.disjoint_left]; intro a haCW haW exact not_obs_of_unobs M.toSWIGGraph (hCWsub haCW) (hW haW) have hFCI : FullCondIndep M CW Zr W hCW_rv hZr_rv hW_rv (M.jointKernel s) := full_globalMarkov_with_fixed M CW Zr W M.fixed hCW_rv hZr_rv hW_rv (refl _) hdSepCW s -- `Zr ⟂ CW | W` form (swap X↔Y), which the Mathlib iff consumes as `g ⟂ᵢ[k] f`. have hFCI_symm : FullCondIndep M Zr CW W hZr_rv hCW_rv hW_rv (M.jointKernel s) := fullCondIndep_symm M hCW_rv hZr_rv hW_rv hFCI haveI : IsProbabilityMeasure M.latentProduct := inferInstance -- Measurability of the `valuesProjection` maps on `RandomValues`. have hCW_proj_meas : Measurable (valuesProjection (Ω := swigΩ Ω) hCW_rv) := by fun_prop have hZr_proj_meas : Measurable (valuesProjection (Ω := swigΩ Ω) hZr_rv) := by fun_prop have hW_proj_meas : Measurable (valuesProjection (Ω := swigΩ Ω) hW_rv) := by fun_prop -- Step 2: Mathlib iff turns `FullCondIndep` into a condDistrib-pair equality -- under `jointKernel s`, conditioning on the pair `(W, Zr)`. have hCI_joint : (fun p => condDistrib (valuesProjection hCW_rv) (fun ξ => (valuesProjection hW_rv ξ, valuesProjection hZr_rv ξ)) (M.jointKernel s) p) =ᵐ[(M.jointKernel s).map (fun ξ => (valuesProjection hW_rv ξ, valuesProjection hZr_rv ξ))] (fun p => ((condDistrib (valuesProjection hCW_rv) (valuesProjection hW_rv) (M.jointKernel s)).prodMkRight _) p) := by have := (ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (μ := M.jointKernel s) (f := valuesProjection hCW_rv) (g := valuesProjection hZr_rv) (k := valuesProjection hW_rv) hCW_proj_meas hZr_proj_meas hW_proj_meas).mp hFCI_symm exact this -- The two coordinate maps on `RandomValues`, and their compositions with `evalMap s`. set Wmap_rv : M.RandomValues → ValuesOn W (swigΩ Ω) := valuesProjection hW_rv with hWmap_rv set Zrmap_rv : M.RandomValues → ValuesOn Zr (swigΩ Ω) := valuesProjection hZr_rv with hZrmap_rv set CWmap_rv : M.RandomValues → ValuesOn CW (swigΩ Ω) := valuesProjection hCW_rv with hCWmap_rv set pairWZr : M.RandomValues → ValuesOn W (swigΩ Ω) × ValuesOn Zr (swigΩ Ω) := fun ξ => (Wmap_rv ξ, Zrmap_rv ξ) with hpairWZr have hpairWZr_meas : Measurable pairWZr := by fun_prop -- Rewrite `jointKernel s` as the pushforward of `latentProduct`. have hjk : M.jointKernel s = M.latentProduct.map (fun ℓ => M.evalMap s ℓ) := jointKernel_apply_eq M s simp only [hjk] at hCI_joint -- Compositions with `evalMap s` reduce to `Zmap`, `Xmap`, `Cmap`. have hcomp_pair : pairWZr ∘ (fun ℓ => M.evalMap s ℓ) = fun ℓ => (Zmap ℓ, Xmap ℓ) := by funext ℓ simp only [hpairWZr, hWmap_rv, hZrmap_rv, Function.comp_apply, hZmap_def, hX_def] rw [hbridge_obs hW hW_rv ℓ, hbridge_obs hZr hZr_rv ℓ] have hcomp_W : Wmap_rv ∘ (fun ℓ => M.evalMap s ℓ) = Zmap := by funext ℓ; simp only [hWmap_rv, Function.comp_apply, hZmap_def] rw [hbridge_obs hW hW_rv ℓ] have hcomp_CW : CWmap_rv ∘ (fun ℓ => M.evalMap s ℓ) = Cmap := by funext ℓ change CWmap_rv (M.evalMap s ℓ) = Cmap ℓ rw [hbridge_lat ℓ] -- Transfer the pair-conditioned `condDistrib` onto `latentProduct`. have htr_pair := ProbabilityTheory.condDistrib_map (ν := M.latentProduct) (f := fun ℓ => M.evalMap s ℓ) hpairWZr_meas.aemeasurable hCW_proj_meas.aemeasurable hev.aemeasurable rw [← MeasureTheory.Measure.map_map hpairWZr_meas hev] at htr_pair have htr_W := ProbabilityTheory.condDistrib_map (ν := M.latentProduct) (f := fun ℓ => M.evalMap s ℓ) hW_proj_meas.aemeasurable hCW_proj_meas.aemeasurable hev.aemeasurable rw [← MeasureTheory.Measure.map_map hW_proj_meas hev] at htr_W -- The `(W, Zr)`-ordered latent pair map and its marginal measure facts. set pairWZr_lat : M.LatentValues → ValuesOn W (swigΩ Ω) × ValuesOn Zr (swigΩ Ω) := fun ℓ => (Zmap ℓ, Xmap ℓ) with hpairWZr_lat have hpairWZr_lat_meas : Measurable pairWZr_lat := by fun_prop -- Push `htr_pair`/`htr_W`/`hCI_joint` filters into `LP.map (·∘E)` form. rw [MeasureTheory.Measure.map_map hpairWZr_meas hev, hcomp_pair, hcomp_CW] at htr_pair rw [MeasureTheory.Measure.map_map hpairWZr_meas hev, hcomp_pair] at hCI_joint rw [MeasureTheory.Measure.map_map hW_proj_meas hev, hcomp_W, hcomp_CW] at htr_W -- `htr_pair` now: condDistrib CWmap_rv pairWZr (LP.map E) =ᵐ[LP.map pairWZr_lat] -- condDistrib Cmap pairWZr_lat LP -- `hCI_joint` now RHS uses prodMkRight of condDistrib CWmap_rv Wmap_rv (LP.map E). -- Reduce prodMkRight to evaluation at `.1`. have hCI_joint' : (fun p => condDistrib CWmap_rv pairWZr (M.latentProduct.map (fun ℓ => M.evalMap s ℓ)) p) =ᵐ[M.latentProduct.map pairWZr_lat] (fun p => condDistrib CWmap_rv Wmap_rv (M.latentProduct.map (fun ℓ => M.evalMap s ℓ)) p.1) := by filter_upwards [hCI_joint] with p hp rw [hp, ProbabilityTheory.Kernel.prodMkRight_apply] -- Lift `htr_W` from the `W`-marginal to the pair-marginal along `fst`. have htr_W_fst : (fun p => condDistrib CWmap_rv Wmap_rv (M.latentProduct.map (fun ℓ => M.evalMap s ℓ)) p.1) =ᵐ[M.latentProduct.map pairWZr_lat] (fun p : ValuesOn W (swigΩ Ω) × ValuesOn Zr (swigΩ Ω) => condDistrib Cmap Zmap M.latentProduct p.1) := by have hfst_marg : (M.latentProduct.map pairWZr_lat).map fst = M.latentProduct.map Zmap := by rw [MeasureTheory.Measure.map_map measurable_fst hpairWZr_lat_meas]; rfl have := MeasureTheory.ae_eq_comp (μ := M.latentProduct.map pairWZr_lat) (f := fst) (g := fun q => condDistrib CWmap_rv Wmap_rv (M.latentProduct.map (fun ℓ => M.evalMap s ℓ)) q) (g' := fun q => condDistrib Cmap Zmap M.latentProduct q) measurable_fst.aemeasurable (by rw [hfst_marg]; exact htr_W) exact this -- Assemble the `(W, Zr)`-ordered equality on `LP.map pairWZr_lat`. have keyWZr : (fun p => condDistrib Cmap pairWZr_lat M.latentProduct p) =ᵐ[M.latentProduct.map pairWZr_lat] (fun p : ValuesOn W (swigΩ Ω) × ValuesOn Zr (swigΩ Ω) => condDistrib Cmap Zmap M.latentProduct p.1) := (htr_pair.symm.trans hCI_joint').trans htr_W_fst -- Swap `(W, Zr)` to `(Zr, W)` via the product-comm measurable equivalence. set e : (ValuesOn W (swigΩ Ω) × ValuesOn Zr (swigΩ Ω)) ≃ᵐ (ValuesOn Zr (swigΩ Ω) × ValuesOn W (swigΩ Ω)) := MeasurableEquiv.prodComm with he_def have hpair_swap : (fun ℓ => (Xmap ℓ, Zmap ℓ)) = e ∘ pairWZr_lat := by funext ℓ; rfl -- `condDistrib Cmap (e ∘ pairWZr_lat) LP (e p) = condDistrib Cmap pairWZr_lat LP p`, a.e. have hreparam := condDistrib_comp_right_measurableEquiv (μ := M.latentProduct) (Y := Cmap) (X := pairWZr_lat) e hCmeas hpairWZr_lat_meas -- Transport the goal (over `LP.map (Xmap, Zmap) = (LP.map pairWZr_lat).map e`) to `keyWZr`. have hmap_e : M.latentProduct.map (fun ℓ => (Xmap ℓ, Zmap ℓ)) = (M.latentProduct.map pairWZr_lat).map e := by rw [hpair_swap, ← MeasureTheory.Measure.map_map e.measurable hpairWZr_lat_meas] -- Final: rewrite the goal's conditioning into `Xmap`/`Zmap`, then chain. change (fun p => condDistrib Cmap (fun ℓ => (Xmap ℓ, Zmap ℓ)) M.latentProduct p) =ᵐ[M.latentProduct.map (fun ℓ => (Xmap ℓ, Zmap ℓ))] (fun p => condDistrib Cmap Zmap M.latentProduct p.2) rw [hmap_e] -- On `(LP.map pairWZr_lat).map e`, pull back along the measurable embedding `e`. rw [EventuallyEq, e.measurableEmbedding.ae_map_iff] filter_upwards [keyWZr, hreparam] with p hkey hrep -- LHS at `e p`: condDistrib Cmap (Xmap,Zmap) LP (e p) = condDistrib Cmap pairWZr_lat LP p. have hLHS : condDistrib Cmap (fun ℓ => (Xmap ℓ, Zmap ℓ)) M.latentProduct (e p) = condDistrib Cmap pairWZr_lat M.latentProduct p := by rw [hpair_swap]; exact hrep change condDistrib Cmap (fun ℓ => (Xmap ℓ, Zmap ℓ)) M.latentProduct (e p) = condDistrib Cmap Zmap M.latentProduct (e p).2 rw [hLHS, hkey] -- RHS: `condDistrib Cmap Zmap LP p.1 = condDistrib Cmap Zmap LP (e p).2`. rfl

theorem doSide_M2_condDistrib_eq_M1_witness (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 : Y ⊆ M'.observed) (hW : W ⊆ M'.observed) (hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed) (hDisj_YZr : Disjoint Y (Z.image SWIGNode.random)) (hWNonDesc : ∀ z ∈ Z, ∀ v ∈ W, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v) [StandardBorelSpace M'.RandomValues] [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [StandardBorelSpace (ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] [Nonempty (ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] [StandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).RandomValues] [StandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).ObservedValues] [StandardBorelSpace (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))] [Nonempty (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn W (swigΩ Ω))] [MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] (s0 : M'.FixedValues) (t : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω)) (h : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) → ValuesOn W (swigΩ Ω) → ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω) → ValuesOn Y (swigΩ Ω)) (hh : Measurable (fun p : (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω)) × ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω) => h p.1.1 p.1.2 p.2)) (hoverride : ∀ (zr : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω)) (w' : ValuesOn W (swigΩ Ω)) (ℓ : M'.LatentValues), h zr w' (valuesProjection (M'.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W)) ℓ) = M'.evalMap_overrideC hY hZrW s0 (valuesUnionMk zr w') ℓ) : (fun w => condDistrib (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY)) (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW)) ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel (M'.fixSetExtend Z hZ_obs hZ_fixed s0 t)) w) =ᵐ[(M'.obsKernel s0).map (valuesProjection hW)] (fun w => ((condDistrib (valuesProjection (M'.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) (fun ℓ : M'.LatentValues => valuesProjection hW (M'.randomToObserved (M'.evalMap s0 ℓ))) M'.latentProduct) w).map (h t w)) := by classical set M2 := M'.fixSet Z hZ_obs hZ_fixed with hM2 set s' := M'.fixSetExtend Z hZ_obs hZ_fixed s0 t with hs' set hY_M2 : Y ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY with hhY_M2 set hW_M2 : W ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW with hhW_M2 set μW := (M'.obsKernel s0).map (valuesProjection hW) with hμW -- Abbreviation: the M2 observed-eval pullback `E2`. set E2 : M2.LatentValues → M2.ObservedValues := fun ℓ => M2.randomToObserved (M2.evalMap s' ℓ) with hE2_def have hE2meas : Measurable E2 := by have hev : Measurable (fun ℓ : M2.LatentValues => M2.evalMap s' ℓ) := by fun_prop exact M2.measurable_randomToObserved.comp hev have hπY : Measurable (valuesProjection (Ω := swigΩ Ω) hY_M2) := by fun_prop have hπW : Measurable (valuesProjection (Ω := swigΩ Ω) hW_M2) := by fun_prop -- Base alignment: the M2 `W`-marginal at the slice `s'` equals `μW` (Rule 3*). have hbase : (M2.obsKernel s').map (valuesProjection hW_M2) = μW := by have hRule3 := obsKernel_fixSet_W_marginal_eq_M1_marginal M' Z hZ_obs hZ_fixed W hW hWNonDesc s' rw [hμW] rw [show (M2.obsKernel s').map (valuesProjection hW_M2) = (M2.obsKernel s').map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW)) from rfl, hRule3, M'.fixSetProj_fixSetExtend Z hZ_obs hZ_fixed s0 t] -- Step A: transport the M2 LHS `condDistrib π_Y π_W (M2.obsKernel s')` onto -- `M2.latentProduct` via `obsKernel_eq_latentProduct_map` + `condDistrib_map`. have hobs : M2.obsKernel s' = M2.latentProduct.map E2 := M2.obsKernel_eq_latentProduct_map s' have hstepA := ProbabilityTheory.condDistrib_map (ν := M2.latentProduct) (f := E2) hπW.aemeasurable hπY.aemeasurable hE2meas.aemeasurable rw [← MeasureTheory.Measure.map_map hπW hE2meas] at hstepA -- `hstepA : condDistrib π_Y π_W (latentProduct.map E2) -- =ᵐ[(latentProduct.map E2).map π_W] condDistrib (π_Y∘E2) (π_W∘E2) latentProduct`. -- Align the base of `hstepA` to `μW`. have hbase' : (M2.latentProduct.map E2).map (valuesProjection hW_M2) = μW := by rw [← hobs]; exact hbase rw [hbase'] at hstepA -- Step B+C (isolated TRUE core): the M2-pullback condDistrib equals the M1 witness kernel. have hcore := doSide_M2_pullback_eq_M1_witness M' Z hZ_obs hZ_fixed Y W hY hZrW hDisj_YZr hWNonDesc s0 t h hh hoverride -- Align the goal's LHS (over `M2.obsKernel s'`) to `hstepA`'s LHS (over `latentProduct.map E2`) -- via `hobs`, handling the dependent `IsFiniteMeasure` instance with `subst`. refine Filter.EventuallyEq.trans ?_ (hstepA.trans hcore) have hcongr : (condDistrib (valuesProjection hY_M2) (valuesProjection hW_M2) (M2.obsKernel s')) = condDistrib (valuesProjection hY_M2) (valuesProjection hW_M2) (M2.latentProduct.map E2) := by congr 1 rw [hcongr]

theorem doSide_eq_witness (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 : Y ⊆ M'.observed) (hW : W ⊆ M'.observed) (hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed) (hDisj_YZr : Disjoint Y (Z.image SWIGNode.random)) (hWNonDesc : ∀ z ∈ Z, ∀ v ∈ W, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v) [StandardBorelSpace M'.RandomValues] [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [StandardBorelSpace (ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] [Nonempty (ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] [StandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).RandomValues] [StandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).ObservedValues] [StandardBorelSpace (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))] [Nonempty (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))] [CountableOrCountablyGenerated M'.FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn W (swigΩ Ω))] [MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] (s0 : M'.FixedValues) (t : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω)) (h : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) → ValuesOn W (swigΩ Ω) → ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω) → ValuesOn Y (swigΩ Ω)) (hh : Measurable (fun p : (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω)) × ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω) => h p.1.1 p.1.2 p.2)) (hoverride : ∀ (zr : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω)) (w' : ValuesOn W (swigΩ Ω)) (ℓ : M'.LatentValues), h zr w' (valuesProjection (M'.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W)) ℓ) = M'.evalMap_overrideC hY hZrW s0 (valuesUnionMk zr w') ℓ) : ∀ᵐ w ∂((M'.obsKernel s0).map (valuesProjection hW)), (M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y W ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW) (M'.fixSetExtend Z hZ_obs hZ_fixed s0 t, w) = ((condDistrib (valuesProjection (M'.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) (fun ℓ : M'.LatentValues => valuesProjection hW (M'.randomToObserved (M'.evalMap s0 ℓ))) M'.latentProduct) w).map (h t w) := by -- Witness-route per-slice identity, **M1-witness-kernel form**. The LHS (the M2 -- `W`-conditional intervened at `t`) equals the M1 posterior witness kernel at -- `(t, w)`. The M2 witness chain (`obsCondKernel_ae_eq_condDistrib`@M2 → -- `condDistrib_map`@M2 → the M2 cut-set factorization with trivial `Zr` -- coordinate → the M2 witness identity) and the cross-SCM identification of the M2 -- witness kernel with the M1 witness kernel via `fixSet_latentProduct_compat` + -- `evalMap_overrideC_fixSet_compat_on_fillZrW`, transported onto the common `μW` -- base by Rule 3* (`obsKernel_fixSet_W_marginal_eq_M1_marginal`). The analytic -- core is isolated as `doSide_M2_condDistrib_eq_M1_witness`; here we discharge -- the assembly (obsCondKernel ↔ condDistrib bridge at M2 + base alignment). classical set M2 := M'.fixSet Z hZ_obs hZ_fixed with hM2 set s' := M'.fixSetExtend Z hZ_obs hZ_fixed s0 t with hs' set hY_M2 : Y ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY with hhY_M2 set hW_M2 : W ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW with hhW_M2 set μW := (M'.obsKernel s0).map (valuesProjection hW) with hμW -- Base alignment: the M2 `W`-marginal at the slice `s'` equals `μW` (Rule 3* + -- `fixSetProj (fixSetExtend s0 t) = s0`). have hbase : (M2.obsKernel s').map (valuesProjection hW_M2) = μW := by have hRule3 := obsKernel_fixSet_W_marginal_eq_M1_marginal M' Z hZ_obs hZ_fixed W hW hWNonDesc s' rw [hμW] rw [show (M2.obsKernel s').map (valuesProjection hW_M2) = (M2.obsKernel s').map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW)) from rfl, hRule3, M'.fixSetProj_fixSetExtend Z hZ_obs hZ_fixed s0 t] -- Step 1: at M2, `obsCondKernel Y W (s', ·) =ᵐ condDistrib π_Y π_W (M2.obsKernel s')`, -- with base `(M2.obsKernel s').map π_W`. have h1 := M2.obsCondKernel_ae_eq_condDistrib Y W hY_M2 hW_M2 s' rw [hbase] at h1 -- Step 2: the analytic core — that condDistrib equals the M1 witness kernel. have h2 := doSide_M2_condDistrib_eq_M1_witness M' Z hZ_obs hZ_fixed Y W hY hW hZrW hDisj_YZr hWNonDesc s0 t h hh hoverride -- Both `h1` and `h2` are stated over the base `μW`; chain. filter_upwards [h1, h2] with w hw1 hw2 -- `hw1 : M2.obsCondKernel Y W (s', w) = condDistrib π_Y π_W (M2.obsKernel s') w` -- `hw2 : condDistrib π_Y π_W (M2.obsKernel s') w = witness` rw [hw1, hw2]

theorem obsCondKernel_fixSet_M1_eq_ae_product (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 : Y ⊆ M'.observed) (hW : W ⊆ M'.observed) (hZr : Z.image SWIGNode.random ⊆ M'.observed) (hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed) (hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W) (hDisj_YZr : Disjoint Y (Z.image SWIGNode.random)) (hWNonDesc : ∀ z ∈ Z, ∀ v ∈ W, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v) (hWNonDescM1 : ∀ D ∈ Z, ∀ w ∈ W, ¬ M'.dag.isAncestor (SWIGNode.random D) w) (hdSep : (M'.fixSet Z hZ_obs hZ_fixed).dag.dSep Y (Z.image SWIGNode.random) (W ∪ (M'.fixSet Z hZ_obs hZ_fixed).fixed)) [StandardBorelSpace M'.RandomValues] [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [StandardBorelSpace (ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] [Nonempty (ValuesOn (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] [StandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).RandomValues] [StandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).ObservedValues] [StandardBorelSpace (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))] [Nonempty (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))] [∀ s : M'.FixedValues, IsFiniteMeasure (M'.jointKernel s)] [∀ s : M'.FixedValues, IsFiniteMeasure (M'.obsKernel s)] [∀ s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues, IsFiniteMeasure ((M'.fixSet Z hZ_obs hZ_fixed).jointKernel s)] [∀ s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues, IsFiniteMeasure ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s)] [CountableOrCountablyGenerated M'.FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn W (swigΩ Ω))] [MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] (s0 : M'.FixedValues) (_hPositivity_ae : (((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ const _ ((M'.obsKernel s0).map (valuesProjection hW))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M'.obsKernel s0).map (valuesProjection hZrW))) : ∀ᵐ p ∂((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ const _ ((M'.obsKernel s0).map (valuesProjection hW))), (M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y W ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW) (M'.fixSetExtend Z hZ_obs hZ_fixed s0 p.1, p.2) = M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (s0, valuesUnionMk p.1 p.2) := by -- **Per-slice posterior-witness construction.** `doSide_eq_witness` gives, -- for each treatment value `t`, the equality of LHS and RHS at the slice -- `s' := fixSetExtend s0 t`, a.e. in `w` under `μW = (M'.obsKernel s0).map π_W` -- (the M2 `W`-marginal at the slice equals `μW` literally by Rule 3*, -- `obsKernel_fixSet_W_marginal_eq_M1_marginal`). Both sides of that per-slice -- identity are pinned to the posterior witness kernel -- `(condDistrib C_W (π_W∘E1) M1.latentProduct w).map (h t w)` — RHS via -- `obsCondKernel_union_eq_witness`@M1, LHS via the M2 witness chain + cross-SCM -- connect. This proof does not rely on the retired rectangle identity -- `obsKernel_fixSet_rect_eq`. Finally `ae_compProd_of_ae_ae` lifts the iterated -- `∀ᵐ t, ∀ᵐ w` statement to the product `νZ ⊗ₘ const μW`. classical set M2 := M'.fixSet Z hZ_obs hZ_fixed with hM2 set hY_M2 : Y ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY with hhY_M2 set hW_M2 : W ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW with hhW_M2 set νZ := (M'.obsKernel s0).map (valuesProjection hZr) with hνZ set μW := (M'.obsKernel s0).map (valuesProjection hW) with hμW set lam := νZ ⊗ₘ const _ μW with hlam -- The fill map and the cut-set factorization data, shared by both witness lemmas. set G : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω) → ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω) := fun p => valuesUnionMk p.1 p.2 with hG have hG_meas : Measurable G := by fun_prop haveI hΩne : ∀ n, Nonempty (Ω n) := fun n => (inferInstance : Nonempty (swigΩ Ω (SWIGNode.random n))) obtain ⟨h, hh, hfac, hoverride⟩ := cutset_factor_pointwise M' Y W Z hY hZrW s0 -- The shared posterior witness kernel, as a function of the conditioning pair. set wk : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω) → Measure (ValuesOn Y (swigΩ Ω)) := fun p => ((condDistrib (valuesProjection (M'.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) (fun ℓ : M'.LatentValues => valuesProjection hW (M'.randomToObserved (M'.evalMap s0 ℓ))) M'.latentProduct) p.2).map (h p.1 p.2) with hwk -- The projection facts: under `G = valuesUnionMk`, the union iso recovers `(t, w)`. have hproj_left : ∀ (t : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω)) (w : ValuesOn W (swigΩ Ω)), valuesProjection (subset_union_left) (valuesUnionMk t w) = t := by intro t w; funext v exact valuesUnionMk_apply_left t w v.property have hproj_right : ∀ (t : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω)) (w : ValuesOn W (swigΩ Ω)), valuesProjection (subset_union_right) (valuesUnionMk t w) = w := by intro t w; funext v have hnotleft : v.val ∉ Z.image SWIGNode.random := fun hv => (Finset.disjoint_left.mp hDisj_ZrW) hv v.property exact valuesUnionMk_apply_right t w (subset_union_right v.property) hnotleft haveI hM2Markov : IsMarkovKernel (M2.obsCondKernel Y W hY_M2 hW_M2) := by unfold SCM.obsCondKernel; infer_instance haveI hM1Markov : IsMarkovKernel (M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW) := by unfold SCM.obsCondKernel; infer_instance -- **RHS = witness** (transport `obsCondKernel_union_eq_witness`@M1 from `μ_C` onto -- `lam` via the product positivity `hPositivity_ae`). This is where positivity is -- consumed. have h_rhs_witness : ∀ᵐ p ∂lam, M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (s0, G p) = wk p := by -- Cutset d-sep at M1, derived from the do-graph d-sep `hdSep`@M2 + criterion (i) -- (`hWNonDescM1`) via the cross-model graph lemma. This REPLACES the deleted -- false hypothesis `hdSepM1 : M'.dag.dSep Y Zr (W∪M'.fixed)`. have hdSepCW : M'.dag.dSep (M'.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (Z.image SWIGNode.random) (W ∪ M'.fixed) := M'.cutsetLatent_dSep_of_fixSet_dSep Z hZ_obs hZ_fixed Y W hW hWNonDescM1 hdSep have hunion := obsCondKernel_union_eq_witness M' Y W Z hY hZrW hDisj_ZrW hdSepCW s0 h hh hfac -- `lam.map G ≪ μ_C` (the positivity assumption) transports the `μ_C`-a.e. identity. have hAC : map G lam ≪ (M'.obsKernel s0).map (valuesProjection hZrW) := _hPositivity_ae have h_mapG : (fun c => M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (s0, c)) =ᵐ[lam.map G] (fun c => ((condDistrib (valuesProjection (M'.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) (fun ℓ : M'.LatentValues => valuesProjection hW (M'.randomToObserved (M'.evalMap s0 ℓ))) M'.latentProduct) (valuesProjection (subset_union_right) c)).map (h (valuesProjection (subset_union_left) c) (valuesProjection (subset_union_right) c))) := hAC.ae_eq hunion have h_prod := MeasureTheory.ae_of_ae_map hG_meas.aemeasurable h_mapG filter_upwards [h_prod] with p hp rw [hp, hwk] -- Rewrite the projections of `G p = valuesUnionMk p.1 p.2` to `p.1`, `p.2`. simp only [hG, hproj_left, hproj_right] -- **LHS = witness** (the do-side per-slice identity, lifted to `lam`). have h_lhs_witness : ∀ᵐ p ∂lam, M2.obsCondKernel Y W hY_M2 hW_M2 (M'.fixSetExtend Z hZ_obs hZ_fixed s0 p.1, p.2) = wk p := by refine MeasureTheory.Measure.ae_compProd_of_ae_ae ?_ ?_ · -- Measurability of the agreement set. have hfst : Measurable (fun p : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω) => M2.obsCondKernel Y W hY_M2 hW_M2 (M'.fixSetExtend Z hZ_obs hZ_fixed s0 p.1, p.2)) := by fun_prop have hwk_meas : Measurable wk := by rw [hwk] exact ProbabilityTheory.Kernel.measurable (witnessKernel M'.latentProduct (Z := fun ℓ => valuesProjection hW (M'.randomToObserved (M'.evalMap s0 ℓ))) (C := valuesProjection (M'.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) hh) exact measurableSet_measure_eq hfst hwk_meas (fun _ => inferInstance) · -- The per-slice posterior witness-kernel identity at `s' := fixSetExtend s0 t`. refine MeasureTheory.ae_of_all _ (fun t => ?_) rw [ProbabilityTheory.Kernel.const_apply] exact SCM.doSide_eq_witness M' Z hZ_obs hZ_fixed Y W hY hW hZrW hDisj_YZr hWNonDesc s0 t h hh hoverride -- Combine: LHS = witness = RHS. filter_upwards [h_lhs_witness, h_rhs_witness] with p hL hR rw [hL, ← hR]

theorem obsSide_eq_witness (M : SCM N Ω) [StandardBorelSpace M.RandomValues] [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] [∀ s : M.FixedValues, IsFiniteMeasure (M.jointKernel s)] (Y W : Finset (SWIGNode N)) (Z : Finset N) [StandardBorelSpace (ValuesOn (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] [Nonempty (ValuesOn (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω))] [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] (hY : Y ⊆ M.observed) (hZr : Z.image SWIGNode.random ⊆ M.observed) (hW : W ⊆ M.observed) (hdSepCW : M.dag.dSep (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (Z.image SWIGNode.random) (W ∪ M.fixed)) (s : M.FixedValues) (h : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) → ValuesOn W (swigΩ Ω) → ValuesOn (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω) → ValuesOn Y (swigΩ Ω)) (hh : Measurable (fun p : (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω)) × ValuesOn (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω) => h p.1.1 p.1.2 p.2)) (hfac : ∀ ℓ : M.LatentValues, valuesProjection hY (M.randomToObserved (M.evalMap s ℓ)) = h (valuesProjection hZr (M.randomToObserved (M.evalMap s ℓ))) (valuesProjection hW (M.randomToObserved (M.evalMap s ℓ))) (valuesProjection (M.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W)) ℓ)) : (fun p : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω) => condDistrib (fun ℓ : M.LatentValues => valuesProjection hY (M.randomToObserved (M.evalMap s ℓ))) (fun ℓ : M.LatentValues => (valuesProjection hZr (M.randomToObserved (M.evalMap s ℓ)), valuesProjection hW (M.randomToObserved (M.evalMap s ℓ)))) M.latentProduct p) =ᵐ[M.latentProduct.map (fun ℓ : M.LatentValues => (valuesProjection hZr (M.randomToObserved (M.evalMap s ℓ)), valuesProjection hW (M.randomToObserved (M.evalMap s ℓ))))] (fun p => (condDistrib (valuesProjection (M.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) (fun ℓ : M.LatentValues => valuesProjection hW (M.randomToObserved (M.evalMap s ℓ))) M.latentProduct p.2).map (h p.1 p.2)) := by haveI : IsProbabilityMeasure M.latentProduct := inferInstance have hX : Measurable (fun ℓ : M.LatentValues => valuesProjection hZr (M.randomToObserved (M.evalMap s ℓ))) := by fun_prop have hZmeas : Measurable (fun ℓ : M.LatentValues => valuesProjection hW (M.randomToObserved (M.evalMap s ℓ))) := by fun_prop have hCmeas : Measurable (valuesProjection (Ω := swigΩ Ω) (M.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) := by fun_prop -- The witness lemma's `Y = h X Z C` pointwise (from `hfac`). have hY_eq : (fun ℓ : M.LatentValues => valuesProjection hY (M.randomToObserved (M.evalMap s ℓ))) = fun ℓ => h (valuesProjection hZr (M.randomToObserved (M.evalMap s ℓ))) (valuesProjection hW (M.randomToObserved (M.evalMap s ℓ))) (valuesProjection (M.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W)) ℓ) := funext hfac have hwit := condDistrib_map_of_condDistrib_fst_eq (Ω := M.LatentValues) (𝒳 := ValuesOn (Z.image SWIGNode.random) (swigΩ Ω)) (𝒵 := ValuesOn W (swigΩ Ω)) (𝒞 := ValuesOn (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (swigΩ Ω)) (𝒴 := ValuesOn Y (swigΩ Ω)) (μ := M.latentProduct) (X := fun ℓ => valuesProjection hZr (M.randomToObserved (M.evalMap s ℓ))) (Z := fun ℓ => valuesProjection hW (M.randomToObserved (M.evalMap s ℓ))) (C := valuesProjection (M.cutsetLatent_subset Y (Z.image SWIGNode.random ∪ W))) (h := h) hX hZmeas hCmeas hh (cutset_condIndep_condDistrib M Y W Z hZr hW hdSepCW s) -- `hwit` conditions `condDistrib (fun ℓ => h (X ℓ)(Z ℓ)(C ℓ)) ...`; rewrite via `hY_eq`. rw [hY_eq] exact hwit