Phase Theory (linguistic-facing API)

Formalization of derivational phases following [Cho00], [Abe12], and [Cit14], built directly on the SO-carrier phase domain (SyntacticObject/Phase.lean, MCB §1.14). This file packages the carrier-native primitives (SO.isPhaseHeadOf, SO.phase/phaseInterior/phaseEdge, SO.Impenetrable, SO.isPhaseHead) into the study-facing Phase record + the PIC-strength / Transfer / feature-inheritance / DP-deactivation layer that the paper-anchored study files consume.

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 (= interior membership, MCB eq 1.14.3).
• Feature Inheritance: C→T and v*→V inheritance ([Cho08]).

Design

A Phase is a tree-relative (tree, head) pair: the head function on SO is the selection-driven head (SO.selHead, Lemma 1.13.7), so the phase domain is read off the carrier with no separate head-function field. Every phase notion delegates to the SO.* phase API, so concrete PIC checks decide. isPhaseHeadOf c so is the projecting head's outer category — convention-independent (the carrier is unordered).

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

Generic phase-head test: is the projecting (selection-driven) head of so exactly c? ([MCB25] Lemma 1.13.7 — the selector projects.) Computable and convention-independent; none (≠ some c) at exocentric nodes.

Equations

• Minimalist.isPhaseHeadOf c so = Minimalist.SO.isPhaseHeadOf c so

Phase-head selectors

Only C is a phase head by default. [Kei20] (ch. 5) argues vP is NOT a phase. For commonly-checked phase categories, call isPhaseHeadOf directly:

• C as phase head: isPhaseHeadOf .C so (linglib default per [Kei20]). The classical [Cho00]/2001 v extension is isPhaseHeadOf .C so || isPhaseHeadOf .v so.
• D as phase head ([Cit14], [Sve04]): isPhaseHeadOf .D so — definite DPs as extraction/scope/spell-out barriers ([DD03], [SH26]).
• SA as phase head: isPhaseHeadOf .SA so — SAP is the highest phase, allocutive probing from SA is root-only.

Voice/v correspondence*: agentive Voice = v*, tracked by VoiceHead.IsPhasal (Voice.lean); recent clause-internal-Voice-phase clients are [ES25b] (Malayic) and [pietraszko-2026] (Ndebele).

inductive Minimalist.PICStrength : Type

The strength of the Phase Impenetrability Condition.

• strong (PIC₁, [Cho00]): only the edge of the immediately lower phase is accessible; the complement freezes when the phase head merges.
• weak (PIC₂, [Cho01]): the complement stays accessible until the next higher phase head merges.
• linearizationBound (no PIC, [FP05], [SCD26]): no structural opacity — movement out of a spelled-out phase is constrained only by the Cyclic-Linearization ordering table ([BD19], [LY24]). SCD 2026 argue this regime for Guébie discontinuous harmony. (Distinct from [Hal19]'s φ-relativized "Raising, unphased".)

The mode is load-bearing: it dispatches admitsExtraction and Agree's validAgreeWithPIC. Modular variants ([DAS15]) are not yet operationalized.

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

@[implicit_reducible]

instance Minimalist.instReprPICStrength : Repr PICStrength

Equations

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

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

Equations

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

@[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 ([MCB25] §1.14): a phase-head leaf head together with the containing tree tree. Phases are tree-relative; the head function is the carrier-native selection head (SO.selHead), so no separate head-function field is needed. Every phase notion — content Φ_ℓ (eq 1.14.2), interior Φ°_ℓ (eq 1.14.3), edge ∂Φ_ℓ (eq 1.14.4) — is a derived accessor over the SO.* phase API.

Per-analysis discipline (Keine 2020 C-only; Chomsky 2000/2001 C+v; Pietraszko 2026 / Erlewine & Sommerlot 2025 also Voice; Citko 2014 also D) is expressed by which leaf a study supplies as head.

• tree : SyntacticObject

  The containing tree T (phases are T-relative, MCB §1.14).

• head : LIToken

  The phase-head leaf ℓ; its maximal projection delimits the phase.

def Minimalist.Phase.content (φ : Phase) : Multiset SyntacticObject

The whole phase Φ_ℓ — all accessible terms in the maximal projection (MCB eq 1.14.2).

Equations

• φ.content = Minimalist.SO.phase φ.tree φ.head

def Minimalist.Phase.interior (φ : Phase) : Multiset SyntacticObject

The interior Φ°_ℓ — the complement domain (= the head's c-command domain); the part the PIC freezes (MCB eq 1.14.3, "Z is the interior of the phase").

Equations

• φ.interior = Minimalist.SO.phaseInterior φ.tree φ.head

def Minimalist.Phase.edge (φ : Phase) : Multiset SyntacticObject

The edge ∂Φ_ℓ — head, specifiers, and modifiers; stays accessible (MCB eq 1.14.4).

Equations

• φ.edge = Minimalist.SO.phaseEdge φ.tree φ.head

def Minimalist.Phase.Impenetrable (φ : Phase) (goal : SyntacticObject) : Prop

Phase Impenetrability Condition: goal is frozen in this phase iff it lies in the interior. True by construction — the PIC is interior membership ([MCB25] §1.14).

Equations

• φ.Impenetrable goal = (goal ∈ φ.interior)

@[implicit_reducible]

instance Minimalist.Phase.instDecidableImpenetrable (φ : Phase) (goal : SyntacticObject) : Decidable (φ.Impenetrable goal)

Equations

• φ.instDecidableImpenetrable goal = Minimalist.Phase.instDecidableImpenetrable._aux_1 φ goal

def Minimalist.Phase.IsWellFormed (φ : Phase) : Prop

A genuine phase: its head projects nontrivially (head ∈ L_Φ(T), MCB Def 1.14.3 eq 1.14.1) — γ_ℓ reaches an internal vertex.

Equations

• φ.IsWellFormed = Minimalist.SO.isPhaseHead φ.tree φ.head

@[implicit_reducible]

instance Minimalist.Phase.instDecidableIsWellFormed (φ : Phase) : Decidable φ.IsWellFormed

Equations

• φ.instDecidableIsWellFormed = Minimalist.Phase.instDecidableIsWellFormed._aux_1 φ

Spell-out triggers

A payload dispatched at the spell-out of matching phases. The payload is generic: the interpretive components read syntax, not conversely, so what a phase triggers — a constraint subranking ([SJI20]'s cophonologies by phase, Phonology/OptimalityTheory/Cophonology.lean), an allosemy rule, a realization rule — lives with the consuming component, and this layer knows only the dispatch.

structure Minimalist.Phase.Trigger (P : Type u_1) : Type u_1

A payload dispatched when a matching phase is spelled out: a phase-head predicate bundled with the payload it activates over the phase complement.

• selector : SyntacticObject → Bool

  Predicate selecting which phase heads activate this trigger.

• payload : P

  The payload dispatched over the matched phase.

def Minimalist.Phase.Trigger.appliesTo {P : Type u_1} (tr : Trigger P) (ph : Phase) : Bool

A trigger applies to a phase iff its selector matches the phase head (the head leaf ph.head, as a leaf SO).

Equations

• tr.appliesTo ph = tr.selector (Minimalist.SO.lexLeaf ph.head)

def Minimalist.Phase.selectTrigger {P : Type u_1} (registry : List (Trigger P)) (ph : Phase) : Option (Trigger P)

The first registered trigger whose selector matches the phase head — first-match encodes lexicographic precedence (the elsewhere ordering of [SJI20]). none when no trigger matches.

Equations

• Minimalist.Phase.selectTrigger registry ph = List.find? (fun (x : Minimalist.Phase.Trigger P) => x.appliesTo ph) registry

theorem Minimalist.Phase.selectTrigger_applies {P : Type u_1} {registry : List (Trigger P)} {ph : Phase} {tr : Trigger P} (h : selectTrigger registry ph = some tr) : tr.appliesTo ph = true

The selected trigger, when present, applies to the phase.

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

Phase φ admits extraction of goal under strength:

• strong/weak: goal is not frozen — ¬ φ.Impenetrable goal.
• linearizationBound: vacuously True — locality is enforced by Cyclic Linearization, not phasehood ([SCD26], [FP05]).

Equations

• Minimalist.admitsExtraction Minimalist.PICStrength.strong φ goal = ¬φ.Impenetrable goal
• Minimalist.admitsExtraction Minimalist.PICStrength.weak φ goal = ¬φ.Impenetrable goal
• Minimalist.admitsExtraction Minimalist.PICStrength.linearizationBound φ goal = True

@[implicit_reducible]

instance Minimalist.instDecidableAdmitsExtraction (strength : PICStrength) (φ : Phase) (goal : SyntacticObject) : Decidable (admitsExtraction strength φ 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 φ goal

Under linearizationBound, every phase admits extraction at the phasehood layer; concrete crashes come from the linearization table. The formal content of [SCD26]'s rejection of strict PIC.

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

Strict PIC₁/PIC₂ both block extraction of a goal frozen in the phase interior.

structure Minimalist.Transfer : Type

Transfer: ship a phase's interior Φ°_ℓ (= the complement domain, MCB eq 1.14.3) to the interfaces — PF (linearization, prosody) and LF (interpretation).

• phase : Phase

  The phase being transferred.

• toPF : Multiset SyntacticObject

  Material sent to PF (phonological form).

• toLF : Multiset SyntacticObject

  Material sent to LF (logical form).

• pf_is_interior : self.toPF = self.phase.interior

  PF domain = interior.

• lf_is_interior : self.toLF = self.phase.interior

  LF domain = interior.

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

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

Equations

• Minimalist.Transfer.fromPhase ph = { phase := ph, toPF := ph.interior, toLF := ph.interior, pf_is_interior := ⋯, lf_is_interior := ⋯ }

Feature Inheritance and KEEP/SHARE/DONATE

[Cho08]'s feature inheritance passes operational features from a phase head to its complement (C → T, v* → V); the head keeps edge features. [Oua08] observes "inheritance" is one of three parametric operations on adjacent functional heads (Berber agreement/anti-agreement diagnoses the choice). [Oli26] extends the typology to Voice* → vMOD transfer in Romance restructuring: under SHARE, φ surfaces at vMOD as well, which is what licenses clitic climbing.

inductive Minimalist.TransferStyle : Type

Style of φ-feature transfer between two adjacent functional heads ([Oua08]).

• keep: φ stays at source — target lacks φ.
• share: φ surfaces at both source and target. Explains clitic reduplication and licenses clitic climbing in [Oli26]'s Voice* → vMOD analysis.
• donate: φ moves source → target. The classical [Cho08] 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 [Cho08]'s C → T / v* → V inheritance (.donate) to [Oua08]'s KEEP/SHARE/DONATE typology and [Oli26]'s Voice* → vMOD .share extension.

• source : SyntacticObject

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

• target : SyntacticObject

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

• locality : SO.immediatelyContains self.source self.target

  Source must immediately contain target.

• style : TransferStyle

  Which transfer operation applies (default: classical [Cho08] donate).

• transferred : FeatureBundle

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

def Minimalist.isPhaseBounded (mover : SyntacticObject) (phases : List Phase) : Prop

A movement is phase-bounded iff the mover is not frozen in the interior of any of the given phases. Under PIC, an element inside a phase interior (= complement) is inaccessible; movement must reach the edge before the phase completes.

Equations

• Minimalist.isPhaseBounded mover phases = ¬∃ ph ∈ phases, ph.Impenetrable mover

N/D-Incorporation ([DD03], [SH26])

[DD03] propose verbs of creation (VOCs) trigger LF noun incorporation — the object DP's head noun incorporates into the verb, neutralizing the DP's phasehood so extraction becomes possible. [SH26] adapt this: it is the determiner that undergoes covert head movement (following [Bos15] on phase collapse), neutralizing the PIC and explaining why VOCs ameliorate (but do not eliminate — the Specificity Condition still applies) definite island effects.

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, so the DP is no longer a phase boundary. Models the [DD03] / [SH26] VOC neutralization of the PIC for definite DPs. wasPhase is stored explicitly so a derivation can record a phasehood decision diverging from the bare categorial test isPhaseHeadOf .D dHead.

• dHead : SyntacticObject

  The D head (before incorporation).

• wasPhase : Bool

  Whether D was originally a phase head (set explicitly per derivation).

• incorporated : Bool

  Whether incorporation has applied.

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.