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 Causation.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 Causation.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 Causation.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 Causation.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 Causation.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 Causation.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 Causation.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 Causation.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.

The strict Schulz/Nadathur development relation T_D ([Sch11b]; [Nad23b] Defs 4–5) never assigns values to undetermined background (parentless) variables and never resolves an inner variable while any parent is u-valued. developDetVtx? is its fixed point: some x is the paper's "s causally entails ⟨v, x⟩"; none means v stays u-valued. Contrast developDetVtx above, which eagerly fires const mechanisms at exogenous vertices — adequate for the PMF stack (where root mechanisms are genuine priors) but unfaithful to the deterministic causal-entailment predicates.

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

Partial per-vertex development: the strict T_D fixed point. Determined vertices keep their value; undetermined exogenous (parentless) vertices stay none; an undetermined inner vertex resolves iff every parent resolves.

Equations

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

theorem Causation.SEM.developDetVtx?_unfold {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] [DecidableEq V] (s : Valuation α) (v : V) : M.developDetVtx? s v = match s.get v with | some x => some x | none => if M.graph.parents v = ∅ then none else if hAll : ∀ (u : ↥(M.graph.parents v)), (M.developDetVtx? s ↑u).isSome = true then some (Mechanism.IsDeterministic.toFun (M.mech v) fun (u : ↥(M.graph.parents v)) => (M.developDetVtx? s ↑u).get ⋯) else none

Step lemma: one layer of WellFounded.fix_eq unfolding for the partial development.

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

A vertex determined in s develops to its value.

theorem Causation.SEM.developDetVtx?_exogenous {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] [DecidableEq V] {s : Valuation α} {v : V} (h : s.get v = none) (hPar : M.graph.parents v = ∅) : M.developDetVtx? s v = none

An undetermined exogenous vertex stays undetermined: T_D never fires parentless mechanisms.

theorem Causation.SEM.developDetVtx?_inner {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] [DecidableEq V] {s : Valuation α} {v : V} (h : s.get v = none) (hPar : M.graph.parents v ≠ ∅) (ρ : (u : ↥(M.graph.parents v)) → α ↑u) (hρ : ∀ (u : ↥(M.graph.parents v)), M.developDetVtx? s ↑u = some (ρ u)) : M.developDetVtx? s v = some (Mechanism.IsDeterministic.toFun (M.mech v) ρ)

An undetermined inner vertex whose parents all resolve fires its mechanism on the resolved parent values.

theorem Causation.SEM.developDetVtx?_inner_none {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] [DecidableEq V] {s : Valuation α} {v : V} (h : s.get v = none) (u : ↥(M.graph.parents v)) (hu : M.developDetVtx? s ↑u = none) : M.developDetVtx? s v = none

An undetermined vertex with an unresolved parent stays unresolved: T_D is strict.

theorem Causation.SEM.developDetVtx_eq_of_developDetVtx?_eq_some {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] [DecidableEq V] {s : Valuation α} {v : V} {x : α v} (h : M.developDetVtx? s v = some x) : M.developDetVtx s v = x

Refinement: wherever the strict dynamics resolves a vertex, the eager-total developDetVtx agrees.

def Causation.SEM.developDetVtxFuel {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.IsDeterministic] [DecidableEq V] (s : Valuation α) : ℕ → (v : V) → Option (α v)

Fuel-indexed computable mirror of developDetVtx?. Structural recursion on fuel, so concrete claims reduce in the kernel and decide works. developDetVtxFuel_eq_developDetVtx? connects it to the canonical fixed point once the fuel exceeds the vertex's rank.

Equations

• One or more equations did not get rendered due to their size.
• M.developDetVtxFuel s 0 x✝ = s.get x✝

theorem Causation.SEM.developDetVtxFuel_eq_developDetVtx? {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] [DecidableEq V] (rank : V → ℕ) (hrank : ∀ {u v : V}, u ∈ M.graph.parents v → rank u < rank v) (s : Valuation α) {n : ℕ} {v : V} : rank v < n → M.developDetVtxFuel s n v = M.developDetVtx? s v

Fuel bridge: with fuel exceeding any rank function that strictly increases along graph edges (e.g. the depth function a concrete model supplies to CausalGraph.IsDAG.of_depth), the fuel mirror computes the strict fixed point. Soundness and completeness in one equation.

theorem Causation.SEM.developDetVtx?_eq_of_fuel {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] [DecidableEq V] (rank : V → ℕ) (hrank : ∀ {u v : V}, u ∈ M.graph.parents v → rank u < rank v) {s : Valuation α} {n : ℕ} {v : V} {o : Option (α v)} (hn : rank v < n) (h : M.developDetVtxFuel s n v = o) : M.developDetVtx? s v = o

Transfer a concrete fuel computation to the canonical strict fixed point. The usual study idiom: developDetVtx?_eq_of_fuel M rank (by intro u v h; revert h; decide) (by omega) (by decide).