@cite{alstott-aravind-2026}: On aspectual coercion in before- and after-clauses

@cite{alstott-aravind-2026} @cite{rett-2020}

Self-paced reading data from 4 experiments testing @cite{rett-2020}'s prediction that aspectual coercion (INCHOAT, COMPLET) incurs measurable processing cost. Under-specification theories (e.g. @cite{anscombe-1964}) do not predict such costs.

Results Summary

Exp	Coercion type	RT effect	Naturalness	Supports Rett?
1a	INCHOAT (within-modifier)	null	null	No
1b	COMPLET (at-modifier)	sig verb+1	sig lower	Yes
2	COMPLET (before-clause)	sig verb+2†	sig lower	Yes
3	INCHOAT (subj-experiencer)	null	null	No
4	INCHOAT (after-clause)	sig verb+2†	sig lower	Yes

† = exploratory analysis (pre-registered verb/verb+1 regions were null)

Key findings:

• Completive coercion consistently shows processing cost (Exps 1b, 2)
• Inchoative coercion in after-clauses shows delayed cost (Exp 4)
• Inchoative coercion in within-modifier contexts shows no cost (Exps 1a, 3)
• Complement coercion (sanity check) replicates across all experiments
• Delayed spillover (verb+2) in connective contexts vs verb+1 in modifier contexts may reflect pragmatic vs semantic coercion (§5.3, §7.3)

inductive Phenomena.TenseAspect.Studies.AlstottAravind2026.Experiment : Type

Experiment identifiers. Exp 1 has two sub-experiments (a and b).

• exp1a : Experiment
• exp1b : Experiment
• exp2 : Experiment
• exp3 : Experiment
• exp4 : Experiment

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instDecidableEqExperiment : DecidableEq Experiment

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instDecidableEqExperiment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprExperiment.repr : Experiment → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprExperiment : Repr Experiment

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprExperiment = { reprPrec := Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprExperiment.repr }

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqExperiment : BEq Experiment

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqExperiment = { beq := Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqExperiment.beq }

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqExperiment.beq : Experiment → Experiment → Bool

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqExperiment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedExperiment : Inhabited Experiment

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedExperiment = { default := Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedExperiment.default }

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedExperiment.default : Experiment

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedExperiment.default = Phenomena.TenseAspect.Studies.AlstottAravind2026.Experiment.exp1a

inductive Phenomena.TenseAspect.Studies.AlstottAravind2026.CoercionType : Type

Types of aspectual coercion tested across experiments.

• inchoative : CoercionType
• completive : CoercionType
• complement : CoercionType

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instDecidableEqCoercionType : DecidableEq CoercionType

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instDecidableEqCoercionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprCoercionType : Repr CoercionType

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprCoercionType = { reprPrec := Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprCoercionType.repr }

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprCoercionType.repr : CoercionType → ℕ → Std.Format

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqCoercionType.beq : CoercionType → CoercionType → Bool

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqCoercionType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqCoercionType : BEq CoercionType

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqCoercionType = { beq := Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqCoercionType.beq }

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedCoercionType.default : CoercionType

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedCoercionType.default = Phenomena.TenseAspect.Studies.AlstottAravind2026.CoercionType.inchoative

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedCoercionType : Inhabited CoercionType

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedCoercionType = { default := Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedCoercionType.default }

inductive Phenomena.TenseAspect.Studies.AlstottAravind2026.SpilloverRegion : Type

Spillover region where an effect was measured.

• verb : SpilloverRegion
• verbPlus1 : SpilloverRegion
• verbPlus2 : SpilloverRegion

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instDecidableEqSpilloverRegion : DecidableEq SpilloverRegion

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instDecidableEqSpilloverRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprSpilloverRegion : Repr SpilloverRegion

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprSpilloverRegion = { reprPrec := Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprSpilloverRegion.repr }

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprSpilloverRegion.repr : SpilloverRegion → ℕ → Std.Format

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqSpilloverRegion.beq : SpilloverRegion → SpilloverRegion → Bool

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqSpilloverRegion.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqSpilloverRegion : BEq SpilloverRegion

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqSpilloverRegion = { beq := Phenomena.TenseAspect.Studies.AlstottAravind2026.instBEqSpilloverRegion.beq }

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedSpilloverRegion.default : SpilloverRegion

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedSpilloverRegion.default = Phenomena.TenseAspect.Studies.AlstottAravind2026.SpilloverRegion.verb

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedSpilloverRegion : Inhabited SpilloverRegion

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedSpilloverRegion = { default := Phenomena.TenseAspect.Studies.AlstottAravind2026.instInhabitedSpilloverRegion.default }

structure Phenomena.TenseAspect.Studies.AlstottAravind2026.ExperimentResult : Type

Result from a self-paced reading experiment.

• experiment : Experiment
• condition : String
• coercionType : CoercionType
• effectBeta : ℚ

  Mixed-effects regression coefficient (log RT)

• se : ℚ

  Standard error of the coefficient

• pValue : ℚ

  p-value

• region : SpilloverRegion

  Spillover region where effect was measured

• significant : Bool

  Whether the effect reached significance (Bonferroni-corrected α = 0.025)

• exploratory : Bool

  Whether the analysis was exploratory (not pre-registered)

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprExperimentResult.repr : ExperimentResult → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprExperimentResult : Repr ExperimentResult

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprExperimentResult = { reprPrec := Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprExperimentResult.repr }

structure Phenomena.TenseAspect.Studies.AlstottAravind2026.NaturalnessResult : Type

Naturalness rating result (ordinal logistic regression).

• experiment : Experiment
• coercionType : CoercionType
• ratingBeta : ℚ

  Regression coefficient for coercion vs control

• se : ℚ

  Standard error of the coefficient

• pValue : ℚ

  p-value

• significant : Bool

  Significant difference?

instance Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprNaturalnessResult : Repr NaturalnessResult

Equations

• Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprNaturalnessResult = { reprPrec := Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprNaturalnessResult.repr }

def Phenomena.TenseAspect.Studies.AlstottAravind2026.instReprNaturalnessResult.repr : NaturalnessResult → ℕ → Std.Format

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp1a_rt : ExperimentResult

Exp 1a: INCHOAT with within-modifier + be-stative verb. E.g. "Within fifteen minutes Jessica was mad in office hours." No significant RT slowdown; no naturalness difference.

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp1a_naturalness : NaturalnessResult

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp1b_rt : ExperimentResult

Exp 1b: COMPLET with at-modifier + accomplishment verb. E.g. "At 9pm sharp Hector built the humble tent." Significant slowdown at verb+1; lower naturalness. Supports Rett's COMPLET operator.

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp1b_naturalness : NaturalnessResult

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp2_rt : ExperimentResult

Exp 2: COMPLET in before-clause with accomplishment EE. E.g. "Emma was irritable before Hector built the tent in the woods." Pre-registered regions (verb, verb+1) showed null effects. Exploratory verb+2 analysis found significant slowdown; lower naturalness. Delayed effect consistent with pragmatic (vs semantic) coercion.

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp2_naturalness : NaturalnessResult

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp3_rt : ExperimentResult

Exp 3: INCHOAT with subject-experiencer verbs in within-modifier context. E.g. "Within fifteen minutes Jessica tolerated the unhelpful professor." No significant RT effect; no naturalness difference.

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp3_naturalness : NaturalnessResult

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp4_rt : ExperimentResult

Exp 4: INCHOAT in after-clause with subject-experiencer EE. E.g. "Dave was regretful after Lara feared the large dog." Pre-registered regions (verb, verb+1) showed null effects. Exploratory verb+2 analysis found significant slowdown; lower naturalness. INCHOAT cost detected in after-clauses but not within-modifier contexts.

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.exp4_naturalness : NaturalnessResult

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.complement_coercion_exp1a : ExperimentResult

Complement coercion (e.g., "continued his article") in Exp 1a at noun+1. This replicates across all experiments, confirming paradigm sensitivity.

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.complement_coercion_exp1b : ExperimentResult

Complement coercion in Exp 1b at noun+1.

Equations

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

def Phenomena.TenseAspect.Studies.AlstottAravind2026.complement_coercion_exp3 : ExperimentResult

Complement coercion in Exp 3 at noun+1.

Equations

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

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.rett_predicts_completive_cost : exp1b_rt.significant = true ∧ exp2_rt.significant = true

Rett's theory correctly predicts completive coercion costs where they occur. Both Exps 1b (at-modifier) and 2 (before-clause) show significant slowdowns.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.rett_predicts_inchoative_in_after : exp4_rt.significant = true ∧ exp4_rt.coercionType = CoercionType.inchoative

Rett's theory correctly predicts inchoative coercion cost in after-clauses. Exp 4 shows significant slowdown for after-start readings.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.within_modifier_not_replicated : exp1a_rt.significant = false ∧ exp3_rt.significant = false

Within-modifier INCHOAT shows no cost: Exps 1a and 3 show null results. This dissociation (null in within-modifier, significant in after-clause) suggests INCHOAT cost is construction-specific, not universal. The paper's §8.2 proposes a non-coercive, Krifka-style scalar implicature analysis for atelic within-modifier sentences.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.complement_coercion_replicates : complement_coercion_exp1a.significant = true ∧ complement_coercion_exp1b.significant = true ∧ complement_coercion_exp3.significant = true

Complement coercion sanity check passes in both sub-experiments.

def Phenomena.TenseAspect.Studies.AlstottAravind2026.processingMeasure : Core.Empirical.MeasureSpec

Processing measure: all experiments use self-paced reading.

Equations

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

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.connective_vs_modifier_spillover : exp2_rt.region = SpilloverRegion.verbPlus2 ∧ exp2_rt.exploratory = true ∧ exp4_rt.region = SpilloverRegion.verbPlus2 ∧ exp4_rt.exploratory = true ∧ exp1b_rt.region = SpilloverRegion.verbPlus1 ∧ exp1b_rt.exploratory = false

Delayed effect in connective contexts: cost at verb+2 (not verb+1). Both connective experiments (2, 4) show verb+2 spillover, while the modifier experiment (1b) shows verb+1. Consistent with pragmatic coercion in connectives being slower to detect than semantic coercion in modifier contexts. Both connective results are exploratory.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.exp2_tests_before_coercion : exp2_rt.coercionType = CoercionType.completive ∧ Fragments.English.TemporalExpressions.before_.coercedReading = some Fragments.English.TemporalExpressions.Reading.beforeFinish

Exp 2 tests the Fragment's coercedReading for before: COMPLET triggers the before-finish reading.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.exp4_tests_after_coercion : exp4_rt.coercionType = CoercionType.inchoative ∧ Fragments.English.TemporalExpressions.after_.coercedReading = some Fragments.English.TemporalExpressions.Reading.afterStart

Exp 4 tests the Fragment's coercedReading for after: INCHOAT triggers the after-start reading.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.exp1b_tests_at_modifier_coercion : exp1b_rt.coercionType = CoercionType.completive ∧ Fragments.English.TemporalExpressions.at_punct.triggeredCoercion = some "COMPLET"

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.exp1a_tests_within_modifier_coercion : exp1a_rt.coercionType = CoercionType.inchoative ∧ Fragments.English.TemporalExpressions.within_.triggeredCoercion = some "INCHOAT"

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.complet_consistently_costly : exp1b_rt.significant = true ∧ exp2_rt.significant = true ∧ exp1b_rt.coercionType = CoercionType.completive ∧ exp2_rt.coercionType = CoercionType.completive

COMPLET is consistently costly across both completive experiments.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.inchoat_construction_specific : exp4_rt.significant = true ∧ exp1a_rt.significant = false ∧ exp3_rt.significant = false ∧ exp4_rt.coercionType = CoercionType.inchoative ∧ exp1a_rt.coercionType = CoercionType.inchoative ∧ exp3_rt.coercionType = CoercionType.inchoative

INCHOAT cost is construction-specific: present in after-clauses (Exp 4), absent in within-modifier contexts (Exps 1a, 3).

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.complet_effect_exceeds_inchoat : exp1b_rt.effectBeta > exp1a_rt.effectBeta

Completive effect size exceeds inchoative in modifier contexts.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.rt_naturalness_converge : exp1b_rt.significant = exp1b_naturalness.significant ∧ exp2_rt.significant = exp2_naturalness.significant ∧ exp4_rt.significant = exp4_naturalness.significant ∧ exp1a_rt.significant = exp1a_naturalness.significant ∧ exp3_rt.significant = exp3_naturalness.significant

RT significance and naturalness significance converge in all 5 experiments: every experiment that shows an RT effect also shows a naturalness effect, and every null RT result has a null naturalness result.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.tagalog_overt_coercion : Fragments.Tagalog.TemporalConnectives.bago_aia.culminating = true ∧ Fragments.Tagalog.TemporalConnectives.bago_aia.reading = Fragments.English.TemporalExpressions.Reading.beforeFinish ∧ Fragments.Tagalog.TemporalConnectives.bago_neut.culminating = false ∧ Fragments.Tagalog.TemporalConnectives.bago_neut.reading = Fragments.English.TemporalExpressions.Reading.beforeStart

Tagalog overtly marks what English coerces covertly: PFV.AIA (ability/involuntary action) → before-finish (COMPLET); PFV.NEUT (neutral) → before-start (no coercion).

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.serbian_overt_coercion : Fragments.Serbian.TemporalConnectives.pre_pfv.culminating = true ∧ Fragments.Serbian.TemporalConnectives.pre_pfv.reading = Fragments.English.TemporalExpressions.Reading.beforeFinish ∧ Fragments.Serbian.TemporalConnectives.pre_impf.culminating = false ∧ Fragments.Serbian.TemporalConnectives.pre_impf.reading = Fragments.English.TemporalExpressions.Reading.beforeStart

Serbian overtly marks what English coerces covertly: perfective → before-finish (COMPLET); imperfective → before-start (no coercion).

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.complet_triple_convergence : exp2_rt.significant = true ∧ exp2_rt.coercionType = CoercionType.completive ∧ Fragments.Tagalog.TemporalConnectives.bago_aia.culminating = true ∧ Fragments.Serbian.TemporalConnectives.pre_pfv.culminating = true

Triple convergence: English processing data (Exp 2), Tagalog morphology, and Serbian morphology all independently support covert COMPLET.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.rett_uniquely_predicts_processing_cost : TemporalConnectives.Compare.rettProfile.predictsProcessingCost = true ∧ TemporalConnectives.Compare.anscombeProfile.predictsProcessingCost = false ∧ TemporalConnectives.Compare.ostProfile.predictsProcessingCost = false ∧ TemporalConnectives.Compare.bcProfile.predictsProcessingCost = false

The paper's central finding: Rett's ambiguity theory predicts processing asymmetries between readings, and this prediction is confirmed by the data. Under-specification theories (Anscombe, B&C, O&ST) do not predict such costs.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.data_supports_rett : TemporalConnectives.Compare.rettProfile.positsCoercion = true ∧ exp1b_rt.significant = true ∧ exp2_rt.significant = true ∧ exp4_rt.significant = true

The data confirms the prediction: significant processing costs exist for coerced readings (Exps 1b, 2, 4). The only theory that predicts this is Rett's, which posits covert coercion operators.

theorem Phenomena.TenseAspect.Studies.AlstottAravind2026.coercion_has_crosslinguistic_reflexes : TemporalConnectives.Compare.rettProfile.positsCoercion = true ∧ Fragments.Tagalog.TemporalConnectives.bago_aia.culminating = true ∧ Fragments.Serbian.TemporalConnectives.pre_pfv.culminating = true

Rett's coercion operators have overt cross-linguistic reflexes: the theory posits coercion, and languages like Tagalog and Serbian realize it morphologically.