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 Minimalist.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 Minimalist.instReprClauseSpine.repr : ClauseSpine → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprClauseSpine : Repr ClauseSpine

Equations

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

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

Does this spine project a given functional head?

Equations

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

def Minimalist.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 => Minimalist.Cat.V

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

The lowest (lexical) head in the spine.

Equations

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

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

Number of projected heads.

Equations

• spine.size = spine.projectedHeads.length

def Minimalist.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

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

def Minimalist.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

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

def Minimalist.ClauseSpine.vP : ClauseSpine

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

Equations

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

def Minimalist.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

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

def Minimalist.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 Minimalist.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.

def Minimalist.ClauseSpine.nmlzP : ClauseSpine

NmlzP-sized clause: [V, Appl, v, Voice, T, Nmlz]. Hindi nominalized clause. @cite{keine-2020} ch. 2: NmlzP is a distinct clause type from CP — their transparency profiles are incomparable (NmlzP blocks Ā but not wh; CP blocks wh but not Ā in Hindi).

Equations

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

def Minimalist.ClauseSpine.forceP : ClauseSpine

ForceP-sized clause: [V, Appl, v, Voice, T, C, Force]. German V2 clause. @cite{keine-2020} ch. 4: V2 clauses in German are structurally larger than V-final (CP) clauses — they project ForceP above CP.

Equations

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

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

VoiceP projects Voice.

theorem Minimalist.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 Minimalist.cP_has_voice : ClauseSpine.cP.projects Cat.Voice = true

CP projects Voice (inherited from the full spine).

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

TP projects Voice.

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

Bare VP does not project Voice.

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

Bare VP does not project Appl.

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

vP does not project Voice.

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

ApplP projects Appl.

theorem Minimalist.nmlzP_has_nmlz : ClauseSpine.nmlzP.projects Cat.Nmlz = true

NmlzP projects Nmlz but not C.

theorem Minimalist.nmlzP_lacks_c : ClauseSpine.nmlzP.projects Cat.C = false

theorem Minimalist.cP_lacks_nmlz : ClauseSpine.cP.projects Cat.Nmlz = false

CP projects C but not Nmlz.

theorem Minimalist.forceP_has_force : ClauseSpine.forceP.projects Cat.Force = true

ForceP projects Force and C.

theorem Minimalist.forceP_has_c : ClauseSpine.forceP.projects Cat.C = true

theorem Minimalist.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.

def Minimalist.ClauseSpine.fLevel (spine : ClauseSpine) : ℕ

The F-level of a clause spine: the fValue of its highest projected head. This bridges ClauseSpine (concrete head list) to ExtendedProjection's F-value hierarchy, enabling @cite{keine-2019}'s transparency calculations.

Example: ClauseSpine.cP.fLevel = 6 (C is F6), ClauseSpine.tP.fLevel = 2 (T is F2).

Equations

• spine.fLevel = Minimalist.fValue spine.highestHead

theorem Minimalist.cP_fLevel : ClauseSpine.cP.fLevel = 6

CP-sized clauses are F6.

theorem Minimalist.tP_fLevel : ClauseSpine.tP.fLevel = 2

TP-sized clauses are F2.

theorem Minimalist.vP_fLevel : ClauseSpine.vP.fLevel = 1

vP-sized clauses are F1.

theorem Minimalist.voiceP_fLevel : ClauseSpine.voiceP.fLevel = 1

VoiceP-sized clauses are F1.

theorem Minimalist.nmlzP_fLevel : ClauseSpine.nmlzP.fLevel = 3

NmlzP-sized clauses are F3 (same as FinP).

theorem Minimalist.forceP_fLevel : ClauseSpine.forceP.fLevel = 6

ForceP-sized clauses are F6 (same as CP in fValue, but structurally larger).

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

Spine sizes are ordered: ApplP < vP < VoiceP < TP < CP < ForceP. NmlzP has the same size as CP (both have 6 projected heads).

theorem Minimalist.nmlzP_cP_same_size : ClauseSpine.nmlzP.size = ClauseSpine.cP.size

NmlzP and CP have the same number of projected heads — their difference is in WHICH heads are projected, not how many.