def Minimalism.covers (x y root : SyntacticObject) : Prop

The covering relation in a partial order.

x covers y (x ⋖ y) iff x properly dominates y with no element in between.

This is a fundamental concept in lattice theory. In the dominance order on a tree, x covers y iff y is the head of x's complement (roughly).

Equations

• Minimalism.covers x y root = (Minimalism.contains x y ∧ ¬∃ (z : Minimalism.SyntacticObject), z ≠ x ∧ z ≠ y ∧ Minimalism.contains x z ∧ Minimalism.contains z y)

theorem Minimalism.covers_asymm {x y root : SyntacticObject} (hxy : covers x y root) (hyx : covers y x root) : False

The covering relation is asymmetric

def Minimalism.headsIn (root : SyntacticObject) : Set SyntacticObject

The set of heads in a structure

Equations

• Minimalism.headsIn root = {x : Minimalism.SyntacticObject | Minimalism.isHeadIn x root}

def Minimalism.isMaximalProjectionOf (x h root : SyntacticObject) : Prop

X is the maximal projection of head H in root iff:

1. X contains H (or X = H)
2. X has the same label as H
3. X doesn't project further (is maximal)

Equations

• Minimalism.isMaximalProjectionOf x h root = (Minimalism.containsOrEq x h ∧ Minimalism.sameLabel h x ∧ Minimalism.isMaximalIn x root)

def Minimalism.hasMaximalProjection (h root : SyntacticObject) : Prop

For any head H in a well-formed tree, there exists a unique maximal projection

Equations

• Minimalism.hasMaximalProjection h root = ∃! x : Minimalism.SyntacticObject, Minimalism.isMaximalProjectionOf x h root

def Minimalism.containsAmongHeads (root x y : SyntacticObject) : Prop

Dominance restricted to heads, lifted to projections.

Heads are leaves (isMinimalIn), so contains x y is always false when both x and y are heads. The correct formulation lifts dominance to maximal projections: head x dominates head y iff x's maximal projection contains y's maximal projection.

Equations

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

def Minimalism.coversAmongHeads (root x y : SyntacticObject) : Prop

Covering restricted to heads (lifted to projections).

x covers y among heads iff x's maximal projection contains y's maximal projection with no intervening head's projection between them.

This is the correct characterization of amalgamation locality (@cite{harizanov-gribanova-2019} §3.3).

Equations

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

theorem Minimalism.covers_among_heads_no_intervener {x y root : SyntacticObject} (h : coversAmongHeads root x y) : ¬∃ (z : SyntacticObject), isHeadIn z root ∧ z ≠ x ∧ z ≠ y ∧ containsAmongHeads root x z ∧ containsAmongHeads root z y

Covering among heads implies no intervening head's projection

def Minimalism.coversProjection (root x y : SyntacticObject) : Prop

Covering relation on projections.

X's projection covers Y's projection iff:

• X's maximal projection properly contains Y's maximal projection
• No intervening head's projection between them

Equations

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

coversAmongHeads ↔ coversProjection

Both definitions restrict the covering relation to heads, lifted to maximal projections. They differ only in how the "no intervening head" clause is packaged:

• coversAmongHeads uses containsAmongHeads (which bundles head-ness and projection existence together)
• coversProjection existentially quantifies over projections at the top level and blocks on intervening heads with their projections

Given unique maximal projections (hasMaximalProjection), the existential witnesses can be identified across the two definitions, making them equivalent.

Why immediatelyCCommands ≠ coversProjection

immediatelyCCommands x y root blocks on ANY z that c-commands between x and y, while coversProjection only blocks on intervening heads. In a standard X-bar tree [TP T [vP v [VP V DP]]], the phrase VP c-commands v (VP's sister is v), and T c-commands VP (T's sister vP contains VP). So VP intervenes between T and v for immediatelyCCommands, making it false — even though VP is not a head and coversProjection root T v holds.

Additionally, c-command (sister-based) only reaches complement-internal heads, while covering reaches specifier-internal heads too. In [TP T [vP [DP D NP] [v' v VP]]], TP covers DP's projection (D is in Spec-vP), but T does not c-command D because T's sister is vP, not DP.

The relationship between c-command-among-heads and covering-among-projections remains an open question requiring infrastructure connecting projections to tree structure (sister domains, projection chains).

theorem Minimalism.coversAmongHeads_iff_coversProjection (x y root : SyntacticObject) (hx : isHeadIn x root) (hy : isHeadIn y root) (hx_proj : hasMaximalProjection x root) (hy_proj : hasMaximalProjection y root) (h_all_proj : ∀ (z : SyntacticObject), isHeadIn z root → hasMaximalProjection z root) : coversAmongHeads root x y ↔ coversProjection root x y

Covering among heads = Covering on projections

coversAmongHeads and coversProjection are equivalent given unique maximal projections for all heads. The proof identifies existential witnesses using the uniqueness from hasMaximalProjection.

This replaces the earlier false conjecture (cCommandsIn ↔ coversProjection), which fails because c-command and covering differ on specifier-internal heads and on phrasal interveners.

inductive Minimalism.GramModule : Type

The grammatical module where an operation applies

• narrowSyntax : GramModule
• pf : GramModule
• lf : GramModule

instance Minimalism.instDecidableEqGramModule : DecidableEq GramModule

Equations

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

def Minimalism.instReprGramModule.repr : GramModule → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.instReprGramModule.repr Minimalism.GramModule.pf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.GramModule.pf")).group prec✝
• Minimalism.instReprGramModule.repr Minimalism.GramModule.lf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.GramModule.lf")).group prec✝

instance Minimalism.instReprGramModule : Repr GramModule

Equations

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

inductive Minimalism.HeadDisplacement : Type

Classification of head displacement phenomena.

Every operation that affects head positions is either:

1. Syntactic (Internal Merge) - takes place in narrow syntax
2. Amalgamation (Raising/Lowering) - takes place at PF

This follows from the Y-model architecture.

• syntactic : Movement → HeadDisplacement

  Syntactic movement: Internal Merge, creates copies, can violate HMC

• amalgam : Amalgamation → HeadDisplacement

  Amalgamation: PF operation, no copies, respects HMC

def Minimalism.HeadDisplacement.module : HeadDisplacement → GramModule

Syntactic movement applies in narrow syntax

Equations

• (Minimalism.HeadDisplacement.syntactic a).module = Minimalism.GramModule.narrowSyntax
• (Minimalism.HeadDisplacement.amalgam a).module = Minimalism.GramModule.pf

theorem Minimalism.head_displacement_exhaustive (d : HeadDisplacement) : (∃ (m : Movement), d = HeadDisplacement.syntactic m) ∨ ∃ (a : Amalgamation), d = HeadDisplacement.amalgam a

THEOREM (Exhaustivity):

Every head displacement is exactly one of syntactic or amalgamation.

This is NOT a stipulation but follows from:

1. Y-model: operations are pre-Spell-Out (syntax) or post-Spell-Out (PF)
2. These modules are disjoint by architecture
3. Head displacement in syntax = Internal Merge
4. Head displacement at PF = Amalgamation (Raising/Lowering)

theorem Minimalism.displacement_modules_disjoint (d : HeadDisplacement) : d.module = GramModule.narrowSyntax ↔ ∃ (m : Movement), d = HeadDisplacement.syntactic m

Syntactic and amalgamation are mutually exclusive (different modules)

theorem Minimalism.hmc_violation_diagnostic (root : SyntacticObject) (m : Movement) (hviol : violatesHMC m root) (a : Amalgamation) : HeadDisplacement.syntactic m ≠ HeadDisplacement.amalgam a

If HMC is violated, the operation must be syntactic

def Minimalism.hasMultiplePronunciations (x root : SyntacticObject) : Prop

An SO x has multiple pronunciations in root if x appears more than once as a subterm of root. Under copy theory, Internal Merge creates copies; verb doubling = multiple copies pronounced.

Equations

• Minimalism.hasMultiplePronunciations x root = ((List.filter (fun (x_1 : Minimalism.SyntacticObject) => x_1 == x) (Minimalism.subterms root)).length > 1)

def Minimalism.isComplexMorphologicalWord (x : SyntacticObject) : Prop

An SO is a complex morphological word if it is a leaf whose LexicalItem has more than one feature bundle (i.e., was produced by LexicalItem.combine during head-to-head amalgamation).

Equations

• Minimalism.isComplexMorphologicalWord (Minimalism.SyntacticObject.leaf tok) = (tok.item.isComplex = true)
• Minimalism.isComplexMorphologicalWord (a.node a_1) = False

axiom Minimalism.verb_doubling_implies_syntactic (x root : SyntacticObject) : hasMultiplePronunciations x root → ∃ (m : Movement), m.mover = x

Verb doubling (multiple copies pronounced) implies syntactic movement

axiom Minimalism.word_formation_implies_amalgamation (complex root : SyntacticObject) : isComplexMorphologicalWord complex → ∃ (a : Amalgamation), True

Word formation implies amalgamation was involved