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

X immediately c-commands Y within tree root iff X c-commands Y (in root) and there is no Z such that X c-commands Z and Z c-commands Y (in root).

This is the "closest" c-command relation.

Equations

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

def Minimalism.respectsHMC (m : Movement) (root : SyntacticObject) : Prop

The Head Movement Constraint (HMC)

A head X can only move to the head Y that immediately c-commands X.

Formally: If X moves to Y, then Y immediately c-commands X's base position, with no intervening heads.

Equations

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

def Minimalism.violatesHMC (m : Movement) (root : SyntacticObject) : Prop

A movement violates HMC iff it doesn't respect it

Equations

• Minimalism.violatesHMC m root = ¬Minimalism.respectsHMC m root

theorem Minimalism.head_to_spec_violates_hmc (m : HeadToSpecMovement) : violatesHMC m.toMovement m.result

Head-to-specifier movement always violates HMC.

From Harizanov (p.12, p.29): In head-to-specifier movement, the head X becomes a maximal projection in its derived position.

This violates HMC because:

• HMC requires isHeadIn mover root
• isHeadIn requires ¬isMaximalIn mover root
• But head-to-spec movement is defined by isMaximalIn mover result
• Therefore the mover is not a head in the result
• Therefore HMC fails

Any head-to-spec movement violates HMC, by the very definition of what head-to-spec movement is.

def Minimalism.respectsHMC_positional (m : Movement) (root : SyntacticObject) (pos : TreePos) : Prop

Position-aware HMC: a head must be non-maximal AT ITS POSITION

Equations

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

def Minimalism.violatesHMC_positional (m : Movement) (root : SyntacticObject) (pos : TreePos) : Prop

Position-aware HMC violation

Equations

• Minimalism.violatesHMC_positional m root pos = ¬Minimalism.respectsHMC_positional m root pos

theorem Minimalism.head_to_spec_violates_hmc_positional (m : HeadToSpecMovementPositional) : violatesHMC_positional m.toMovement m.result derivedSpecPosition

Head-to-specifier movement (positional) violates HMC

This version works correctly with multidominance:

• The mover is maximal AT ITS DERIVED POSITION
• This means it is not a head at that position
• Therefore HMC fails for the derived position

Unlike the global version, we don't need to claim global maximality.

structure Minimalism.Amalgamation : Type

Amalgamation: a post-syntactic (PF) operation

Unlike syntactic head movement, Amalgamation:

1. Happens at PF, not in narrow syntax
2. Respects the HMC (is strictly local)
3. Results in phonological fusion without syntactic effects

From Harizanov (Section 3.3): Amalgamation "trades" the syntactic relation between a head X and the head Y of its complement for a PF relation of affixation. Since affixation requires adjacency, Amalgamation is strictly local and cannot skip intervening heads.

Example: French V-to-T "Jean ne parlait pas français" - V amalgamates with T at PF

• target : SyntacticObject

  The element that amalgamates (the "target")

• host : SyntacticObject

  The host (what it amalgamates to)

• is_local (root : SyntacticObject) : immediatelyCCommands self.host self.target root

  Amalgamation is LOCAL: host immediately c-commands target. This is the defining property that distinguishes Amalgamation from syntactic head movement.

theorem Minimalism.amalgamation_no_intervener (a : Amalgamation) (root : SyntacticObject) : ¬∃ (z : SyntacticObject), z ≠ a.host ∧ z ≠ a.target ∧ cCommandsIn root a.host z ∧ cCommandsIn root z a.target

Amalgamation cannot skip intervening elements.

This formalizes Harizanov's claim (Section 3.3, p.15): "Amalgamation-based displacement obeys the Head Movement Constraint"

The proof is immediate from the definition: Amalgamation requires immediatelyCCommands host target root, which by definition means there is NO z such that host c-commands z and z c-commands target.

This is what distinguishes Amalgamation from syntactic head movement, which can skip intervening heads (as shown by Bulgarian LHM and V2).

theorem Minimalism.intervener_rules_out_amalgamation (host target intervener root : SyntacticObject) (h_neq_host : intervener ≠ host) (h_neq_target : intervener ≠ target) (h_host_cmd : cCommandsIn root host intervener) (h_int_cmd : cCommandsIn root intervener target) : ¬∃ (a : Amalgamation), a.host = host ∧ a.target = target

If there's an intervening element, the displacement cannot be Amalgamation

This provides a diagnostic: if we observe a head displacement that skips an intervening head, we know it must be syntactic movement, not Amalgamation.

From Harizanov (Section 3.3): The properties of Amalgamation-based displacement "differ substantially from those of Internal Merge."

theorem Minimalism.amalgamation_host_ccommands_target (a : Amalgamation) (root : SyntacticObject) : cCommandsIn root a.host a.target

Amalgamation respects locality (the host c-commands the target within root)

def Minimalism.isSyntacticHeadMovement (m : Movement) (root : SyntacticObject) : Prop

Diagnostic: does this movement involve syntactic head movement?

Equations

• Minimalism.isSyntacticHeadMovement m root = Minimalism.violatesHMC m root

def Minimalism.compatibleWithAmalgamation (m : Movement) (root : SyntacticObject) : Prop

Diagnostic: is this compatible with Amalgamation?

Equations

• Minimalism.compatibleWithAmalgamation m root = Minimalism.respectsHMC m root