The Three Measures

All three are defined within structural causal models. SUF is continuous ∈ [0,1], INT is continuous ∈ [0,1], ALT is ℕ.

structure CaoWhiteLassiter2025.CausalMeasures : Type

The three causal measures that jointly predict causative verb acceptability.

• suf: Probability of sufficiency ([Pea19]). Continuous [0,1]. Computed via probSufficiency over a (possibly probabilistic) SEM V α.
• int: Degree of intention. Continuous [0,1]. How much the causer intended the outcome relative to alternatives.
• alt: Number of alternative actions available to the causee. ℕ. Fewer alternatives → stronger causal influence.

• suf : ℚ
• int : ℚ
• alt : ℕ

@[implicit_reducible]

instance CaoWhiteLassiter2025.instReprCausalMeasures : Repr CausalMeasures

Equations

• CaoWhiteLassiter2025.instReprCausalMeasures = { reprPrec := CaoWhiteLassiter2025.instReprCausalMeasures.repr }

def CaoWhiteLassiter2025.instReprCausalMeasures.repr : CausalMeasures → ℕ → Std.Format

Equations

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

def CaoWhiteLassiter2025.instDecidableEqCausalMeasures.decEq (x✝ x✝¹ : CausalMeasures) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance CaoWhiteLassiter2025.instDecidableEqCausalMeasures : DecidableEq CausalMeasures

Equations

• CaoWhiteLassiter2025.instDecidableEqCausalMeasures = CaoWhiteLassiter2025.instDecidableEqCausalMeasures.decEq

SUF: Pearl's probability of sufficiency

[Pea19]'s probability of sufficiency — the counterfactual probability that intervening to set cause := xC produces effect = xE, against a factual context observed (cause took some other value, effect did not obtain). Built on the substrate's counterfactualSimulate (Pearl 3-step abduction–action–prediction, via the high-stability reduction in cfSeed) and the canonical PMF.probOfSet.

noncomputable def CaoWhiteLassiter2025.probSufficiency {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Causation.DecidableValuation α] (M : Causation.SEM V α) [M.graph.IsDAG] (observed : Causation.Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : ENNReal

Probability of sufficiency ([Pea19]), the SUF measure of [CWL25]: the counterfactual probability that intervening cause := xC yields effect = xE, evaluated against the factual context observed.

Pearl's three-step abduction–action–prediction, expressed via the substrate's counterfactualSimulate (develop of cfSeed): abduction preserves causally-independent observations and regenerates descendants (the high-stability reduction, [Las17b], [LK15]); action sets cause := xC; prediction reads off the probability of effect = xE via PMF.probOfSet.

Distinct from plain interventional probability P(effect | do(cause)): causally-independent parents of effect recorded in observed are preserved rather than re-sampled — the oxygen-vs-match contrast [Pea19] uses to motivate the measure.

Equations

• CaoWhiteLassiter2025.probSufficiency M observed cause xC effect xE = (M.counterfactualSimulate observed cause xC).probOfSet {v : Causation.Valuation α | v.hasValue effect xE}

theorem CaoWhiteLassiter2025.probSufficiency_of_deterministic {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Causation.DecidableValuation α] (M : Causation.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (observed : Causation.Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : probSufficiency M observed cause xC effect xE = if (M.developDet (M.cfSeed observed cause xC)).hasValue effect xE then 1 else 0

Under IsDeterministic, probSufficiency collapses to the {0,1} indicator of whether the counterfactual development hits effect = xE. Follows from counterfactualSimulate_eq_pure_of_deterministic plus PMF.toOuterMeasure_pure_apply.

theorem CaoWhiteLassiter2025.cfSeed_empty {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : Causation.SEM V α) (cause : V) (xC : α cause) : M.cfSeed Causation.Valuation.empty cause xC = Causation.Valuation.empty.extend cause xC

At the empty (vacuous-abduction) context, cfSeed reduces to a plain extend: with nothing observed, abduction preserves nothing and the counterfactual seed merely sets the cause.

Deterministic limit

In the deterministic limit (every mechanism a Dirac), SUF collapses to a {0,1} indicator. At the vacuous (empty) context this is exactly the [NL20] Def-23 sufficiency predicate causallySufficient — with nothing observed, Pearl's counterfactual degenerates to the bare interventional development of cause := true.

noncomputable def CaoWhiteLassiter2025.deterministicSuf {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (background : Causation.Valuation fun (x : V) => Bool) (cause effect : V) : ENNReal

Deterministic SUF as a {0,1} indicator over a BoolSEM: the [NL20] Def-23 sufficiency predicate causallySufficient.

Equations

• CaoWhiteLassiter2025.deterministicSuf M background cause effect = if M.causallySufficient background cause effect then 1 else 0

theorem CaoWhiteLassiter2025.probSufficiency_empty_eq_deterministicSuf {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (c e : V) : probSufficiency M Causation.Valuation.empty c true e true = deterministicSuf M Causation.Valuation.empty c e

Grounding theorem: at the empty context (vacuous abduction), the counterfactual probSufficiency reduces to the deterministic {0,1} indicator deterministicSuf — i.e. to [NL20]'s Def-23 sufficiency. Makes "interventional = counterfactual at a vacuous context" a theorem rather than a conflation.

ALT → ActionType Bridge

Cao et al.'s continuous ALT measure generalizes the binary Volitional/NonVolitional distinction in CoerciveImplication.

def CaoWhiteLassiter2025.altToActionType (alt : ℕ) : Causation.CoerciveImplication.ActionType

Map ALT count to the categorical ActionType from CoerciveImplication.

• ALT = 0: causee had no choice → NonVolitional (forced action)
• ALT > 0: causee could have done otherwise → Volitional

Equations

• CaoWhiteLassiter2025.altToActionType alt = if alt > 0 then Causation.CoerciveImplication.ActionType.Volitional else Causation.CoerciveImplication.ActionType.NonVolitional

theorem CaoWhiteLassiter2025.alt_zero_nonvolitional : altToActionType 0 = Causation.CoerciveImplication.ActionType.NonVolitional

theorem CaoWhiteLassiter2025.alt_positive_volitional (n : ℕ) (h : n > 0) : altToActionType n = Causation.CoerciveImplication.ActionType.Volitional

Interaction Profiles

The core empirical finding: each verb has a unique set of reliable interaction terms among SUF, INT, and ALT.

inductive CaoWhiteLassiter2025.InteractionTerm : Type

Two-way and three-way interaction terms from the regression model.

• sufInt : InteractionTerm
• sufAlt : InteractionTerm
• intAlt : InteractionTerm
• sufIntAlt : InteractionTerm

@[implicit_reducible]

instance CaoWhiteLassiter2025.instDecidableEqInteractionTerm : DecidableEq InteractionTerm

Equations

• CaoWhiteLassiter2025.instDecidableEqInteractionTerm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CaoWhiteLassiter2025.instReprInteractionTerm : Repr InteractionTerm

Equations

• CaoWhiteLassiter2025.instReprInteractionTerm = { reprPrec := CaoWhiteLassiter2025.instReprInteractionTerm.repr }

def CaoWhiteLassiter2025.instReprInteractionTerm.repr : InteractionTerm → ℕ → Std.Format

Equations

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

structure CaoWhiteLassiter2025.InteractionProfile : Type

A verb's interaction profile: which interaction terms reliably predict its acceptability.

• verb : String
• reliablePositive : List InteractionTerm
• reliableNegative : List InteractionTerm

@[implicit_reducible]

instance CaoWhiteLassiter2025.instReprInteractionProfile : Repr InteractionProfile

Equations

• CaoWhiteLassiter2025.instReprInteractionProfile = { reprPrec := CaoWhiteLassiter2025.instReprInteractionProfile.repr }

def CaoWhiteLassiter2025.instReprInteractionProfile.repr : InteractionProfile → ℕ → Std.Format

Equations

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

def CaoWhiteLassiter2025.causeProfile : InteractionProfile

Equations

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

def CaoWhiteLassiter2025.makeProfile : InteractionProfile

Equations

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

def CaoWhiteLassiter2025.forceProfile : InteractionProfile

Equations

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

theorem CaoWhiteLassiter2025.make_has_unique_sufInt : makeProfile.reliablePositive.contains InteractionTerm.sufInt = true ∧ causeProfile.reliablePositive.contains InteractionTerm.sufInt = false ∧ forceProfile.reliablePositive.contains InteractionTerm.sufInt = false ∧ causeProfile.reliableNegative.contains InteractionTerm.sufInt = false ∧ forceProfile.reliableNegative.contains InteractionTerm.sufInt = false

make uniquely has a reliable SUF×INT interaction.

theorem CaoWhiteLassiter2025.shared_interactions : causeProfile.reliablePositive.contains InteractionTerm.sufAlt = true ∧ makeProfile.reliablePositive.contains InteractionTerm.sufAlt = true ∧ forceProfile.reliablePositive.contains InteractionTerm.sufAlt = true ∧ causeProfile.reliablePositive.contains InteractionTerm.intAlt = true ∧ makeProfile.reliablePositive.contains InteractionTerm.intAlt = true ∧ forceProfile.reliablePositive.contains InteractionTerm.intAlt = true

All three verbs share the SUF×ALT and INT×ALT interactions.

theorem CaoWhiteLassiter2025.make_force_both_assert_sufficiency_different_profiles : Features.Causative.make.assertsSufficiency = true ∧ Features.Causative.force.assertsSufficiency = true ∧ makeProfile.reliablePositive ≠ forceProfile.reliablePositive

make and force both assert sufficiency at the enum level but have different interaction profiles.

Main Effects

The regression coefficients for the main effects, showing the direction and relative magnitude of each measure's contribution.

structure CaoWhiteLassiter2025.MainEffects : Type

Main effect coefficients from the Bayesian regression.

-- UNVERIFIED: coefficient values (+1.19, +0.54, -0.82) need verification

• sufResidAlt : ℚ
• int : ℚ
• alt : ℚ

@[implicit_reducible]

instance CaoWhiteLassiter2025.instReprMainEffects : Repr MainEffects

Equations

• CaoWhiteLassiter2025.instReprMainEffects = { reprPrec := CaoWhiteLassiter2025.instReprMainEffects.repr }

def CaoWhiteLassiter2025.instReprMainEffects.repr : MainEffects → ℕ → Std.Format

Equations

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

def CaoWhiteLassiter2025.modelIMainEffects : MainEffects

Equations

• CaoWhiteLassiter2025.modelIMainEffects = { sufResidAlt := 119 / 100, int := 54 / 100, alt := -82 / 100 }

theorem CaoWhiteLassiter2025.suf_largest_main_effect : modelIMainEffects.sufResidAlt > modelIMainEffects.int ∧ modelIMainEffects.sufResidAlt > -modelIMainEffects.alt

theorem CaoWhiteLassiter2025.alt_negative_effect : modelIMainEffects.alt < 0

Probabilistic example: genuinely fractional SUF

A 2-vertex SEM whose effect mechanism is PMF.bernoulli p — genuinely probabilistic, not Dirac. Demonstrates that probSufficiency accepts non-deterministic SEMs (no IsDeterministic constraint).

inductive CaoWhiteLassiter2025.ProbabilisticExample.V : Type

A 2-vertex SEM: cause (root) and effect (one parent: cause).

• cause : V
• effect : V

@[implicit_reducible]

instance CaoWhiteLassiter2025.ProbabilisticExample.instDecidableEqV : DecidableEq V

Equations

• CaoWhiteLassiter2025.ProbabilisticExample.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CaoWhiteLassiter2025.ProbabilisticExample.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance CaoWhiteLassiter2025.ProbabilisticExample.instReprV : Repr V

Equations

• CaoWhiteLassiter2025.ProbabilisticExample.instReprV = { reprPrec := CaoWhiteLassiter2025.ProbabilisticExample.instReprV.repr }

def CaoWhiteLassiter2025.ProbabilisticExample.instReprV.repr : V → ℕ → Std.Format

Equations

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

def CaoWhiteLassiter2025.ProbabilisticExample.graph : Causation.CausalGraph V

Equations

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

noncomputable def CaoWhiteLassiter2025.ProbabilisticExample.effectMech (p : NNReal) (h : p ≤ 1) : Causation.Mechanism graph (fun (x : V) => Bool) V.effect

The probabilistic mechanism for effect: ignores parent value, returns Bernoulli(p) directly. Genuinely non-Dirac when p ∉ {0, 1}.

Equations

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

noncomputable def CaoWhiteLassiter2025.ProbabilisticExample.model (p : NNReal) (h : p ≤ 1) : Causation.BoolSEM V

A genuinely probabilistic SEM (not IsDeterministic for p ∉ {0,1}).

Equations

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

def CaoWhiteLassiter2025.ProbabilisticExample.vDepth : V → ℕ

Depth function for V: cause is a root, effect has depth 1.

Equations

• CaoWhiteLassiter2025.ProbabilisticExample.vDepth CaoWhiteLassiter2025.ProbabilisticExample.V.cause = 0
• CaoWhiteLassiter2025.ProbabilisticExample.vDepth CaoWhiteLassiter2025.ProbabilisticExample.V.effect = 1

instance CaoWhiteLassiter2025.ProbabilisticExample.instIsDAGVGraph : graph.IsDAG

instance CaoWhiteLassiter2025.ProbabilisticExample.instIsDAGVGraphBoolModel (p : NNReal) (h : p ≤ 1) : (model p h).graph.IsDAG