Structural Equation Model

@cite{nadathur-lauer-2020}

Theory-neutral infrastructure for deterministic causal and counterfactual reasoning based on Pearl's structural causal model framework.

• Variable: Named causal variables
• Situation: Partial valuations (Variable → Option Bool)
• CausalLaw: Structural equations (preconditions → effect)
• CausalDynamics: Collections of causal laws
• normalDevelopment: Forward propagation to fixpoint
• intervene: Pearl's do-operator (set variable, cut incoming laws)
• causallyNecessary / causallySufficient: Counterfactual tests
• manipulates: Does intervening on X change Y?

For the probabilistic causal Bayes net layer (WorldState, CausalRelation, NoisyOR), see Core.CausalBayesNet.

structure Core.StructuralEquationModel.Variable : Type

A variable in a causal model. Variables are named entities whose values are determined by causal laws.

• name : String

def Core.StructuralEquationModel.instDecidableEqVariable.decEq (x✝ x✝¹ : Variable) : Decidable (x✝ = x✝¹)

Equations

• Core.StructuralEquationModel.instDecidableEqVariable.decEq { name := a } { name := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Core.StructuralEquationModel.instDecidableEqVariable : DecidableEq Variable

Equations

• Core.StructuralEquationModel.instDecidableEqVariable = Core.StructuralEquationModel.instDecidableEqVariable.decEq

instance Core.StructuralEquationModel.instHashableVariable : Hashable Variable

Equations

• Core.StructuralEquationModel.instHashableVariable = { hash := Core.StructuralEquationModel.instHashableVariable.hash }

def Core.StructuralEquationModel.instHashableVariable.hash : Variable → UInt64

Equations

• Core.StructuralEquationModel.instHashableVariable.hash { name := a } = mixHash 0 (hash a)

def Core.StructuralEquationModel.instReprVariable.repr : Variable → ℕ → Std.Format

Equations

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

instance Core.StructuralEquationModel.instReprVariable : Repr Variable

Equations

• Core.StructuralEquationModel.instReprVariable = { reprPrec := Core.StructuralEquationModel.instReprVariable.repr }

instance Core.StructuralEquationModel.instInhabitedVariable : Inhabited Variable

Equations

• Core.StructuralEquationModel.instInhabitedVariable = { default := Core.StructuralEquationModel.instInhabitedVariable.default }

def Core.StructuralEquationModel.instInhabitedVariable.default : Variable

Equations

• Core.StructuralEquationModel.instInhabitedVariable.default = { name := default }

instance Core.StructuralEquationModel.instBEqVariable : BEq Variable

Equations

• Core.StructuralEquationModel.instBEqVariable = { beq := fun (a b : Core.StructuralEquationModel.Variable) => decide (a = b) }

instance Core.StructuralEquationModel.instLawfulBEqVariable : LawfulBEq Variable

instance Core.StructuralEquationModel.instToStringVariable : ToString Variable

Equations

• Core.StructuralEquationModel.instToStringVariable = { toString := fun (v : Core.StructuralEquationModel.Variable) => v.name }

def Core.StructuralEquationModel.mkVar (name : String) : Variable

Create a variable from a string literal.

Equations

• Core.StructuralEquationModel.mkVar name = { name := name }

structure Core.StructuralEquationModel.Situation : Type

Situation (Definition 9 from @cite{nadathur-lauer-2020})

A partial valuation: some variables have known values, others are undetermined. Situations are partial functions — crucial for modeling what's "given" vs what's computed, and for counterfactual reasoning (removing a cause = setting it to false).

• valuation : Variable → Option Bool

  The partial valuation: Variable → Option Bool

theorem Core.StructuralEquationModel.Situation.ext_iff {x y : Situation} : x = y ↔ x.valuation = y.valuation

theorem Core.StructuralEquationModel.Situation.ext {x y : Situation} (valuation : x.valuation = y.valuation) : x = y

def Core.StructuralEquationModel.Situation.empty : Situation

The empty situation: nothing is determined.

Equations

• Core.StructuralEquationModel.Situation.empty = { valuation := fun (x : Core.StructuralEquationModel.Variable) => none }

def Core.StructuralEquationModel.Situation.get (s : Situation) (v : Variable) : Option Bool

Get the value of a variable (if determined).

Equations

• s.get v = s.valuation v

def Core.StructuralEquationModel.Situation.hasValue (s : Situation) (v : Variable) (val : Bool) : Bool

Check if a variable has a specific value in the situation.

Equations

• s.hasValue v val = (s.valuation v == some val)

def Core.StructuralEquationModel.Situation.extend (s : Situation) (v : Variable) (val : Bool) : Situation

Extend a situation with a new assignment: s ⊕ {v = val}. If the variable was already determined, the new value overwrites.

Equations

• s.extend v val = { valuation := fun (v' : Core.StructuralEquationModel.Variable) => if (v' == v) = true then some val else s.valuation v' }

def Core.StructuralEquationModel.Situation.remove (s : Situation) (v : Variable) : Situation

Remove a variable from the situation (set to undetermined).

Equations

• s.remove v = { valuation := fun (v' : Core.StructuralEquationModel.Variable) => if (v' == v) = true then none else s.valuation v' }

def Core.StructuralEquationModel.Situation.merge (s1 s2 : Situation) : Situation

Combine two situations (right takes precedence).

Equations

• s1.merge s2 = { valuation := fun (v : Core.StructuralEquationModel.Variable) => s2.valuation v <|> s1.valuation v }

instance Core.StructuralEquationModel.Situation.instInhabited : Inhabited Situation

Equations

• Core.StructuralEquationModel.Situation.instInhabited = { default := Core.StructuralEquationModel.Situation.empty }

def Core.StructuralEquationModel.Situation.allExtensions (s : Situation) : List Variable → List Situation

Enumerate all extensions of a situation over a list of free variables. Each variable can be left undetermined, set true, or set false. Called only on variables NOT already determined in s.

Scalability: produces 3^n situations for n free variables. This is acceptable for the small models in @cite{nadathur-lauer-2020} (typically 2–4 variables) but would need pruning or symbolic reasoning for larger causal networks.

Equations

• One or more equations did not get rendered due to their size.
• s.allExtensions [] = [s]

@[simp]

theorem Core.StructuralEquationModel.Situation.extend_hasValue_same {s : Situation} {v : Variable} {val bval : Bool} : (s.extend v val).hasValue v bval = (val == bval)

Extending at v and querying v returns whether the values match.

@[simp]

theorem Core.StructuralEquationModel.Situation.extend_hasValue_diff {s : Situation} {v w : Variable} {val bval : Bool} (h : w ≠ v) : (s.extend v val).hasValue w bval = s.hasValue w bval

Extending at v doesn't affect queries at a different variable w.

theorem Core.StructuralEquationModel.Situation.extend_eq_self {s : Situation} {v : Variable} {val : Bool} (h : s.hasValue v val = true) : s.extend v val = s

Extending at a value already present is identity.

def Core.StructuralEquationModel.Situation.trueLE (s₁ s₂ : Situation) : Prop

s₁ ⊑ s₂ in the true-content ordering: every variable true in s₁ is also true in s₂. This is the natural preorder for reasoning about monotonicity of positive causal dynamics.

Equations

• s₁.trueLE s₂ = ∀ (v : Core.StructuralEquationModel.Variable), s₁.hasValue v true = true → s₂.hasValue v true = true

theorem Core.StructuralEquationModel.Situation.trueLE_refl (s : Situation) : s.trueLE s

theorem Core.StructuralEquationModel.Situation.trueLE_trans {s₁ s₂ s₃ : Situation} (h₁₂ : s₁.trueLE s₂) (h₂₃ : s₂.trueLE s₃) : s₁.trueLE s₃

structure Core.StructuralEquationModel.CausalLaw : Type

Causal Law (Definition 10 from @cite{nadathur-lauer-2020})

A causal law specifies: if all preconditions hold, the effect follows. In notation: ⟨{(v₁, val₁), …, (vₙ, valₙ)}, (vₑ, valₑ)⟩.

• preconditions : List (Variable × Bool)

  Preconditions that must all hold

• effect : Variable

  The variable affected by this law

• effectValue : Bool

  The value the effect variable gets (default: true)

instance Core.StructuralEquationModel.instReprCausalLaw : Repr CausalLaw

Equations

• Core.StructuralEquationModel.instReprCausalLaw = { reprPrec := Core.StructuralEquationModel.instReprCausalLaw.repr }

def Core.StructuralEquationModel.instReprCausalLaw.repr : CausalLaw → ℕ → Std.Format

Equations

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

instance Core.StructuralEquationModel.instInhabitedCausalLaw : Inhabited CausalLaw

Equations

• Core.StructuralEquationModel.instInhabitedCausalLaw = { default := Core.StructuralEquationModel.instInhabitedCausalLaw.default }

def Core.StructuralEquationModel.instInhabitedCausalLaw.default : CausalLaw

Equations

• Core.StructuralEquationModel.instInhabitedCausalLaw.default = { preconditions := default, effect := default, effectValue := default }

def Core.StructuralEquationModel.CausalLaw.preconditionsMet (law : CausalLaw) (s : Situation) : Bool

Check if all preconditions of a law are satisfied in a situation.

Equations

• law.preconditionsMet s = law.preconditions.all fun (x : Core.StructuralEquationModel.Variable × Bool) => match x with | (v, val) => s.hasValue v val

def Core.StructuralEquationModel.CausalLaw.apply (law : CausalLaw) (s : Situation) : Situation

Apply a law to a situation (if preconditions met, set effect).

Equations

• law.apply s = bif law.preconditionsMet s then s.extend law.effect law.effectValue else s

def Core.StructuralEquationModel.CausalLaw.simple (cause effect : Variable) : CausalLaw

Create a simple law: if cause = true, then effect = true.

Equations

• Core.StructuralEquationModel.CausalLaw.simple cause effect = { preconditions := [(cause, true)], effect := effect }

def Core.StructuralEquationModel.CausalLaw.conjunctive (cause1 cause2 effect : Variable) : CausalLaw

Create a conjunctive law: if cause1 = true ∧ cause2 = true, then effect = true.

Equations

• Core.StructuralEquationModel.CausalLaw.conjunctive cause1 cause2 effect = { preconditions := [(cause1, true), (cause2, true)], effect := effect }

@[simp]

theorem Core.StructuralEquationModel.CausalLaw.apply_of_not_met {law : CausalLaw} {s : Situation} (h : law.preconditionsMet s = false) : law.apply s = s

If preconditions are not met, applying the law is a no-op. Avoids leaving stuck if false = true then … terms in goals.

@[simp]

theorem Core.StructuralEquationModel.CausalLaw.apply_of_met {law : CausalLaw} {s : Situation} (h : law.preconditionsMet s = true) : law.apply s = s.extend law.effect law.effectValue

If preconditions are met, applying the law extends the situation.

@[simp]

theorem Core.StructuralEquationModel.CausalLaw.simple_effect (c e : Variable) : (simple c e).effect = e

The effect variable of a simple law.

@[simp]

theorem Core.StructuralEquationModel.CausalLaw.simple_effectValue (c e : Variable) : (simple c e).effectValue = true

The effect value of a simple law (always true).

structure Core.StructuralEquationModel.CausalDynamics : Type

Causal Dynamics: A collection of causal laws. Represents the structural equations of a causal model. Multiple laws can affect the same variable (disjunctive causation).

• laws : List CausalLaw

  The laws governing causal propagation

instance Core.StructuralEquationModel.instReprCausalDynamics : Repr CausalDynamics

Equations

• Core.StructuralEquationModel.instReprCausalDynamics = { reprPrec := Core.StructuralEquationModel.instReprCausalDynamics.repr }

def Core.StructuralEquationModel.instReprCausalDynamics.repr : CausalDynamics → ℕ → Std.Format

Equations

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

def Core.StructuralEquationModel.instInhabitedCausalDynamics.default : CausalDynamics

Equations

• Core.StructuralEquationModel.instInhabitedCausalDynamics.default = { laws := default }

instance Core.StructuralEquationModel.instInhabitedCausalDynamics : Inhabited CausalDynamics

Equations

• Core.StructuralEquationModel.instInhabitedCausalDynamics = { default := Core.StructuralEquationModel.instInhabitedCausalDynamics.default }

def Core.StructuralEquationModel.CausalDynamics.empty : CausalDynamics

Empty dynamics (no causal laws).

Equations

• Core.StructuralEquationModel.CausalDynamics.empty = { laws := [] }

def Core.StructuralEquationModel.CausalDynamics.ofList (laws : List CausalLaw) : CausalDynamics

Create dynamics from a list of laws.

Equations

• Core.StructuralEquationModel.CausalDynamics.ofList laws = { laws := laws }

def Core.StructuralEquationModel.CausalDynamics.disjunctiveCausation (cause1 cause2 effect : Variable) : CausalDynamics

Disjunctive causation: A ∨ B → C. Either cause alone suffices.

Equations

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

def Core.StructuralEquationModel.CausalDynamics.conjunctiveCausation (cause1 cause2 effect : Variable) : CausalDynamics

Conjunctive causation: A ∧ B → C. Both causes required.

Equations

• Core.StructuralEquationModel.CausalDynamics.conjunctiveCausation cause1 cause2 effect = { laws := [Core.StructuralEquationModel.CausalLaw.conjunctive cause1 cause2 effect] }

def Core.StructuralEquationModel.CausalDynamics.causalChain (a b c : Variable) : CausalDynamics

Causal chain: A → B → C.

Equations

• Core.StructuralEquationModel.CausalDynamics.causalChain a b c = { laws := [Core.StructuralEquationModel.CausalLaw.simple a b, Core.StructuralEquationModel.CausalLaw.simple b c] }

def Core.StructuralEquationModel.isPositiveDynamics (dyn : CausalDynamics) : Bool

A dynamics is positive if all preconditions require true and all effect values are true. Positive dynamics have no inhibitory connections: causes can only enable effects, never block them.

This is the key structural condition for monotonicity results: in positive dynamics, adding true values to a situation can only enable more laws, never block them.

Equations

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

def Core.StructuralEquationModel.applyLawsOnce (dyn : CausalDynamics) (s : Situation) : Situation

Apply all laws once to a situation (one step of forward propagation).

Equations

• Core.StructuralEquationModel.applyLawsOnce dyn s = List.foldl (fun (s' : Core.StructuralEquationModel.Situation) (law : Core.StructuralEquationModel.CausalLaw) => law.apply s') s dyn.laws

def Core.StructuralEquationModel.isFixpoint (dyn : CausalDynamics) (s : Situation) : Bool

Check if a situation is a fixpoint (no law can change it).

Equations

• Core.StructuralEquationModel.isFixpoint dyn s = dyn.laws.all fun (law : Core.StructuralEquationModel.CausalLaw) => !law.preconditionsMet s || s.hasValue law.effect law.effectValue

def Core.StructuralEquationModel.normalDevelopment (dyn : CausalDynamics) (s : Situation) (fuel : ℕ := 100) : Situation

Normal Causal Development (Definition 15)

Iterate forward propagation until fixpoint. Uses bounded iteration (fuel) to ensure termination.

Equations

• One or more equations did not get rendered due to their size.
• Core.StructuralEquationModel.normalDevelopment dyn s 0 = s

@[simp]

theorem Core.StructuralEquationModel.normalDevelopment_succ (dyn : CausalDynamics) (s : Situation) (n : ℕ) : normalDevelopment dyn s (n + 1) = have s' := applyLawsOnce dyn s; bif isFixpoint dyn s' then s' else normalDevelopment dyn s' n

Unfold normalDevelopment one step.

theorem Core.StructuralEquationModel.normalDevelopment_succ_fix {dyn : CausalDynamics} {s : Situation} {n : ℕ} (h : isFixpoint dyn (applyLawsOnce dyn s) = true) : normalDevelopment dyn s (n + 1) = applyLawsOnce dyn s

If the first round reaches a fixpoint, normalDevelopment returns it.

theorem Core.StructuralEquationModel.normalDevelopment_succ_step {dyn : CausalDynamics} {s : Situation} {n : ℕ} (h : isFixpoint dyn (applyLawsOnce dyn s) = false) : normalDevelopment dyn s (n + 1) = normalDevelopment dyn (applyLawsOnce dyn s) n

If the first round is NOT a fixpoint, normalDevelopment recurses.

theorem Core.StructuralEquationModel.normalDevelopment_fixpoint_after_one (dyn : CausalDynamics) (s : Situation) {fuel : ℕ} (h : isFixpoint dyn (applyLawsOnce dyn s) = true) : normalDevelopment dyn s (fuel + 1) = applyLawsOnce dyn s

If the result of one round of law application is a fixpoint, normalDevelopment returns that result.

theorem Core.StructuralEquationModel.normalDevelopment_fixpoint_after_two (dyn : CausalDynamics) (s : Situation) {fuel : ℕ} (h1 : isFixpoint dyn (applyLawsOnce dyn s) = false) (h2 : isFixpoint dyn (applyLawsOnce dyn (applyLawsOnce dyn s)) = true) : normalDevelopment dyn s (fuel + 2) = applyLawsOnce dyn (applyLawsOnce dyn s)

If the first round is not a fixpoint but the second is, normalDevelopment returns the second-round result.

theorem Core.StructuralEquationModel.normalDevelopment_fixpoint_at (dyn : CausalDynamics) (s : Situation) (n : ℕ) {fuel : ℕ} (hnfix : ∀ (k : ℕ), k < n → isFixpoint dyn ((applyLawsOnce dyn)^[k + 1] s) = false) (hfix : isFixpoint dyn ((applyLawsOnce dyn)^[n + 1] s) = true) : normalDevelopment dyn s (fuel + n + 1) = (applyLawsOnce dyn)^[n + 1] s

General fixpoint theorem: if applyLawsOnce reaches a fixpoint after exactly n + 1 rounds, then normalDevelopment with sufficient fuel returns (applyLawsOnce dyn)^[n + 1] s.

_after_one and _after_two are special cases for n = 0 and n = 1.

theorem Core.StructuralEquationModel.CausalLaw.apply_of_fixpoint {law : CausalLaw} {s : Situation} (h : (!law.preconditionsMet s || s.hasValue law.effect law.effectValue) = true) : law.apply s = s

If a law's fixpoint condition holds (preconditions unmet or effect present), applying the law is a no-op.

theorem Core.StructuralEquationModel.applyLawsOnce_of_fixpoint {dyn : CausalDynamics} {s : Situation} (h : isFixpoint dyn s = true) : applyLawsOnce dyn s = s

Applying all laws to a fixpoint situation is a no-op.

theorem Core.StructuralEquationModel.normalDevelopment_of_fixpoint {dyn : CausalDynamics} {s : Situation} (h : isFixpoint dyn s = true) (fuel : ℕ) : normalDevelopment dyn s fuel = s

Normal development from a fixpoint is a no-op regardless of fuel.

theorem Core.StructuralEquationModel.empty_dynamics_fixpoint (s : Situation) : isFixpoint CausalDynamics.empty s = true

Empty dynamics: any situation is a fixpoint.

theorem Core.StructuralEquationModel.empty_dynamics_unchanged (s : Situation) (fuel : ℕ) : normalDevelopment CausalDynamics.empty s fuel = s

Normal development of empty dynamics returns the input unchanged.

theorem Core.StructuralEquationModel.positive_normalDevelopment_grows (dyn : CausalDynamics) (s : Situation) (fuel : ℕ) (hPos : isPositiveDynamics dyn = true) : Core.StructuralEquationModel.trueLE✝ s (normalDevelopment dyn s fuel)

For positive dynamics, normal development is inflationary (extensive): every truth in s is preserved. This is one of the three closure-operator axioms. Used by CausalClosure.lean to build the ClosureOperator instance.

theorem Core.StructuralEquationModel.normalDevelopment_trueLE_positive (dyn : CausalDynamics) (s₁ s₂ : Situation) (fuel : ℕ) (hPos : isPositiveDynamics dyn = true) (hLE : s₁.trueLE s₂) : (normalDevelopment dyn s₁ fuel).trueLE (normalDevelopment dyn s₂ fuel)

For positive dynamics, normalDevelopment is monotone in the trueLE ordering. If s₁ ⊑ s₂ (every true in s₁ is true in s₂), then normalDevelopment(s₁) ⊑ normalDevelopment(s₂).

def Core.StructuralEquationModel.developsToBe (dyn : CausalDynamics) (s : Situation) (v : Variable) (val : Bool) : Bool

Check if a variable develops to a specific value.

Equations

• Core.StructuralEquationModel.developsToBe dyn s v val = (Core.StructuralEquationModel.normalDevelopment dyn s).hasValue v val

def Core.StructuralEquationModel.developsToTrue (dyn : CausalDynamics) (s : Situation) (v : Variable) : Bool

Check if a variable becomes true after normal development.

Equations

• Core.StructuralEquationModel.developsToTrue dyn s v = Core.StructuralEquationModel.developsToBe dyn s v true

def Core.StructuralEquationModel.factuallyDeveloped (dyn : CausalDynamics) (s : Situation) (cause effect : Variable) : Bool

The cause is present and the effect holds after normal development.

Shared primitive for actuallyCaused (Necessity.lean) and complementActualized (Ability.lean).

Equations

• Core.StructuralEquationModel.factuallyDeveloped dyn s cause effect = (s.hasValue cause true && (Core.StructuralEquationModel.normalDevelopment dyn s).hasValue effect true)

theorem Core.StructuralEquationModel.factuallyDeveloped_iff (dyn : CausalDynamics) (s : Situation) (cause effect : Variable) : factuallyDeveloped dyn s cause effect = (s.hasValue cause true && (normalDevelopment dyn s).hasValue effect true)

factuallyDeveloped unfolds to a conjunction of two hasValue checks.

def Core.StructuralEquationModel.hasDirectLaw (dyn : CausalDynamics) (cause effect : Variable) : Bool

Does any causal law directly connect cause to effect?

Equations

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

def Core.StructuralEquationModel.hasIndependentSource (dyn : CausalDynamics) (cause intermediate : Variable) : Bool

Does the intermediate have a causal law not depending on cause?

Equations

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

def Core.StructuralEquationModel.allVariables (dyn : CausalDynamics) : List Variable

All variables mentioned in a dynamics (preconditions and effects).

Equations

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

def Core.StructuralEquationModel.innerVariables (dyn : CausalDynamics) : List Variable

Inner (endogenous) variables: those appearing as effects of laws.

Equations

• Core.StructuralEquationModel.innerVariables dyn = (List.map (fun (x : Core.StructuralEquationModel.CausalLaw) => x.effect) dyn.laws).eraseDups

def Core.StructuralEquationModel.intervene (dyn : CausalDynamics) (s : Situation) (target : Variable) (val : Bool) : CausalDynamics × Situation

Intervene: Pearl's do(X = val).

Sets variable target to val and removes all laws that would determine target, so the intervention overrides the structural equations rather than being overwritten by them.

Equations

• Core.StructuralEquationModel.intervene dyn s target val = ({ laws := List.filter (fun (x : Core.StructuralEquationModel.CausalLaw) => x.effect != target) dyn.laws }, s.extend target val)

def Core.StructuralEquationModel.manipulates (dyn : CausalDynamics) (s : Situation) (cause effect : Variable) : Bool

Manipulates: Does intervening on cause change the value of effect?

Compares normal development under do(cause = true) vs do(cause = false). If the effect's value differs, then cause manipulates effect.

This is the interventionist criterion for causation: X causes Y iff there exists an intervention on X that changes Y.

Equations

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

def Core.StructuralEquationModel.causallySufficient (dyn : CausalDynamics) (s : Situation) (cause effect : Variable) : Bool

Causal Sufficiency (@cite{nadathur-lauer-2020}, Definition 23). C is causally sufficient for E in situation s iff adding C and developing normally produces E.

Equations

• Core.StructuralEquationModel.causallySufficient dyn s cause effect = (Core.StructuralEquationModel.normalDevelopment dyn (s.extend cause true)).hasValue effect true

def Core.StructuralEquationModel.isConsistentSuper (dyn : CausalDynamics) (base s' : Situation) (innerVars : List Variable) : Bool

Is s' a consistent supersituation of base under dynamics dyn? (@cite{nadathur-2024} Definition 9b)

For each inner variable newly determined in s' (not in base), the dynamics from base must not entail the opposite value.

Approximation: this is a per-variable check — it verifies each inner variable independently against the development of base, not the joint development of s'. This is sound (anything inconsistent per-variable is also inconsistent jointly) but conservative: it may admit supersituations that become inconsistent only through variable interactions. For the small models in @cite{nadathur-lauer-2020} this is adequate.

Equations

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

def Core.StructuralEquationModel.causallyNecessary (dyn : CausalDynamics) (s : Situation) (cause effect : Variable) : Bool

Causal Necessity (@cite{nadathur-2024} Definition 10b).

⟨cause, true⟩ is causally necessary for ⟨effect, true⟩ relative to situation s under dynamics dyn iff:

• Precondition: s ⊭_D ⟨cause, true⟩ and s ⊭_D ⟨effect, true⟩
• (i) Achievability: s[cause ↦ true] has a consistent supersituation s' with effect ∉ dom(s') where s' ⊨_D ⟨effect, true⟩
• (ii) But-for: no consistent supersituation s' of s with effect ∉ dom(s') satisfies s' ⊨_D ⟨effect, true⟩ while s' ⊭_D ⟨cause, true⟩

This supersedes the simple but-for test from @cite{nadathur-lauer-2020} Definition 24. The key improvement: the precondition prevents vacuous necessity when cause/effect are already entailed, and achievability ensures the effect is reachable before testing but-for.

Equations

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

structure Core.StructuralEquationModel.CausalProfile : Type

Causal profile: packages the counterfactual properties of a cause-effect pair in a structural model.

• sufficient : Bool
• necessary : Bool
• direct : Bool

def Core.StructuralEquationModel.instDecidableEqCausalProfile.decEq (x✝ x✝¹ : CausalProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Core.StructuralEquationModel.instDecidableEqCausalProfile : DecidableEq CausalProfile

Equations

• Core.StructuralEquationModel.instDecidableEqCausalProfile = Core.StructuralEquationModel.instDecidableEqCausalProfile.decEq

instance Core.StructuralEquationModel.instReprCausalProfile : Repr CausalProfile

Equations

• Core.StructuralEquationModel.instReprCausalProfile = { reprPrec := Core.StructuralEquationModel.instReprCausalProfile.repr }

def Core.StructuralEquationModel.instReprCausalProfile.repr : CausalProfile → ℕ → Std.Format

Equations

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

instance Core.StructuralEquationModel.instBEqCausalProfile : BEq CausalProfile

Equations

• Core.StructuralEquationModel.instBEqCausalProfile = { beq := Core.StructuralEquationModel.instBEqCausalProfile.beq }

def Core.StructuralEquationModel.instBEqCausalProfile.beq : CausalProfile → CausalProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Core.StructuralEquationModel.instBEqCausalProfile.beq x✝¹ x✝ = false

def Core.StructuralEquationModel.extractProfile (dyn : CausalDynamics) (bg : Situation) (cause effect : Variable) : CausalProfile

Extract the causal profile of a cause-effect pair.

Equations

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

theorem Core.StructuralEquationModel.simple_law_necessity (c e : Variable) : causallyNecessary { laws := [CausalLaw.simple c e] } Situation.empty c e = true

For a simple causal law c → e, the cause is necessary for the effect relative to the empty background under @cite{nadathur-2024} Definition 10b.

The argument:

1. Precondition: normalDevelopment(empty) = empty, so neither cause nor effect is entailed
2. Achievability: extending with c=true fires the law → e=true
3. But-for: every consistent supersituation of empty either (a) has c=true, in which case normalDev preserves it (blocking the ¬cause conjunct), or (b) has c≠true, in which case the law doesn't fire and e remains unset (blocking the effect conjunct)