SEM: Bundled Structural Equation Model (V2)

A SEM V α is a CausalGraph V together with a Mechanism for every vertex. Replaces the old CausalDynamics (which conflated the implicit graph topology with the precondition-list mechanism content into a single List CausalLaw).

IsDeterministic and IsBool are Prop mixin classes that consumers can require — mirroring the mathlib pattern where typeclass mixins mark properties of a structure value (IsMarkovKernel etc.).

Phase A scope: structure + mixins only. Forward propagation, intervention, and counterfactual queries live in SEM/Basic.lean.

structure Core.Causal.SEM (V : Type u_1) (α : V → Type u_2) : Type (max u_1 u_2)

A structural equation model: a causal graph with a mechanism at every vertex over a per-vertex value type α.

Replaces the old CausalDynamics. The graph topology is now explicit (graph.parents v) and separate from mechanism content (mech v); the value type is parameterized (α : V → Type*) instead of hardcoded Bool.

• graph : CausalGraph V

  The underlying causal graph (parent finsets per vertex).

• mech (v : V) : Mechanism self.graph α v

  The mechanism at each vertex: parent values ↦ distribution over α v.

class Core.Causal.SEM.IsDeterministic {V : Type u_1} {α : V → Type u_2} (M : SEM V α) : Type (max u_1 u_2)

The SEM is fully deterministic: every vertex's mechanism is Dirac.

• mech_det (v : V) : (M.mech v).IsDeterministic

@[implicit_reducible]

instance Core.Causal.SEM.instIsDeterministicMechOfIsDeterministic {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [h : M.IsDeterministic] (v : V) : (M.mech v).IsDeterministic

Project per-vertex Mechanism.IsDeterministic from SEM.IsDeterministic.

Equations

• M.instIsDeterministicMechOfIsDeterministic v = Core.Causal.SEM.IsDeterministic.mech_det v