SCM.ID.Discrete ID
Discrete ID support: point-mass algebra, positivity conditions, and the executable checker for finite/discrete identification formulas.
Mass 5 core · 16 supporting This file provides the finite-measure primitives used by the discrete ID lane: singleton masses, marginal singleton masses, and conditional masses as ratios. ★ valuesOn_measure_eq_of_singletonMass_eq
Finite masses for discrete ID
This file provides the finite-measure primitives used by the discrete ID lane: singleton masses, marginal singleton masses, and conditional masses as ratios. The definitions are intentionally point-mass based, so later ID proofs can state positivity on the actual denominators used by a formula.
The main API includes:
* singletonMass, marginalMass, conditionalMass, and
conditionalDenominator for writing finite observational formulas.
* measure_eq_of_singletonMass_eq and valuesOn_measure_eq_of_singletonMass_eq,
which reduce equality of finite/countable measures to equality of all singleton
masses.
* singletonMass_map_eq_sum_fiber, singletonMass_comp_eq_sum, and the
point-mass specializations for constant or degenerate mixtures.
* conditionalMass_mul_denominator, the algebraic cancellation lemma that
recovers the joint point mass from a conditional-mass ratio once the actual
denominator is nonzero and finite.
def singletonMass reviewed
⚑ flagged
Causalean.SCM.ID.DiscreteID
The mass that a measure assigns to a single point.
Definition (Lean source)
noncomputable def singletonMass {α : Type*} [MeasurableSpace α]
(μ : Measure α) (x : α) : ENNReal :=
μ ({x} : Set α)
def marginalMass reviewed
⚑ flagged
Causalean.SCM.ID.DiscreteID
The marginal mass of a selected coordinate value.
Definition (Lean source)
noncomputable def marginalMass {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
(μ : Measure α) (f : α → β) (_hf : Measurable f) (y : β) : ENNReal :=
singletonMass (μ.map f) y
def conditionalMass reviewed
⚑ flagged
Causalean.SCM.ID.DiscreteID
A discrete conditional mass, written as a ratio of a joint point mass to a marginal point mass. A sound ID formula must separately carry positivity for the denominator when it uses this value.
Definition (Lean source)
noncomputable def conditionalMass {α β : Type*}
[MeasurableSpace α] [MeasurableSpace β]
(μ : Measure (α × β)) (a : α) (b : β) : ENNReal :=
singletonMass μ (a, b) / singletonMass (μ.map snd) b
def conditionalDenominator reviewed
⚑ flagged
Causalean.SCM.ID.DiscreteID
The denominator used by conditionalMass.
Definition (Lean source)
noncomputable def conditionalDenominator {α β : Type*}
[MeasurableSpace α] [MeasurableSpace β]
(μ : Measure (α × β)) (b : β) : ENNReal :=
singletonMass (μ.map snd) b
theorem valuesOn_measure_eq_of_singletonMass_eq reviewed
⚑ flagged
Causalean.SCM.ID.DiscreteID
For two measures on a finite-coordinate product over countable value spaces, if every value assignment carries the same singleton point mass under both measures, then the two measures are equal.
Formal statement
hypotheses
conclusion
μ = ν
Proof (Lean source)
theorem valuesOn_measure_eq_of_singletonMass_eq
{M : Type*}
{Ω' : M → Type*} [∀ m, MeasurableSpace (Ω' m)] [∀ m, Countable (Ω' m)]
(I : Finset M)
{μ ν : Measure (ValuesOn I Ω')}
(h : ∀ x : ValuesOn I Ω', singletonMass μ x = singletonMass ν x) :
μ = ν :=
measure_eq_of_singletonMass_eq h
16 supporting declarations (lemmas, instances)
-
singletonMass_applytheoremhypothesesconclusionsingletonMass μ x = μ ({x} : Set α)Proof (Lean source)
@[simp] theorem singletonMass_apply {α : Type*} [MeasurableSpace α] (μ : Measure α) (x : α) : singletonMass μ x = μ ({x} : Set α) := rfl -
measure_eq_of_singletonMass_eqtheorem — Measures on a countable space are equal when all singleton masses agree.Proof (Lean source)
theorem measure_eq_of_singletonMass_eq {α : Type*} [MeasurableSpace α] [Countable α] {μ ν : Measure α} (h : ∀ x : α, singletonMass μ x = singletonMass ν x) : μ = ν := MeasureTheory.Measure.ext_of_singleton h -
eq_of_ae_eq_of_forall_singletonMass_ne_zerotheorem — An almost-everywhere equality is pointwise when every singleton has nonzero mass.hypothesesconclusion∀ x : α, f x = g xProof (Lean source)
theorem eq_of_ae_eq_of_forall_singletonMass_ne_zero {α β : Type*} [MeasurableSpace α] {μ : Measure α} {f g : α → β} (hμ : ∀ x : α, singletonMass μ x ≠ 0) (hfg : f =ᵐ[μ] g) : ∀ x : α, f x = g x := by intro x by_contra hx have hnull : μ {y | ¬ f y = g y} = 0 := MeasureTheory.ae_iff.mp hfg have hsubset : ({x} : Set α) ⊆ {y | ¬ f y = g y} := by intro y hy have hyx : y = x := by simpa using hy simpa [hyx] using hx have hxzero : singletonMass μ x = 0 := by rw [singletonMass_apply] exact MeasureTheory.measure_mono_null hsubset hnull exact hμ x hxzero -
singletonMass_maptheorem — The singleton mass of a mapped measure is the mass of the corresponding fibre.hypothesesconclusionsingletonMass (μ.map f) y = μ (f ⁻¹' ({y} : Set β))Proof (Lean source)
theorem singletonMass_map {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y : β) : singletonMass (μ.map f) y = μ (f ⁻¹' ({y} : Set β)) := by rw [singletonMass_apply, MeasureTheory.Measure.map_apply hf (MeasurableSet.singleton y)] -
singletonMass_map_const_eq_univtheorem — If a measurable map is pointwise constant, the pushed-forward measure has all mass at that constant value.hypothesesconclusionsingletonMass (μ.map f) y0 = μ univProof (Lean source)
theorem singletonMass_map_const_eq_univ {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y0 : β) (hconst : ∀ x : α, f x = y0) : singletonMass (μ.map f) y0 = μ univ := by rw [singletonMass_map μ hf y0] congr ext x simp [hconst x] -
singletonMass_map_const_eq_zero_of_netheorem — If a measurable map is pointwise constant at y0, the pushed-forward measure has zero singleton mass at every different value.hypothesesconclusionsingletonMass (μ.map f) y = 0Proof (Lean source)
theorem singletonMass_map_const_eq_zero_of_ne {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y0 y : β) (hconst : ∀ x : α, f x = y0) (hy : y ≠ y0) : singletonMass (μ.map f) y = 0 := by rw [singletonMass_map μ hf y] have hpre : f ⁻¹' ({y} : Set β) = (∅ : Set α) := by ext x have hy' : y0 ≠ y := fun h => hy h.symm simp [hconst x, hy'] rw [hpre, MeasureTheory.measure_empty] -
singletonMass_map_const_eq_onetheorem — A pointwise constant measurable map from a probability measure gives unit singleton mass at the constant value.hypothesesconclusionsingletonMass (μ.map f) y0 = 1Proof (Lean source)
theorem singletonMass_map_const_eq_one {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y0 : β) (hconst : ∀ x : α, f x = y0) (hμ : μ univ = 1) : singletonMass (μ.map f) y0 = 1 := by rw [singletonMass_map_const_eq_univ μ hf y0 hconst, hμ] -
singletonMass_map_eq_sum_fibertheorem — On a finite measurable-singleton space, the singleton mass of a pushed-forward measure is the finite sum of singleton masses over the fiber.hypothesesconclusionsingletonMass (μ.map f) y = ∑ x : α, if f x = y then singletonMass μ x else 0Proof (Lean source)
theorem singletonMass_map_eq_sum_fiber {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [DecidableEq β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y : β) : singletonMass (μ.map f) y = ∑ x : α, if f x = y then singletonMass μ x else 0 := by classical let s : Finset α := Finset.univ.filter fun x => f x = y have hs : (s : Set α) = f ⁻¹' ({y} : Set β) := by ext x simp [s] calc singletonMass (μ.map f) y = μ (f ⁻¹' ({y} : Set β)) := by exact singletonMass_map μ hf y _ = μ (s : Set α) := by rw [← hs] _ = ∑ x ∈ s, μ ({x} : Set α) := by rw [← MeasureTheory.sum_measure_singleton (μ := μ) (s := s)] _ = ∑ x : α, if f x = y then singletonMass μ x else 0 := by have hsum : (∑ x : α, if f x = y then singletonMass μ x else 0) = ∑ x ∈ s, μ ({x} : Set α) := by simp [singletonMass, s, Finset.sum_filter] exact hsum.symm -
sum_singletonMass_eq_univtheorem — On a finite measurable-singleton space, the sum of all singleton masses is the total mass of the measure.Proof (Lean source)
theorem sum_singletonMass_eq_univ {α : Type*} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (μ : Measure α) : (∑ x : α, singletonMass μ x) = μ univ := by classical calc (∑ x : α, singletonMass μ x) = ∑ x ∈ (Finset.univ : Finset α), μ ({x} : Set α) := by simp [singletonMass] _ = μ ((Finset.univ : Finset α) : Set α) := by rw [MeasureTheory.sum_measure_singleton] _ = μ univ := by simp -
sum_singletonMass_eq_onetheorem — On a finite measurable-singleton probability space, singleton masses sum to one.Proof (Lean source)
theorem sum_singletonMass_eq_one {α : Type*} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (μ : Measure α) [IsProbabilityMeasure μ] : (∑ x : α, singletonMass μ x) = 1 := by rw [sum_singletonMass_eq_univ] exact MeasureTheory.measure_univ -
singletonMass_comp_eq_sumtheorem — On a finite source space, the singleton mass of a kernel mixture is the finite weighted sum of the singleton masses of the kernel slices.Proof (Lean source)
theorem singletonMass_comp_eq_sum {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (μ : Measure α) (κ : Kernel α β) (y : β) : singletonMass (κ ∘ₘ μ) y = ∑ x : α, singletonMass μ x * singletonMass (κ x) y := by rw [singletonMass_apply, MeasureTheory.Measure.bind_apply (MeasurableSet.singleton y) κ.aemeasurable] rw [MeasureTheory.lintegral_fintype] simp [singletonMass, mul_comm] -
singletonMass_comp_eq_of_consttheorem — A finite kernel mixture has the common singleton mass of its slices when the finite singleton masses of the mixing measure sum to one.hypothesesα β :μ :Measure ακ :Kernel α βy :βc :hμ :(∑ x : α, singletonMass μ x) = 1hconst :∀ x : α, singletonMass (κ x) y = cconclusionsingletonMass (κ ∘ₘ μ) y = cProof (Lean source)
theorem singletonMass_comp_eq_of_const {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (μ : Measure α) (κ : Kernel α β) (y : β) (c : ENNReal) (hμ : (∑ x : α, singletonMass μ x) = 1) (hconst : ∀ x : α, singletonMass (κ x) y = c) : singletonMass (κ ∘ₘ μ) y = c := by rw [singletonMass_comp_eq_sum] calc (∑ x : α, singletonMass μ x * singletonMass (κ x) y) = ∑ x : α, singletonMass μ x * c := by apply Finset.sum_congr rfl intro x _hx rw [hconst x] _ = (∑ x : α, singletonMass μ x) * c := by rw [Finset.sum_mul] _ = c := by rw [hμ, one_mul] -
singletonMass_comp_eq_of_pointMasstheorem — A finite kernel mixture has the singleton mass of one slice when the mixing measure is a point mass at that slice.hypothesesα β :μ :Measure ακ :Kernel α βx0 :αy :βhμ0 :singletonMass μ x0 = 1hμzero :∀ x : αifx ≠ x0thensingletonMass μ x = 0conclusionsingletonMass (κ ∘ₘ μ) y = singletonMass (κ x0) yProof (Lean source)
theorem singletonMass_comp_eq_of_pointMass {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Finite α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (μ : Measure α) (κ : Kernel α β) (x0 : α) (y : β) (hμ0 : singletonMass μ x0 = 1) (hμzero : ∀ x : α, x ≠ x0 → singletonMass μ x = 0) : singletonMass (κ ∘ₘ μ) y = singletonMass (κ x0) y := by classical letI : Fintype α := ofFinite α rw [singletonMass_comp_eq_sum] rw [Finset.sum_eq_single x0] · rw [hμ0, one_mul] · intro x _hx hx rw [hμzero x hx, zero_mul] · intro hx exact (hx (Finset.mem_univ x0)).elim -
valuesProjection_surjectivetheorem — Coordinate restriction is surjective when every omitted coordinate has at least one default value.hypothesesconclusionSurjective (valuesProjection (Ω := Ω') hJI)Proof (Lean source)
theorem valuesProjection_surjective {M : Type*} {I J : Finset M} {Ω' : M → Type*} [∀ m, MeasurableSpace (Ω' m)] [∀ m : {m // m ∈ I}, Nonempty (Ω' m.val)] (hJI : J ⊆ I) : Surjective (valuesProjection (Ω := Ω') hJI) := by classical intro y refine ⟨fun i => if h : i.val ∈ J then y ⟨i.val, h⟩ else Classical.choice (inferInstance : Nonempty (Ω' i.val)), ?_⟩ funext j simp [valuesProjection] -
conditionalDenominator_applytheoremhypothesesconclusionProof (Lean source)
@[simp] theorem conditionalDenominator_apply {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure (α × β)) (b : β) : conditionalDenominator μ b = singletonMass (μ.map snd) b := rfl -
conditionalMass_mul_denominatortheorem — Multiplying a discrete conditional mass by its actual denominator recovers the joint point mass, provided that denominator is nonzero and finite.hypothesesα β :μ :Measure (α × β)a :αb :βh0 :conditionalDenominator μ b ≠ 0htop :conditionalDenominator μ b ≠ ∞conclusionProof (Lean source)
theorem conditionalMass_mul_denominator {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure (α × β)) (a : α) (b : β) (h0 : conditionalDenominator μ b ≠ 0) (htop : conditionalDenominator μ b ≠ ∞) : conditionalMass μ a b * conditionalDenominator μ b = singletonMass μ (a, b) := by rw [conditionalMass, conditionalDenominator] exact ENNReal.div_mul_cancel h0 htop
Positive 4 core · 4 supporting The discrete ID lane uses ratio-based conditional masses. ★ map_valuesProjection
Positivity assumptions for discrete ID formulas
The discrete ID lane uses ratio-based conditional masses. This file records the nonzero point-mass assumptions needed to make those ratios meaningful. The default model-level predicate is full observational support on every observed assignment at every fixed slice; later formula-level soundness lemmas can weaken it to only the denominators actually used by a concrete formula.
Important declarations are PositiveMass, DiscretePositive, and
StandardDiscretePositive, together with transport lemmas showing that positive
point mass is preserved by measurable surjections and coordinate projections.
These lemmas turn full observational support into the denominator positivity
needed by conditionalMass.
def PositiveMass reviewed
⚑ flagged
Causalean.SCM.ID.DiscreteID
A measure has full point-mass support when every singleton has nonzero mass.
Definition (Lean source)
def PositiveMass {α : Type*} [MeasurableSpace α] (μ : Measure α) : Prop :=
∀ x : α, singletonMass μ x ≠ 0
def DiscretePositive reviewed
⚑ flagged
Causalean.SCM.ID.DiscreteID
A discrete SCM has full observational support on every observed assignment, at every fixed-value slice. This is strong but non-vacuous, and it is the safe default assumption for first-pass discrete ID soundness.
Definition (Lean source)
theorem map_valuesProjection reviewed
⚑ flagged
Causalean.SCM.ID.DiscreteID.PositiveMass
If a measure assigns nonzero point mass to every value assignment on the full index set, then restricting to the values on a subset of coordinates reached by projection preserves this: the pushed-forward measure still assigns nonzero point mass to every value assignment on that subset.
Formal statement
hypotheses
M :
∀ m, MeasurableSpace (Ω' m)
∀ m, Nonempty (Ω' m)
MeasurableSingletonClass (ValuesOn J Ω')
hμ :
hJI :
J ⊆ I
conclusion
PositiveMass (μ.map (valuesProjection (Ω := Ω') hJI))
Proof (Lean source)
theorem PositiveMass.map_valuesProjection
{M : Type*}
{I J : Finset M} {Ω' : M → Type*}
[∀ m, MeasurableSpace (Ω' m)] [∀ m, Nonempty (Ω' m)]
[MeasurableSingletonClass (ValuesOn J Ω')]
{μ : Measure (ValuesOn I Ω')}
(hμ : PositiveMass μ) (hJI : J ⊆ I) :
PositiveMass (μ.map (valuesProjection (Ω := Ω') hJI)) :=
by
classical
exact PositiveMass.map_of_surjective (measurable_valuesProjection hJI) hμ
(valuesProjection_surjective hJI)
def StandardDiscretePositive reviewed
⚑ flagged
Causalean.SCM.ID.DiscreteID
The structural assumptions for the first discrete ID soundness target.
Definition (Lean source)
4 supporting declarations (lemmas, instances)
-
eq_of_ae_eqtheorem — Under positive point mass at every point, almost-everywhere equality is pointwise equality.hypothesesconclusion∀ x : α, f x = g xProof (Lean source)
theorem PositiveMass.eq_of_ae_eq {α β : Type*} [MeasurableSpace α] {μ : Measure α} (hμ : PositiveMass μ) {f g : α → β} (hfg : f =ᵐ[μ] g) : ∀ x : α, f x = g x := eq_of_ae_eq_of_forall_singletonMass_ne_zero hμ hfg -
map_of_surjectivetheorem — Positive point mass is preserved by a measurable surjection.Proof (Lean source)
theorem PositiveMass.map_of_surjective {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] {μ : Measure α} {f : α → β} (hf : Measurable f) (hμ : PositiveMass μ) (hsurj : Surjective f) : PositiveMass (μ.map f) := by intro y rcases hsurj y with ⟨x, hx⟩ rw [singletonMass_map μ hf y] intro hzero have hsubset : ({x} : Set α) ⊆ f ⁻¹' ({y} : Set β) := by intro z hz change f z = y rw [show z = x by simpa using hz, hx] have hle : μ ({x} : Set α) ≤ μ (f ⁻¹' ({y} : Set β)) := MeasureTheory.measure_mono hsubset have hxzero : singletonMass μ x = 0 := by rw [singletonMass_apply] exact le_antisymm (by simpa [hzero] using hle) zero_le exact hμ x hxzero -
of_map_injectivetheorem — Positive point mass can be pulled back across an injective measurable map when the pushed-forward measure is positive at every image value.Proof (Lean source)
theorem PositiveMass.of_map_injective {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] {μ : Measure α} {f : α → β} (hf : Measurable f) (hinj : Injective f) (hmap : PositiveMass (μ.map f)) : PositiveMass μ := by intro x have hxmap : singletonMass (μ.map f) (f x) ≠ 0 := hmap (f x) rw [singletonMass_map μ hf (f x)] at hxmap have hpre : f ⁻¹' ({f x} : Set β) = ({x} : Set α) := by ext y constructor · intro hy have hfy : f y = f x := by simpa using hy exact hinj hfy · intro hy have hyx : y = x := by simpa using hy simp [hyx] rw [hpre] at hxmap exact hxmap -
conditionalDenominator_ne_zero_of_positive_marginaltheorem — A positive marginal point mass is exactly the nonzero denominator needed by the finite conditional-mass ratio.hypothesesconclusionconditionalDenominator μ b ≠ 0Proof (Lean source)
theorem conditionalDenominator_ne_zero_of_positive_marginal {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure (α × β)} (hμ : PositiveMass (μ.map snd)) (b : β) : conditionalDenominator μ b ≠ 0 := hμ b
Checker 3 core · 5 supporting id_sound_rec proves soundness for the *declarative* success certificate idSucceedsRec (an inductive predicate — an existence claim needing a hand-built derivation). ★ idAlgorithm_sound
The executable ID algorithm and its soundness
id_sound_rec proves soundness for the declarative success certificate
idSucceedsRec (an inductive predicate — an existence claim needing a hand-built
derivation). This file adds the executable checker: a computable
Bool-valued function idAlgorithm that runs Tian's IDENTIFY procedure with a
fuel bound, together with idAlgorithm_sound — when the checker reports true,
the interventional query is identified.
* cFactorReachableRecB — computable, choice-free fuel-bounded IDENTIFY
reachability (mirrors the inductive CFactorReachableRec, using
cComponentSet.any in place of the noncomputable containingCComponent).
* idAlgorithm — the runnable checker: valid intervention, observed query,
and every post-intervention ancestral district recursively reachable.
* idAlgorithm_sound — the public soundness theorem: idAlgorithm … = true implies
IdentifiableUnder … (interventionalQuery X Y) over the standard discrete
positive model class. Obtained from id_sound_rec_discrete through the
structural bridge idAlgorithm_success_toRec.
def cFactorReachableRecB reviewed
⚑ flagged
Causalean.SCM.ID
Computable fuel-bounded IDENTIFY reachability. Returns true when the c-factor Q[C] can be recovered from Q[T] within fuel IDENTIFY steps. This is the executable mirror of the inductive CFactorReachableRec: it is choice-free (it searches (G.induce A).cComponentSet with any instead of naming the component via the noncomputable containingCComponent).
Definition (Lean source)
def cFactorReachableRecB (G : SWIGGraph N) :
ℕ → Finset (SWIGNode N) → Finset (SWIGNode N) → Bool
| 0, _, _ => false
| fuel + 1, T, C =>
decide C.Nonempty && decide (C ⊆ T) &&
(let A := inducedAncestral G T C
if A = C then true
else if A = T then false
else decide (∃ C' ∈ (G.induce A).cComponentSet,
C ⊆ C' ∧ cFactorReachableRecB G fuel C' C = true))
def idAlgorithm reviewed
⚑ flagged
Causalean.SCM.ID
The executable ID checker. Runs the recursive Tian–Shpitser algorithm on (G, X, Y) with fuel reduction steps: it requires a valid intervention split, an observed query disjoint from X, and that every c-component of the post-intervention ancestral graph is recursively reachable from its containing district. Computable — usable with #eval / decide on concrete graphs.
Definition (Lean source)
def idAlgorithm (fuel : ℕ) (G : SWIGGraph N)
(X : Finset N) (Y : Finset (SWIGNode N)) : Bool :=
if h : interventionValid X G then
decide (Y ⊆ G.observed) &&
decide (∀ d ∈ X, SWIGNode.random d ∉ Y) &&
decide (∀ S ∈ ((G.splitMono X h.1 h.2).induce
((G.splitMono X h.1 h.2).dag.ancestralSet Y)).cComponentSet,
∃ C ∈ G.cComponentSet,
S ⊆ C ∧ cFactorReachableRecB G fuel C S = true)
else
false
theorem idAlgorithm_sound reviewed
⚑ flagged
Causalean.SCM.ID
Soundness of the executable ID algorithm. When the runnable checker idAlgorithm returns true on the graph G, intervention set X, query Y, and the given fuel bound, the interventional query P(Y ∣ do(X)) is identified within the standard discrete positive model class.
Formal statement
hypotheses
∀ n, StandardBorelSpace (Ω n)
∀ n, Nonempty (Ω n)
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
fuel :
ℕ
G :
X :
Finset N
h :
idAlgorithm fuel G X Y = true
conclusion
Proof (Lean source)
theorem idAlgorithm_sound
[∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)]
[∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)]
(fuel : ℕ) (G : SWIGGraph N) (X : Finset N) (Y : Finset (SWIGNode N))
(h : idAlgorithm fuel G X Y = true) :
IdentifiableUnder G (fun _ => True) StandardDiscretePositive
(interventionalQuery (Ω := Ω) X Y) :=
id_sound_rec_discrete X Y G (idAlgorithm_success_toRec fuel G X Y h)
5 supporting declarations (lemmas, instances)
-
containingCComponent_eq_of_mem_of_subsettheorem — The unique c-component containing a nonempty set S is containingCComponent. Bridges the checker's cComponentSet.any search to the reachability predicate's choice-based containingCComponent.hypothesesG :hne :S.Nonemptyhmem :C' ∈ G.cComponentSethsub :S ⊆ C'conclusioncontainingCComponent G S = C'Proof (Lean source)
theorem containingCComponent_eq_of_mem_of_subset (G : SWIGGraph N) {S C' : Finset (SWIGNode N)} (hne : S.Nonempty) (hmem : C' ∈ G.cComponentSet) (hsub : S ⊆ C') : containingCComponent G S = C' := by classical have hchoose : hne.choose ∈ C' := hsub hne.choose_spec have hcomponent : G.cComponentOf hne.choose = C' := G.cComponentOf_eq_of_mem_cComponentSet hmem hchoose simpa [containingCComponent, hne] using hcomponent -
cComponentSet_nonemptytheorem — Every c-component in a graph's c-component set contains at least one node.Proof (Lean source)
theorem cComponentSet_nonempty (G : SWIGGraph N) {C : Finset (SWIGNode N)} (hmem : C ∈ G.cComponentSet) : C.Nonempty := by classical rw [SWIGGraph.cComponentSet, mem_image] at hmem obtain ⟨v, hv, rfl⟩ := hmem exact ⟨v, G.mem_cComponentOf_self hv⟩ -
cFactorReachableRecB_soundtheorem — Soundness of the computable reachability check. If the fuel-bounded checker accepts, the inductive reachability certificate holds.Proof (Lean source)
theorem cFactorReachableRecB_sound (G : SWIGGraph N) : ∀ (fuel : ℕ) (T C : Finset (SWIGNode N)), cFactorReachableRecB G fuel T C = true → CFactorReachableRec G T C := by classical intro fuel induction fuel with | zero => intro T C h simp [cFactorReachableRecB] at h | succ fuel ih => intro T C h simp only [cFactorReachableRecB, Bool.and_eq_true, decide_eq_true_eq] at h rcases h with ⟨⟨hne, hCT⟩, hinner⟩ by_cases hAC : inducedAncestral G T C = C · exact CFactorReachableRec.base hne hCT hAC · by_cases hAT : inducedAncestral G T C = T · have hinner' : (if T = C then true else false) = true := by simpa only [hAT, ↓reduceIte] using hinner have hTC : T = C := by by_contra hTC simp only [hTC, ↓reduceIte] at hinner' exact Bool.false_ne_true hinner' exact elim (hAC (hAT.trans hTC)) · have hex : ∃ C' ∈ (G.induce (inducedAncestral G T C)).cComponentSet, C ⊆ C' ∧ cFactorReachableRecB G fuel C' C = true := by simpa only [hAC, hAT, ↓reduceIte, decide_eq_true_eq] using hinner rcases hex with ⟨C', hC', hCC', hrecB⟩ have hrec : CFactorReachableRec G C' C := ih C' C hrecB have hcontain : containingCComponent (G.induce (inducedAncestral G T C)) C = C' := containingCComponent_eq_of_mem_of_subset (G.induce (inducedAncestral G T C)) hne hC' hCC' exact CFactorReachableRec.step hne hCT hAC hAT (hcontain ▸ hrec) -
instDecidableInterventionValidinstance — Validity of an intervention split is decidable — enables the executable idAlgorithm to branch on it.instance instDecidableInterventionValid (X : Finset N) (G : SWIGGraph N) : Decidable (interventionValid X G) := by unfold interventionValid infer_instance -
idAlgorithm_success_toRectheorem — A successful run yields the graphical certificate. idAlgorithm … = true implies the declarative recursive success certificate idSucceedsRec.hypothesesconclusionidSucceedsRec X Y GProof (Lean source)
theorem idAlgorithm_success_toRec (fuel : ℕ) (G : SWIGGraph N) (X : Finset N) (Y : Finset (SWIGNode N)) (h : idAlgorithm fuel G X Y = true) : idSucceedsRec X Y G := by classical unfold idAlgorithm at h by_cases hX : interventionValid X G · simp only [hX, dite_true, Bool.and_eq_true, decide_eq_true_eq] at h rcases h with ⟨⟨hYobs, hdisj⟩, hcert⟩ refine ⟨hX, hYobs, hdisj, ?_⟩ intro S hS rcases hcert S hS with ⟨C, hC, hSC, hrecB⟩ have hSne : S.Nonempty := cComponentSet_nonempty _ hS have hrec : CFactorReachableRec G C S := cFactorReachableRecB_sound G fuel C S hrecB have hcontain : containingCComponent G S = C := containingCComponent_eq_of_mem_of_subset G hSne hC hSC exact hcontain ▸ hrec · simp [hX] at h