Unaccusativity Bridge @cite{storment-2026}

Connects empirical diagnostic data to lexical annotations, syntactic theory (Voice, TransitivityClass, auxiliary selection, smuggling), and semantic proto-role predictions.

@cite{storment-2026}: QI via Smuggling

Quotative inversion (QI) is an unaccusativity diagnostic: manner-of-speaking verbs like whisper permit QI ("whispered Mary") because they are unaccusative, while agentive communication verbs like speak block QI (*"spoke Mary") because they are unergative.

The syntactic mechanism is smuggling: VP moves to Spec-VoiceP, making the theme subject accessible to T⁰ for Case licensing. This is possible iff Voice is not a phase head (non-thematic Voice), which correlates with unaccusativity.

QI ∥ LI (Unified Smuggling)

@cite{storment-2026} argues QI and locative inversion share the same mechanism: @cite{collins-2005} @cite{dowty-1991} @cite{lu-degen-2025} smuggling of VP to Spec-VoiceP. Both are blocked by the transitivity constraint (§5) and both require non-phase Voice. They differ in input (quote vs locative PP).

Dowty Divergence

Proto-role counting predicts MoS verb subjects as proto-agents (volitional, sentient speaker), yet QI classifies these verbs as unaccusative. This is a known divergence: unaccusativity is a syntactic diagnostic that does not always align with semantic proto-role predictions.

Each theorem ties to exactly one verb's unaccusative field. Changing the annotation breaks exactly one theorem.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.whisper_unaccusative : Fragments.English.Predicates.Verbal.whisper.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.murmur_unaccusative : Fragments.English.Predicates.Verbal.murmur.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.shout_unaccusative : Fragments.English.Predicates.Verbal.shout.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.cry_unaccusative : Fragments.English.Predicates.Verbal.cry.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.scream_unaccusative : Fragments.English.Predicates.Verbal.scream.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.seem_unaccusative : Fragments.English.Predicates.Verbal.seem.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.arrive_unaccusative : Fragments.English.Predicates.Verbal.arrive.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mumble_unaccusative : Fragments.English.Predicates.Verbal.mumble.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mutter_unaccusative : Fragments.English.Predicates.Verbal.mutter.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.shriek_unaccusative : Fragments.English.Predicates.Verbal.shriek.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.yell_unaccusative : Fragments.English.Predicates.Verbal.yell.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.groan_unaccusative : Fragments.English.Predicates.Verbal.groan.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.grumble_unaccusative : Fragments.English.Predicates.Verbal.grumble.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.hiss_unaccusative : Fragments.English.Predicates.Verbal.hiss.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.sigh_unaccusative : Fragments.English.Predicates.Verbal.sigh.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.whimper_unaccusative : Fragments.English.Predicates.Verbal.whimper.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.snap_unaccusative : Fragments.English.Predicates.Verbal.snap.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.speak_not_unaccusative : Fragments.English.Predicates.Verbal.speak.unaccusative = false

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.talk_not_unaccusative : Fragments.English.Predicates.Verbal.talk.unaccusative = false

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.run_not_unaccusative : Fragments.English.Predicates.Verbal.run.unaccusative = false

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.sleep_not_unaccusative : Fragments.English.Predicates.Verbal.sleep.unaccusative = false

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.kick_not_unaccusative : Fragments.English.Predicates.Verbal.kick.unaccusative = false

Each theorem connects a diagnostic datum to the corresponding lexical annotation. If either changes, the theorem breaks.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_whisper_agrees : Data.qi_whisper.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.whisper.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_murmur_agrees : Data.qi_murmur.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.murmur.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_shout_agrees : Data.qi_shout.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.shout.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_cry_agrees : Data.qi_cry.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.cry.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_scream_agrees : Data.qi_scream.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.scream.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_mumble_agrees : Data.qi_mumble.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.mumble.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_mutter_agrees : Data.qi_mutter.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.mutter.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_shriek_agrees : Data.qi_shriek.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.shriek.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_yell_agrees : Data.qi_yell.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.yell.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_groan_agrees : Data.qi_groan.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.groan.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_grumble_agrees : Data.qi_grumble.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.grumble.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_hiss_agrees : Data.qi_hiss.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.hiss.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_sigh_agrees : Data.qi_sigh.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.sigh.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_whimper_agrees : Data.qi_whimper.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.whimper.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_snap_agrees : Data.qi_snap.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.snap.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_speak_agrees : Data.qi_speak.result = Data.DiagnosticResult.fails ∧ Fragments.English.Predicates.Verbal.speak.unaccusative = false

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_talk_agrees : Data.qi_talk.result = Data.DiagnosticResult.fails ∧ Fragments.English.Predicates.Verbal.talk.unaccusative = false

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.there_arrive_agrees : Data.there_arrive.result = Data.DiagnosticResult.passes ∧ Fragments.English.Predicates.Verbal.arrive.unaccusative = true

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.deriveTransitivityClass (v : Core.Verbs.VerbCore) : AuxiliaryVerbs.Selection.TransitivityClass

Derive TransitivityClass from VerbCore fields: unaccusative → .unaccusative, complement-taking → .transitive, otherwise → .unergative.

Equations

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

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.whisper_transitivity : deriveTransitivityClass Fragments.English.Predicates.Verbal.whisper.toVerbCore = AuxiliaryVerbs.Selection.TransitivityClass.unaccusative

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.murmur_transitivity : deriveTransitivityClass Fragments.English.Predicates.Verbal.murmur.toVerbCore = AuxiliaryVerbs.Selection.TransitivityClass.unaccusative

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.speak_transitivity : deriveTransitivityClass Fragments.English.Predicates.Verbal.speak.toVerbCore = AuxiliaryVerbs.Selection.TransitivityClass.unergative

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.talk_transitivity : deriveTransitivityClass Fragments.English.Predicates.Verbal.talk.toVerbCore = AuxiliaryVerbs.Selection.TransitivityClass.unergative

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.arrive_transitivity : deriveTransitivityClass Fragments.English.Predicates.Verbal.arrive.toVerbCore = AuxiliaryVerbs.Selection.TransitivityClass.unaccusative

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.kick_transitivity : deriveTransitivityClass Fragments.English.Predicates.Verbal.kick.toVerbCore = AuxiliaryVerbs.Selection.TransitivityClass.transitive

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.seem_transitivity : deriveTransitivityClass Fragments.English.Predicates.Verbal.seem.toVerbCore = AuxiliaryVerbs.Selection.TransitivityClass.unaccusative

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.unaccToVoice (unacc : Bool) : Minimalism.VoiceFlavor

Map unaccusativity to Voice flavor: unaccusative verbs project non-thematic Voice (no external argument); others project agentive Voice.

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.unaccToVoice unacc = if unacc = true then Minimalism.VoiceFlavor.nonThematic else Minimalism.VoiceFlavor.agentive

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.whisper_voice : unaccToVoice Fragments.English.Predicates.Verbal.whisper.unaccusative = Minimalism.VoiceFlavor.nonThematic

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.murmur_voice : unaccToVoice Fragments.English.Predicates.Verbal.murmur.unaccusative = Minimalism.VoiceFlavor.nonThematic

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.speak_voice : unaccToVoice Fragments.English.Predicates.Verbal.speak.unaccusative = Minimalism.VoiceFlavor.agentive

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.talk_voice : unaccToVoice Fragments.English.Predicates.Verbal.talk.unaccusative = Minimalism.VoiceFlavor.agentive

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.arrive_voice : unaccToVoice Fragments.English.Predicates.Verbal.arrive.unaccusative = Minimalism.VoiceFlavor.nonThematic

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.seem_voice : unaccToVoice Fragments.English.Predicates.Verbal.seem.unaccusative = Minimalism.VoiceFlavor.nonThematic

In split-auxiliary languages (Italian, French, German), unaccusative verbs select be and unergative verbs select have. We verify this via canonicalSelection ∘ deriveTransitivityClass.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.whisper_canonical_aux : AuxiliaryVerbs.Selection.canonicalSelection (deriveTransitivityClass Fragments.English.Predicates.Verbal.whisper.toVerbCore) = AuxiliaryVerbs.Selection.PerfectAux.be

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.murmur_canonical_aux : AuxiliaryVerbs.Selection.canonicalSelection (deriveTransitivityClass Fragments.English.Predicates.Verbal.murmur.toVerbCore) = AuxiliaryVerbs.Selection.PerfectAux.be

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.speak_canonical_aux : AuxiliaryVerbs.Selection.canonicalSelection (deriveTransitivityClass Fragments.English.Predicates.Verbal.speak.toVerbCore) = AuxiliaryVerbs.Selection.PerfectAux.have

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.talk_canonical_aux : AuxiliaryVerbs.Selection.canonicalSelection (deriveTransitivityClass Fragments.English.Predicates.Verbal.talk.toVerbCore) = AuxiliaryVerbs.Selection.PerfectAux.have

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.whisper_levin_class : Fragments.English.Predicates.Verbal.whisper.levinClass = some LevinClass.mannerOfSpeaking

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.murmur_levin_class : Fragments.English.Predicates.Verbal.murmur.levinClass = some LevinClass.mannerOfSpeaking

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.speak_levin_class : Fragments.English.Predicates.Verbal.speak.levinClass = some LevinClass.mannerOfSpeaking

MoS verb subjects are volitional, sentient speakers — Dowty's proto-role counting yields P-Agent > P-Patient, predicting unergative. But QI says these verbs are unaccusative. This is a documented divergence between semantic proto-role predictions and syntactic diagnostics.

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.mosSubjectProfile : Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile

MoS subject entailment profile: volitional (P-Agent), sentient (P-Agent), exists independently (P-Agent), but no P-Patient entailments.

Equations

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

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_predicts_unergative : Semantics.Lexical.Verb.EntailmentProfile.predictsUnergative mosSubjectProfile = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_not_unaccusative_by_counting : Semantics.Lexical.Verb.EntailmentProfile.predictsUnaccusative mosSubjectProfile = false

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.whisper_dowty_diverges : Semantics.Lexical.Verb.EntailmentProfile.predictsUnergative mosSubjectProfile = true ∧ Fragments.English.Predicates.Verbal.whisper.unaccusative = true

Divergence: Dowty predicts MoS subjects are unergative, but QI classifies them as unaccusative.

The smuggling analysis (@cite{collins-2005}, applied to QI by @cite{storment-2026}) derives QI licensing from two independently motivated properties:

1. **Voice is non-phase** (= unaccusative): complement remains extractable
2. **Verb has a complement** (the quote): there is something to smuggle

We verify that `licensesQI` (defined in `Movement/Smuggling.lean` over
Voice + complement availability) matches the empirical QI diagnostic data
when applied to the Voice and complement type derived from each verb's
lexical entry. 

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.hasComplement (v : Core.Verbs.VerbCore) : Bool

Derive whether a verb has a complement (ComplementType ≠.none).

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.hasComplement v = (v.complementType != Core.Verbs.ComplementType.none)

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.voiceFor (v : Core.Verbs.VerbCore) : Minimalism.VoiceHead

Derive Voice head from unaccusativity annotation.

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.voiceFor v = if v.unaccusative = true then Minimalism.voiceAnticausative else Minimalism.voiceAgent

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.derivedQI (v : Core.Verbs.VerbCore) : Bool

Derived QI licensing: combines Voice (from unaccusativity) and complement availability (from complementType).

Equations

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

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.whisper_qi_derived : derivedQI Fragments.English.Predicates.Verbal.whisper.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.murmur_qi_derived : derivedQI Fragments.English.Predicates.Verbal.murmur.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.shout_qi_derived : derivedQI Fragments.English.Predicates.Verbal.shout.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.cry_qi_derived : derivedQI Fragments.English.Predicates.Verbal.cry.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.scream_qi_derived : derivedQI Fragments.English.Predicates.Verbal.scream.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mumble_qi_derived : derivedQI Fragments.English.Predicates.Verbal.mumble.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mutter_qi_derived : derivedQI Fragments.English.Predicates.Verbal.mutter.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.shriek_qi_derived : derivedQI Fragments.English.Predicates.Verbal.shriek.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.yell_qi_derived : derivedQI Fragments.English.Predicates.Verbal.yell.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.groan_qi_derived : derivedQI Fragments.English.Predicates.Verbal.groan.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.grumble_qi_derived : derivedQI Fragments.English.Predicates.Verbal.grumble.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.hiss_qi_derived : derivedQI Fragments.English.Predicates.Verbal.hiss.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.sigh_qi_derived : derivedQI Fragments.English.Predicates.Verbal.sigh.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.whimper_qi_derived : derivedQI Fragments.English.Predicates.Verbal.whimper.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.snap_qi_derived : derivedQI Fragments.English.Predicates.Verbal.snap.toVerbCore = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.speak_qi_blocked : derivedQI Fragments.English.Predicates.Verbal.speak.toVerbCore = false

speak is blocked: agentive Voice makes vP a phase (blocks smuggling), AND it has no complement (.none) — doubly ruled out.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.talk_qi_blocked : derivedQI Fragments.English.Predicates.Verbal.talk.toVerbCore = false

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.arrive_no_qi : derivedQI Fragments.English.Predicates.Verbal.arrive.toVerbCore = false

arrive is unaccusative but has no complement to smuggle — so it doesn't license QI. This is correct: *"arrived Mary" requires a fronted locative (LI), not a fronted quote (QI).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_data_consistent : (Data.qi_whisper.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.whisper.toVerbCore = true) ∧ (Data.qi_murmur.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.murmur.toVerbCore = true) ∧ (Data.qi_shout.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.shout.toVerbCore = true) ∧ (Data.qi_cry.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.cry.toVerbCore = true) ∧ (Data.qi_scream.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.scream.toVerbCore = true) ∧ (Data.qi_mumble.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.mumble.toVerbCore = true) ∧ (Data.qi_mutter.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.mutter.toVerbCore = true) ∧ (Data.qi_shriek.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.shriek.toVerbCore = true) ∧ (Data.qi_yell.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.yell.toVerbCore = true) ∧ (Data.qi_groan.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.groan.toVerbCore = true) ∧ (Data.qi_grumble.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.grumble.toVerbCore = true) ∧ (Data.qi_hiss.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.hiss.toVerbCore = true) ∧ (Data.qi_sigh.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.sigh.toVerbCore = true) ∧ (Data.qi_whimper.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.whimper.toVerbCore = true) ∧ (Data.qi_snap.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.snap.toVerbCore = true) ∧ (Data.qi_speak.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.speak.toVerbCore = true) ∧ (Data.qi_talk.result = Data.DiagnosticResult.passes) = (derivedQI Fragments.English.Predicates.Verbal.talk.toVerbCore = true)

Quotative inversion and locative inversion share the same mechanism (smuggling of VP to Spec-VoiceP, @cite{storment-2026} §6) but differ in their inputs and distribution:

- QI requires a quote complement; LI requires a fronted locative PP
- Both are subject to the transitivity constraint (§5): multiple DP
  arguments block inversion due to Case licensing limitations
- QI degrades with pronominal subjects; LI categorically blocks them

Despite sharing a mechanism, their distributional differences confirm
they are distinct diagnostic constructions with different triggers. 

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_li_diverge_on_whisper : Data.qi_whisper.result = Data.DiagnosticResult.passes ∧ Data.loc_whisper.result = Data.DiagnosticResult.marginal

whisper passes QI but is only marginal in LI — same mechanism (smuggling), different inputs.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.li_blocks_transitive : Data.li_kick.result = Data.DiagnosticResult.fails ∧ Data.qi_whisper_transitive.result = Data.DiagnosticResult.passes

LI blocks transitive verbs; QI with just a quote complement is fine, but both show a transitivity constraint with multiple DP arguments.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.li_vs_qi_pronouns : Data.li_arrive_pronoun.result = Data.DiagnosticResult.fails ∧ Data.qi_whisper_pronoun.result = Data.DiagnosticResult.marginal

LI categorically blocks pronominal subjects; QI merely degrades them.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_transitivity_constraint : Data.qi_whisper_double_obj.result = Data.DiagnosticResult.fails ∧ Data.qi_whisper_transitive.result = Data.DiagnosticResult.passes

The transitivity constraint (§5): QI is blocked when multiple DP arguments compete for Case licensing.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.li_arrive_smuggling_unified : unaccToVoice Fragments.English.Predicates.Verbal.arrive.unaccusative = Minimalism.VoiceFlavor.nonThematic ∧ Data.loc_arrive.result = Data.DiagnosticResult.passes

Unified smuggling analysis (§6): LI with arrive works because arrive projects non-thematic (non-phase) Voice, permitting VP to smuggle to Spec-VoiceP — the same mechanism that licenses QI.

MoS verbs participate in two seemingly opposite phenomena:

1. **MoS islands**: wh-extraction FROM WITHIN
   the complement is degraded (discourse backgroundedness)
2. **Quotative inversion**: VP-smuggling to Spec-VoiceP
   is grammatical (A-movement, not extraction from complement)

These are not contradictory — they're different operations:
- MoS islands: wh-movement from within CP complement (blocked by discourse)
- QI smuggling: A-movement of VP to Spec-VoiceP (licensed by syntax)

The asymmetry validates both analyses simultaneously: MoS islands are
discourse-sourced (not syntactic), so they don't block the syntactic
VP-movement that produces QI. 

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_island_compatible_with_qi : constraintSource ConstraintType.mannerOfSpeaking = IslandSource.discourse ∧ derivedQI Fragments.English.Predicates.Verbal.whisper.toVerbCore = true

MoS islands are discourse-sourced, not syntactic — so they don't block the syntactic smuggling operation that produces QI.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_extraction_asymmetry : constraintSource ConstraintType.mannerOfSpeaking = IslandSource.discourse ∧ derivedQI Fragments.English.Predicates.Verbal.whisper.toVerbCore = true ∧ derivedQI Fragments.English.Predicates.Verbal.murmur.toVerbCore = true ∧ derivedQI Fragments.English.Predicates.Verbal.shout.toVerbCore = true ∧ derivedQI Fragments.English.Predicates.Verbal.mumble.toVerbCore = true ∧ derivedQI Fragments.English.Predicates.Verbal.mutter.toVerbCore = true

The extraction asymmetry: sub-extraction from MoS complement is discourse-blocked, but whole-complement fronting (QI) is syntactically licensed. Same verbs, same complements, different operations, different sources.

The smuggling derivation of QI assigns each major constituent to a structural position. Each position has observable consequences that are tested against the §3 structural evidence data.

1. **Theme** → Spec-TP (A-movement): controls agreement, licenses
   raising, does NOT license parasitic gaps (A ≠ Ā)
2. **Agent** → Spec-vP (in-situ): conjoint domain in Setswana,
   does not control agreement (defective circumvention)
3. **VP** → Spec-VoiceP (smuggling): VP-internal material precedes
   Agent; vP-external adjuncts follow Agent
4. **Quote** → DiscourseP (clause-external): can split around
   V + Agent, need not be grammatical 

inductive Phenomena.ArgumentStructure.Unaccusativity.Bridge.QIPosition : Type

Structural position in QI derivation.

• specTP : QIPosition
• specVoiceP : QIPosition
• specvP : QIPosition
• discourseP : QIPosition

instance Phenomena.ArgumentStructure.Unaccusativity.Bridge.instDecidableEqQIPosition : DecidableEq QIPosition

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.instDecidableEqQIPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ArgumentStructure.Unaccusativity.Bridge.instReprQIPosition : Repr QIPosition

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.instReprQIPosition = { reprPrec := Phenomena.ArgumentStructure.Unaccusativity.Bridge.instReprQIPosition.repr }

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.instReprQIPosition.repr : QIPosition → ℕ → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIPosition : BEq QIPosition

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIPosition = { beq := Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIPosition.beq }

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIPosition.beq : QIPosition → QIPosition → Bool

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.ArgumentStructure.Unaccusativity.Bridge.QIDerivation : Type

The QI derivation assigns constituents to structural positions. Each position has testable predictions (§3).

• themePosition : QIPosition
• agentPosition : QIPosition
• vpPosition : QIPosition
• quotePosition : QIPosition

instance Phenomena.ArgumentStructure.Unaccusativity.Bridge.instReprQIDerivation : Repr QIDerivation

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.instReprQIDerivation = { reprPrec := Phenomena.ArgumentStructure.Unaccusativity.Bridge.instReprQIDerivation.repr }

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.instReprQIDerivation.repr : QIDerivation → ℕ → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIDerivation : BEq QIDerivation

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIDerivation = { beq := Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIDerivation.beq }

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIDerivation.beq : QIDerivation → QIDerivation → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Unaccusativity.Bridge.instBEqQIDerivation.beq x✝¹ x✝ = false

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.qiSmuggling : QIDerivation

The smuggling derivation of QI.

Equations

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

Each structural position predicts observable properties. We verify each prediction against the §3 data.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.theme_specTP_agreement : qiSmuggling.themePosition = QIPosition.specTP ∧ Data.qi_agreement_english.result = Data.DiagnosticResult.passes

Theme in Spec-TP → agreement can track agent via defective circumvention: probe first hits phi-deficient Theme, then optionally re-probes and finds Agent (§3.1).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.theme_specTP_setswana_sm17 : qiSmuggling.themePosition = QIPosition.specTP ∧ Data.qi_agreement_setswana.result = Data.DiagnosticResult.passes

Theme in Spec-TP → Setswana SM surfaces as default SM17 because Theme is phi-deficient; probe doesn't reach Agent (§3.1).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.theme_specTP_no_parasitic_gap : qiSmuggling.themePosition = QIPosition.specTP ∧ Data.qi_parasitic_gap_blocked.result = Data.DiagnosticResult.fails

Theme in Spec-TP → A-movement → parasitic gaps NOT licensed. A-movement chains cannot license PGs; only Ā-chains can (§3.2).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.theme_specTP_raising : qiSmuggling.themePosition = QIPosition.specTP ∧ Data.qi_raising.result = Data.DiagnosticResult.passes

Theme in Spec-TP → compatible with subject-to-subject raising. Theme can A-move through intermediate Spec-TP positions (§3.3).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.agent_specvP_conjoint : qiSmuggling.agentPosition = QIPosition.specvP ∧ Data.qi_conjoint_disjoint.result = Data.DiagnosticResult.fails

Agent in Spec-vP → Setswana disjoint morpheme blocked. Disjoint form requires the subject to be vP-external; Agent remains vP-internal in QI (§3.4).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.quote_discourseP_split : qiSmuggling.quotePosition = QIPosition.discourseP ∧ Data.qi_quote_split.result = Data.DiagnosticResult.passes

Quote in DiscourseP → quote can split around verb + agent. A constituent in Spec-TP cannot split; DiscourseP can (§3.5).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.quote_discourseP_nongrammatical : qiSmuggling.quotePosition = QIPosition.discourseP ∧ Data.qi_quote_nongrammatical.result = Data.DiagnosticResult.passes

Quote in DiscourseP → quote need not be grammatical. Clause-external status means quote is not subject to clausal well-formedness requirements (§3.5).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.vp_smuggling_ordering : qiSmuggling.vpPosition = QIPosition.specVoiceP ∧ Data.qi_ordering_complement.result = Data.DiagnosticResult.passes ∧ Data.qi_ordering_depictive.result = Data.DiagnosticResult.passes ∧ Data.qi_ordering_manner.result = Data.DiagnosticResult.passes ∧ Data.qi_ordering_purpose.result = Data.DiagnosticResult.passes

VP smuggling predicts: VP-internal material (complements) precedes Agent; vP-external material (adjuncts) follows Agent. The ordering data from Setswana (§2) confirms both predictions.

Levin & Rappaport @cite{levin-hovav-1995} predict unaccusativity from verb class membership: CoS classes (§45) predict unaccusative for their inchoative alternant, manner-of-motion (§51.3) predicts unergative, inherently directed motion (§51.1) predicts unaccusative, and emission classes (§43) predict unaccusative.

The function `LevinClass.predictsUnaccusative` (in RootDimensions.lean)
encodes these predictions. Here we verify them against Fragment entries
that carry both `.levinClass` and `.unaccusative` annotations. 

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.arrive_levin_agrees : Fragments.English.Predicates.Verbal.arrive.levinClass = some LevinClass.inherentlyDirectedMotion ∧ LevinClass.inherentlyDirectedMotion.predictsUnaccusative = true ∧ Fragments.English.Predicates.Verbal.arrive.unaccusative = true

arrive (§51.1 inherentlyDirectedMotion) → predicted + empirically unaccusative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.run_levin_agrees : Fragments.English.Predicates.Verbal.run.levinClass = some LevinClass.mannerOfMotion ∧ LevinClass.mannerOfMotion.predictsUnaccusative = false ∧ Fragments.English.Predicates.Verbal.run.unaccusative = false

run (§51.3 mannerOfMotion) → predicted + empirically unergative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.exist_levin_agrees : Fragments.English.Predicates.Verbal.exist.levinClass = some LevinClass.exist ∧ LevinClass.exist.predictsUnaccusative = true ∧ Fragments.English.Predicates.Verbal.exist.unaccusative = true

exist (§47) → predicted + empirically unaccusative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.appear_levin_agrees : Fragments.English.Predicates.Verbal.appear.levinClass = some LevinClass.appear ∧ LevinClass.appear.predictsUnaccusative = true ∧ Fragments.English.Predicates.Verbal.appear.unaccusative = true

appear (§48) → predicted + empirically unaccusative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.glow_levin_agrees : Fragments.English.Predicates.Verbal.glow.levinClass = some LevinClass.lightEmission ∧ LevinClass.lightEmission.predictsUnaccusative = true ∧ Fragments.English.Predicates.Verbal.glow.unaccusative = true

glow (§43.1 lightEmission) → predicted + empirically unaccusative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.buzz_levin_agrees : Fragments.English.Predicates.Verbal.buzz.levinClass = some LevinClass.soundEmission ∧ LevinClass.soundEmission.predictsUnaccusative = true ∧ Fragments.English.Predicates.Verbal.buzz.unaccusative = true

buzz (§43.2 soundEmission) → predicted + empirically unaccusative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.bleed_levin_agrees : Fragments.English.Predicates.Verbal.bleed.levinClass = some LevinClass.substanceEmission ∧ LevinClass.substanceEmission.predictsUnaccusative = true ∧ Fragments.English.Predicates.Verbal.bleed.unaccusative = true

bleed (§43.4 substanceEmission) → predicted + empirically unaccusative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.rust_levin_agrees : Fragments.English.Predicates.Verbal.rust.levinClass = some LevinClass.entitySpecificCoS ∧ LevinClass.entitySpecificCoS.predictsUnaccusative = true ∧ Fragments.English.Predicates.Verbal.rust.unaccusative = true

rust (§45.5 entitySpecificCoS) → predicted + empirically unaccusative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.fidget_levin_agrees : Fragments.English.Predicates.Verbal.fidget.levinClass = some LevinClass.bodyInternalMotion ∧ LevinClass.bodyInternalMotion.predictsUnaccusative = false ∧ Fragments.English.Predicates.Verbal.fidget.unaccusative = false

fidget (§49 bodyInternalMotion) → predicted + empirically unergative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.kick_levin_agrees : Fragments.English.Predicates.Verbal.kick.levinClass = some LevinClass.hit ∧ LevinClass.hit.predictsUnaccusative = false ∧ Fragments.English.Predicates.Verbal.kick.unaccusative = false

kick (§18.1 hit) → predicted + empirically not unaccusative.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_levin_diverges : LevinClass.mannerOfSpeaking.predictsUnaccusative = false ∧ Fragments.English.Predicates.Verbal.whisper.levinClass = some LevinClass.mannerOfSpeaking ∧ Fragments.English.Predicates.Verbal.whisper.unaccusative = true ∧ Fragments.English.Predicates.Verbal.speak.levinClass = some LevinClass.mannerOfSpeaking ∧ Fragments.English.Predicates.Verbal.speak.unaccusative = false

MoS verbs: Levin class does NOT predict unaccusativity (agentive manner activity), but they ARE empirically unaccusative (@cite{storment-2026} QI diagnostic). This divergence motivates Storment's syntactic analysis (smuggling) over a purely lexical-semantic account of unaccusativity.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_within_class_split : Fragments.English.Predicates.Verbal.whisper.levinClass = Fragments.English.Predicates.Verbal.speak.levinClass ∧ Fragments.English.Predicates.Verbal.whisper.unaccusative = true ∧ Fragments.English.Predicates.Verbal.speak.unaccusative = false

The MoS split: both whisper and speak are §37.3 mannerOfSpeaking, but they diverge on unaccusativity. Levin class membership alone cannot explain this.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.break_causativeInchoative_unaccusative : Fragments.English.Predicates.Verbal.break_.levinClass = some LevinClass.break_ ∧ LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.break_.predictsUnaccusative = true ∧ Fragments.English.Predicates.Verbal.break_.unaccusative = false

Break (§45.1): the Fragment entry is the transitive causative form (unaccusative = false), but the class predicts an unaccusative inchoative alternant ("the vase broke"). The causative/inchoative alternation is the bridge between the transitive entry and the predicted unaccusativity.