Resultatives as Concealed Causatives

@cite{baglini-bar-asher-siegal-2025} @cite{goldberg-jackendoff-2004} @cite{levin-2019} @cite{martin-rose-nichols-2025} @cite{nadathur-lauer-2020}

Connects the resultative construction to the causative semantics infrastructure:

1. Causal Dynamics: causative resultatives modeled as concrete CausalDynamics with structural sufficiency proofs and CC-selection constraints (Baglini & Bar-Asher @cite{baglini-bar-asher-siegal-2025})
2. Tightness via Causal Necessity: @cite{levin-2019} concealed causative constraint — intervening causers with independent energy sources disrupt necessity under counterfactual intervention, formalized through completesForEffect (not graph-structural checks)
3. Thick/Thin Convergence: three independent paths (@cite{martin-rose-nichols-2025}, @cite{goldberg-jackendoff-2004}, @cite{embick-2009}) converge on .make/makeSem
4. Aspect: resultative telicizes activity verbs via bounded RP
5. ChangeOfState: constructional BECOME maps to CoSType.inception
6. Müller decomposability: all subconstructions decompose into universal schemata

Causal Dynamics (@cite{nadathur-lauer-2020}; Baglini & Bar-Asher @cite{baglini-bar-asher-siegal-2025})

The constructional CAUSE in causative resultatives maps to @cite{nadathur-lauer-2020} causal sufficiency: the verbal subevent is sufficient for the constructional result. We build concrete CausalDynamics and prove structural sufficiency/necessity results.

CC-selection (Baglini & Bar-Asher @cite{baglini-bar-asher-siegal-2025})

The resultative construction performs CC-selection: it constrains which condition from a causal model can fill the cause role. Causative resultatives select via completion of a sufficient set: the verbal subevent must be the final condition that makes the result inevitable. Combined with the temporal constraint (G&J Principle 33), this gives the BBS2025 completion event analysis.

Causal models for causative resultatives

Each causative resultative maps to a concrete CausalDynamics where the verbal subevent variable causally determines the result variable.

def Causative.Resultatives.hammeringVar : Core.StructuralEquationModel.Variable

Equations

• Causative.Resultatives.hammeringVar = Core.StructuralEquationModel.mkVar "hammering"

def Causative.Resultatives.flatVar : Core.StructuralEquationModel.Variable

Equations

• Causative.Resultatives.flatVar = Core.StructuralEquationModel.mkVar "flat"

def Causative.Resultatives.hammerFlatModel : Core.StructuralEquationModel.CausalDynamics

"She hammered the metal flat": hammering → flat.

Equations

• Causative.Resultatives.hammerFlatModel = { laws := [Core.StructuralEquationModel.CausalLaw.simple Causative.Resultatives.hammeringVar Causative.Resultatives.flatVar] }

def Causative.Resultatives.kickingVar : Core.StructuralEquationModel.Variable

Equations

• Causative.Resultatives.kickingVar = Core.StructuralEquationModel.mkVar "kicking"

def Causative.Resultatives.inFieldVar : Core.StructuralEquationModel.Variable

Equations

• Causative.Resultatives.inFieldVar = Core.StructuralEquationModel.mkVar "in_field"

def Causative.Resultatives.kickIntoFieldModel : Core.StructuralEquationModel.CausalDynamics

"She kicked the ball into the field": kicking → in_field.

Equations

• Causative.Resultatives.kickIntoFieldModel = { laws := [Core.StructuralEquationModel.CausalLaw.simple Causative.Resultatives.kickingVar Causative.Resultatives.inFieldVar] }

def Causative.Resultatives.laughingVar : Core.StructuralEquationModel.Variable

Equations

• Causative.Resultatives.laughingVar = Core.StructuralEquationModel.mkVar "laughing"

def Causative.Resultatives.sillyVar : Core.StructuralEquationModel.Variable

Equations

• Causative.Resultatives.sillyVar = Core.StructuralEquationModel.mkVar "silly"

def Causative.Resultatives.laughSillyModel : Core.StructuralEquationModel.CausalDynamics

"She laughed herself silly" (fake reflexive): laughing → silly.

Equations

• Causative.Resultatives.laughSillyModel = { laws := [Core.StructuralEquationModel.CausalLaw.simple Causative.Resultatives.laughingVar Causative.Resultatives.sillyVar] }

Sufficiency proofs (@cite{nadathur-lauer-2020} Def 23)

theorem Causative.Resultatives.hammer_sufficient_for_flat : Core.StructuralEquationModel.causallySufficient hammerFlatModel Core.StructuralEquationModel.Situation.empty hammeringVar flatVar = true

Hammering is causally sufficient for flatness.

theorem Causative.Resultatives.kick_sufficient_for_field : Core.StructuralEquationModel.causallySufficient kickIntoFieldModel Core.StructuralEquationModel.Situation.empty kickingVar inFieldVar = true

Kicking is causally sufficient for being in the field.

theorem Causative.Resultatives.laugh_sufficient_for_silly : Core.StructuralEquationModel.causallySufficient laughSillyModel Core.StructuralEquationModel.Situation.empty laughingVar sillyVar = true

Laughing is causally sufficient for becoming silly (fake reflexive).

Necessity proofs

Single-pathway resultatives: verbal subevent is both sufficient and necessary.

theorem Causative.Resultatives.hammer_necessary_for_flat : Core.StructuralEquationModel.causallyNecessary hammerFlatModel Core.StructuralEquationModel.Situation.empty hammeringVar flatVar = true

Hammering is causally necessary for flatness. Under @cite{nadathur-2024} Def 10b, the background must NOT include the cause (precondition rejects it).

theorem Causative.Resultatives.hammer_flat_make_and_cause : NadathurLauer2020.makeSem hammerFlatModel Core.StructuralEquationModel.Situation.empty hammeringVar flatVar = true ∧ NadathurLauer2020.causeSem hammerFlatModel Core.StructuralEquationModel.Situation.empty hammeringVar flatVar = true

Both makeSem and causeSem hold for "hammer flat" (no overdetermination).

Noncausative resultatives = empty dynamics

"The river froze solid": RESULT relation, no CAUSE.

def Causative.Resultatives.freezingVar : Core.StructuralEquationModel.Variable

Equations

• Causative.Resultatives.freezingVar = Core.StructuralEquationModel.mkVar "freezing"

def Causative.Resultatives.solidVar : Core.StructuralEquationModel.Variable

Equations

• Causative.Resultatives.solidVar = Core.StructuralEquationModel.mkVar "solid"

def Causative.Resultatives.freezeSolidModel : Core.StructuralEquationModel.CausalDynamics

Noncausative resultatives have empty causal dynamics.

Equations

• Causative.Resultatives.freezeSolidModel = Core.StructuralEquationModel.CausalDynamics.empty

theorem Causative.Resultatives.freeze_not_sufficient : Core.StructuralEquationModel.causallySufficient freezeSolidModel Core.StructuralEquationModel.Situation.empty freezingVar solidVar = false

In the empty model, freezing is NOT sufficient for solidity.

theorem Causative.Resultatives.causative_dynamics_noncausative_empty : hammerFlatModel.laws.length > 0 ∧ kickIntoFieldModel.laws.length > 0 ∧ laughSillyModel.laws.length > 0 ∧ freezeSolidModel.laws.length = 0

Causative → non-empty dynamics; noncausative → empty.

Agreement with Boolean flags

theorem Causative.Resultatives.causative_iff_has_cause (e : ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeEntry) : e.subconstruction.isCausative = e.subevents.constructional.hasCause → (e.subconstruction.isCausative = true ↔ e.subevents.constructional.hasCause = true)

Causative entries have CAUSE; noncausative entries do not.

theorem Causative.Resultatives.causativeResultativeHasCAUSE : ((List.filter (fun (x : ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeEntry) => x.subconstruction.isCausative) ConstructionGrammar.Studies.GoldbergJackendoff2004.allEntries).all fun (x : ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeEntry) => x.subevents.constructional.hasCause) = true

All causative entries in the data have CAUSE (verified empirically).

theorem Causative.Resultatives.causative_means_have_cause : ((List.filter (fun (e : ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeEntry) => e.subconstruction.isCausative && e.subevents.relation == ConstructionGrammar.Studies.GoldbergJackendoff2004.SubeventRelation.means) ConstructionGrammar.Studies.GoldbergJackendoff2004.allEntries).all fun (x : ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeEntry) => x.subevents.constructional.hasCause) = true

MEANS-relation causative entries all have CAUSE.

CC-selection (Baglini & Bar-Asher @cite{baglini-bar-asher-siegal-2025})

Different causative constructions constrain which condition from a causal model can be selected as "the cause." BBS2025 call this CC-selection.

• Overt "cause" (BBS2025, Formula 11): the subject must be an INUS member of a sufficient set — any contributing condition qualifies
• CoS/lexical causatives (BBS2025, Formula 14): the subject must be the completion event — the last condition to be realized, whose occurrence makes the result inevitable
• Resultatives pattern with CoS: the verbal subevent completes the sufficient set for the constructional result

inductive Causative.Resultatives.CCSelectionMode : Type

How a causative construction selects its cause (BBS2025).

• memberOfSufficientSet : CCSelectionMode

  Overt "cause": subject is any member of a sufficient set (BBS2025 §4.1)

• completionOfSufficientSet : CCSelectionMode

  CoS/resultative: subject completes a sufficient set (BBS2025 §4.2)

def Causative.Resultatives.instReprCCSelectionMode.repr : CCSelectionMode → ℕ → Std.Format

Equations

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

instance Causative.Resultatives.instReprCCSelectionMode : Repr CCSelectionMode

Equations

• Causative.Resultatives.instReprCCSelectionMode = { reprPrec := Causative.Resultatives.instReprCCSelectionMode.repr }

instance Causative.Resultatives.instDecidableEqCCSelectionMode : DecidableEq CCSelectionMode

Equations

• Causative.Resultatives.instDecidableEqCCSelectionMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Causative.Resultatives.instBEqCCSelectionMode.beq : CCSelectionMode → CCSelectionMode → Bool

Equations

• Causative.Resultatives.instBEqCCSelectionMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Causative.Resultatives.instBEqCCSelectionMode : BEq CCSelectionMode

Equations

• Causative.Resultatives.instBEqCCSelectionMode = { beq := Causative.Resultatives.instBEqCCSelectionMode.beq }

def Causative.Resultatives.resultativeCCSelection : CCSelectionMode

Resultatives select via completion (like CoS verbs).

Equations

• Causative.Resultatives.resultativeCCSelection = Causative.Resultatives.CCSelectionMode.completionOfSufficientSet

def Causative.Resultatives.completesForEffect (dyn : Core.StructuralEquationModel.CausalDynamics) (background : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) : Bool

BBS2025 completion event: sufficient + but-for necessary in context. Uses simple counterfactual but-for rather than @cite{nadathur-2024} Def 10b's supersituation necessity: the cause must be needed in the CURRENT background, not resilient against all possible supersituations. This is the right granularity for completion events — intermediate variables in causal chains are passive (no independent source), so simple but-for captures tightness correctly.

Equations

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

theorem Causative.Resultatives.hammer_completes_for_flat : completesForEffect hammerFlatModel Core.StructuralEquationModel.Situation.empty hammeringVar flatVar = true

Hammering completes the sufficient set for flatness.

theorem Causative.Resultatives.kick_completes_for_field : completesForEffect kickIntoFieldModel Core.StructuralEquationModel.Situation.empty kickingVar inFieldVar = true

Kicking completes the sufficient set for in-field.

Temporal constraint as completion event (G&J Principle 33)

def Causative.Resultatives.isCompletionEvent (dyn : Core.StructuralEquationModel.CausalDynamics) (background : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) (order : ConstructionGrammar.Studies.GoldbergJackendoff2004.TemporalOrder) : Bool

Causal completion + temporal ordering.

Equations

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

theorem Causative.Resultatives.hammer_is_completion_event : isCompletionEvent hammerFlatModel Core.StructuralEquationModel.Situation.empty hammeringVar flatVar ConstructionGrammar.Studies.GoldbergJackendoff2004.TemporalOrder.verbalFirst = true

Hammering is a completion event for flatness (verbal precedes result).

theorem Causative.Resultatives.hammer_completion_simultaneous : isCompletionEvent hammerFlatModel Core.StructuralEquationModel.Situation.empty hammeringVar flatVar ConstructionGrammar.Studies.GoldbergJackendoff2004.TemporalOrder.simultaneous = true

Hammering is a completion event when simultaneous with result.

theorem Causative.Resultatives.hammer_not_completion_if_result_first : isCompletionEvent hammerFlatModel Core.StructuralEquationModel.Situation.empty hammeringVar flatVar ConstructionGrammar.Studies.GoldbergJackendoff2004.TemporalOrder.constructionalFirst = false

Result preceding verbal subevent violates temporal constraint.

CausativeBuilder bridge

def Causative.Resultatives.resultativeCausativeBuilder : NadathurLauer2020.CausativeBuilder

The resultative construction uses .make (sufficiency).

Equations

• Causative.Resultatives.resultativeCausativeBuilder = NadathurLauer2020.Builder.CausativeBuilder.make

theorem Causative.Resultatives.resultative_is_make : resultativeCausativeBuilder = NadathurLauer2020.Builder.CausativeBuilder.make

Resultative causation uses the .make builder.

theorem Causative.Resultatives.resultative_cause_matches_make_verb : Fragments.English.Predicates.Verbal.make.causativeBuilder = some resultativeCausativeBuilder

Resultative CAUSE matches the Fragment entry for "make".

theorem Causative.Resultatives.resultative_cause_differs_from_cause_verb : Fragments.English.Predicates.Verbal.cause.causativeBuilder ≠ some resultativeCausativeBuilder

Resultative CAUSE ≠ "cause" verb (.make ≠ .cause).

theorem Causative.Resultatives.prevent_incompatible_with_resultative : NadathurLauer2020.Builder.CausativeBuilder.prevent ≠ resultativeCausativeBuilder

.prevent is incompatible with resultatives.

@cite{levin-2019}'s Tightness via Causal Necessity

Resultatives require tightness: no intervening causer with its own energy source. Tightness ≡ completesForEffect (sufficiency + necessity). The necessity component does the explanatory work: causallyNecessary runs normalDevelopment with cause=false. An intermediate with an independent energy source still fires without the cause, so necessity fails.

Example	Chain	Indep. source?	completesForEffect
"hammer metal flat"	direct	—	true
"drink teapot dry"	passive chain	No	true
"kick door open" (direct)	direct	—	true
*"kick door open" (via ball)	active chain	Yes	false

hasDirectLaw (graph inspection) is insufficient: it rejects "drink teapot dry" (passive chain, no direct law, but tight).

def Causative.Resultatives.drinkTeapotDryModel : Core.StructuralEquationModel.CausalDynamics

"Drink the teapot dry": passive chain (Levin §4). drinking → tea_removal → teapot_dry. Tea removal has no independent energy source.

Equations

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

def Causative.Resultatives.kickDoorViaBallModel : Core.StructuralEquationModel.CausalDynamics

*"Kick the door open" via ball (UNAVAILABLE, Levin §7). kick → ball_motion → door_open, plus ball_energy → ball_motion. The ball has an independent energy source.

Equations

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

def Causative.Resultatives.ballHasEnergyBg : Core.StructuralEquationModel.Situation

Background: ball has its own energy.

Equations

• Causative.Resultatives.ballHasEnergyBg = Core.StructuralEquationModel.Situation.empty.extend Causative.Resultatives.ballEnergyVar✝ true

def Causative.Resultatives.kickDoorDirectModel : Core.StructuralEquationModel.CausalDynamics

"Kick the door open" (direct, available reading). kick → door_open.

Equations

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

Tightness = completesForEffect

Each theorem runs normalDevelopment under counterfactual intervention (cause=true for sufficiency, cause=false for necessity).

theorem Causative.Resultatives.hammer_flat_tight : completesForEffect hammerFlatModel Core.StructuralEquationModel.Situation.empty hammeringVar flatVar = true

theorem Causative.Resultatives.drink_teapot_dry_tight : completesForEffect drinkTeapotDryModel Core.StructuralEquationModel.Situation.empty Causative.Resultatives.drinkingVar✝ Causative.Resultatives.teapotDryVar✝ = true

Tight despite being a chain: removing drinking leaves tea_removal undetermined (no independent source), so teapot_dry doesn't fire.

theorem Causative.Resultatives.kick_door_via_ball_not_tight : completesForEffect kickDoorViaBallModel ballHasEnergyBg Causative.Resultatives.kickingDoorVar✝ Causative.Resultatives.doorOpenVar✝ = false

NOT tight: removing kicking still allows ball_energy → ball_motion → door_open. The kick is not necessary.

theorem Causative.Resultatives.kick_door_direct_tight : completesForEffect kickDoorDirectModel Core.StructuralEquationModel.Situation.empty Causative.Resultatives.kickingDoorVar✝ Causative.Resultatives.doorOpenVar✝ = true

theorem Causative.Resultatives.drink_dry_no_direct_law_but_tight : Core.StructuralEquationModel.hasDirectLaw drinkTeapotDryModel Causative.Resultatives.drinkingVar✝ Causative.Resultatives.teapotDryVar✝ = false ∧ completesForEffect drinkTeapotDryModel Core.StructuralEquationModel.Situation.empty Causative.Resultatives.drinkingVar✝¹ Causative.Resultatives.teapotDryVar✝¹ = true

hasDirectLaw (graph inspection) incorrectly rejects the passive chain "drink teapot dry" — no direct law, but tight.

Intervening causer = independent source

theorem Causative.Resultatives.ball_has_independent_source : Core.StructuralEquationModel.hasIndependentSource kickDoorViaBallModel Causative.Resultatives.kickingDoorVar✝ Causative.Resultatives.ballMotionVar✝ = true

Ball has an independent source (ball_energy law).

theorem Causative.Resultatives.tea_no_independent_source : Core.StructuralEquationModel.hasIndependentSource drinkTeapotDryModel Causative.Resultatives.drinkingVar✝ Causative.Resultatives.teaRemovalVar✝ = false

Tea removal has no independent source.

theorem Causative.Resultatives.independent_source_disrupts_tightness (cause intermediate effect indepSrc : Core.StructuralEquationModel.Variable) (hci : cause ≠ intermediate) (hce : cause ≠ effect) (hie : intermediate ≠ effect) (hsc : indepSrc ≠ cause) (hsi : indepSrc ≠ intermediate) (hse : indepSrc ≠ effect) : have chain := Core.StructuralEquationModel.CausalDynamics.causalChain cause intermediate effect; completesForEffect chain Core.StructuralEquationModel.Situation.empty cause effect = true → have withIndep := { laws := [Core.StructuralEquationModel.CausalLaw.simple cause intermediate, Core.StructuralEquationModel.CausalLaw.simple intermediate effect, Core.StructuralEquationModel.CausalLaw.simple indepSrc intermediate] }; have bg := Core.StructuralEquationModel.Situation.empty.extend indepSrc true; completesForEffect withIndep bg cause effect = false

For a chain a → b → c, an active independent source for b disrupts completesForEffect for a → c. The independent source fires b even with a=false, so a is not necessary.

theorem Causative.Resultatives.independent_source_disrupts_tightness_concrete : completesForEffect drinkTeapotDryModel Core.StructuralEquationModel.Situation.empty Causative.Resultatives.drinkingVar✝ Causative.Resultatives.teapotDryVar✝ = true ∧ completesForEffect kickDoorViaBallModel ballHasEnergyBg Causative.Resultatives.kickingDoorVar✝ Causative.Resultatives.doorOpenVar✝ = false

Concrete witness: passive chain tight, active chain not tight.

Contiguity (Levin §4)

Nonselected-NP resultatives require contiguity between verb's object and affected entity. All types involve passive intermediates (no independent source), so completesForEffect holds.

inductive Causative.Resultatives.ContiguityType : Type

Spatial contiguity preserving tightness in nonselected NP resultatives.

• containerContents : ContiguityType
• contentsContainer : ContiguityType
• impingement : ContiguityType

instance Causative.Resultatives.instDecidableEqContiguityType : DecidableEq ContiguityType

Equations

• Causative.Resultatives.instDecidableEqContiguityType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Causative.Resultatives.instReprContiguityType.repr : ContiguityType → ℕ → Std.Format

Equations

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

instance Causative.Resultatives.instReprContiguityType : Repr ContiguityType

Equations

• Causative.Resultatives.instReprContiguityType = { reprPrec := Causative.Resultatives.instReprContiguityType.repr }

instance Causative.Resultatives.instBEqContiguityType : BEq ContiguityType

Equations

• Causative.Resultatives.instBEqContiguityType = { beq := Causative.Resultatives.instBEqContiguityType.beq }

def Causative.Resultatives.instBEqContiguityType.beq : ContiguityType → ContiguityType → Bool

Equations

• Causative.Resultatives.instBEqContiguityType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Causative.Resultatives.ContiguityType.intermediateIsPassive : ContiguityType → Bool

All contiguity types involve passive intermediates (no independent energy source), so necessity propagates through the chain.

Equations

• Causative.Resultatives.ContiguityType.containerContents.intermediateIsPassive = true
• Causative.Resultatives.ContiguityType.contentsContainer.intermediateIsPassive = true
• Causative.Resultatives.ContiguityType.impingement.intermediateIsPassive = true

Three-Way Convergence: Thick ↔ P-CAUSE ↔ Resultative

Three independently-defined modules converge on the same prediction:

1. ProductionDependence.lean: Thick manner → P-CAUSE → .make builder
2. Resultatives.lean: Resultative CAUSE → .make builder
3. ThickThin.lean: Thick manner → ASR-compatible (empirical data)

This convergence is non-trivial: each path was formalized independently following different papers (@cite{martin-rose-nichols-2025}, @cite{goldberg-jackendoff-2004}, @cite{embick-2009}). The fact that they agree validates the cross-module architecture.

theorem Causative.Resultatives.thick_manner_resultative_convergence : MartinRoseNichols2025.productionConstraint MartinRoseNichols2025.ThickThinClass.thickManner = MartinRoseNichols2025.CausationType.production ∧ MartinRoseNichols2025.CausationType.production.analogousBuilder = NadathurLauer2020.Builder.CausativeBuilder.make ∧ resultativeCausativeBuilder = NadathurLauer2020.Builder.CausativeBuilder.make ∧ MartinRoseNichols2025.CausationType.production.analogousBuilder = resultativeCausativeBuilder

Three independent paths converge on .make.

theorem Causative.Resultatives.thin_incompatible_with_resultative_cause : MartinRoseNichols2025.productionConstraint MartinRoseNichols2025.ThickThinClass.thin = MartinRoseNichols2025.CausationType.dependence ∧ MartinRoseNichols2025.CausationType.dependence.analogousBuilder = NadathurLauer2020.Builder.CausativeBuilder.cause ∧ NadathurLauer2020.Builder.CausativeBuilder.cause ≠ resultativeCausativeBuilder

Thin → .cause ≠ resultative .make (*kill open).

Aspect: activity + bounded RP → accomplishment

theorem Causative.Resultatives.resultativeTelicizes : Semantics.Tense.Aspect.LexicalAspect.activityProfile.telicize.toVendlerClass = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

Bounded RP telicizes activity (reuses telicize_activity).

theorem Causative.Resultatives.resultativeAspectShift : ConstructionGrammar.Studies.GoldbergJackendoff2004.resultativeVendlerClass ConstructionGrammar.Studies.GoldbergJackendoff2004.Boundedness.bounded = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

The resultative construction's aspect shift: for any activity verb with a bounded RP, the result is an accomplishment.

theorem Causative.Resultatives.resultative_aspect_agrees_with_telicize : ConstructionGrammar.Studies.GoldbergJackendoff2004.resultativeVendlerClass ConstructionGrammar.Studies.GoldbergJackendoff2004.Boundedness.bounded = Semantics.Tense.Aspect.LexicalAspect.activityProfile.telicize.toVendlerClass

The resultative-derived aspect matches the general telicize operation when starting from an activity.

theorem Causative.Resultatives.activity_entries_become_accomplishments : ((List.filter (fun (e : ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeEntry) => e.bareVerbClass == Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity && e.rpBoundedness == ConstructionGrammar.Studies.GoldbergJackendoff2004.Boundedness.bounded) ConstructionGrammar.Studies.GoldbergJackendoff2004.allEntries).all fun (e : ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeEntry) => ConstructionGrammar.Studies.GoldbergJackendoff2004.resultativeVendlerClass e.rpBoundedness == Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment) = true

Activity verbs in the data that get bounded RPs become accomplishments.

ChangeOfState: BECOME = inception (¬P → P)

def Causative.Resultatives.resultStateMapsToCoS : Semantics.Lexical.Verb.ChangeOfState.CoSType

Constructional BECOME = CoS inception.

Equations

• Causative.Resultatives.resultStateMapsToCoS = Semantics.Lexical.Verb.ChangeOfState.CoSType.inception

theorem Causative.Resultatives.all_have_become : (ConstructionGrammar.Studies.GoldbergJackendoff2004.allEntries.all fun (x : ConstructionGrammar.Studies.GoldbergJackendoff2004.ResultativeEntry) => x.subevents.constructional.hasBecome) = true

All resultative entries have BECOME.

theorem Causative.Resultatives.inception_presupposes_not_prior {W : Type u_1} (P : W → Bool) (w : W) : Semantics.Lexical.Verb.ChangeOfState.priorStatePresup Semantics.Lexical.Verb.ChangeOfState.CoSType.inception P w = !P w

Inception presupposes ¬P before.

theorem Causative.Resultatives.inception_asserts_result {W : Type u_1} (P : W → Bool) : Semantics.Lexical.Verb.ChangeOfState.resultStateAssertion Semantics.Lexical.Verb.ChangeOfState.CoSType.inception P = P

Inception asserts P after.

Müller Decomposability

All four resultative subconstructions are fully abstract and therefore decomposable into Müller's universal schemata.

Causative subconstructions → [HS, HC, HC] (same as parent resultative) Noncausative subconstructions → [HS, HC] (intransitive, fewer complements)

theorem Causative.Resultatives.allResultativesFullyCompositional : (ConstructionGrammar.Studies.GoldbergJackendoff2004.resultativeFamily.all fun (c : ConstructionGrammar.ArgStructureConstruction) => ConstructionGrammar.isFullyCompositional c.construction) = true

All four subconstructions are fully compositional.

theorem Causative.Resultatives.causative_decompose_like_parent : ConstructionGrammar.decompose ConstructionGrammar.Studies.GoldbergJackendoff2004.causativePropertyConstruction = ConstructionGrammar.decompose ConstructionGrammar.resultative ∧ ConstructionGrammar.decompose ConstructionGrammar.Studies.GoldbergJackendoff2004.causativePathConstruction = ConstructionGrammar.decompose ConstructionGrammar.resultative

Causative subconstructions decompose like the parent resultative into three combination steps.

theorem Causative.Resultatives.noncausative_fewer_steps : (ConstructionGrammar.decompose ConstructionGrammar.Studies.GoldbergJackendoff2004.noncausativePropertyConstruction).length < (ConstructionGrammar.decompose ConstructionGrammar.Studies.GoldbergJackendoff2004.causativePropertyConstruction).length ∧ (ConstructionGrammar.decompose ConstructionGrammar.Studies.GoldbergJackendoff2004.noncausativePathConstruction).length < (ConstructionGrammar.decompose ConstructionGrammar.Studies.GoldbergJackendoff2004.causativePathConstruction).length

Noncausative subconstructions decompose into two combination steps (one fewer than the causative, reflecting their intransitivity).

theorem Causative.Resultatives.decomposition_reflects_transitivity : (ConstructionGrammar.decompose ConstructionGrammar.Studies.GoldbergJackendoff2004.causativePropertyConstruction).length = 3 ∧ (ConstructionGrammar.decompose ConstructionGrammar.Studies.GoldbergJackendoff2004.noncausativePropertyConstruction).length = 2

The causative/noncausative split is reflected in decomposition length: causative = 3 steps, noncausative = 2 steps.

Cross-linguistic Resultative Parameters (@cite{tay-2024})

Resultative constructions vary cross-linguistically along dimensions orthogonal to the G&J subconstruction typology. @cite{tay-2024} identifies three: realization (how the result predicate is morphosyntactically encoded), orientation (whether DOR holds), and phase grammaticalization.

inductive Causative.Resultatives.ResultativeRealization : Type

How the result predicate is morphosyntactically realized.

• syntacticAdjunct : ResultativeRealization

  English: result AP/PP is a syntactic adjunct

• verbCompound : ResultativeRealization

  Mandarin V-V: V2 morphologically incorporated into V1

• deComplement : ResultativeRealization

  Mandarin V-de: result clause introduced by particle de

instance Causative.Resultatives.instDecidableEqResultativeRealization : DecidableEq ResultativeRealization

Equations

• Causative.Resultatives.instDecidableEqResultativeRealization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Causative.Resultatives.instBEqResultativeRealization.beq : ResultativeRealization → ResultativeRealization → Bool

Equations

• Causative.Resultatives.instBEqResultativeRealization.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Causative.Resultatives.instBEqResultativeRealization : BEq ResultativeRealization

Equations

• Causative.Resultatives.instBEqResultativeRealization = { beq := Causative.Resultatives.instBEqResultativeRealization.beq }

instance Causative.Resultatives.instReprResultativeRealization : Repr ResultativeRealization

Equations

• Causative.Resultatives.instReprResultativeRealization = { reprPrec := Causative.Resultatives.instReprResultativeRealization.repr }

def Causative.Resultatives.instReprResultativeRealization.repr : ResultativeRealization → ℕ → Std.Format

Equations

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

inductive Causative.Resultatives.ResultOrientation : Type

Whether the result predicate targets the subject or object. English enforces DOR (Direct Object Restriction): the result must predicate of the direct object. Mandarin allows subject-oriented resultatives productively (kū-lèi "cry-tired").

• objectOriented : ResultOrientation
• subjectOriented : ResultOrientation

instance Causative.Resultatives.instDecidableEqResultOrientation : DecidableEq ResultOrientation

Equations

• Causative.Resultatives.instDecidableEqResultOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Causative.Resultatives.instBEqResultOrientation : BEq ResultOrientation

Equations

• Causative.Resultatives.instBEqResultOrientation = { beq := Causative.Resultatives.instBEqResultOrientation.beq }

def Causative.Resultatives.instBEqResultOrientation.beq : ResultOrientation → ResultOrientation → Bool

Equations

• Causative.Resultatives.instBEqResultOrientation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Causative.Resultatives.instReprResultOrientation : Repr ResultOrientation

Equations

• Causative.Resultatives.instReprResultOrientation = { reprPrec := Causative.Resultatives.instReprResultOrientation.repr }

def Causative.Resultatives.instReprResultOrientation.repr : ResultOrientation → ℕ → Std.Format

Equations

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

inductive Causative.Resultatives.PhaseComplement : Type

Phase complements: a grammaticalized closed-class subset of Mandarin V2 resultatives with fixed change-of-state semantics. Maps to CoSType from ChangeOfState.Theory.

• dao : PhaseComplement
• wan : PhaseComplement
• hao : PhaseComplement
• diao : PhaseComplement
• zhu : PhaseComplement

instance Causative.Resultatives.instDecidableEqPhaseComplement : DecidableEq PhaseComplement

Equations

• Causative.Resultatives.instDecidableEqPhaseComplement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Causative.Resultatives.instBEqPhaseComplement : BEq PhaseComplement

Equations

• Causative.Resultatives.instBEqPhaseComplement = { beq := Causative.Resultatives.instBEqPhaseComplement.beq }

def Causative.Resultatives.instBEqPhaseComplement.beq : PhaseComplement → PhaseComplement → Bool

Equations

• Causative.Resultatives.instBEqPhaseComplement.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Causative.Resultatives.instReprPhaseComplement.repr : PhaseComplement → ℕ → Std.Format

Equations

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

instance Causative.Resultatives.instReprPhaseComplement : Repr PhaseComplement

Equations

• Causative.Resultatives.instReprPhaseComplement = { reprPrec := Causative.Resultatives.instReprPhaseComplement.repr }

def Causative.Resultatives.PhaseComplement.cosType : PhaseComplement → Semantics.Lexical.Verb.ChangeOfState.CoSType

Phase complements have fixed CoS semantics, bridging Mandarin morphology to the cross-linguistic CoSType infrastructure in ChangeOfState.Theory.

Equations

• Causative.Resultatives.PhaseComplement.dao.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.inception
• Causative.Resultatives.PhaseComplement.wan.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation
• Causative.Resultatives.PhaseComplement.hao.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.inception
• Causative.Resultatives.PhaseComplement.diao.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.inception
• Causative.Resultatives.PhaseComplement.zhu.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation

theorem Causative.Resultatives.inceptive_phases_share_presup : PhaseComplement.dao.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.inception ∧ PhaseComplement.hao.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.inception ∧ PhaseComplement.diao.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.inception

All inceptive phase complements share the presupposition ¬P.

theorem Causative.Resultatives.phase_complements_cover_cos_types : PhaseComplement.dao.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.inception ∧ PhaseComplement.wan.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation ∧ PhaseComplement.zhu.cosType = Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation

Phase complements cover all three CoS types (inception, cessation, continuation).