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. Continuous [0,1]. Computed via SEM.probabilisticSuf 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.

@[implicit_reducible]

instance CaoWhiteLassiter2025.instDecidableEqCausalMeasures : DecidableEq CausalMeasures

Equations

• CaoWhiteLassiter2025.instDecidableEqCausalMeasures = CaoWhiteLassiter2025.instDecidableEqCausalMeasures.decEq

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

Equations

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

Deterministic SUF

In the deterministic limit (every mechanism a Dirac), SUF collapses to a {0,1} indicator. probabilisticSuf_of_deterministic is the bridge that recovers this special case from the canonical PMF form.

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

Deterministic SUF as a {0,1} indicator over a BoolSEM with IsDeterministic.

Equations

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

theorem CaoWhiteLassiter2025.probabilisticSuf_eq_deterministicSuf {V : Type u_1} [Fintype V] [DecidableEq V] (M : Core.Causal.BoolSEM V) [M.graph.IsDAG] [Core.Causal.SEM.IsDeterministic M] (bg : Core.Causal.Valuation fun (x : V) => Bool) (c e : V) (hc : bg.get c = none) : Core.Causal.SEM.probabilisticSuf M bg c true e true = deterministicSuf M bg c e

Grounding theorem: under IsDeterministic, the canonical PMF-valued probabilisticSuf collapses to the deterministic {0,1} indicator. Recovers the legacy "shoehorned" SUF as a special case rather than a parallel definition.

ALT → ActionType Bridge

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

def CaoWhiteLassiter2025.altToActionType (alt : ℕ) : Semantics.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 Semantics.Causation.CoerciveImplication.ActionType.Volitional else Semantics.Causation.CoerciveImplication.ActionType.NonVolitional

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

theorem CaoWhiteLassiter2025.alt_positive_volitional (n : ℕ) (h : n > 0) : altToActionType n = Semantics.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 ⋯

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

Equations

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

@[implicit_reducible]

instance CaoWhiteLassiter2025.instReprInteractionTerm : Repr InteractionTerm

Equations

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

structure CaoWhiteLassiter2025.InteractionProfile : Type

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

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

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

Equations

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

@[implicit_reducible]

instance CaoWhiteLassiter2025.instReprInteractionProfile : Repr InteractionProfile

Equations

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

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 probabilisticSuf 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.

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

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.graph : Core.Causal.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) : Core.Causal.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) : Core.Causal.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