Quotative Inversion as Smuggling

@cite{storment-2026}

Formalizes @cite{storment-2026}: the smuggling derivation of quotative inversion in English and Setswana.

Storment's central claims

• §2 + §3: In QI clauses ("Hello," said Mary), the VP containing the quote moves to a position above the agentive AGENT, which remains in-situ in Spec,vP. Evidence: agreement, parasitic gaps, raising, conjoint/disjoint marking in Setswana.
• §4: This is smuggling (@cite{collins-2005}): the VP moves to Spec,VoiceP, making the theme accessible to T⁰ for Case licensing. The smuggling projection is identified as VoiceP, which is not the external-argument-introducing head (departing from @cite{kratzer-1996}/Pylkkänen).
• §5: The transitivity constraint — QI is blocked when multiple DPs compete for Case licensing — falls out from the Case-licensing configuration after smuggling.
• §6: Locative inversion shares the same mechanism. QI and LI are both nonactive inverse-voice constructions.

Cross-paper meta-bridges (live elsewhere per CLAUDE.md convention)

The following comparisons are the formalizer's synthesis, not Storment's claims. They live in topic-named files alongside this study:

• ../Unaccusativity/ProtoRoles.lean — Dowty proto-role profiles vs. Storment's QI-based unaccusativity classification (the MoS divergence)
• ../Unaccusativity/VerbClasses.lean — Levin verb classes vs. the QI classification (alignment + the §37.3 within-class split)
• ../Unaccusativity/IslandSensitivity.lean — @cite{storment-2026}'s smuggling-licenses-QI prediction vs. @cite{lu-pan-degen-2025}'s discourse-sourced MoS island finding (compatibility, not contradiction)

§1 + §2. Lexical annotations and QI data

Per @cite{storment-2026}, every MoS verb passes the QI diagnostic and is classified unaccusative; the canonical communication verbs speak/ talk fail QI and are unergative. Quantified theorems collapse the per-verb pattern; specific instances are recoverable by fin_cases.

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.mosUnaccusatives : List Fragments.English.Predicates.Verbal.VerbEntry

MoS verbs annotated unaccusative on the basis of the QI diagnostic.

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.communicationUnergatives : List Fragments.English.Predicates.Verbal.VerbEntry

Canonical unergative communication verbs that fail QI.

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Bridge.communicationUnergatives = [Fragments.English.Predicates.Verbal.speak, Fragments.English.Predicates.Verbal.talk]

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_unaccusatives_annotated (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → v.unaccusative = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.communication_unergatives_annotated (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → v.unaccusative = false

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

§3. TransitivityClass derivation

Maps a VerbCore to its three-way transitivity classification used by the auxiliary-selection system (Phenomena/AuxiliaryVerbs/Selection.lean). Stays in this study file because TransitivityClass lives in Phenomena/ and cannot be imported by Theories/.

def Phenomena.ArgumentStructure.Unaccusativity.Bridge.deriveTransitivityClass (v : Semantics.Lexical.VerbCore) : AuxiliaryVerbs.Selection.TransitivityClass

Derive TransitivityClass from VerbCore fields.

Equations

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

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_unaccusatives_transitivity (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → deriveTransitivityClass v.toVerbCore = AuxiliaryVerbs.Selection.TransitivityClass.unaccusative

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.communication_unergatives_transitivity (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → deriveTransitivityClass v.toVerbCore = AuxiliaryVerbs.Selection.TransitivityClass.unergative

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

§4. Voice bridge

VerbCore.voiceFor (defined in Theories/Interfaces/SyntaxSemantics/ VerbSmuggling.lean) maps unaccusative→non-thematic Voice and unergative→agentive Voice. Per @cite{storment-2026}'s §4.3, the Voice head is the smuggling projection (not the external-argument introducer of @cite{kratzer-1996}); permitting smuggling is equivalent to being non-phase, which is equivalent to not introducing an external argument.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_unaccusatives_nonThematic_voice (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → v.voiceFor = Minimalist.voiceAnticausative

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.communication_unergatives_agentive_voice (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → v.voiceFor = Minimalist.voiceAgent

§5. Auxiliary selection bridge

In split-auxiliary languages (Italian, French, German), unaccusatives select be and unergatives select have.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_unaccusatives_select_be (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → AuxiliaryVerbs.Selection.canonicalSelection (deriveTransitivityClass v.toVerbCore) = AuxiliaryVerbs.Selection.PerfectAux.be

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.communication_unergatives_select_have (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → AuxiliaryVerbs.Selection.canonicalSelection (deriveTransitivityClass v.toVerbCore) = AuxiliaryVerbs.Selection.PerfectAux.have

§6. Levin §37.3 mannerOfSpeaking class membership

Pure data — the divergence and within-class split analysis lives in ../Unaccusativity/VerbClasses.lean.

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

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

§8. Smuggling derivation of QI

VerbCore.derivedQI (defined in Theories/Interfaces/SyntaxSemantics/ VerbSmuggling.lean) derives QI licensing from two independently motivated properties: (1) Voice is non-phase (= unaccusative); (2) verb has a complement (the quote).

These two properties are then verified against the empirical QI diagnostic data: every MoS unaccusative with a complement is correctly predicted to license QI; agentive speak/talk is correctly predicted to block QI; unaccusative arrive (no complement) is correctly predicted not to license QI (it requires LI, not QI).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.mos_unaccusatives_derivedQI (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → v.derivedQI = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.communication_unergatives_derivedQI (v : Fragments.English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → v.derivedQI = false

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

arrive is unaccusative but has no complement: 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_matches_derivedQI (p : Data.DiagnosticDatum × Semantics.Lexical.VerbCore) : p ∈ [(Data.qi_whisper, Fragments.English.Predicates.Verbal.whisper.toVerbCore), (Data.qi_murmur, Fragments.English.Predicates.Verbal.murmur.toVerbCore), (Data.qi_shout, Fragments.English.Predicates.Verbal.shout.toVerbCore), (Data.qi_cry, Fragments.English.Predicates.Verbal.cry.toVerbCore), (Data.qi_scream, Fragments.English.Predicates.Verbal.scream.toVerbCore), (Data.qi_mumble, Fragments.English.Predicates.Verbal.mumble.toVerbCore), (Data.qi_mutter, Fragments.English.Predicates.Verbal.mutter.toVerbCore), (Data.qi_shriek, Fragments.English.Predicates.Verbal.shriek.toVerbCore), (Data.qi_yell, Fragments.English.Predicates.Verbal.yell.toVerbCore), (Data.qi_groan, Fragments.English.Predicates.Verbal.groan.toVerbCore), (Data.qi_grumble, Fragments.English.Predicates.Verbal.grumble.toVerbCore), (Data.qi_hiss, Fragments.English.Predicates.Verbal.hiss.toVerbCore), (Data.qi_sigh, Fragments.English.Predicates.Verbal.sigh.toVerbCore), (Data.qi_whimper, Fragments.English.Predicates.Verbal.whimper.toVerbCore), (Data.qi_snap, Fragments.English.Predicates.Verbal.snap.toVerbCore), (Data.qi_speak, Fragments.English.Predicates.Verbal.speak.toVerbCore), (Data.qi_talk, Fragments.English.Predicates.Verbal.talk.toVerbCore)] → (p.1.result = Data.DiagnosticResult.passes ↔ p.2.derivedQI = true)

Consistency: each (verb, QI-datum) pair has its empirical result matching derivedQI. Pairs the diagnostic data in Unaccusativity/Data.lean with the smuggling prediction.

§9. QI ∥ LI distributional contrasts (Storment §6)

Storment §6: QI and LI share the smuggling mechanism but differ in their inputs (quote vs. locative PP) and distribution. Both are subject to the transitivity constraint (§5). The shared inverse-voice family membership is captured by Minimalist.qiCanonical and liCanonical in Theories/Syntax/Minimalism/Movement/InverseVoice.lean.

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.qi_transitivity_constraint : Data.qi_warn_double_obj.result = Data.DiagnosticResult.fails ∧ Data.qi_whisper_transitive.result = Data.DiagnosticResult.passes

The transitivity constraint (§5): QI is blocked with multiple DP arguments (using warn per Storment eq. 125, naturally ditransitive); QI is fine with a quote + PP goal.

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.li_blocks_transitive : Data.li_kick.result = Data.DiagnosticResult.fails

LI blocks transitive verbs, just as QI does.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.li_arrive_smuggling_unified : Fragments.English.Predicates.Verbal.arrive.voiceFor = Minimalist.voiceAnticausative ∧ Data.loc_arrive.result = Data.DiagnosticResult.passes

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

§11 + §12. The QI derivation (Storment §3 + §4)

The smuggling derivation assigns each major constituent to a structural position. Each position predicts observable consequences tested against the §3 structural-evidence data.

Quote vs. quotative operator (Storment §3.5, eq. 103). The quote itself is not in the syntactic derivation — it may be totally absent from QI clauses (Says me!). What sits in Spec,TP is a null quotative operator (the THEME), bound by a Discourse⁰[QUOT] head in DiscourseP. The fields below distinguish the operator's landing site (Spec,TP) from the quote's binding head (DiscourseP).

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

Structural position in the QI derivation.

• specTP : QIPosition
• specVoiceP : QIPosition
• specvP : QIPosition
• discourseQUOT : QIPosition

@[implicit_reducible]

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 ⋯

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

The QI derivation assigns four major constituents to structural positions. Note that quoteBinder is the binding head in DiscourseP, not the quote itself (which is not in the syntax — Storment §3.5).

• themePosition : QIPosition
• agentPosition : QIPosition
• vpPosition : QIPosition
• quoteBinder : QIPosition

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Storment's smuggling derivation of QI.

Equations

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

Each structural position predicts an observable property. We verify each prediction against the §3 data. The bridge theorems below pair the position assignment (Storment's claim) with the empirical observation (also Storment's claim).

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

Theme-as-operator in Spec,TP → agreement can track agent via defective circumvention (§3.1).

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

Theme-as-operator is phi-deficient → Setswana SM surfaces as default SM17 (§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-as-operator A-moves → cannot license parasitic gaps (§3.2).

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

Theme-as-operator A-moves → compatible with subject-to-subject raising (§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 (§3.4).

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.quote_discourseQUOT_split : qiSmuggling.quoteBinder = QIPosition.discourseQUOT ∧ Data.qi_quote_split.result = Data.DiagnosticResult.passes ∧ Data.qi_quote_nongrammatical.result = Data.DiagnosticResult.passes

Quote (separately from operator) bound by Discourse⁰[QUOT] → can split around verb + agent, need not be grammatical (§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 (§2).

§13. Inverse-voice family membership

QI is one instance of the inverse-voice family (§4.3 + §6 + §7). The canonical instance lives in Theories/Syntax/Minimalism/Movement/ InverseVoice.lean; here we just affirm membership.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_is_inverse_voice : Minimalist.qiCanonical.kind = Minimalist.InverseVoiceKind.quotativeInversion ∧ Minimalist.qiCanonical.licensed = true

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.qi_li_share_voice : Minimalist.qiCanonical.voice = Minimalist.liCanonical.voice

§14. Defective circumvention derives the agreement contrast

Storment §3.1.4 (eq. 59): the difference between Setswana QI agreement (always SM17 default) and English QI agreement (optionally tracks the postverbal agent) reduces to a single parameter — whether the probe T⁰ is allowed to re-probe past the defective quotative-theme operator. The defective-circumvention operation is in Theories/Syntax/Minimalism/ Probing/DefectiveCircumvention.lean; here we wire it to the QI agreement data.

The theorems abstract over the precise feature bundles and feature- compatibility predicate — Storment's substantive claim is that the operation is the same and only the allowReprobe parameter varies.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.setswana_vs_english_reduces_to_reprobe (probe alpha beta : Minimalist.FeatureBundle) (compat : Minimalist.FeatureBundle → Minimalist.FeatureBundle → Bool) (hd : Minimalist.Probing.DefectiveGoal probe alpha) (hc : compat alpha beta = true) : Minimalist.Probing.defectiveCircumvention probe alpha beta false compat = Minimalist.Probing.ProbingOutcome.defaultAgreement ∧ Minimalist.Probing.defectiveCircumvention probe alpha beta true compat = Minimalist.Probing.ProbingOutcome.trackLower

The same defective-probing situation produces Setswana's obligatory default agreement (no re-probe) and English's optional agent-tracking agreement (re-probe with compatible features) — a single Bool parameter accounts for the cross-linguistic split.

theorem Phenomena.ArgumentStructure.Unaccusativity.Bridge.english_qi_clash_on_incompatible_agent (probe alpha beta : Minimalist.FeatureBundle) (compat : Minimalist.FeatureBundle → Minimalist.FeatureBundle → Bool) (hd : Minimalist.Probing.DefectiveGoal probe alpha) (hc : compat alpha beta = false) : Minimalist.Probing.defectiveCircumvention probe alpha beta true compat = Minimalist.Probing.ProbingOutcome.featureClash

Storment's English-specific prediction: a 1st/2nd person agent (whose phi-features clash with the defective theme's [3]) cannot license re-probe — *"What do we do now?" ask we. The derivation crashes on feature incompatibility (eq. 46, page 14).