Mechanism: PMF-Valued Structural Equation per Vertex (V2)

A Mechanism G α v is the structural equation at vertex v: it takes a value assignment to v's parents and returns a PMF (α v) — a probability distribution over possible values of v.

This single type unifies deterministic and stochastic mechanisms via the mathlib Kernel.deterministic := dirac ∘ f pattern (see Mathlib/Probability/Kernel/Basic.lean):

• Deterministic mechanism = PMF.pure-valued (Dirac delta) — see Mechanism/Deterministic.lean
• Stochastic mechanism = arbitrary PMF-valued run

A computable DetSEM structure (bare per-vertex functions, Dirac embedding) was considered and declined (2026-06 audit): kernel reduction already routes through IsDeterministic.toFun without touching PMF, and the fuel mirror (SEM.developDetVtxFuel) provides the computable evaluation path, so the refactor buys no proof power for its migration cost. The noncomputable markers on concrete study SEMs are the accepted residue.

IsDeterministic is a Prop mixin class that consumers can require when they need to extract the deterministic function (mirroring IsMarkovKernel in Mathlib/Probability/Kernel/Defs.lean).

structure Causation.Mechanism {V : Type u_1} (G : CausalGraph V) (α : V → Type u_2) (v : V) : Type (max u_1 u_2)

A causal mechanism for vertex v in graph G: takes a value assignment to v's parents and returns a distribution over α v. PMF-valued so deterministic and stochastic mechanisms share one type (deterministic = Dirac PMF).

• run : ((u : ↥(G.parents v)) → α ↑u) → PMF (α v)

  The structural function: parent assignment ↦ distribution over v's value.

class Causation.Mechanism.IsDeterministic {V : Type u_1} {α : V → Type u_2} {G : CausalGraph V} {v : V} (m : Mechanism G α v) : Type (max u_1 u_2)

A mechanism is deterministic when it carries an explicit total function over parents whose lifting via PMF.pure agrees with run.

Data-carrying class (not Prop) so consumers can extract toFun computably. Compare mathlib Module R M (data-carrying) vs IsMarkovKernel (Prop); we choose data-carrying because the underlying function is uniquely determined and useful in proofs.

• toFun : ((u : ↥(G.parents v)) → α ↑u) → α v

  The deterministic function over parent assignments.

• run_eq (ρ : (u : ↥(G.parents v)) → α ↑u) : m.run ρ = PMF.pure (toFun m ρ)

  The mechanism's run is the Dirac of toFun.