Resultatives as Concealed Causatives

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

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 Phenomena.Constructions.Resultatives.Studies.Levin2026 and Studies.Tay2024. Per-datum @cite{goldberg-jackendoff-2004} verifications live in Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.

Sections:

1. Causative bridge: deriveCausativeBuilder derives the resultative's Causative value from the @cite{goldberg-jackendoff-2004} MEANS subevent relation + constructional CAUSE flag. Specialized to MEANS-relation causative resultatives; @cite{goldberg-jackendoff-2004}'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 (@cite{baglini-bar-asher-siegal-2025}, alongside change-of-state verbs).
3. Three-way convergence: @cite{martin-rose-nichols-2025} 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.
6. Compositional decomposition: subconstructions decompose into universal schemata (isFullyCompositional).
7. Cross-linguistic typological parameters: ResultativeRealization, ResultOrientation. Mandarin-specific phase-complement morpheme data (PhaseComplement enum + cosType) lives in Fragments.Mandarin.Resultatives.

Agreement with Boolean flags

theorem Semantics.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 (@cite{baglini-bar-asher-siegal-2025})

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

def Semantics.Causation.Resultatives.resultativeCCSelection : CCSelection.CCSelectionMode

Resultatives select via completion (like CoS verbs).

Equations

• Semantics.Causation.Resultatives.resultativeCCSelection = Semantics.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 (@cite{goldberg-jackendoff-2004}): 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 Semantics.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

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

theorem Semantics.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 Semantics.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 Semantics.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 Semantics.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 Semantics.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 Semantics.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 Semantics.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 Semantics.Causation.Resultatives.resultative_is_make : resultativeCausativeBuilder = Features.Causative.make

The derived builder is .make.

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

.prevent is incompatible with resultatives.

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

theorem Semantics.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: @cite{martin-rose-nichols-2025} thick manner classification + .production analogous-builder + the resultative-from-MEANS+CAUSE derivation above.

theorem Semantics.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 Semantics.Causation.Resultatives.resultative_telicizes : Features.activityProfile.telicize.toVendlerClass = Features.VendlerClass.accomplishment

Bounded RP telicizes activity.

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

The resultative construction's aspect shift.

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

ChangeOfState: BECOME = inception (¬P → P)

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

Constructional BECOME = CoS inception.

Equations

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

theorem Semantics.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 Semantics.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.

Compositional decomposition

theorem Semantics.Causation.Resultatives.allResultativesFullyCompositional : (ConstructionGrammar.Resultatives.resultativeFamily.all fun (c : ConstructionGrammar.ArgStructureConstruction) => ConstructionGrammar.isFullyCompositional c.construction) = true

All four subconstructions are fully compositional.

theorem Semantics.Causation.Resultatives.causative_decompose_like_parent : ConstructionGrammar.decompose ConstructionGrammar.Resultatives.causativePropertyConstruction = ConstructionGrammar.decompose ConstructionGrammar.resultative ∧ ConstructionGrammar.decompose ConstructionGrammar.Resultatives.causativePathConstruction = ConstructionGrammar.decompose ConstructionGrammar.resultative

Causative subconstructions decompose like the parent resultative.

theorem Semantics.Causation.Resultatives.noncausative_fewer_steps : (ConstructionGrammar.decompose ConstructionGrammar.Resultatives.noncausativePropertyConstruction).length < (ConstructionGrammar.decompose ConstructionGrammar.Resultatives.causativePropertyConstruction).length ∧ (ConstructionGrammar.decompose ConstructionGrammar.Resultatives.noncausativePathConstruction).length < (ConstructionGrammar.decompose ConstructionGrammar.Resultatives.causativePathConstruction).length

Noncausative subconstructions decompose into fewer combination steps.

theorem Semantics.Causation.Resultatives.decomposition_reflects_transitivity : (ConstructionGrammar.decompose ConstructionGrammar.Resultatives.causativePropertyConstruction).length = 3 ∧ (ConstructionGrammar.decompose ConstructionGrammar.Resultatives.noncausativePropertyConstruction).length = 2

Cross-linguistic Resultative Parameters

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

inductive Semantics.Causation.Resultatives.ResultativeRealization : Type

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

@[implicit_reducible]

instance Semantics.Causation.Resultatives.instDecidableEqResultativeRealization : DecidableEq ResultativeRealization

Equations

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

@[implicit_reducible]

instance Semantics.Causation.Resultatives.instReprResultativeRealization : Repr ResultativeRealization

Equations

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

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

Equations

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

inductive Semantics.Causation.Resultatives.ResultOrientation : Type

• objectOriented : ResultOrientation
• subjectOriented : ResultOrientation

@[implicit_reducible]

instance Semantics.Causation.Resultatives.instDecidableEqResultOrientation : DecidableEq ResultOrientation

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Causation.Resultatives.instReprResultOrientation : Repr ResultOrientation

Equations

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