@[reducible, inline]

abbrev Minimalism.MValue : Type

An M-value is a bundle of morphological features (tense, agreement) shared between terminal nodes via GenHM.

We reuse FeatureBundle since M-values are grammatical features.

Equations

• Minimalism.MValue = Minimalism.FeatureBundle

inductive Minimalism.TerminalStrength : Type

Terminal strength determines whether a head can host M-value pronunciation.

Strong terminals can bear inflectional morphology. Weak terminals (Neg, Foc) cannot host inflection and act as chain-splitters when they intervene.

• strong : TerminalStrength
• weak : TerminalStrength

instance Minimalism.instDecidableEqTerminalStrength : DecidableEq TerminalStrength

Equations

• Minimalism.instDecidableEqTerminalStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.instReprTerminalStrength.repr : TerminalStrength → ℕ → Std.Format

Equations

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

instance Minimalism.instReprTerminalStrength : Repr TerminalStrength

Equations

• Minimalism.instReprTerminalStrength = { reprPrec := Minimalism.instReprTerminalStrength.repr }

def Minimalism.instBEqTerminalStrength.beq : TerminalStrength → TerminalStrength → Bool

Equations

• Minimalism.instBEqTerminalStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqTerminalStrength : BEq TerminalStrength

Equations

• Minimalism.instBEqTerminalStrength = { beq := Minimalism.instBEqTerminalStrength.beq }

def Minimalism.TerminalStrengthAssignment : Type

A language-specific assignment of strength to syntactic categories.

Equations

• Minimalism.TerminalStrengthAssignment = (Minimalism.Cat → Minimalism.TerminalStrength)

def Minimalism.defaultStrength : TerminalStrengthAssignment

Default strength assignment for English.

• V, T, C: strong (can host inflection)
• Neg, Foc: weak (cannot host inflection; split GenHM chains)
• All other categories: strong by default

Equations

• Minimalism.defaultStrength Minimalism.Cat.Neg = Minimalism.TerminalStrength.weak
• Minimalism.defaultStrength Minimalism.Cat.Foc = Minimalism.TerminalStrength.weak
• Minimalism.defaultStrength x✝ = Minimalism.TerminalStrength.strong

structure Minimalism.GenHMRelation : Type

The Generalized Head Movement relation.

GenHM relates two terminal nodes X (probe) and Y (goal) in a local syntactic configuration, sharing an M-value between them. This is an instance of Agree specialized for head displacement.

• probe : SyntacticObject

  The higher terminal (e.g., T or C) — the probe

• goal : SyntacticObject

  The lower terminal (e.g., V or Aux) — the goal

• mValue : MValue

  The shared morphological features

• feature : FeatureVal

  The feature type being shared (tense, phi, etc.)

• root : SyntacticObject

  The containing tree

• probe_commands_goal : cCommandsIn self.root self.probe self.goal

  Structural condition: probe c-commands goal

• goal_has_mvalue : hasValuedFeature self.mValue self.feature = true

  The goal bears valued M-features

• probe_needs_mvalue : hasUnvaluedFeature self.mValue self.feature = true

  The probe bears unvalued M-features

def Minimalism.genHM_to_agree (g : GenHMRelation) : AgreeRelation

GenHM is an instance of Agree: it relates a probe with unvalued features to a goal with valued features under c-command.

Equations

• Minimalism.genHM_to_agree g = { probe := g.probe, goal := g.goal, feature := g.feature, probeFeatures := g.mValue, goalFeatures := g.mValue }

theorem Minimalism.genHM_is_agree (g : GenHMRelation) : validAgree (genHM_to_agree g) g.root

A valid GenHM relation satisfies the conditions for valid Agree.

inductive Minimalism.ChainSplitReason : Type

The reason a GenHM chain is split, preventing M-value lowering.

@cite{arregi-pietraszko-2021} identify three structurally distinct configurations that split a chain (§4.1):

1. Split-by-Intervention: A weak terminal (Neg, Foc) between probe and goal blocks M-value transmission.
2. Split-by-Displacement: The probe is displaced (e.g., T to C in SAI), breaking the structural adjacency needed for lowering.
3. Split-by-Deletion: The goal is absent — deleted at PF (VP ellipsis) or anaphoric (tag questions) — so lowering has no target.

All three produce the same PF effect: the M-value cannot lower and is stranded on the probe.

• weakIntervener (cat : Cat) : ChainSplitReason

  A weak terminal intervenes between probe and goal (e.g., Neg in "Sue does not eat fish", Foc in "Sue DOES eat fish")

• probeDisplaced : ChainSplitReason

  The probe is displaced away from the goal (e.g., T displaced to C in SAI: "Where does Sue eat fish?")

• goalAbsent : ChainSplitReason

  The goal is absent — deleted (VP ellipsis: "She runs faster than he does") or anaphoric (tag questions: "She likes him, doesn't she?")

def Minimalism.instDecidableEqChainSplitReason.decEq (x✝ x✝¹ : ChainSplitReason) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.instDecidableEqChainSplitReason.decEq (Minimalism.ChainSplitReason.weakIntervener a) (Minimalism.ChainSplitReason.weakIntervener b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalism.instDecidableEqChainSplitReason.decEq (Minimalism.ChainSplitReason.weakIntervener cat) Minimalism.ChainSplitReason.probeDisplaced = isFalse ⋯
• Minimalism.instDecidableEqChainSplitReason.decEq (Minimalism.ChainSplitReason.weakIntervener cat) Minimalism.ChainSplitReason.goalAbsent = isFalse ⋯
• Minimalism.instDecidableEqChainSplitReason.decEq Minimalism.ChainSplitReason.probeDisplaced (Minimalism.ChainSplitReason.weakIntervener cat) = isFalse ⋯
• Minimalism.instDecidableEqChainSplitReason.decEq Minimalism.ChainSplitReason.probeDisplaced Minimalism.ChainSplitReason.probeDisplaced = isTrue ⋯
• Minimalism.instDecidableEqChainSplitReason.decEq Minimalism.ChainSplitReason.goalAbsent (Minimalism.ChainSplitReason.weakIntervener cat) = isFalse ⋯
• Minimalism.instDecidableEqChainSplitReason.decEq Minimalism.ChainSplitReason.goalAbsent Minimalism.ChainSplitReason.goalAbsent = isTrue ⋯

instance Minimalism.instDecidableEqChainSplitReason : DecidableEq ChainSplitReason

Equations

• Minimalism.instDecidableEqChainSplitReason = Minimalism.instDecidableEqChainSplitReason.decEq

def Minimalism.instReprChainSplitReason.repr : ChainSplitReason → ℕ → Std.Format

Equations

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

instance Minimalism.instReprChainSplitReason : Repr ChainSplitReason

Equations

• Minimalism.instReprChainSplitReason = { reprPrec := Minimalism.instReprChainSplitReason.repr }

instance Minimalism.instBEqChainSplitReason : BEq ChainSplitReason

Equations

• Minimalism.instBEqChainSplitReason = { beq := Minimalism.instBEqChainSplitReason.beq }

def Minimalism.instBEqChainSplitReason.beq : ChainSplitReason → ChainSplitReason → Bool

Equations

• Minimalism.instBEqChainSplitReason.beq (Minimalism.ChainSplitReason.weakIntervener a) (Minimalism.ChainSplitReason.weakIntervener b) = (a == b)
• Minimalism.instBEqChainSplitReason.beq Minimalism.ChainSplitReason.probeDisplaced Minimalism.ChainSplitReason.probeDisplaced = true
• Minimalism.instBEqChainSplitReason.beq Minimalism.ChainSplitReason.goalAbsent Minimalism.ChainSplitReason.goalAbsent = true
• Minimalism.instBEqChainSplitReason.beq x✝¹ x✝ = false

structure Minimalism.GenHMChain : Type

A GenHM chain between a probe and a goal, possibly split.

The chain captures the structural configuration relevant for PF spell-out: whether the M-value can lower from probe to goal, or is stranded on the probe. The splitReason field tracks both whether the chain is split and why.

• probeCat : Cat

  Category of the probe (T or C)

• goalCat : Cat

  Category of the goal (V)

• splitReason : Option ChainSplitReason

  Why the chain is split, if at all. none = clear chain.

• strength : TerminalStrengthAssignment

  The strength assignment for this language

def Minimalism.GenHMChain.isSplit (chain : GenHMChain) : Bool

Is the chain split? A split chain strands the M-value on the probe.

Equations

• chain.isSplit = chain.splitReason.isSome

def Minimalism.GenHMChain.wellFormed (chain : GenHMChain) : Bool

A chain is well-formed when split-by-intervention involves a genuinely weak head in the given strength assignment.

Equations

• chain.wellFormed = match chain.splitReason with | some (Minimalism.ChainSplitReason.weakIntervener cat) => chain.strength cat == Minimalism.TerminalStrength.weak | x => true

inductive Minimalism.SpellOutTarget : Type

Where the M-value is pronounced at PF.

• .onGoal: M-value lowers to the goal (= affix hopping / T-lowering)
• .onProbe: M-value stays on the probe (= "raising" / stranding)

• onGoal : SpellOutTarget
• onProbe : SpellOutTarget

instance Minimalism.instDecidableEqSpellOutTarget : DecidableEq SpellOutTarget

Equations

• Minimalism.instDecidableEqSpellOutTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.instReprSpellOutTarget.repr : SpellOutTarget → ℕ → Std.Format

Equations

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

instance Minimalism.instReprSpellOutTarget : Repr SpellOutTarget

Equations

• Minimalism.instReprSpellOutTarget = { reprPrec := Minimalism.instReprSpellOutTarget.repr }

def Minimalism.instBEqSpellOutTarget.beq : SpellOutTarget → SpellOutTarget → Bool

Equations

• Minimalism.instBEqSpellOutTarget.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqSpellOutTarget : BEq SpellOutTarget

Equations

• Minimalism.instBEqSpellOutTarget = { beq := Minimalism.instBEqSpellOutTarget.beq }

def Minimalism.spellOutTarget (chain : GenHMChain) : SpellOutTarget

Determine where the M-value is spelled out.

The M-value surfaces on the goal (lower terminal) unless the chain is split, in which case it is stranded on the probe (higher terminal). The reason for the split is irrelevant — only whether it is split.

Equations

• Minimalism.spellOutTarget chain = if chain.isSplit = true then Minimalism.SpellOutTarget.onProbe else Minimalism.SpellOutTarget.onGoal

def Minimalism.needsDoSupportGenHM (chain : GenHMChain) (probeHasContent : Bool) : Bool

The do-support condition.

Do-support is triggered when:

1. The M-value is stranded on the probe (chain is split), AND
2. The probe has no independent lexical content (is a contentless T head)

This is a PF repair strategy: the grammar inserts do to host tense features that cannot lower to V and have no other host.

Equations

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

theorem Minimalism.doSupport_is_lastResort (chain : GenHMChain) (probeHasContent : Bool) : needsDoSupportGenHM chain probeHasContent = true → spellOutTarget chain = SpellOutTarget.onProbe ∧ probeHasContent = false

Do-support is a last resort: it is only used when the M-value cannot reach the goal AND the probe cannot host it independently.

theorem Minimalism.lowering_when_not_split (chain : GenHMChain) (h : chain.isSplit = false) : spellOutTarget chain = SpellOutTarget.onGoal

Theorem 1: Lowering when chain is clear.

When the chain is not split, the M-value surfaces on the goal (= T-lowering / affix hopping).

theorem Minimalism.raising_when_split (chain : GenHMChain) (h : chain.isSplit = true) : spellOutTarget chain = SpellOutTarget.onProbe

Theorem 2: Raising when chain is split.

When the chain is split (by intervention, displacement, or deletion), the M-value surfaces on the probe (= "raising" / stranding).

theorem Minimalism.doSupport_iff_split_and_empty (chain : GenHMChain) (probeContent : Bool) : needsDoSupportGenHM chain probeContent = true ↔ chain.isSplit = true ∧ probeContent = false

Theorem 3: Do-support iff split and contentless.

Do-support is triggered iff (a) the chain is split AND (b) the probe has no lexical content.

theorem Minimalism.doSupport_uniform_across_contexts (chain₁ chain₂ : GenHMChain) (content₁ content₂ : Bool) (h_same_split : chain₁.isSplit = chain₂.isSplit) (h_same_content : content₁ = content₂) : needsDoSupportGenHM chain₁ content₁ = needsDoSupportGenHM chain₂ content₂

Theorem 4: Do-support is uniform across contexts.

For ANY GenHM chain with the same split status and probe content, do-support is triggered or not uniformly. The specific reason for the split (intervention, displacement, deletion) is irrelevant. This is the parallelism theorem.

theorem Minimalism.auxiliaries_dont_need_doSupport (chain : GenHMChain) : needsDoSupportGenHM chain true = false

Theorem 5: Auxiliaries don't need do-support.

When the probe IS the auxiliary (T = Aux with lexical content), do-support is never needed, regardless of chain structure.

theorem Minimalism.lexical_verb_needs_doSupport_when_split (chain : GenHMChain) (h : chain.isSplit = true) : needsDoSupportGenHM chain false = true

Corollary: Lexical verbs need do-support when chain is split.

inductive Minimalism.HeadDisplacementExt : Type

Extended head displacement classification.

Adds GenHM as a third option alongside syntactic movement and amalgamation.

• syntactic : Movement → HeadDisplacementExt
• amalgam : Amalgamation → HeadDisplacementExt
• genHM : GenHMRelation → HeadDisplacementExt

theorem Minimalism.genHM_subsumes_raising_lowering (chain : GenHMChain) : spellOutTarget chain = SpellOutTarget.onGoal ∨ spellOutTarget chain = SpellOutTarget.onProbe

GenHM subsumes both "raising" and "lowering" as surface realizations of a single operation.

def Minimalism.genHM_to_vMovementParam (chain : GenHMChain) : VMovementParam

GenHM chain structure determines the surface pattern captured by VMovementParam.

Equations

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

theorem Minimalism.genHM_clear_chain_is_raises (chain : GenHMChain) (h : chain.isSplit = false) : genHM_to_vMovementParam chain = VMovementParam.raises

When the chain is clear, the surface pattern is V-raising.

theorem Minimalism.genHM_split_chain_is_inSitu (chain : GenHMChain) (h : chain.isSplit = true) : genHM_to_vMovementParam chain = VMovementParam.inSitu

When the chain is split, the surface pattern is V-in-situ.