Overall Acceptance Rates (Figure 4)

Proportion of "Yes" (Accurate) responses by verb. Ordering: caused > made > forced.

Rates stored as percentages (Nat) to avoid heavy Mathlib imports.

structure Phenomena.Causatives.AcceptanceRate : Type

An experimental observation: verb form paired with acceptance rate (%).

• verb : String
• ratePct : Nat

instance Phenomena.Causatives.instReprAcceptanceRate : Repr AcceptanceRate

Equations

• Phenomena.Causatives.instReprAcceptanceRate = { reprPrec := Phenomena.Causatives.instReprAcceptanceRate.repr }

def Phenomena.Causatives.instReprAcceptanceRate.repr : AcceptanceRate → Nat → Std.Format

Equations

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

def Phenomena.Causatives.instDecidableEqAcceptanceRate.decEq (x✝ x✝¹ : AcceptanceRate) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Causatives.instDecidableEqAcceptanceRate : DecidableEq AcceptanceRate

Equations

• Phenomena.Causatives.instDecidableEqAcceptanceRate = Phenomena.Causatives.instDecidableEqAcceptanceRate.decEq

def Phenomena.Causatives.instBEqAcceptanceRate.beq : AcceptanceRate → AcceptanceRate → Bool

Equations

• Phenomena.Causatives.instBEqAcceptanceRate.beq { verb := a, ratePct := a_1 } { verb := b, ratePct := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Causatives.instBEqAcceptanceRate.beq x✝¹ x✝ = false

instance Phenomena.Causatives.instBEqAcceptanceRate : BEq AcceptanceRate

Equations

• Phenomena.Causatives.instBEqAcceptanceRate = { beq := Phenomena.Causatives.instBEqAcceptanceRate.beq }

def Phenomena.Causatives.causedRate : AcceptanceRate

Equations

• Phenomena.Causatives.causedRate = { verb := "caused", ratePct := 48 }

def Phenomena.Causatives.madeRate : AcceptanceRate

Equations

• Phenomena.Causatives.madeRate = { verb := "made", ratePct := 40 }

def Phenomena.Causatives.forcedRate : AcceptanceRate

Equations

• Phenomena.Causatives.forcedRate = { verb := "forced", ratePct := 35 }

theorem Phenomena.Causatives.acceptance_ordering : causedRate.ratePct > madeRate.ratePct ∧ madeRate.ratePct > forcedRate.ratePct

Acceptance ordering: caused > made > forced (Figure 4).

Main Effect Coefficients (Model I, Table 2)

Bayesian logistic regression with verb × SUFresidALT × INT × ALT.

Coefficients stored as (numerator, denominator=100) to avoid ℚ imports.

structure Phenomena.Causatives.Coefficient : Type

A regression coefficient with its 95% credible interval. Values are × 100 (e.g., 119 means 1.19).

• name : String
• estimate100 : Int
• lowerCI100 : Int
• upperCI100 : Int

instance Phenomena.Causatives.instReprCoefficient : Repr Coefficient

Equations

• Phenomena.Causatives.instReprCoefficient = { reprPrec := Phenomena.Causatives.instReprCoefficient.repr }

def Phenomena.Causatives.instReprCoefficient.repr : Coefficient → Nat → Std.Format

Equations

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

instance Phenomena.Causatives.instDecidableEqCoefficient : DecidableEq Coefficient

Equations

• Phenomena.Causatives.instDecidableEqCoefficient = Phenomena.Causatives.instDecidableEqCoefficient.decEq

def Phenomena.Causatives.instDecidableEqCoefficient.decEq (x✝ x✝¹ : Coefficient) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Causatives.instBEqCoefficient : BEq Coefficient

Equations

• Phenomena.Causatives.instBEqCoefficient = { beq := Phenomena.Causatives.instBEqCoefficient.beq }

def Phenomena.Causatives.instBEqCoefficient.beq : Coefficient → Coefficient → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Causatives.instBEqCoefficient.beq x✝¹ x✝ = false

def Phenomena.Causatives.Coefficient.isReliable (c : Coefficient) : Bool

A coefficient is reliable when its 95% CI excludes 0.

Equations

• c.isReliable = (decide (c.lowerCI100 > 0) && decide (c.upperCI100 > 0) || decide (c.lowerCI100 < 0) && decide (c.upperCI100 < 0))

def Phenomena.Causatives.coeff_sufResidAlt : Coefficient

Equations

• Phenomena.Causatives.coeff_sufResidAlt = { name := "SUFresidALT", estimate100 := 119, lowerCI100 := 89, upperCI100 := 150 }

def Phenomena.Causatives.coeff_int : Coefficient

Equations

• Phenomena.Causatives.coeff_int = { name := "INT", estimate100 := 54, lowerCI100 := 28, upperCI100 := 81 }

def Phenomena.Causatives.coeff_alt : Coefficient

Equations

• Phenomena.Causatives.coeff_alt = { name := "ALT", estimate100 := -82, lowerCI100 := -111, upperCI100 := -55 }

theorem Phenomena.Causatives.suf_reliable : coeff_sufResidAlt.isReliable = true

theorem Phenomena.Causatives.int_reliable : coeff_int.isReliable = true

theorem Phenomena.Causatives.alt_reliable : coeff_alt.isReliable = true

theorem Phenomena.Causatives.suf_largest_main_effect : coeff_sufResidAlt.estimate100 > coeff_int.estimate100 ∧ coeff_sufResidAlt.estimate100 > -coeff_alt.estimate100

SUF has the largest absolute main effect.

theorem Phenomena.Causatives.alt_negative : coeff_alt.estimate100 < 0

ALT has a negative main effect (more alternatives → less acceptable).

Per-Verb Interaction Reliability (Table 1)

Estimates of interaction intercepts by verb. Light grey = unreliable.

structure Phenomena.Causatives.VerbInteraction : Type

Per-verb reliable interaction from Table 1. positive = reliable positive effect.

• verb : String
• interaction : String
• positive : Bool

def Phenomena.Causatives.instReprVerbInteraction.repr : VerbInteraction → Nat → Std.Format

Equations

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

instance Phenomena.Causatives.instReprVerbInteraction : Repr VerbInteraction

Equations

• Phenomena.Causatives.instReprVerbInteraction = { reprPrec := Phenomena.Causatives.instReprVerbInteraction.repr }

def Phenomena.Causatives.made_sufInt : VerbInteraction

made uniquely has a reliable SUFresidALT×INT interaction (Table 1).

Equations

• Phenomena.Causatives.made_sufInt = { verb := "made", interaction := "SUFresidALT:INT", positive := true }

def Phenomena.Causatives.caused_sufAlt : VerbInteraction

All verbs share reliable SUFresidALT×ALT interaction.

Equations

• Phenomena.Causatives.caused_sufAlt = { verb := "caused", interaction := "SUFresidALT:ALT", positive := true }

def Phenomena.Causatives.made_sufAlt : VerbInteraction

Equations

• Phenomena.Causatives.made_sufAlt = { verb := "made", interaction := "SUFresidALT:ALT", positive := true }

def Phenomena.Causatives.forced_sufAlt : VerbInteraction

Equations

• Phenomena.Causatives.forced_sufAlt = { verb := "forced", interaction := "SUFresidALT:ALT", positive := true }

def Phenomena.Causatives.caused_intAlt : VerbInteraction

All verbs share reliable INT×ALT interaction.

Equations

• Phenomena.Causatives.caused_intAlt = { verb := "caused", interaction := "INT:ALT", positive := true }

def Phenomena.Causatives.made_intAlt : VerbInteraction

Equations

• Phenomena.Causatives.made_intAlt = { verb := "made", interaction := "INT:ALT", positive := true }

def Phenomena.Causatives.forced_intAlt : VerbInteraction

Equations

• Phenomena.Causatives.forced_intAlt = { verb := "forced", interaction := "INT:ALT", positive := true }

Acceptability Contrasts (examples 3-7)

From the paper's examples showing non-interchangeability.

inductive Phenomena.Causatives.Acceptability : Type

Acceptability judgment for a causative verb in context.

• acceptable : Acceptability
• marginal : Acceptability
• unacceptable : Acceptability

instance Phenomena.Causatives.instDecidableEqAcceptability : DecidableEq Acceptability

Equations

• Phenomena.Causatives.instDecidableEqAcceptability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Causatives.instReprAcceptability.repr : Acceptability → Nat → Std.Format

Equations

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

instance Phenomena.Causatives.instReprAcceptability : Repr Acceptability

Equations

• Phenomena.Causatives.instReprAcceptability = { reprPrec := Phenomena.Causatives.instReprAcceptability.repr }

def Phenomena.Causatives.instBEqAcceptability.beq : Acceptability → Acceptability → Bool

Equations

• Phenomena.Causatives.instBEqAcceptability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Causatives.instBEqAcceptability : BEq Acceptability

Equations

• Phenomena.Causatives.instBEqAcceptability = { beq := Phenomena.Causatives.instBEqAcceptability.beq }

structure Phenomena.Causatives.CausativeJudgment : Type

A single acceptability judgment: verb + context + status.

• verb : String
• context : String
• judgment : Acceptability
• source : String

instance Phenomena.Causatives.instReprCausativeJudgment : Repr CausativeJudgment

Equations

• Phenomena.Causatives.instReprCausativeJudgment = { reprPrec := Phenomena.Causatives.instReprCausativeJudgment.repr }

def Phenomena.Causatives.instReprCausativeJudgment.repr : CausativeJudgment → Nat → Std.Format

Equations

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

def Phenomena.Causatives.ex5a : CausativeJudgment

Example (5): mentioning a habit (low sufficiency, low intention).

Equations

• Phenomena.Causatives.ex5a = { verb := "caused", context := "go to gym by mentioning how habit helped", judgment := Phenomena.Causatives.Acceptability.acceptable, source := "ex. 5a" }

def Phenomena.Causatives.ex5b : CausativeJudgment

Equations

• Phenomena.Causatives.ex5b = { verb := "made", context := "go to gym by mentioning how habit helped", judgment := Phenomena.Causatives.Acceptability.unacceptable, source := "ex. 5b" }

def Phenomena.Causatives.ex5c : CausativeJudgment

Equations

• Phenomena.Causatives.ex5c = { verb := "forced", context := "go to gym by mentioning how habit helped", judgment := Phenomena.Causatives.Acceptability.unacceptable, source := "ex. 5c" }

def Phenomena.Causatives.ex7a : CausativeJudgment

Example (7): holding child hostage (high sufficiency, high intention, low alternatives).

Equations

• Phenomena.Causatives.ex7a = { verb := "caused", context := "go to gym by holding child hostage", judgment := Phenomena.Causatives.Acceptability.acceptable, source := "ex. 7a" }

def Phenomena.Causatives.ex7b : CausativeJudgment

Equations

• Phenomena.Causatives.ex7b = { verb := "made", context := "go to gym by holding child hostage", judgment := Phenomena.Causatives.Acceptability.acceptable, source := "ex. 7b" }

def Phenomena.Causatives.ex7c : CausativeJudgment

Equations

• Phenomena.Causatives.ex7c = { verb := "forced", context := "go to gym by holding child hostage", judgment := Phenomena.Causatives.Acceptability.acceptable, source := "ex. 7c" }

theorem Phenomena.Causatives.all_acceptable_high_suf_int_low_alt : ex7a.judgment = Acceptability.acceptable ∧ ex7b.judgment = Acceptability.acceptable ∧ ex7c.judgment = Acceptability.acceptable

In high-SUF, high-INT, low-ALT contexts, all three verbs are acceptable.

theorem Phenomena.Causatives.only_cause_low_suf : ex5a.judgment = Acceptability.acceptable ∧ ex5b.judgment = Acceptability.unacceptable ∧ ex5c.judgment = Acceptability.unacceptable

In low-SUF contexts, only cause is acceptable.