Phase theory on the SO carrier

[MCB25] §1.14 (Def 1.14.1–1.14.4); [Cho00].

P3b — phase-head identification: derived from the selection-driven head (SO.outerCatC, #800) — the projecting head's outer category. Because the head is the selector (Lemma 1.13.7), the test is convention-independent (the carrier is unordered anyway).

P3c-2 — the structural phase domain (Def 1.14.2–1.14.3), grounded directly in MCB rather than the legacy section-based phaseComplementZ/complementInPlanar walk (which carried a side parameter and a non-commutative <|> fallback — a section artifact with no place on the unordered carrier). MCB states everything in terms of subtrees, containment, and the head's sister — exactly the invariant, decidable P2 substrate (subtrees/Acc/containsOrEq/areSistersIn/cCommandsIn, #797–798) and the selection head (selHead, #800). So the whole phase domain is a filter over the already-lifted subterm API — no section, no Quot.out, no fresh PermEquiv proof, and every notion decides.

The keystone identity: the interior Φ°_ℓ (Def 1.14.3) is the phase head's c-command domain, {T_v ∈ Acc(T) | T_v ⊆ T_{s_ℓ}} = Acc.filter (cCommandsIn … (lexLeaf ℓ)) — the standard "complement domain = head's c-command domain" falling out of the formalization.

def Minimalist.SO.isPhaseHeadOf (c : Cat) (s : SO) : Bool

Phase-head test on SO ([MCB25] Lemma 1.13.7): is the projecting (selection-driven) head's outer category exactly c? none (≠ some c) at exocentric nodes. The carrier-native counterpart of Minimalist.isPhaseHeadOf.

Phase-head selectors (call directly): C — isPhaseHeadOf .C (linglib default per [Kei20]; the Chomsky v-phase extension is … .C s || … .v s); D — isPhaseHeadOf .D ([Cit14]); SA — isPhaseHeadOf .SA.

Equations

• Minimalist.SO.isPhaseHeadOf c s = (s.outerCatC == some c)

@[simp]

theorem Minimalist.SO.isPhaseHeadOf_lexLeaf (c : Cat) (tok : LIToken) : isPhaseHeadOf c (lexLeaf tok) = (tok.item.outerCat == c)

The phase domain (MCB Def 1.14.2–1.14.3)

The head function on SO is selHead (#800); a phase is relative to a tree T and a phase-head leaf ℓ (the study supplies which leaf, per the per-analysis discipline — C / C+v / +D / +Voice). Every notion is a filter over the invariant subterm API (subtrees/Acc/containsOrEq/areSistersIn/cCommandsIn), so it decides — no section, no Quot.out, no fresh PermEquiv proof.

def Minimalist.SO.isPhaseHead (T : SO) (ℓ : LIToken) : Prop

L_Φ(T) ([MCB25] Def 1.14.3 eq 1.14.1): ℓ is a phase head in T when its projection path γ_ℓ is nontrivial — the leaf lexLeaf ℓ has a mother whose head is still ℓ (so γ_ℓ reaches an internal vertex). Read off selHead at the mother; section-free.

Equations

• T.isPhaseHead ℓ = ∃ n ∈ T.subtrees, n.immediatelyContains (Minimalist.SO.lexLeaf ℓ) ∧ n.selHead = some ℓ

@[implicit_reducible]

instance Minimalist.instDecidableIsPhaseHead (T : SO) (ℓ : LIToken) : Decidable (T.isPhaseHead ℓ)

Equations

• Minimalist.instDecidableIsPhaseHead T ℓ = Multiset.decidableExistsMultiset

def Minimalist.SO.withinProjection (T : SO) (ℓ : LIToken) (Tv : SO) : Prop

Within the maximal projection T_v ⊆ T_{v_ℓ} ([MCB25] Def 1.14.3): section-free characterization — T_v is contained in some ℓ-headed subtree. The maximal projection v_ℓ is the largest ℓ-headed subtree, so T_v ⊆ T_{v_ℓ} iff T_v sits inside one of them (all ℓ-headed vertices lie on γ_ℓ below v_ℓ).

Equations

• T.withinProjection ℓ Tv = ∃ p ∈ T.subtrees, p.selHead = some ℓ ∧ p.containsOrEq Tv

@[implicit_reducible]

instance Minimalist.instDecidableWithinProjection (T : SO) (ℓ : LIToken) (Tv : SO) : Decidable (T.withinProjection ℓ Tv)

Equations

• Minimalist.instDecidableWithinProjection T ℓ Tv = Multiset.decidableExistsMultiset

def Minimalist.SO.phase (T : SO) (ℓ : LIToken) : Multiset SO

The phase Φ_ℓ ([MCB25] Def 1.14.3 eq 1.14.2): {T_v ∈ Acc'(T) | T_v ⊆ T_{v_ℓ}} — all accessible terms within the maximal projection (Acc'(T) = T.subtrees, including the root).

Equations

• T.phase ℓ = Multiset.filter (fun (Tv : Minimalist.SO) => T.withinProjection ℓ Tv) T.subtrees

def Minimalist.SO.phaseInterior (T : SO) (ℓ : LIToken) : Multiset SO

The interior Φ°_ℓ ([MCB25] Def 1.14.3 eq 1.14.3): {T_v ∈ Acc(T) | T_v ⊆ T_{s_ℓ}} — the head's sister T_{s_ℓ} and all of its accessible terms; the part the PIC freezes ("Z is the interior of the phase").

This is the phase head's c-command domain: T_v ⊆ T_{s_ℓ} exactly when the sister of ℓ contains-or-equals T_v, i.e. cCommandsIn T (lexLeaf ℓ) T_v (#798). The textbook "complement domain = head's c-command domain", by construction — and Acc(T) = T.Acc (non-root).

Equations

• T.phaseInterior ℓ = Multiset.filter (fun (Tv : Minimalist.SO) => T.cCommandsIn (Minimalist.SO.lexLeaf ℓ) Tv) T.Acc

def Minimalist.SO.phaseEdge (T : SO) (ℓ : LIToken) : Multiset SO

The edge ∂Φ_ℓ ([MCB25] Def 1.14.3 eq 1.14.4): {T_v ∈ Acc'(T) | T_v ⊆ T_{v_ℓ} ∧ T_v ⊄ T_{s_ℓ}} — the phase content not in the interior (head, specifiers, modifiers); = Φ_ℓ when the complement is empty. Computed as phase ∖ interior.

Equations

• T.phaseEdge ℓ = Multiset.filter (fun (Tv : Minimalist.SO) => Tv ∉ T.phaseInterior ℓ) (T.phase ℓ)

def Minimalist.SO.Impenetrable (T : SO) (ℓ : LIToken) (goal : SO) : Prop

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

Equations

• T.Impenetrable ℓ goal = (goal ∈ T.phaseInterior ℓ)

@[implicit_reducible]

instance Minimalist.instDecidableImpenetrable (T : SO) (ℓ : LIToken) (goal : SO) : Decidable (T.Impenetrable ℓ goal)

Equations

• Minimalist.instDecidableImpenetrable T ℓ goal = Minimalist.instDecidableImpenetrable._aux_1 T ℓ goal

Membership characterizations

@[simp]

theorem Minimalist.SO.mem_phase {T : SO} {ℓ : LIToken} {Tv : SO} : Tv ∈ T.phase ℓ ↔ Tv ∈ T.subtrees ∧ T.withinProjection ℓ Tv

@[simp]

theorem Minimalist.SO.mem_phaseInterior {T : SO} {ℓ : LIToken} {Tv : SO} : Tv ∈ T.phaseInterior ℓ ↔ Tv ∈ T.Acc ∧ T.cCommandsIn (lexLeaf ℓ) Tv

The interior is the phase head's (non-root) c-command domain — the keystone identity (MCB Def 1.14.3, "Z is the interior of the phase").

@[simp]

theorem Minimalist.SO.mem_phaseEdge {T : SO} {ℓ : LIToken} {Tv : SO} : Tv ∈ T.phaseEdge ℓ ↔ Tv ∈ T.phase ℓ ∧ Tv ∉ T.phaseInterior ℓ

theorem Minimalist.SO.Impenetrable_iff {T : SO} {ℓ : LIToken} {goal : SO} : T.Impenetrable ℓ goal ↔ goal ∈ T.Acc ∧ T.cCommandsIn (lexLeaf ℓ) goal

The PIC freezes exactly the head's (non-root) c-command domain.

decide demonstrations

Phase-head checks reduce on concrete mk-built trees. A two-leaf clause where the left head c-selects the right: the selector projects, regardless of which side it sits on (the carrier is unordered) — so the phase head is the selector.

decide demonstrations — the phase domain

A clause [C [T V]]: C selects T, T selects V, so C projects and its sister is the TP. The phase headed by C freezes everything inside TP (the interior), keeps C itself at the edge. Both layers tested: a deep term is impenetrable, the head is not, and the head's projection is detected.