structure Minimalism.Movement : Type

A movement operation tracks the mover, target, and result

• mover : SyntacticObject

  The element that moves

• target : SyntacticObject

  The target (landing site structure)

• result : SyntacticObject

  The resulting structure after movement

• mover_in_target : contains self.target self.mover

  The mover must be contained in the target (Internal Merge)

• is_merge : self.result = merge self.mover self.target

  The result is formed by merging mover and target

structure Minimalism.HeadToSpecMovementextends Minimalism.Movement : Type

Head-to-specifier movement: mover becomes maximal

In head-to-spec, the moved head X:

1. Was a head in base position (+min, -max)
2. Becomes a phrase in derived position (+max)
3. The target Y projects (X is a specifier of Y)

Example: Bulgarian LHM where V moves to Spec-CP

• mover : SyntacticObject
• target : SyntacticObject
• result : SyntacticObject
• mover_in_target : contains self.target self.mover
• is_merge : self.result = merge self.mover self.target
• mover_was_head : isHeadIn self.mover self.target

  Mover was a head in the target (before extraction)

• mover_is_maximal : isMaximalIn self.mover self.result

  In the result, mover is maximal (a phrase)

• target_projects : projectsIn self.target self.result

  The target projects (mover is a specifier)

theorem Minimalism.head_to_spec_yields_maximal (m : HeadToSpecMovement) : isPhraseIn m.mover m.result

Key property: head-to-spec yields a maximal element

theorem Minimalism.head_to_spec_target_labels (m : HeadToSpecMovement) : sameLabel m.target m.result

Head-to-spec: the target determines the label

structure Minimalism.HeadToHeadMovementextends Minimalism.Movement : Type

Head-to-head movement: mover reprojects (stays minimal)

In head-to-head, the moved head X:

1. Was a head in base position (+min, -max)
2. Stays a head in derived position (+min, -max)
3. X reprojects: X's label becomes the label of the result
4. Requires X to be (or become) a complex LI

Example: V-to-T movement where V reprojects within the T complex

• mover : SyntacticObject
• target : SyntacticObject
• result : SyntacticObject
• mover_in_target : contains self.target self.mover
• is_merge : self.result = merge self.mover self.target
• mover_was_head : isHeadIn self.mover self.target

  Mover was a head in the target

• mover_is_minimal : isMinimalIn self.mover self.result

  In the result, mover is still minimal (still a head)

• mover_not_maximal : ¬isMaximalIn self.mover self.result

  Mover is NOT maximal (it projects/reprojects)

• mover_is_complex : ∃ (tok : LIToken), self.mover.getLIToken = some tok ∧ tok.item.isComplex = true

  The mover's LI is complex (or becomes complex)

theorem Minimalism.head_to_head_yields_minimal (m : HeadToHeadMovement) : isMinimalIn m.mover m.result

Key property: head-to-head yields a minimal element

theorem Minimalism.head_to_head_mover_labels (m : HeadToHeadMovement) : ∃ (z : SyntacticObject), containsOrEq m.result z ∧ projectsIn m.mover z

Head-to-head: the mover determines the label (reprojection)

def Minimalism.formComplexLI (target mover : LIToken) : LIToken

When X moves to Y via head-to-head, Y absorbs X's features

The target becomes a complex LI: [Y-features, X-features] This is how reprojection works: Y's category extends with X's

Equations

• Minimalism.formComplexLI target mover = { item := target.item.combine mover.item, id := target.id }

theorem Minimalism.complex_li_outer_projects (target mover : LIToken) : (formComplexLI target mover).item.outerCat = target.item.outerCat

Complex LI enables reprojection: the outer features project

structure Minimalism.MovementTypeComparison : Prop

Summary of the two movement types

• h2s_maximal (m : HeadToSpecMovement) : isMaximalIn m.mover m.result

  Head-to-spec: mover ends up maximal

• h2h_minimal (m : HeadToHeadMovement) : isMinimalIn m.mover m.result

  Head-to-head: mover stays minimal

• h2s_target_projects (m : HeadToSpecMovement) : projectsIn m.target m.result

  Head-to-spec: target projects

• h2h_mover_reprojects (m : HeadToHeadMovement) : ¬isMaximalIn m.mover m.result

  Head-to-head: mover reprojects (via complex LI)

def Minimalism.movementType (mover_max : Bool) : String

The key diagnostic

Equations

• Minimalism.movementType mover_max = if mover_max = true then "head-to-specifier" else "head-to-head"

def Minimalism.isSinglePredicate (m : HeadToHeadMovement) : Prop

Head-to-head results in a single complex LI (single predicate)

Equations

• Minimalism.isSinglePredicate m = ∃ (tok : Minimalism.LIToken), m.result.getLIToken = some tok ∧ tok.item.isComplex = true

def Minimalism.areSeparatePredicates (m : HeadToSpecMovement) : Prop

Head-to-spec keeps predicates separate

Equations

• Minimalism.areSeparatePredicates m = ∃ (tok₁ : Minimalism.LIToken), ∃ (tok₂ : Minimalism.LIToken), m.mover.getLIToken = some tok₁ ∧ m.target.getLIToken = some tok₂ ∧ tok₁ ≠ tok₂

def Minimalism.isLocal (m : Movement) : Prop

A movement is local iff no phase head intervenes between target and mover (derived from Phase Impenetrability Condition).

Equations

• Minimalism.isLocal m = ¬∃ (ph : Minimalism.SyntacticObject), Minimalism.isPhaseHead ph = true ∧ Minimalism.contains m.target ph ∧ Minimalism.contains ph m.mover

theorem Minimalism.head_to_head_is_local (m : HeadToHeadMovement) (h : isLocal m.toMovement) : isLocal m.toMovement

Head-to-head movement must be phase-bounded.

This follows from PIC: the mover is inside a phase complement, which becomes inaccessible once the phase is complete. Head-to-head movement must therefore be strictly local (within a single phase).

structure Minimalism.HeadToSpecMovementPositionalextends Minimalism.Movement : Type

Head-to-specifier movement with position-specific maximality.

This structure uses position-indexed maximality rather than global maximality. The mover is maximal AT ITS DERIVED POSITION (Spec), even if it projects at other positions (e.g., its base position in VP under multidominance).

In Internal Merge forming {X, Y}:

• X (mover) goes to the LEFT (specifier position = derivedSpecPosition)
• Y (target) stays on the RIGHT and projects

• mover : SyntacticObject
• target : SyntacticObject
• result : SyntacticObject
• mover_in_target : contains self.target self.mover
• is_merge : self.result = merge self.mover self.target
• mover_was_head : isHeadIn self.mover self.target

  Mover was a head somewhere in the target (before extraction)

• mover_maximal_at_derived : isMaximalAtPosition self.mover self.result derivedSpecPosition

  At the derived position (Spec), mover is maximal

• target_projects : projectsIn self.target self.result

  The target projects (determines the label of result)

theorem Minimalism.head_to_spec_mover_position (m : HeadToSpecMovementPositional) : atPosition m.result derivedSpecPosition = some m.mover

In head-to-spec, the mover is at the left daughter of result

theorem Minimalism.head_to_spec_target_labels_positional (m : HeadToSpecMovementPositional) : sameLabel m.target m.result

The target (Y) projects, so it has the same label as the result

def Minimalism.positionalToGlobal (m : HeadToSpecMovementPositional) (h : ¬∃ (z : SyntacticObject), isTermOf z m.result ∧ projectsIn m.mover z) : HeadToSpecMovement

Convert positional head-to-spec to the standard version when possible.

If an element is maximal at its derived position AND doesn't project anywhere else in the result, then global maximality holds.

This doesn't apply in true multidominance where the element projects at some other position, but works for simple cases.

Equations

• Minimalism.positionalToGlobal m h = { toMovement := m.toMovement, mover_was_head := ⋯, mover_is_maximal := ⋯, target_projects := ⋯ }