Classification of Merge into Three Combination Schemata

@cite{mueller-2013}

Explicit classification of Minimalist Merge operations into @cite{mueller-2013}'s three universal combination schemata: Head-Complement, Head-Specifier, Head-Filler.

The existing MergeUnification.lean proves that Internal and External Merge are the same operation. This file further classifies Merge by combination kind:

Merge type	Precondition	Schema
External (selection holds)	selects a b	Head-Complement
External (specifier)	neither selects, arg is maximal	Head-Specifier
Internal	contains target mover	Head-Filler

MCB alignment

Per @cite{marcolli-chomsky-berwick-2025} §1.13.6, head identification is parametric over a HeadFunction. All head-aware definitions in this file take h : HeadFunction explicitly; there is no hidden default. Callers wanting English-like leftmost-headed semantics pass HeadFunction.leftSpine; derivation-anchored Studies pass the head function tracked through the derivation; etc.

Connection to @cite{mueller-2013}

• §2.1: External Merge with selection ≈ Head-Complement
• §2.2: External Merge without selection ≈ Head-Specifier
• §2.3: Internal Merge ≈ Head-Filler

Selection (LIToken-level primitive + h-parametric SO wrapper)

def Minimalist.LIToken.selects (selector selected : LIToken) : Prop

LIToken-level c-selection: selector selects selected iff selector's outermost selectional feature equals selected's outer category. Pure LIToken relation; no SO structure involved.

Equations

• selector.selects selected = (List.head? selector.item.outerSel = some selected.item.outerCat)

@[implicit_reducible]

instance Minimalist.instDecidableSelects (lt1 lt2 : LIToken) : Decidable (lt1.selects lt2)

Equations

• Minimalist.instDecidableSelects lt1 lt2 = id inferInstance

def Minimalist.selects (h : HeadFunction) (a b : SyntacticObject) : Prop

SO-level c-selection parameterised over a head function: a selects b (under h) iff h's head-leaf for a selects h's head-leaf for b.

Equations

• Minimalist.selects h a b = (h.head a).selects (h.head b)

@[implicit_reducible]

noncomputable instance Minimalist.instDecidableSelects_1 (h : HeadFunction) (a b : SyntacticObject) : Decidable (selects h a b)

Equations

• Minimalist.instDecidableSelects_1 h a b = id inferInstance

Classification of Merge

noncomputable def Minimalist.classifyExternalMerge (h : HeadFunction) (a b : SyntacticObject) : Core.CombinationKind

Classify an External Merge under head function h.

Equations

• Minimalist.classifyExternalMerge h a b = if Minimalist.selects h a b ∨ Minimalist.selects h b a then Core.CombinationKind.headComplement else Core.CombinationKind.headSpecifier

def Minimalist.classifyInternalMerge : Core.CombinationKind

Classify an Internal Merge (head-function-independent: IM is always Head-Filler regardless of which side projects).

Equations

• Minimalist.classifyInternalMerge = Core.CombinationKind.headFiller

Which daughter is the head?

noncomputable def Minimalist.mergeHead (h : HeadFunction) (a b result : SyntacticObject) : Option SyntacticObject

Determine which daughter is the head of a Merge under head function h. The head is the daughter whose head leaf agrees with the result's.

Equations

• Minimalist.mergeHead h a b result = if h.head result = h.head a then some a else if h.head result = h.head b then some b else none

Key theorems

theorem Minimalist.selection_implies_headComplement (h : HeadFunction) (a b : SyntacticObject) (hs : selects h a b) : classifyExternalMerge h a b = Core.CombinationKind.headComplement

External Merge with selection is Head-Complement (under any h).

theorem Minimalist.no_selection_implies_headSpecifier (h : HeadFunction) (a b : SyntacticObject) (ha : ¬selects h a b) (hb : ¬selects h b a) : classifyExternalMerge h a b = Core.CombinationKind.headSpecifier

External Merge without selection is Head-Specifier (under any h).

theorem Minimalist.internal_merge_is_headFiller : classifyInternalMerge = Core.CombinationKind.headFiller

Internal Merge is always Head-Filler.

theorem Minimalist.classify_external_exhaustive (h : HeadFunction) (a b : SyntacticObject) : classifyExternalMerge h a b = Core.CombinationKind.headComplement ∨ classifyExternalMerge h a b = Core.CombinationKind.headSpecifier

The classification is exhaustive (under any h).

theorem Minimalist.head_node_eq_daughter (h : HeadFunction) (a b : SyntacticObject) : h.head (a.node b) = h.head a ∨ h.head (a.node b) = h.head b

Head Feature Principle (MCB §1.13.6 / Minimalist analogue): under any head function h and the externalize choice it supplies, h.head (.node a b) is one of h.head a or h.head b.

TODO: with headAt h so := leftmostLeafPlanar (h.section_.σ so), proving this requires reasoning about what h.section_.σ (a*b) looks like — concretely, that it's some planar tree whose leftmost leaf descends from either a or b. This needs a coherence lemma about how externalize interacts with binary nodes, which is part of the Tier A cascade.

Concrete sanity-check examples (D-N selects, V-DP selects, label projection) were removed: their decide-based proofs failed because the recursive classifyExternalMerge / labelCat evaluations do not reduce in the kernel. The substantive statements they made are: (1) D selects N, so D→N merge is .headComplement; (2) V selects D, so V→DP merge is .headComplement; (3) label {D, N} = some .D (head feature principle).

Monovalent Verb Serialization Problem (@cite{mueller-2013} §2.3)

In Stabler's non-directional MG, a monovalent verb's only argument is classified as a complement (Head-Complement, since the verb selects it). Left-to-right linearization places the complement after the head, yielding "*Sleeps Max" instead of "Max sleeps".

Stabler's fix — positing an ad hoc empty object — is "entirely stipulative and entirely ad hoc, being motivated only by the wish to have uniform structures" (Müller, p. 937).

def Minimalist.sleepsToken : LIToken

"sleeps" — a monovalent verb (category V, selects D).

Equations

• Minimalist.sleepsToken = { item := Minimalist.LexicalItem.simple Minimalist.Cat.V [Minimalist.Cat.D] "sleeps", id := 200 }

def Minimalist.maxToken : LIToken

"Max" — a proper name (category D, no selectional features).

Equations

• Minimalist.maxToken = { item := Minimalist.LexicalItem.simple Minimalist.Cat.D [] "Max", id := 201 }

Theorem monovalent_classified_as_complement — that classifyExternalMerge sleepsToken maxToken = .headComplement (V selects D, so the argument is a complement) — was removed for the same decide-doesn't-reduce reason. The Müller argument (Stabler's linearization yields "*Sleeps Max" instead of "Max sleeps", requiring an ad hoc empty object) stands in the section docstring above.

theorem Minimalist.monovalent_wrong_linearization : HeadFunction.leftSpine.phonYield (merge (SyntacticObject.leaf sleepsToken) (SyntacticObject.leaf maxToken)) = ["sleeps", "Max"]

Left-to-right linearization of merge(sleeps, Max) gives "sleeps Max". This is the wrong order for English — it should be "Max sleeps".

TODO Phase 2: phonYield is Quot.out-based after the FreeCommMagma migration; decide no longer reduces. Re-prove with parameterized linearization.

theorem Minimalist.monovalent_desired_order_differs : ["Max", "sleeps"] ≠ HeadFunction.leftSpine.phonYield (merge (SyntacticObject.leaf sleepsToken) (SyntacticObject.leaf maxToken))

The desired order differs from the linearization.