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 — see Mechanism/PMF.lean

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 Core.Causal.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 Core.Causal.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.