Clause Spine: Fine-Grained Clause Size

@cite{elkins-torrence-brown-2026} @cite{grimshaw-2005} @cite{wurmbrand-2014}

ComplementSize (ExtendedProjection/Basic.lean) classifies clausal complements by their highest functional head, which works well for tense-Agree transparency and CTP classification. But it can't distinguish VoiceP from ApplP, since both have fValue = 1. Languages like Mam need this distinction: =(y)a' appears when Voice⁰ is projected but not when only Appl⁰ is.

ClauseSpine records the full list of projected heads, enabling per-head projection queries.

structure Minimalism.ClauseSpine : Type

A clause spine: the ordered sequence of functional heads projected in a clause, from lowest (V) to highest (e.g., C). Unlike ComplementSize, which records only the highest head, ClauseSpine records every projected head, enabling per-head queries.

Example: a transitive clause with Voice projects [V, Appl, v, Voice], while an infinitival without Voice projects [V, Appl].

• projectedHeads : List Cat

  Projected heads, ordered bottom-up (V first, highest last). Non-empty: every clause projects at least a lexical head.

• nonempty : self.projectedHeads ≠ []

  The spine is non-empty

def Minimalism.instReprClauseSpine.repr : ClauseSpine → ℕ → Std.Format

Equations

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

instance Minimalism.instReprClauseSpine : Repr ClauseSpine

Equations

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

def Minimalism.ClauseSpine.projects (spine : ClauseSpine) (c : Cat) : Bool

Does this spine project a given functional head?

Equations

• spine.projects c = spine.projectedHeads.any fun (x : Minimalism.Cat) => x == c

def Minimalism.ClauseSpine.highestHead (spine : ClauseSpine) : Cat

The highest head in the spine (always exists by nonempty invariant).

Equations

• spine.highestHead = match spine.projectedHeads.getLast? with | some c => c | none => Minimalism.Cat.V

def Minimalism.ClauseSpine.lowestHead (spine : ClauseSpine) : Cat

The lowest (lexical) head in the spine.

Equations

• spine.lowestHead = match spine.projectedHeads.head? with | some c => c | none => Minimalism.Cat.V

def Minimalism.ClauseSpine.size (spine : ClauseSpine) : ℕ

Number of projected heads.

Equations

• spine.size = spine.projectedHeads.length

def Minimalism.ClauseSpine.applP : ClauseSpine

ApplP-sized clause: [V, Appl]. Infinitival complement without Voice. In Mam, this is the size of infinitival complements where =(y)a' is impossible — Voice is not projected, so there is no host for [oblique].

Equations

• Minimalism.ClauseSpine.applP = { projectedHeads := [Minimalism.Cat.V, Minimalism.Cat.Appl], nonempty := Minimalism.ClauseSpine.applP._proof_1 }

def Minimalism.ClauseSpine.bareVP : ClauseSpine

Bare VP: [V]. Minimal clause — just the lexical verb. In Mam, this is the size of infinitival complements: the embedded clause is just VP, lacking Voice, Appl, v.

Equations

• Minimalism.ClauseSpine.bareVP = { projectedHeads := [Minimalism.Cat.V], nonempty := Minimalism.ClauseSpine.bareVP._proof_1 }

def Minimalism.ClauseSpine.vP : ClauseSpine

vP-sized clause: [V, v]. Light verb shell without Voice or Appl.

Equations

• Minimalism.ClauseSpine.vP = { projectedHeads := [Minimalism.Cat.V, Minimalism.Cat.v], nonempty := Minimalism.ClauseSpine.vP._proof_1 }

def Minimalism.ClauseSpine.voiceP : ClauseSpine

VoiceP-sized clause: [V, Appl, v, Voice]. Projects Voice head. In Mam, this is the size of "aspectless" complements — Voice is projected, so [oblique] can be hosted, and =(y)a' is obligatory on oblique extraction.

Equations

• Minimalism.ClauseSpine.voiceP = { projectedHeads := [Minimalism.Cat.V, Minimalism.Cat.Appl, Minimalism.Cat.v, Minimalism.Cat.Voice], nonempty := Minimalism.ClauseSpine.voiceP._proof_1 }

def Minimalism.ClauseSpine.tP : ClauseSpine

TP-sized clause: [V, Appl, v, Voice, T]. Full inflectional domain.

Equations

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

def Minimalism.ClauseSpine.cP : ClauseSpine

CP-sized clause: [V, Appl, v, Voice, T, C]. Full finite clause.

Equations

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

theorem Minimalism.voiceP_has_voice : ClauseSpine.voiceP.projects Cat.Voice = true

VoiceP projects Voice.

theorem Minimalism.applP_lacks_voice : ClauseSpine.applP.projects Cat.Voice = false

ApplP does not project Voice. This is the key distinction that ComplementSize cannot capture (both have fValue = 1 as highest head).

theorem Minimalism.cP_has_voice : ClauseSpine.cP.projects Cat.Voice = true

CP projects Voice (inherited from the full spine).

theorem Minimalism.tP_has_voice : ClauseSpine.tP.projects Cat.Voice = true

TP projects Voice.

theorem Minimalism.bareVP_lacks_voice : ClauseSpine.bareVP.projects Cat.Voice = false

Bare VP does not project Voice.

theorem Minimalism.bareVP_lacks_appl : ClauseSpine.bareVP.projects Cat.Appl = false

Bare VP does not project Appl.

theorem Minimalism.vP_lacks_voice : ClauseSpine.vP.projects Cat.Voice = false

vP does not project Voice.

theorem Minimalism.applP_has_appl : ClauseSpine.applP.projects Cat.Appl = true

ApplP projects Appl.

theorem Minimalism.voiceP_applP_same_fLevel : fValue ClauseSpine.voiceP.highestHead = fValue ClauseSpine.applP.highestHead

VoiceP and ApplP have the same fValue for their highest head, showing why ComplementSize can't distinguish them.

theorem Minimalism.spine_size_ordering : ClauseSpine.applP.size < ClauseSpine.voiceP.size ∧ ClauseSpine.voiceP.size < ClauseSpine.tP.size ∧ ClauseSpine.tP.size < ClauseSpine.cP.size

Spine sizes are ordered: ApplP < vP < VoiceP < TP < CP.