@cite{olivier-2026} — Auxiliary Switch in Romance restructuring

Olivier (2026) analyses Auxiliary Switch (AS) in Romance restructuring clauses: in [Modal + BE-selecting-Infinitive] configurations, the matrix auxiliary surfaces as BE rather than its expected HAVE. The phenomenon is attested across Romance and in earlier French; the paper focuses on Modern Italian and diachronic French.

Three structural conditions

The paper argues that AS arises only when all three conditions hold:

1. Matrix verb is modal (e.g. vouloir 'want', pouvoir 'can').
2. Matrix verb is in compound tense (HAVE/BE + participle).
3. Embedded verb is BE-selecting — unaccusative or reflexive.

Trigger condition for reflexive complements

When the embedded verb is reflexive, AS is licensed only if the reflexive clitic climbs into the matrix domain. A reflexive clitic that stays low does not trigger AS. With unaccusative embedded verbs, no overt clitic is needed: AS is licensed by the embedded verb's ID-feature alone.

Refinement of @cite{harley-ritter-2002}

Olivier extends the person-feature geometry with an ID-subfeature (a referential-identity index). Two pronouns can share φ-values yet differ in ID. Auxiliary selection by T is then sensitive to ID-identity between T and vAux: BE iff T[ID:α] = vAux[ID:α], HAVE otherwise. Reflexive clitics carry an unvalued ID that gets valued through binding by Voice*, which is how clitic climbing of a reflexive equates IDs across the matrix and embedded domains and triggers AS.

Diachronic French scope

The paper documents AS in French across the 14th–19th centuries, with the construction declining in lockstep with the loss of clitic climbing. The decade-binned counts in the paper's reflexive-with-climbing table show a steady drop; we encode a representative subset below — not the full corpus.

Connection to TransferStyle

The KEEP / SHARE / DONATE distinction in Minimalist.FeatureInheritance.style parametrizes whether a language permits AS. Modern French has lost the .share option on the relevant Voice* → vMOD edge (giving KEEP); Italian permits it optionally; Sardinian-style varieties realise it obligatorily. We do not formalise the language-level configuration here; this study file commits only to the per-clause prediction.

Analytic commitments and empirical caveats

DM elsewhere inversion (vs @cite{amato-2025})

Olivier (rule 55) takes HAVE as the more specific allomorph and BE as elsewhere. @cite{amato-2025} (rule 48) takes the opposite convention: HAVE is vAux[Pers:α] and BE is the elsewhere allomorph. This inversion is load-bearing for Olivier's account of how Modern French acquirers default to a non-AS grammar (HAVE-elsewhere is the unmarked acquirer's hypothesis). The two analyses are formalised as parallel theory instances in this file and in Amato2025.lean; neither is canonical at this layer.

19th-century counterexamples

The diachronic French corpus shows roughly 29% of climbing-with- modal-with-compound-with-reflexive cases in 1800–1849 not exhibiting AS. Olivier attributes these to Chateaubriand-stylistic decorum (Iglesias 2015). The categorical generalisation formalised below should therefore be read as "strong tendency", not exceptionless. The decorum-based attribution is post-hoc and unfalsifiable; a future revision should encode exception rates by period rather than treating the generalisation as universally quantified.

Modern French data skepticism

The Modern French AS attestations in the paper's appendix include online forum posts where the author notes spelling errors in homophonous infinitive/participle pairs (pu/pues, déplacer/déplacées). These could be performance errors rather than grammatical AS. We do not encode Modern French AS as a theorem in this file; we encode only the diachronic French (14th–19th c.) and the Italian/Sardinian generalisations.

Matrix-verb taxonomy and clitic position

inductive Phenomena.AuxiliaryVerbs.Studies.Olivier2026.RestructuringMatrix : Type

The matrix verb's restructuring type. Only .modal matrix verbs can host Auxiliary Switch (@cite{olivier-2026}). Control and raising matrices are not restructuring heads in the relevant sense; .none is for non-restructuring contexts.

• modal : RestructuringMatrix
• control : RestructuringMatrix
• raising : RestructuringMatrix
• none : RestructuringMatrix

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqRestructuringMatrix : DecidableEq RestructuringMatrix

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqRestructuringMatrix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRestructuringMatrix.repr : RestructuringMatrix → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRestructuringMatrix : Repr RestructuringMatrix

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRestructuringMatrix = { reprPrec := Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRestructuringMatrix.repr }

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.RestructuringMatrix.isModal : RestructuringMatrix → Bool

Whether this matrix is a modal restructuring head — the only case that licenses AS (@cite{olivier-2026}).

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.RestructuringMatrix.modal.isModal = true
• x✝.isModal = false

inductive Phenomena.AuxiliaryVerbs.Studies.Olivier2026.RefCliticPosition : Type

Position of an embedded reflexive clitic relative to the matrix domain. .climbed means the clitic surfaces in the matrix (clitic climbing); .low means it stays in the embedded clause; .none means there is no reflexive (e.g. unaccusative or transitive complement).

• none : RefCliticPosition
• low : RefCliticPosition
• climbed : RefCliticPosition

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqRefCliticPosition : DecidableEq RefCliticPosition

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqRefCliticPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRefCliticPosition : Repr RefCliticPosition

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRefCliticPosition = { reprPrec := Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRefCliticPosition.repr }

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRefCliticPosition.repr : RefCliticPosition → ℕ → Std.Format

Equations

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

Restructuring clauses

structure Phenomena.AuxiliaryVerbs.Studies.Olivier2026.RestructuringClause : Type

A [Modal + Infinitive] restructuring clause as @cite{olivier-2026} models it. The four fields are exactly the structural diagnostics the AS rule consults.

• matrixModal : Bool

  Is the matrix a modal restructuring head?

• compoundTense : Bool

  Is the matrix in a compound (HAVE/BE + participle) tense?

• embeddedClass : Selection.TransitivityClass

  Transitivity class of the embedded verb.

• refCliticPos : RefCliticPosition

  Position of the embedded reflexive clitic, if any.

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqRestructuringClause : DecidableEq RestructuringClause

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqRestructuringClause = Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqRestructuringClause.decEq

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqRestructuringClause.decEq (x✝ x✝¹ : RestructuringClause) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRestructuringClause : Repr RestructuringClause

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRestructuringClause = { reprPrec := Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRestructuringClause.repr }

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprRestructuringClause.repr : RestructuringClause → ℕ → Std.Format

Equations

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

The Auxiliary Switch predicate

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.AuxiliarySwitchOccurs (c : RestructuringClause) : Prop

Does this restructuring clause exhibit Auxiliary Switch?

Per @cite{olivier-2026}, AS occurs iff: (1) the matrix is modal, AND (2) the matrix is in a compound tense, AND (3) the embedded verb is BE-selecting (unaccusative or reflexive), AND (4) if the embedded verb is reflexive, the clitic has climbed to the matrix.

Conditions (1)–(3) are necessary; condition (4) is the reflexive-specific trigger. Unaccusative complements license AS without any overt clitic trigger.

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidablePredRestructuringClauseAuxiliarySwitchOccurs : DecidablePred AuxiliarySwitchOccurs

Equations

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

inductive Phenomena.AuxiliaryVerbs.Studies.Olivier2026.ASCondition : Type

The three (purely structural) preconditions on AS, used as discriminators in completeness theorems below.

• matrixIsModal : ASCondition
• matrixInCompoundTense : ASCondition
• embeddedSelectsBe : ASCondition

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqASCondition : DecidableEq ASCondition

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqASCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprASCondition.repr : ASCondition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprASCondition : Repr ASCondition

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprASCondition = { reprPrec := Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprASCondition.repr }

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.conditionsSatisfied (c : RestructuringClause) : List ASCondition

The list of necessary AS conditions a clause satisfies (excluding the reflexive-specific climbing trigger). A clause satisfies all three iff AS is structurally possible — climbing then decides whether AS actually occurs in the reflexive case.

Equations

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

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.predictedMatrixAux (c : RestructuringClause) : Selection.PerfectAux

The matrix auxiliary actually predicted for a restructuring clause: BE if AS is triggered, HAVE otherwise. The HAVE default matches what a modal (unergative-like) matrix verb would select on its own argument structure.

Equations

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

Examples (paper examples 1–3, schematic)

These are schematic instantiations of the configurations used in the paper's introductory examples. We do not cite paper-internal example or page numbers here (the brief flagged this as a hallucination risk); the gloss strings describe the configuration in content terms.

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.haveWantTransitive : RestructuringClause

HAVE-want (no AS): modal in compound tense, but the embedded verb is transitive — fails condition (3). Predicts HAVE.

Equations

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

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.beWantCome : RestructuringClause

BE-want-come: modal in compound tense, embedded unaccusative — AS is triggered, no clitic needed. Predicts BE.

Equations

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

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.beWantReflexiveClimbed : RestructuringClause

BE-want-REFL-hide: modal in compound tense, embedded reflexive with the clitic climbed to the matrix. AS is triggered. Predicts BE.

Equations

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

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.haveWantReflexiveLow : RestructuringClause

HAVE-want-REFL-hide: same as above but the reflexive clitic stays low. Trigger fails — AS does not apply. Predicts HAVE.

Equations

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

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.haveControlUnaccusative : RestructuringClause

Non-modal control matrix: cannot trigger AS even with a BE-selecting complement. Predicts HAVE.

Equations

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

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.simpleTenseModal : RestructuringClause

Modal in simple (non-compound) tense: AS requires a compound matrix, so this predicts HAVE (vacuously — there is no perfect auxiliary to switch).

Equations

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

Diachronic French sample (representative subset of Table 1)

inductive Phenomena.AuxiliaryVerbs.Studies.Olivier2026.FrenchPeriod : Type

A coarse decade-binned period for the diachronic French data.

• p1300_1349 : FrenchPeriod
• p1450_1499 : FrenchPeriod
• p1550_1599 : FrenchPeriod
• p1650_1699 : FrenchPeriod
• p1750_1799 : FrenchPeriod
• p1850_1899 : FrenchPeriod

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqFrenchPeriod : DecidableEq FrenchPeriod

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instDecidableEqFrenchPeriod x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprFrenchPeriod : Repr FrenchPeriod

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprFrenchPeriod = { reprPrec := Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprFrenchPeriod.repr }

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprFrenchPeriod.repr : FrenchPeriod → ℕ → Std.Format

Equations

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

structure Phenomena.AuxiliaryVerbs.Studies.Olivier2026.DiachronicDatum : Type

A diachronic data point: counts of AS vs no-AS tokens in reflexive-with-climbing complements for a given period.

The figures here are a representative subset of the decade-binned counts the paper reports — not the full corpus. Quantitative claims should be checked against the published table; this sample captures the qualitative trend (AS attested early, declining over the span, near-vanishing by the 19th c.).

• period : FrenchPeriod
• asCount : ℕ
• noSwitchCount : ℕ
• hasClimbing : Bool

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprDiachronicDatum.repr : DiachronicDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprDiachronicDatum : Repr DiachronicDatum

Equations

• Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprDiachronicDatum = { reprPrec := Phenomena.AuxiliaryVerbs.Studies.Olivier2026.instReprDiachronicDatum.repr }

def Phenomena.AuxiliaryVerbs.Studies.Olivier2026.diachronicSample : List DiachronicDatum

Representative subset of the paper's reflexive-with-climbing table. Not the full corpus. Numbers are illustrative of the declining trajectory; verify against the published source for any quantitative claim.

Equations

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

Theorems

theorem Phenomena.AuxiliaryVerbs.Studies.Olivier2026.as_requires_modal (c : RestructuringClause) (h : c.matrixModal = false) : ¬AuxiliarySwitchOccurs c

A non-modal matrix never triggers Auxiliary Switch.

theorem Phenomena.AuxiliaryVerbs.Studies.Olivier2026.as_requires_compound (c : RestructuringClause) (h : c.compoundTense = false) : ¬AuxiliarySwitchOccurs c

A non-compound matrix tense never triggers Auxiliary Switch.

theorem Phenomena.AuxiliaryVerbs.Studies.Olivier2026.as_requires_be_selecting (c : RestructuringClause) (h : c.embeddedClass = Selection.TransitivityClass.transitive) : ¬AuxiliarySwitchOccurs c

A transitive embedded verb never triggers Auxiliary Switch.

Per-example smoke tests

Single-witness checks on the example clauses defined above. The
universally-quantified versions below are the load-bearing claims;
these document expected outputs. 

Universally-quantified predictions

theorem Phenomena.AuxiliaryVerbs.Studies.Olivier2026.reflexive_climbing_triggers_as (c : RestructuringClause) (hM : c.matrixModal = true) (hC : c.compoundTense = true) (hRefl : c.embeddedClass = Selection.TransitivityClass.reflexive) (hClimb : c.refCliticPos = RefCliticPosition.climbed) : AuxiliarySwitchOccurs c

For any modal-compound-reflexive clause with a climbed clitic, @cite{olivier-2026} predicts AS. Generalizes the one-witness smoke test above.

theorem Phenomena.AuxiliaryVerbs.Studies.Olivier2026.reflexive_low_no_as (c : RestructuringClause) (hRefl : c.embeddedClass = Selection.TransitivityClass.reflexive) (hLow : c.refCliticPos ≠ RefCliticPosition.climbed) : ¬AuxiliarySwitchOccurs c

For any modal-compound-reflexive clause whose clitic stays low, AS does NOT trigger — climbing is the load-bearing trigger condition (one of @cite{olivier-2026}'s central empirical claims).

theorem Phenomena.AuxiliaryVerbs.Studies.Olivier2026.unaccusative_no_clitic_triggers_as (c : RestructuringClause) (hM : c.matrixModal = true) (hC : c.compoundTense = true) (hUnacc : c.embeddedClass = Selection.TransitivityClass.unaccusative) : AuxiliarySwitchOccurs c

For any modal-compound-unaccusative clause with no clitic, AS is predicted even without a climbing trigger — unaccusatives carry the relevant ID-feature inherently.

Bridge to canonical (non-restructuring) auxiliary selection

theorem Phenomena.AuxiliaryVerbs.Studies.Olivier2026.selection_matches_canonical_outside_restructuring (c : RestructuringClause) (h : ¬AuxiliarySwitchOccurs c) : predictedMatrixAux c = Selection.canonicalSelection Selection.TransitivityClass.unergative

For clauses that fail any AS condition, the predicted matrix auxiliary equals HAVE — matching canonicalSelection .unergative (modal verbs being unergative-like). This is true by definition of predictedMatrixAux (it returns HAVE in the non-AS branch); the theorem documents the design intent — outside the restructuring window, the matrix auxiliary is whatever its own argument structure dictates under the canonical Burzio rule.