SEM: Deterministic Specialization (canonical developDet)

Per-vertex form of forward development for deterministic acyclic SEMs. The per-vertex pattern is intrinsically the deterministic specialization — see "Why per-vertex is deterministic-only" below.

developDetVtx M s v : α v is the per-vertex value, defined via IsDAG.wf.fix (recurses on IsStrictAncestor). The whole-valuation wrapper developDet M s : Valuation α is the canonical public name for "develop a deterministic acyclic SEM against a partial valuation." Returns some at every vertex (every vertex reaches a value via parent recursion bottoming out at roots).

Mathlib analogue: Mathlib/Probability/Kernel/Deterministic.lean — canonical type is the general Kernel α β (measure-valued); the deterministic case is a Dirac specialization with its own constructor and bridge theorems. Same pattern here: canonical develop M s : PMF (Valuation α) (in Basic.lean) lives alongside this deterministic specialization, connected by develop_eq_pure_of_deterministic.

Why per-vertex is deterministic-only

The deterministic per-vertex recursion developDetVtx M s v = mech.toFun (M.mech v) (fun u => developDetVtx M s u.val) works because each vertex has a unique value computable from parents.

Generalizing to stochastic (return PMF (α v)) requires composing per-parent marginals into a joint parent assignment to feed to the mechanism. But marginals don't compose into joints via PMF.bind without independence, and parents may be correlated through shared ancestors. Counterexample: A → B, A → C, mechanisms B := A, C := A. Per-vertex marginals: B Bernoulli(0.5), C Bernoulli(0.5). Naive PMF.bind composition: joint = uniform over (0,0)/(0,1)/(1,0)/(1,1). Truth: joint = (0,0) w.p. 0.5 OR (1,1) w.p. 0.5. The naive composition is mathematically wrong.

The canonical stochastic object is the joint develop M s : PMF (Valuation α) (in Basic.lean), which threads PMF.bind through the partial joint, preserving correlations. There is no clean per-vertex form for stochastic SEMs without belief-propagation infrastructure.

The computational specialization developDetOn M vs n s (in Basic.lean) is a separate axis — kernel-reducible iteration over an explicit vertex list, for proofs over concrete SEMs. Polynomial.eval₂ analogue.

Reduction

developDetVtx M s v reduces structurally via:

1. rw [developDetVtx_unfold] (or the convenience lemmas developDetVtx_extended/developDetVtx_undet) — opens one layer of the WellFounded.fix_eq recursion.
2. rfl (or simp when s.get v is determined) — closes when ground.

For 5-vertex SEMs, ~5 layers of unfolding suffice. No Fintype reasoning; no opaque Multiset.toList.

noncomputable def Core.Causal.SEM.developDetVtx {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [hDag : M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) : α v

Per-vertex forward development: given a deterministic acyclic SEM M and a partial valuation s, compute the value at vertex v by recursing on parents via IsStrictAncestor well-foundedness.

For determined vertices (s.get v = some x), returns x (idempotent on extension). For undetermined vertices, applies M.mech v's deterministic function to the recursively-computed parent values.

Total: every vertex in a deterministic acyclic SEM reaches a value (roots either have explicit values in s or are computed by their constant mechanisms). The whole-valuation wrapper developDet therefore returns some everywhere.

Equations

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

noncomputable def Core.Causal.SEM.developDet {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) : Valuation α

Canonical forward development of a deterministic acyclic SEM against a partial valuation, returning a Valuation α. Wraps developDetVtx with some at every vertex. Total under IsDAG + IsDeterministic.

Replaces the old Basic.lean developDet (Fintype-based, iteration-based, noncomputable, opaque). Same call-site shape ((M.developDet s).hasValue v x); cleanly reducible internals.

Equations

• M.developDet s v = some (M.developDetVtx s v)

theorem Core.Causal.SEM.developDetVtx_unfold {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) : M.developDetVtx s v = match s.get v with | some x => x | none => Mechanism.IsDeterministic.toFun (M.mech v) fun (u : ↥(M.graph.parents v)) => M.developDetVtx s ↑u

Step lemma: one layer of WellFounded.fix_eq unfolding. Use with rw to open developDetVtx M s v in proofs.

theorem Core.Causal.SEM.developDetVtx_extended {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) (x : α v) (h : s.get v = some x) : M.developDetVtx s v = x

When v is already determined in s, development is the value.

theorem Core.Causal.SEM.developDetVtx_undet {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) (h : s.get v = none) : M.developDetVtx s v = Mechanism.IsDeterministic.toFun (M.mech v) fun (u : ↥(M.graph.parents v)) => M.developDetVtx s ↑u

When v is undetermined in s, development applies the mechanism to the recursively-developed parent values.

@[simp]

theorem Core.Causal.SEM.developDet_isSome {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) : (M.developDet s v).isSome = true

developDet M s always returns some at every vertex.

theorem Core.Causal.SEM.developDet_apply {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) : M.developDet s v = some (M.developDetVtx s v)

developDet is some ∘ developDetVtx.

theorem Core.Causal.SEM.developDet_hasValue_iff {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) (x : α v) : (M.developDet s).hasValue v x ↔ M.developDetVtx s v = x

(M.developDet s).hasValue v x ↔ developDetVtx M s v = x.