SEM: Forward Propagation, Intervention, Fixpoint (V2)

• intervene (Pearl do(v := x)): replace the mechanism for v with Mechanism.const x.

• ready/parentAssignment: a vertex is ready when all its parents are determined; the parent assignment can then be built as a Π-type.

• singleStepAtDet: per-vertex step. Computable. Three structural rewrite cases (extend / skip-determined / skip-not-ready) provide the simp normal form for unfolding stepOnceDetOn against a concrete list.

• stepOnceDetOn (vs : List V): foldl over an explicit vertex list. Computable; reduces structurally via the simp lemmas. Use this when consumers need decide-style kernel reduction on a concrete SEM.

• stepOnceDet (Fintype-based): canonical name, defined as stepOnceDetOn over (Fintype.elems : Finset V).toList. Noncomputable because Finset.toList is. Use for general theorems.

• developDetOn (vs : List V) (n : ℕ): bounded iteration of stepOnceDetOn. Computable. Consumers use this with their explicit list

  • iteration count for kernel-verifiable proofs.

• developDet: canonical Fintype-based wrapper. Iterates stepOnceDet for Fintype.card V steps — enough to reach the fixpoint regardless of vertex order. Noncomputable.

Mathlib pattern

This mirrors Polynomial/MvPolynomial: the canonical types are noncomputable (defined via Quotient/Finsupp), but consumers needing kernel evaluation supply explicit data and use the .eval-style computable variants. Structural simp lemmas let proofs unfold via rewriting rather than runtime evaluation.

noncomputable def Core.Causal.SEM.intervene {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) (v : V) (x : α v) : SEM V α

Pearl's do(v := x) intervention: replace the mechanism for v with the constant Dirac-PMF mechanism returning x. Other vertices' mechanisms are unchanged.

Equations

• M.intervene v x = { graph := M.graph, mech := fun (w : V) => if h : w = v then ⋯ ▸ Core.Causal.Mechanism.const x else M.mech w }

@[simp]

theorem Core.Causal.SEM.intervene_graph {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) (v : V) (x : α v) : (M.intervene v x).graph = M.graph

@[simp]

theorem Core.Causal.SEM.intervene_mech_self {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) (v : V) (x : α v) : (M.intervene v x).mech v = Mechanism.const x

The intervened vertex's mechanism becomes a constant Dirac.

@[simp]

theorem Core.Causal.SEM.intervene_mech_other {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) {v w : V} (x : α v) (h : w ≠ v) : (M.intervene v x).mech w = M.mech w

Other vertices' mechanisms are unaffected by intervention.

instance Core.Causal.SEM.instIsDAGGraphIntervene {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) [h : M.graph.IsDAG] (v : V) (x : α v) : (M.intervene v x).graph.IsDAG

An intervention preserves the graph (only the mechanism at v is replaced), so it preserves the IsDAG mixin.

@[implicit_reducible]

noncomputable instance Core.Causal.SEM.instIsDeterministicIntervene {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) [M.IsDeterministic] (v : V) (x : α v) : (M.intervene v x).IsDeterministic

An intervention preserves the IsDeterministic mixin: the intervened vertex becomes a Mechanism.const (a Dirac), and other vertices' mechanisms are unchanged.

Equations

• One or more equations did not get rendered due to their size.

def Core.Causal.SEM.ready {V : Type u_1} {α : V → Type u_2} (M : SEM V α) (s : Valuation α) (v : V) : Prop

A vertex is ready in a valuation when all its parents have determined values. Required precondition for firing the mechanism.

Equations

• M.ready s v = ∀ u ∈ M.graph.parents v, (s.get u).isSome = true

@[implicit_reducible]

instance Core.Causal.SEM.instDecidableReadyOfDecidableValuation {V : Type u_1} {α : V → Type u_2} [DecidableValuation α] (M : SEM V α) (s : Valuation α) (v : V) : Decidable (M.ready s v)

Equations

• M.instDecidableReadyOfDecidableValuation s v = Core.Causal.SEM.instDecidableReadyOfDecidableValuation._aux_1 M s v

def Core.Causal.SEM.parentAssignment {V : Type u_1} {α : V → Type u_2} (M : SEM V α) (s : Valuation α) (v : V) (h : M.ready s v) (u : ↥(M.graph.parents v)) : α ↑u

Build the parent-assignment Π-type, given that all parents are determined. Computable: Option.get on a value known to be some.

Equations

• M.parentAssignment s v h u = (s.get ↑u).get ⋯

def Core.Causal.SEM.singleStepAtDet {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (s : Valuation α) (v : V) : Valuation α

Per-vertex step of stepOnceDet. Computable. Three structural cases surfaced via simp lemmas (singleStepAtDet_extend, _skip_determined, _skip_not_ready) so consumers can unfold via simp rather than relying on decide reducing through opaque definitions.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Causal.SEM.singleStepAtDet_extend {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (s : Valuation α) (v : V) (hUndet : (s.get v).isNone = true) (hR : M.ready s v) : M.singleStepAtDet s v = s.extend v (Mechanism.IsDeterministic.toFun (M.mech v) (M.parentAssignment s v hR))

Structural unfolding: when v is undetermined and ready, the step extends the valuation with the mechanism's value at v.

@[simp]

theorem Core.Causal.SEM.singleStepAtDet_skip_determined {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (s : Valuation α) (v : V) (hDet : (s.get v).isSome = true) : M.singleStepAtDet s v = s

Structural unfolding: a determined vertex is skipped.

theorem Core.Causal.SEM.singleStepAtDet_skip_not_ready {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (s : Valuation α) (v : V) (hNR : ¬M.ready s v) : M.singleStepAtDet s v = s

Structural unfolding: an unready vertex is skipped.

def Core.Causal.SEM.stepOnceDetOn {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (vs : List V) (s : Valuation α) : Valuation α

One forward-development sweep over an explicit vertex list. Computable. Each fold step is singleStepAtDet.

Equations

• M.stepOnceDetOn vs s = List.foldl M.singleStepAtDet s vs

@[simp]

theorem Core.Causal.SEM.stepOnceDetOn_nil {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (s : Valuation α) : M.stepOnceDetOn [] s = s

@[simp]

theorem Core.Causal.SEM.stepOnceDetOn_cons {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (v : V) (vs : List V) (s : Valuation α) : M.stepOnceDetOn (v :: vs) s = M.stepOnceDetOn vs (M.singleStepAtDet s v)

The canonical developDet (per-vertex, via IsDAG.wf.fix) lives in PerVertex.lean. Below is the computational specialization: developDetOn M vs n s iterates stepOnceDetOn n times over an explicit vertex list vs. Computable; reducible structurally for kernel-verifiable proofs on concrete SEMs.

Mathlib analogue: `Polynomial.eval` (canonical) vs `Polynomial.eval₂`
with explicit ring hom (computational). Same mathematical object;
different reduction profiles.

`stepOnceDet` (the Fintype-based wrapper) is kept here as an internal
helper for the PMF stack's `stepOnce_eq_pure_of_deterministic` bridge —
see below. It's not part of the public API; consumers use either
`developDetOn` (computational) or `developDet` (canonical, in PerVertex.lean). 

noncomputable def Core.Causal.SEM.stepOnceDet {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (s : Valuation α) : Valuation α

One forward-development sweep using the Fintype enumeration of V. Internal helper for stepOnce_eq_pure_of_deterministic; not a public API. Public consumers use developDetOn (explicit list) or developDet (canonical per-vertex).

Equations

• M.stepOnceDet s = M.stepOnceDetOn Fintype.elems.toList s

def Core.Causal.SEM.developDetOn {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (vs : List V) (n : ℕ) (s : Valuation α) : Valuation α

Forward-development of a deterministic acyclic SEM against an explicit vertex list, with n iterations. Computable; consumers use this for kernel-verifiable proofs on concrete SEMs.

Fintype.card V iterations always suffice to reach the fixpoint (each effective iteration determines ≥1 more vertex).

Equations

• M.developDetOn vs n s = (M.stepOnceDetOn vs)^[n] s

@[simp]

theorem Core.Causal.SEM.developDetOn_zero {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (vs : List V) (s : Valuation α) : M.developDetOn vs 0 s = s

theorem Core.Causal.SEM.developDetOn_succ {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (vs : List V) (n : ℕ) (s : Valuation α) : M.developDetOn vs (n + 1) s = M.developDetOn vs n (M.stepOnceDetOn vs s)

Soundness bridge connecting the iteration form (developDetOn, computable, decide-friendly) to the canonical per-vertex form (developDet, abstract, WellFounded.fix-based).

**Direction**: `developDetOn → developDet`. If iteration produces
`some x` at `v`, then the canonical `developDetVtx M s v = x`. Lets
consumers prove `(M.developDet s).hasValue v x` by computing the
matching `developDetOn` claim with `decide`, then applying the bridge.

The reverse direction (completeness) requires proving that
`Fintype.card V` iterations always reach all reachable values —
deferred (would need induction on topological depth).

**Mathlib analogue**: `Multiset.sum_toList`, `Filter.tendsto_atTop_iff`
— bridges between an abstract canonical form and its computational
specialization, providing the connecting API. 

theorem Core.Causal.SEM.developDetVtx_of_developDetOn_hasValue {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] {M : SEM V α} [M.graph.IsDAG] [M.IsDeterministic] {s : Valuation α} {vs : List V} {n : ℕ} {v : V} {x : α v} (h : (M.developDetOn vs n s).hasValue v x) : M.developDetVtx s v = x

Soundness bridge: if iteration produces value x at v, then the canonical developDetVtx M s v = x.

Lets consumers prove abstract developDet-flavored claims by computing the corresponding developDetOn form with decide and lifting via this bridge.

The reverse direction (completeness — every vertex eventually determined) requires substrate work on topological depth and is deferred.

theorem Core.Causal.SEM.developDet_hasValue_of_developDetOn_hasValue {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] {M : SEM V α} [M.graph.IsDAG] [M.IsDeterministic] {s : Valuation α} {vs : List V} {n : ℕ} {v : V} {x : α v} (h : (M.developDetOn vs n s).hasValue v x) : (M.developDet s).hasValue v x

Valuation-form bridge: if iteration's hasValue claim holds, so does the canonical developDet's.

Completeness counterpart to the soundness bridge above. For a Fintype V + IsDAG + IsDeterministic SEM, Fintype.card V iterations of stepOnceDetOn over any vertex list covering all of V produce the canonical answer at every vertex.

Proof outline:
1. Monotonicity: `s.le (singleStepAtDet M s v)`, etc.
2. Single-step progress: undetermined+ready ⇒ determined after step.
3. IsDAG min: nonempty undetermined set has a `WellFounded.has_min`
   member whose strict ancestors (and so parents) are all determined,
   hence ready.
4. Pass-progress: every non-fixed pass strictly decreases `undetCount`.
5. Bound: after `Fintype.card V` passes, `undetCount = 0`. 

theorem Core.Causal.SEM.developDetOn_hasValue_developDetVtx {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] [Fintype V] {M : SEM V α} [M.graph.IsDAG] [M.IsDeterministic] {s : Valuation α} {vs : List V} (hCovers : ∀ (v : V), v ∈ vs) {n : ℕ} (hN : Fintype.card V ≤ n) (v : V) : (M.developDetOn vs n s).hasValue v (M.developDetVtx s v)

Headline completeness theorem: under Fintype V, IsDAG, and IsDeterministic, the iteration form developDetOn reaches the canonical developDetVtx value at every vertex, given a covering list and at least Fintype.card V iterations.

Proof: combine existence (developDetOn_isSome_of_card_le, bounded by Fintype.card V since undetCount s ≤ Fintype.card V) with soundness (developDetVtx_of_developDetOn_hasValue).

theorem Core.Causal.SEM.developDetOn_hasValue_iff {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] [Fintype V] {M : SEM V α} [M.graph.IsDAG] [M.IsDeterministic] {s : Valuation α} {vs : List V} (hCovers : ∀ (v : V), v ∈ vs) {n : ℕ} (hN : Fintype.card V ≤ n) (v : V) (x : α v) : (M.developDetOn vs n s).hasValue v x ↔ M.developDetVtx s v = x

Iff form of the bridge: under IsDAG + IsDeterministic + Fintype with sufficient iterations, developDetOn membership and developDetVtx equality coincide. Soundness gives →; completeness gives ← via the headline theorem.

theorem Core.Causal.SEM.developDet_hasValue_iff_developDetOn_hasValue {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] [Fintype V] {M : SEM V α} [M.graph.IsDAG] [M.IsDeterministic] {s : Valuation α} {vs : List V} (hCovers : ∀ (v : V), v ∈ vs) {n : ℕ} (hN : Fintype.card V ≤ n) (v : V) (x : α v) : (M.developDet s).hasValue v x ↔ (M.developDetOn vs n s).hasValue v x

Consumer Iff: developDet (canonical, opaque) and developDetOn (computational, decide-friendly) agree as hasValue predicates under IsDAG + IsDeterministic + Fintype + sufficient iterations. The decide-shaped form for (M.developDet s).hasValue v x proofs.

theorem Core.Causal.SEM.developDet_intervene_eq_developDet_extend {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [hDag : M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (h : s.get cause = none) : (M.intervene cause xC).developDet s = M.developDet (s.extend cause xC)

Intervention-as-Extend bridge: for an acyclic deterministic SEM with cause undetermined in s, Pearl-intervening to set cause := xC is equivalent (at the level of developDet) to extending the valuation with cause = xC and developing under the original mechanisms.

Load-bearing substrate fact connecting probabilisticSuf (intervene-based) to causallySufficient (extend-based). The proof goes by IsDAG.wf.induction on vertices: at cause both sides produce xC (LHS via the constant intervention mechanism; RHS via developDetVtx_extended short-circuit on the extended valuation); off-cause both sides reduce to the same mechanism applied to recursively-equal parent values via the IH.

The dependent-typeclass equality (toFun ((M.intervene cause xC).mech w) ρ = toFun (M'.mech w) ρ for M' = M.intervene cause xC or M) is discharged via the Mechanism.toFun_eq_of_mech_eq helper above, which routes through run_eq to bypass motive-not-type-correct issues that block direct rewriting of the mechanism.

Mathlib pattern: develop is PMF-valued unconditionally — the mathematical object that doesn't presuppose deterministic mechanisms. The developDet machinery above is the deterministic-as-Dirac specialization, connected to develop via develop_eq_pure_of_deterministic.

This mirrors Mathlib/Probability/Kernel/Basic.lean where Kernel α β is always measure-valued and Kernel.deterministic (f : α → β) is the Dirac specialization. Consumers needing the deterministic function go through developDet; consumers chaining probabilistic operations go through develop. The bridge theorem connects them — no API drift.

noncomputable def Core.Causal.SEM.singleStepAt {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) (s : Valuation α) (v : V) : PMF (Valuation α)

Per-vertex probabilistic step. Samples the mechanism's output PMF, extending the valuation with the sampled value. Reduces to singleStepAtDet-via-Dirac when the mechanism IsDeterministic.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Causal.SEM.singleStepAt_eq_pure_of_deterministic {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (s : Valuation α) (v : V) : M.singleStepAt s v = PMF.pure (M.singleStepAtDet s v)

Bridge: under IsDeterministic, the PMF step collapses to a Dirac of the deterministic step.

noncomputable def Core.Causal.SEM.stepOnce {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) (s : Valuation α) : PMF (Valuation α)

One PMF-valued forward sweep using the Fintype enumeration of V. Threads PMF.bind through each per-vertex step. Noncomputable because PMF is.

Equations

• M.stepOnce s = List.foldl (fun (acc : PMF (Core.Causal.Valuation α)) (v : V) => acc.bind fun (x : Core.Causal.Valuation α) => M.singleStepAt x v) (PMF.pure s) Fintype.elems.toList

theorem Core.Causal.SEM.stepOnce_eq_pure_of_deterministic {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (s : Valuation α) : M.stepOnce s = PMF.pure (M.stepOnceDet s)

Bridge: under IsDeterministic, stepOnce is the Dirac of stepOnceDet.

noncomputable def Core.Causal.SEM.develop {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] (s : Valuation α) : PMF (Valuation α)

Canonical PMF-valued forward-development. Iterates PMF.bind · stepOnce for Fintype.card V rounds. Mathlib-style: PMF-valued unconditionally; IsDeterministic consumers get back to a Valuation α via develop_eq_pure_of_deterministic below.

Equations

• M.develop s = (fun (p : PMF (Core.Causal.Valuation α)) => p.bind M.stepOnce)^[Fintype.card V] (PMF.pure s)

theorem Core.Causal.SEM.develop_eq_pure_of_deterministic {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) : M.develop s = PMF.pure (M.developDet s)

Bridge theorem (load-bearing): under IsDeterministic, the canonical PMF-valued develop collapses to the Dirac of the deterministic-specialization developDet (per-vertex, in SEM/Deterministic.lean).

This is the central correctness statement that lets the deterministic-as-Dirac pattern work cleanly. The two definitions are mathematically the same object viewed two ways:

• develop threads PMF.bind through the partial joint via iteration over Fintype.elems.toList.
• developDet recurses per-vertex via IsDAG.wf.fix, bottoming out at roots. Under IsDeterministic, the joint collapses to a Dirac at the valuation produced by per-vertex recursion.

Proof: PMF iteration collapses to PMF.pure ((stepOnceDet M)^[n] s) by induction on n (using stepOnce_eq_pure_of_deterministic + PMF.pure_bind). The pointwise equality with developDet M s follows from the completeness bridge developDetOn_hasValue_developDetVtx over the Fintype.elems.toList covering with Fintype.card V iterations: every vertex's iterated value equals some (developDetVtx M s v), definitionally developDet M s v.

Topological-order independence (deferred)

develop_perm_invariant — different topological sorts of an acyclic DAG give the same PMF. Provable via PMF.bind_comm + a lemma showing singleStepAt M s v is a no-op (PMF.pure s) when v is not yet ready. Not load-bearing for current consumers; deferred until a study needs to reason about develop against a hand-picked vertex order.