Phase Theory

Formalization of derivational phases following @cite{chomsky-2000}, @cite{abels-2012}, and @cite{citko-2014}.

Key Ideas

• CP and v*P are phases: derivational domains shipped to PF/LF incrementally
• Phase Impenetrability Condition (PIC): material inside a phase complement becomes inaccessible once the phase is complete
• Anti-locality: complements of phase heads cannot move to Spec of the same phase head
• Feature Inheritance: C→T and v*→V inheritance

Design

isPhaseHeadOf c so is derived from HeadFunction.leftSpine.outerCat so — the leftmost leaf's outer category under the harmonic head-initial convention. For head-final analyses (Korean, Japanese), supply a head function with headSide := .final (e.g. HeadFunction.rightSpine) and lift via Minimalist.Labeling.labelRoot h so directly. A latent trap: any head-final consumer that calls isPhaseHeadOf will silently misfire — flagged for h-parameterization in a future session.

noncomputable def Minimalist.isPhaseHeadOf (c : Cat) (so : SyntacticObject) : Bool

Generic phase-head test: is the head of so (under leftSpine) exactly c? Uses SyntacticObject.outerCat = leftmostLeaf.outerCat, which @cite{marcolli-chomsky-berwick-2025} §1.13 frames as the leftSpine head function applied to so. For non-leftmost-headed analyses, use Minimalist.Labeling.labelRoot h so == some c with the study's chosen h : HeadFunction.

Equations

• Minimalist.isPhaseHeadOf c so = (Minimalist.HeadFunction.leftSpine.outerCat so == c)

Phase-head selectors

Only C is a phase head by default. @cite{keine-2020} (ch. 5) argues that vP is NOT a phase: φ-Agree and wh-licensing can cross unboundedly many vPs but not CPs, selective opacity creates intractable problems for vP phases, and previous arguments for vP phases (reconstruction, Dinka successive cyclicity, Indonesian meN-deletion) can be reanalyzed.

For commonly-checked phase categories, call isPhaseHeadOf directly:

• C as phase head: isPhaseHeadOf .C so (linglib default per @cite{keine-2020}). The classical Chomsky-2000/2001 extension to v as a phase head is isPhaseHeadOf .C so || isPhaseHeadOf .v so.

• D as phase head (@cite{citko-2014} §2.5, @cite{svenonius-2004}): isPhaseHeadOf .D so. Several analyses treat definite DPs as phases: extraction barriers (@cite{chomsky-2000}, @cite{davies-dubinsky-2003}, @cite{shen-huang-2026} — definite island effect; VOCs neutralize via N/D-incorporation), scope barriers (QR cannot escape DP), spell-out domains (definite D triggers Transfer of its complement).

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

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.IsPhasal in Theories/Syntax/Minimalist/Voice.lean, with the per-construction override semantics described in that file's "Voice/Phase Bridge" section. The two convergent recent clients of clause-internal Voice phasehood are @cite{erlewine-sommerlot-2025} (Malayic, A′-extraction) and @cite{pietraszko-2026} (Ndebele, A-movement & φ-agreement).

inductive Minimalist.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.
• linearizationBound (no PIC, @cite{fox-pesetsky-2005}, @cite{sande-clem-dabkowski-2026}): No structural opacity at all — the only constraints on movement out of an already-spelled-out phase are the ordering statements emitted at that phase's spell-out (Cyclic Linearization). Material can be moved out of the complement of any phase, provided the resulting Ordering Table remains consistent. This is the regime argued for by SCD 2026 §6.2 (against both PIC₁ and PIC₂): Guébie discontinuous harmony requires that the particle, after being spelled out inside the lower vP phase, remains accessible to A′-fronting in the higher CP phase. Adopted independently by @cite{branan-davis-2019}, @cite{halpert-2019}, @cite{lee-yip-2024} among others. See Theories/Syntax/Minimalist/Linearization/Cyclic.lean for the ordering-only locality machinery this mode delegates to.

Modular variants (e.g., the @cite{d-alessandro-scheer-2015} "Modular PIC" proposal that PIC strength is parametrized per interface module) are not yet operationalized in this enum.

TODO: the strong/weak distinction is not yet operationalized in phaseImpenetrable, which currently models only the structural "goal sits in the complement" check shared by both variants. The real distinction lies in when the check fires relative to merge of the next phase head — that requires a derivational timeline that this static API doesn't yet expose. Callers using strong or weak get the same structural answer; callers using linearizationBound should consult Cyclic.SpelloutAndCheck rather than phaseImpenetrable.

• strong : PICStrength
• weak : PICStrength
• linearizationBound : PICStrength

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

Equations

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

@[implicit_reducible]

instance Minimalist.instReprPICStrength : Repr PICStrength

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqPICStrength : DecidableEq PICStrength

Equations

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

structure Minimalist.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.

Per-analysis discipline determines which heads count as phase heads — Keine 2020 (C-only), Chomsky 2000/2001 (C + v), Pietraszko 2026 + Erlewine & Sommerlot 2025 (also Voice via VoiceHead.IsPhasal), Citko 2014 (also D). The struct is intentionally permissive about head's category so all four can register Phase instances.

• head : SyntacticObject

  The phase head (per-analysis: C, v, Voice, D, …)

• complement : SyntacticObject

  The complement domain (shipped to interfaces)

• edge : SyntacticObject

  The edge (specifier, accessible for further operations)

noncomputable def Minimalist.phaseComplement? : SyntacticObject → Option SyntacticObject

The phase complement is the right daughter of the phase node, picked via the planar Quot.out representative. Phase 1.0 noncomputable placeholder; the parameterized version phaseComplementWith? below takes a HeadFunction for explicit externalize choice.

Equations

• Minimalist.phaseComplement? so = match Quot.out so with | FreeMagma.of a => none | a.mul r => some (FreeCommMagma.mk r)

def Minimalist.phaseComplementWith? (h : HeadFunction) (so : SyntacticObject) : Option SyntacticObject

Parameterized phase-complement accessor: under harmonic head-initial convention (head daughter to the LEFT of the planar representative), the complement is the RIGHT daughter of h.section_.σ so. Computable when h.section_.σ is.

Returns none when h.section_.σ so is a leaf or trace (no daughter structure). For nodes, returns the right daughter as a SyntacticObject.

Equations

• Minimalist.phaseComplementWith? h so = match h.section_.σ so with | FreeMagma.of a => none | a.mul r => some (FreeCommMagma.mk r)

def Minimalist.phaseImpenetrable (phase goal : SyntacticObject) : Prop

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

The strong/weak (PIC₁/PIC₂) distinction is about when the check fires relative to the merge of the next phase head; structurally both variants ask the same question — is the goal sitting inside the phase's complement? — so this predicate is currently strength-agnostic. See PICStrength for the TODO.

Equations

• Minimalist.phaseImpenetrable phase goal = match Minimalist.phaseComplement? phase with | some complement => Minimalist.contains complement goal | none => False

@[implicit_reducible]

noncomputable instance Minimalist.instDecidablePhaseImpenetrable (phase goal : SyntacticObject) : Decidable (phaseImpenetrable phase goal)

Equations

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

def Minimalist.admitsExtraction (strength : PICStrength) (phase goal : SyntacticObject) : Prop

A phase admits movement of goal out of phase.complement under strength. For strong/weak, this is the negation of phaseImpenetrable. For linearizationBound, the predicate is vacuously True — actual constraint comes from the Cyclic Linearization table, not from phasehood per se.

The point of the predicate is to make the SCD-2026 stance ("PIC is too strong, Cyclic Linearization is enough") expressible as a different PICStrength argument rather than a different theorem statement. Callers who pick linearizationBound should also feed the derivation through Minimalist.Linearization.SpelloutAndCheck to confirm it does not crash on ordering grounds.

Equations

• Minimalist.admitsExtraction Minimalist.PICStrength.strong phase goal = ¬Minimalist.phaseImpenetrable phase goal
• Minimalist.admitsExtraction Minimalist.PICStrength.weak phase goal = ¬Minimalist.phaseImpenetrable phase goal
• Minimalist.admitsExtraction Minimalist.PICStrength.linearizationBound phase goal = True

@[implicit_reducible]

noncomputable instance Minimalist.instDecidableAdmitsExtraction (strength : PICStrength) (phase goal : SyntacticObject) : Decidable (admitsExtraction strength phase goal)

Equations

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

theorem Minimalist.linearizationBound_admits_all (phase goal : SyntacticObject) : admitsExtraction PICStrength.linearizationBound phase goal

Under linearizationBound, every phase admits extraction at the phasehood layer. Concrete crashes come from the linearization table (see Minimalist.Linearization.SpelloutAndCheck). This is the formal content of @cite{sande-clem-dabkowski-2026}'s rejection of strict PIC.

theorem Minimalist.strict_PIC_blocks {strength : PICStrength} (h : strength = PICStrength.strong ∨ strength = PICStrength.weak) {phase goal : SyntacticObject} (hp : phaseImpenetrable phase goal) : ¬admitsExtraction strength phase goal

Strict PIC₁/PIC₂ both block extraction from a phase complement. The mode-as-data design lets a study file pick its locality regime by passing the PICStrength argument explicitly.

structure Minimalist.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 Minimalist.Transfer.fromPhase (ph : Phase) : Transfer

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

Equations

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

Feature Inheritance and KEEP/SHARE/DONATE

@cite{chomsky-2008}'s feature inheritance has phase heads passing operational features to their complements: C → T (tense/agreement), v* → V (case/agreement). The phase head retains its edge features while the inheritor takes over the agreement-driving features.

@cite{ouali-2008} observes that "inheritance" is only one of three possible feature operations on adjacent functional heads, and that the choice is parametric (Berber agreement/anti-agreement is the empirical diagnostic):

• KEEP: φ stays at the source head; the target lacks φ.
• SHARE: φ surfaces at both source and target. This explains clitic reduplication and is the operation @cite{olivier-2026} argues for in Romance restructuring (Voice* → vMOD share).
• DONATE: φ moves source → target; the source loses φ. This is the classical @cite{chomsky-2008} C → T / v* → V inheritance.

@cite{olivier-2026} extends this typology to Voice* → vMOD feature transfer in Romance restructuring clauses: under SHARE, φ-features are present at vMOD as well as Voice*, which is what enables clitic climbing (the climbing clitic enters Agree with the higher copy). The KEEP / SHARE / DONATE choice is parametric across languages and across constructions; we model it via a style field on FeatureInheritance.

inductive Minimalist.TransferStyle : Type

Style of φ-feature transfer between two adjacent functional heads (@cite{ouali-2008}).

• keep: φ stays at source — target lacks φ.
• share: φ surfaces at both source and target. Explains clitic reduplication and licenses clitic climbing in @cite{olivier-2026}'s Voice* → vMOD analysis of Romance restructuring.
• donate: φ moves source → target. The classical @cite{chomsky-2008} C → T / v* → V inheritance.

• keep : TransferStyle
• share : TransferStyle
• donate : TransferStyle

@[implicit_reducible]

instance Minimalist.instDecidableEqTransferStyle : DecidableEq TransferStyle

Equations

• Minimalist.instDecidableEqTransferStyle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.instReprTransferStyle.repr : TransferStyle → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprTransferStyle : Repr TransferStyle

Equations

• Minimalist.instReprTransferStyle = { reprPrec := Minimalist.instReprTransferStyle.repr }

structure Minimalist.FeatureInheritance : Type

Feature inheritance / sharing between two adjacent heads.

Generalizes @cite{chomsky-2008}'s C → T and v* → V inheritance (the .donate style) to cover @cite{ouali-2008}'s KEEP/SHARE/DONATE typology and @cite{olivier-2026}'s extension to Voice* → vMOD feature transfer in Romance restructuring clauses (the .share style).

• source : SyntacticObject

  The feature-bearing source head (phase head, Voice*, etc.).

• target : SyntacticObject

  The head receiving features (T, V, vMOD).

• locality : immediatelyContains self.source self.target

  Source must immediately contain target.

• style : TransferStyle

  Which transfer operation applies (default: classical @cite{chomsky-2008} donate).

• transferred : FeatureBundle

  The features transferred (default: none specified at this layer).

def Minimalist.isPhaseBounded (mover target : SyntacticObject) (phases : List Phase) : 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

• Minimalist.isPhaseBounded mover target phases = ¬∃ ph ∈ phases, Minimalist.phaseImpenetrable ph.head mover ∧ Minimalist.contains target ph.head

N/D-Incorporation (@cite{davies-dubinsky-2003}, @cite{shen-huang-2026})

@cite{davies-dubinsky-2003} propose that verbs of creation (VOCs) trigger LF noun incorporation: the head noun of the object DP incorporates into the verb. This has the effect of neutralizing the DP's phasehood — the D head is no longer a blocking category, and extraction from the DP becomes possible.

@cite{shen-huang-2026} adapt this analysis: it is the determiner that undergoes covert head movement to the verb (following @cite{boskovic-2015} on phase collapse). The incorporation neutralizes the PIC, explaining why VOCs ameliorate (but do not eliminate) definite island effects — the Specificity Condition still applies independently.

Three conditions for incorporation (@cite{davies-dubinsky-2003}:28–29):

1. The noun is a result nominal
2. The object is complement of a causative verb semantically related to the denoted result (e.g., write-book)
3. The verb's subject controls the agentive subject of the object

structure Minimalist.DPPhaseStatus : Type

Whether a DP's phase status has been deactivated by incorporation.

When incorporated = true, the D head has been absorbed into the verb via head movement. The DP is no longer a phase boundary — isPhaseHeadOf .D is irrelevant because the D head is no longer projecting independently.

This models the effect described by @cite{davies-dubinsky-2003} and @cite{shen-huang-2026}: VOCs neutralize the PIC for definite DPs.

Note: the wasPhase default isPhaseHeadOf .D dHead from the prior planar substrate is Phase-1.0 unavailable as a default (since isPhaseHeadOf is now noncomputable). Callers must supply the field explicitly.

• dHead : SyntacticObject

  The D head (before incorporation)

• wasPhase : Bool

  Whether D was originally a phase head. Set explicitly per derivation; in Phase 1.0 the substrate cannot compute this from dHead alone.

• incorporated : Bool

  Whether incorporation has applied

def Minimalist.instReprDPPhaseStatus.repr : DPPhaseStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprDPPhaseStatus : Repr DPPhaseStatus

Equations

• Minimalist.instReprDPPhaseStatus = { reprPrec := Minimalist.instReprDPPhaseStatus.repr }

def Minimalist.DPPhaseStatus.isActivePhase (s : DPPhaseStatus) : Bool

A DP is an active phase barrier iff it was originally a phase AND has not been deactivated by incorporation.

Equations

• s.isActivePhase = (s.wasPhase && !s.incorporated)

theorem Minimalist.incorporation_deactivates (s : DPPhaseStatus) (h_phase : s.wasPhase = true) (h_inc : s.incorporated = true) : s.isActivePhase = false

Incorporation deactivates phasehood: a D-phase that undergoes incorporation is no longer an active phase barrier.

theorem Minimalist.no_incorporation_preserves (s : DPPhaseStatus) (h_phase : s.wasPhase = true) (h_no_inc : s.incorporated = false) : s.isActivePhase = true

Without incorporation, a D-phase remains active.

theorem Minimalist.non_phase_never_active (s : DPPhaseStatus) (h : s.wasPhase = false) : s.isActivePhase = false

Non-phases are never active barriers, regardless of incorporation.