Resultatives as Concealed Causatives

[BBS25] [GJ04] [Lev19] [MRN25]

Theory-side connection between the resultative construction and the causative semantics infrastructure. Per-scenario BoolSEM witnesses (HammerFlat, IndependentSourceBreaksNecessity, etc.) live with the paper that uses them — see Levin2026 and Studies.Tay2024. Per-datum [GJ04] verifications live in GoldbergJackendoff2004.

Sections:

1. Causative bridge: deriveCausativeBuilder derives the resultative's Causative value from the [GJ04] MEANS subevent relation + constructional CAUSE flag. Specialized to MEANS-relation causative resultatives; [GJ04]'s sound-emission and disappearance subtypes (RESULT/INSTANCE relations) are out of scope for the derivation here and would need their own builders.
2. CC-selection: resultatives select via completion of a sufficient set ([BBS25], alongside change-of-state verbs).
3. Three-way convergence: [MRN25] thick manner ↔ .production ↔ .make builder ↔ resultative builder. Independently motivated paths converge on .make.
4. Aspect: bounded RP telicizes activity → accomplishment.
5. ChangeOfState: constructional BECOME maps to CoSType.inception. (Schema decomposition of the subconstruction family lives with [Mul13]'s apparatus in Studies/Mueller2013.lean.)
6. Cross-linguistic typological parameters: ResultativeRealization, ResultOrientation. Mandarin-specific phase-complement morpheme data (PhaseComplement enum + cosType) lives in Mandarin.Resultatives.

Agreement with Boolean flags

theorem Causation.Resultatives.causative_iff_has_cause (sc : ConstructionGrammar.Resultatives.ResultativeSubconstruction) : sc.isCausative = sc.constructionalDesc.hasCause

isCausative ↔ hasCause — derived from the subconstruction, not stipulated.

CC-selection ([BBS25])

Resultatives select via completion of a sufficient set: the verbal subevent must be the final condition that makes the result inevitable.

def Causation.Resultatives.resultativeCCSelection : CCSelection.CCSelectionMode

Resultatives select via completion (like CoS verbs).

Equations

• Causation.Resultatives.resultativeCCSelection = Causation.CCSelection.CCSelectionMode.completionOfSufficientSet

Causative bridge: derived from SubeventRelation + CAUSE

The resultative's Causative is .make, derived from two independently-motivated properties:

1. MEANS relation ([GJ04]): the verbal subevent is the means by which the constructional subevent is brought about. MEANS ↔ causal sufficiency.
2. CAUSE in constructional subevent: causative subconstructions have hasCause = true.

MEANS + CAUSE → sufficiency. Among sufficiency builders, .make is uniquely the neutral builder (no coercion .force, no barrier-removal .enable).

Note: this derivation handles MEANS-relation resultatives only. Sound- emission and disappearance subtypes (SubeventRelation.result/.instance_) would map to different builders or remain unanalyzed here.

def Causation.Resultatives.deriveCausativeBuilder (rel : ConstructionGrammar.Resultatives.SubeventRelation) (desc : ConstructionGrammar.Resultatives.SubeventDesc) : Option Features.Causative

Derive the Causative from MEANS subevent relation + CAUSE flag. Always yields .make for MEANS+CAUSE; non-MEANS yields none.

Equations

• Causation.Resultatives.deriveCausativeBuilder ConstructionGrammar.Resultatives.SubeventRelation.means desc = some Features.Causative.make
• Causation.Resultatives.deriveCausativeBuilder rel✝ desc = none

theorem Causation.Resultatives.make_unique_neutral_sufficiency (b : Features.Causative) (hs : b.assertsSufficiency = true) (hc : b.isCoercive = false) (hp : b.isPermissive = false) : b = Features.Causative.make

.make is the unique builder asserting neutral sufficiency.

theorem Causation.Resultatives.means_cause_derives_make (desc : ConstructionGrammar.Resultatives.SubeventDesc) (h : desc.hasCause = true) : deriveCausativeBuilder ConstructionGrammar.Resultatives.SubeventRelation.means desc = some Features.Causative.make

MEANS + CAUSE derives .make.

theorem Causation.Resultatives.causative_means_derives_make (sc : ConstructionGrammar.Resultatives.ResultativeSubconstruction) (h : sc.isCausative = true) : deriveCausativeBuilder ConstructionGrammar.Resultatives.SubeventRelation.means sc.constructionalDesc = some Features.Causative.make

For any causative subconstruction with MEANS relation, the derived builder is .make.

theorem Causation.Resultatives.noncausative_no_builder (sc : ConstructionGrammar.Resultatives.ResultativeSubconstruction) (h : sc.isCausative = false) : deriveCausativeBuilder ConstructionGrammar.Resultatives.SubeventRelation.means sc.constructionalDesc = none

Noncausative subconstructions don't derive a Causative.

theorem Causation.Resultatives.non_means_no_builder (desc : ConstructionGrammar.Resultatives.SubeventDesc) : deriveCausativeBuilder ConstructionGrammar.Resultatives.SubeventRelation.result desc = none ∧ deriveCausativeBuilder ConstructionGrammar.Resultatives.SubeventRelation.instance_ desc = none ∧ deriveCausativeBuilder ConstructionGrammar.Resultatives.SubeventRelation.coOccurrence desc = none

Non-MEANS relations never derive a Causative.

theorem Causation.Resultatives.derived_asserts_sufficiency (rel : ConstructionGrammar.Resultatives.SubeventRelation) (desc : ConstructionGrammar.Resultatives.SubeventDesc) (b : Features.Causative) (h : deriveCausativeBuilder rel desc = some b) : b.assertsSufficiency = true

When deriveCausativeBuilder succeeds, the result asserts sufficiency.

def Causation.Resultatives.resultativeCausativeBuilder : Features.Causative

The resultative Causative, derived from MEANS + CAUSE.

Equations

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

theorem Causation.Resultatives.resultative_is_make : resultativeCausativeBuilder = Features.Causative.make

The derived builder is .make.

theorem Causation.Resultatives.prevent_incompatible_with_resultative : Features.Causative.prevent ≠ resultativeCausativeBuilder

.prevent is incompatible with resultatives.

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

theorem Causation.Resultatives.thick_manner_resultative_convergence : ProductionDependence.productionConstraint ProductionDependence.ThickThinClass.thickManner = ProductionDependence.CausationType.production ∧ ProductionDependence.CausationType.production.analogousBuilder = Features.Causative.make ∧ resultativeCausativeBuilder = Features.Causative.make ∧ ProductionDependence.CausationType.production.analogousBuilder = resultativeCausativeBuilder

Three independent paths converge on .make: [MRN25] thick manner classification + .production analogous-builder + the resultative-from-MEANS+CAUSE derivation above.

theorem Causation.Resultatives.thin_incompatible_with_resultative_cause : ProductionDependence.productionConstraint ProductionDependence.ThickThinClass.thin = ProductionDependence.CausationType.dependence ∧ ProductionDependence.CausationType.dependence.analogousBuilder = Features.Causative.cause ∧ Features.Causative.cause ≠ resultativeCausativeBuilder

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

Aspect: activity + bounded RP → accomplishment

theorem Causation.Resultatives.resultative_telicizes : Features.activityProfile.telicize.toVendlerClass = Features.VendlerClass.accomplishment

Bounded RP telicizes activity.

theorem Causation.Resultatives.resultative_aspect_shift : ConstructionGrammar.Resultatives.resultativeVendlerClass ConstructionGrammar.Resultatives.Boundedness.bounded = Features.VendlerClass.accomplishment

The resultative construction's aspect shift.

theorem Causation.Resultatives.resultative_aspect_agrees_with_telicize : ConstructionGrammar.Resultatives.resultativeVendlerClass ConstructionGrammar.Resultatives.Boundedness.bounded = Features.activityProfile.telicize.toVendlerClass

ChangeOfState: BECOME = inception (¬P → P)

def Causation.Resultatives.resultStateMapsToCoS : Features.ChangeOfState.CoSType

Constructional BECOME = CoS inception.

Equations

• Causation.Resultatives.resultStateMapsToCoS = Features.ChangeOfState.CoSType.inception

theorem Causation.Resultatives.inception_presupposes_not_prior {W : Type u_1} (P : W → Prop) (w : W) : Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.inception P w ↔ ¬P w

Inception presupposes ¬P before.

theorem Causation.Resultatives.inception_asserts_result {W : Type u_1} (P : W → Prop) : Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.inception P = P

Inception asserts P after.

Cross-linguistic Resultative Parameters

ResultativeRealization and ResultOrientation are theory-neutral typological parameters. Mandarin-specific phase complements (PhaseComplement enum + per-morpheme cosType) live in Mandarin.Resultatives.

inductive Causation.Resultatives.ResultativeRealization : Type

• syntacticAdjunct : ResultativeRealization
• verbCompound : ResultativeRealization
• deComplement : ResultativeRealization

@[implicit_reducible]

instance Causation.Resultatives.instDecidableEqResultativeRealization : DecidableEq ResultativeRealization

Equations

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

@[implicit_reducible]

instance Causation.Resultatives.instReprResultativeRealization : Repr ResultativeRealization

Equations

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

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

Equations

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

inductive Causation.Resultatives.ResultOrientation : Type

• objectOriented : ResultOrientation
• subjectOriented : ResultOrientation

@[implicit_reducible]

instance Causation.Resultatives.instDecidableEqResultOrientation : DecidableEq ResultOrientation

Equations

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

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

Equations

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

@[implicit_reducible]

instance Causation.Resultatives.instReprResultOrientation : Repr ResultOrientation

Equations

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