def Minimalism.isPhaseHead (so : SyntacticObject) : Bool

Identify phase heads from the formal category system.

C and v are phase heads. This is DERIVED from labelCat, not stipulated.

Voice/v correspondence*: In the Kratzer/Schäfer framework, agentive Voice = v*. But Cat.Voice can be either a phase head (agentive) or not (anticausative). This flavor-level distinction is tracked by VoiceHead.phaseHead in Core/Voice.lean, with bridge theorems in Core/Voice.lean § 8.

Equations

• Minimalism.isPhaseHead so = match Minimalism.labelCat so with | some Minimalism.Cat.C => true | some Minimalism.Cat.v => true | x => false

def Minimalism.isDPhaseHead (so : SyntacticObject) : Bool

D as a phase head (@cite{citko-2014} §2.5, @cite{svenonius-2004}).

Some analyses treat DP as a phase. This is a weaker claim used for scope barriers (QR cannot escape DP).

Equations

• Minimalism.isDPhaseHead so = match Minimalism.labelCat so with | some Minimalism.Cat.D => true | x => false

def Minimalism.isSAPhaseHead (so : SyntacticObject) : Bool

SA as a phase head. SAP is the highest phase — since it cannot embed, allocutive agreement probing from SA is root-only.

Equations

• Minimalism.isSAPhaseHead so = match Minimalism.labelCat so with | some Minimalism.Cat.SA => true | x => false

def Minimalism.isPhaseHeadExt (so : SyntacticObject) (dpIsPhase : Bool := false) : Bool

Extended phase head identification (C, v, optionally D)

Equations

• Minimalism.isPhaseHeadExt so dpIsPhase = (Minimalism.isPhaseHead so || dpIsPhase && Minimalism.isDPhaseHead so)

inductive Minimalism.PICStrength : Type

The strength of the Phase Impenetrability Condition.

• strong (PIC₁, @cite{chomsky-2000}): Only the edge (specifier) of the immediately lower phase is accessible. The complement is frozen as soon as the phase head is merged.
• weak (PIC₂, @cite{chomsky-2001}): The complement of a phase is accessible until the next higher phase head is merged.

• strong : PICStrength
• weak : PICStrength

def Minimalism.instReprPICStrength.repr : PICStrength → ℕ → Std.Format

Equations

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

instance Minimalism.instReprPICStrength : Repr PICStrength

Equations

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

instance Minimalism.instDecidableEqPICStrength : DecidableEq PICStrength

Equations

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

structure Minimalism.Phase : Type

A phase: a derivational cycle with head, complement, and edge.

The phase head determines the domain boundary. Material in the complement is shipped to PF/LF; material at the edge remains accessible for further operations.

• head : SyntacticObject

  The phase head (C or v*)

• isHead : isPhaseHead self.head = true

  Proof that the head is indeed a phase head

• complement : SyntacticObject

  The complement domain (shipped to interfaces)

• edge : SyntacticObject

  The edge (specifier, accessible for further operations)

def Minimalism.phaseImpenetrable (strength : PICStrength) (phase goal : SyntacticObject) : Prop

Phase Impenetrability Condition: material inside a phase complement is inaccessible to operations outside the phase.

Under the strong PIC, the complement is frozen as soon as the phase head is merged. Under the weak PIC, it is frozen when the next phase head is merged.

Equations

• Minimalism.phaseImpenetrable Minimalism.PICStrength.strong (a.node complement) goal = Minimalism.contains complement goal
• Minimalism.phaseImpenetrable Minimalism.PICStrength.strong (Minimalism.SyntacticObject.leaf a) goal = False
• Minimalism.phaseImpenetrable Minimalism.PICStrength.weak (a.node complement) goal = Minimalism.contains complement goal
• Minimalism.phaseImpenetrable Minimalism.PICStrength.weak (Minimalism.SyntacticObject.leaf a) goal = False

def Minimalism.antiLocality (head complement mover : SyntacticObject) : Prop

Anti-locality: the complement of a phase head H cannot move to Spec-H.

This is "too local" — movement must cross at least one maximal projection. @cite{abels-2012} derives this from the independently motivated ban on complement-to-specifier movement within a single phase.

This is a derivational constraint: a derivation that applies Internal Merge to move the complement of H to Spec-H is illicit. We model this as a predicate on derivations rather than on structures.

Equations

• Minimalism.antiLocality head complement mover = (Minimalism.immediatelyContains head complement → mover ≠ complement)

theorem Minimalism.stranding_from_antilocality_pic (ph : Phase) (h_imm : immediatelyContains ph.head ph.complement) (h_anti : antiLocality ph.head ph.complement ph.complement) : False

Stranding Generalization: Complements of phase heads cannot be stranded by movement of the head.

DERIVED from Anti-locality + PIC:

• By Anti-locality, complement of H can't move to Spec-HP
• By PIC, complement of H can't move out of HP (frozen)
• Therefore: complement of a phase head is immovable = stranded

structure Minimalism.Transfer : Type

Transfer: ship a phase complement to the interfaces (PF and LF).

When a phase is complete, its complement domain is transferred:

• To PF for phonological computation (linearization, prosody)
• To LF for semantic interpretation

• phase : Phase

  The phase being transferred

• toPF : SyntacticObject

  Material sent to PF (phonological form)

• toLF : SyntacticObject

  Material sent to LF (logical form)

• pf_is_complement : self.toPF = self.phase.complement

  PF domain = complement

• lf_is_complement : self.toLF = self.phase.complement

  LF domain = complement

def Minimalism.Transfer.fromPhase (ph : Phase) : Transfer

Create a transfer from a phase (PF and LF receive the complement)

Equations

• Minimalism.Transfer.fromPhase ph = { phase := ph, toPF := ph.complement, toLF := ph.complement, pf_is_complement := ⋯, lf_is_complement := ⋯ }

structure Minimalism.FeatureInheritance : Type

Feature Inheritance: phase heads pass features to their complements.

• C passes tense/agreement features to T
• v* passes case/agreement features to V

The phase head retains its edge features (EPP, etc.) but the "operational" features are inherited by the complement head.

• phaseHead : SyntacticObject

  The phase head (C or v*)

• inheritor : SyntacticObject

  The inheriting head (T or V)

• locality : immediatelyContains self.phaseHead self.inheritor

  The phase head must immediately contain the inheritor

def Minimalism.cToTInheritance (cHead tHead : SyntacticObject) (h : immediatelyContains cHead tHead) : FeatureInheritance

C→T inheritance: C is a phase head, T inherits

Equations

• Minimalism.cToTInheritance cHead tHead h = { phaseHead := cHead, inheritor := tHead, locality := h }

def Minimalism.vToVInheritance (vHead vbHead : SyntacticObject) (h : immediatelyContains vHead vbHead) : FeatureInheritance

v*→V inheritance: v* is a phase head, V inherits

Equations

• Minimalism.vToVInheritance vHead vbHead h = { phaseHead := vHead, inheritor := vbHead, locality := h }

def Minimalism.isPhaseBounded (mover target : SyntacticObject) (phases : List Phase) (strength : PICStrength) : Prop

A movement is phase-bounded iff the mover does not cross a phase boundary.

Under PIC, an element inside a phase complement is inaccessible. This means movement must target the edge before the phase is complete.

Equations

• Minimalism.isPhaseBounded mover target phases strength = ¬∃ (ph : Minimalism.Phase), ph ∈ phases ∧ Minimalism.phaseImpenetrable strength ph.head mover ∧ Minimalism.contains target ph.head

theorem Minimalism.pic_blocks_agree (strength : PICStrength) (phase _probe goal : SyntacticObject) (h_impenetrable : phaseImpenetrable strength phase goal) (_h_outside : ¬contains phase _probe) : phaseImpenetrable strength phase goal

Phase-bounded locality subsumes Relativized Minimality (@cite{rizzi-1990}) for Agree: if a goal is inside a phase complement, no probe outside can reach it.