Documentation

@[implicit_reducible]

instance Minimalist.instReprCatFeatures :

Repr CatFeatures

Equations

Minimalist.instReprCatFeatures = { reprPrec := Minimalist.instReprCatFeatures.repr }

def Minimalist.instReprCatFeatures.repr :

CatFeatures → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqCatFeatures :

DecidableEq CatFeatures

Equations

Minimalist.instDecidableEqCatFeatures = Minimalist.instDecidableEqCatFeatures.decEq

def Minimalist.instDecidableEqCatFeatures.decEq (x✝ x✝¹ : CatFeatures) :

Decidable (x✝ = x✝¹)

Equations

Minimalist.instDecidableEqCatFeatures.decEq { plusV := a, plusN := a_1 } { plusV := b, plusN := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

def Minimalist.catFeatures :

Cat → CatFeatures

Compute @cite{chomsky-1970}'s [±V, ±N] features from Cat. Functional categories inherit features from their lexical anchor:

v, T, C inherit [+V, -N] from V
n, Num, Q, D inherit [-V, +N] from N

Equations

Minimalist.catFeatures Minimalist.Cat.V = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.v = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Voice = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Appl = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.T = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Foc = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Top = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Fin = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.C = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.SA = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Force = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Neg = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Mod = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Rel = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Pol = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Asp = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Evid = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Nmlz = { plusV := true, plusN := false }
Minimalist.catFeatures Minimalist.Cat.N = { plusV := false, plusN := true }
Minimalist.catFeatures Minimalist.Cat.n = { plusV := false, plusN := true }
Minimalist.catFeatures Minimalist.Cat.Num = { plusV := false, plusN := true }
Minimalist.catFeatures Minimalist.Cat.Q = { plusV := false, plusN := true }
Minimalist.catFeatures Minimalist.Cat.D = { plusV := false, plusN := true }
Minimalist.catFeatures Minimalist.Cat.K = { plusV := false, plusN := true }
Minimalist.catFeatures Minimalist.Cat.A = { plusV := true, plusN := true }
Minimalist.catFeatures Minimalist.Cat.a = { plusV := true, plusN := true }
Minimalist.catFeatures Minimalist.Cat.P = { plusV := false, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Place = { plusV := false, plusN := false }
Minimalist.catFeatures Minimalist.Cat.Path = { plusV := false, plusN := false }

Instances For

def Minimalist.fValue :

Cat → ℕ

Grimshaw's F-value: the functional level within an extended projection.

F-values are globally aligned across category families to capture the verbal–nominal parallelism.

The nominal spine follows @cite{borer-2005}'s ordering: Q (classifier / individuation, CL#) is at F2, below Num (number / counting, #) at F3. This reflects the semantic composition order: individuation must precede counting (you can't count what hasn't been individuated). See Borer2005.lean for the formal argument.

F-level	Role	Verbal	Nominal
F0	Lexical (content)	V	N
F1	Categorizer	v, Voice, Appl	n (gender/class)
F2	Specification	T, Neg, Asp, Mod	Q (classifier/CL#)
F3	Inner edge	Fin	Num (number/#)
F4	Discourse/ref	Foc	D (definiteness)
F5	Topic	Top, Rel
F6	Clause/force	C, Force
F7	Speech act	SA

Verbal–nominal parallelism: The parallelism is robust at F0 (lexical anchors) and F1 (categorizers: v ↔ n). At F2–F3, the verbal and nominal spines are analogous but not isomorphic: T/Asp specify temporal properties while Q specifies individuation; Fin types the clause while Num types the nominal. The semantic functions differ, but both occupy the same structural zone.

The verbal C-domain is internally ordered per @cite{rizzi-1997}: Fin(F3) < Foc(F4) < Top(F5) < C(F6).

Equations

Instances For

def Minimalist.categoryConsistent (c1 c2 : Cat) :

Bool

Category consistency: two categories share [±V, ±N] features. This is the core constraint on Extended Projections — V and T are consistent (both [+V, -N]), but V and D are not.

Equations

Minimalist.categoryConsistent c1 c2 = (Minimalist.catFeatures c1 == Minimalist.catFeatures c2)

Instances For

def Minimalist.fMonotone (lower upper : Cat) :

Bool

F-value monotonicity: F-values must not decrease going up the tree. In an EP, each head's F-value is ≥ the one below it.

Equations

Minimalist.fMonotone lower upper = decide (Minimalist.fValue lower ≤ Minimalist.fValue upper)

Instances For

def Minimalist.perfectProjection (c1 c2 : Cat) :

Bool

Perfect projection: same [±V, ±N] AND same F-value. E.g., two V heads (F0, [+V, -N]) are perfect projections of each other. Distinct from EP extension, where F-value increases.

Equations

Minimalist.perfectProjection c1 c2 = (Minimalist.categoryConsistent c1 c2 && Minimalist.fValue c1 == Minimalist.fValue c2)

Instances For

def Minimalist.isLHead (c : Cat) :

Bool

Is this category a lexical head (F0)? L-heads are content categories: V, N, A, P.

Equations

Minimalist.isLHead c = (Minimalist.fValue c == 0)

Instances For

def Minimalist.isFHead (c : Cat) :

Bool

Is this category a functional head (F1+)? F-heads are functional categories: v, D, T, C.

Equations

Minimalist.isFHead c = decide (Minimalist.fValue c > 0)

Instances For

def Minimalist.isCPArea (c : Cat) :

Bool

Is this category in the CP area (left periphery)? @cite{rizzi-1997}: Fin (F3) is the boundary between the inflectional domain (F0–F2) and the left periphery (F3+). Categories at or above Fin belong to the CP area.

Equations

Minimalist.isCPArea c = decide (Minimalist.fValue c ≥ Minimalist.fValue Minimalist.Cat.Fin)

Instances For

inductive Minimalist.CatFamily :

The four lexical category families, each defining an EP domain. All categories in an EP must belong to the same family.

verbal : CatFamily
nominal : CatFamily
adjectival : CatFamily
adpositional : CatFamily

Instances For

def Minimalist.instReprCatFamily.repr :

CatFamily → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.instReprCatFamily :

Repr CatFamily

Equations

Minimalist.instReprCatFamily = { reprPrec := Minimalist.instReprCatFamily.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqCatFamily :

DecidableEq CatFamily

Equations

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

def Minimalist.catFamily :

Cat → CatFamily

Map a category to its family. This determines which EP it can participate.

Equations

Instances For

structure Minimalist.CategorialFeatures :

@cite{panagiotidis-2015} categorial features: [N] and [V] as substantive, LF-interpretable features with semantic content.

[N] = sortal perspective / referentiality (capacity to introduce a discourse referent, following @cite{longobardi-1994}, @cite{longobardi-2005}; §4.3 p84)
[V] = temporal perspective / eventivity (capacity to anchor to time/events; §4.3 p85)

This contrasts with @cite{chomsky-1970}'s [±V, ±N] diacritics (see CatFeatures): Chomsky's features are arbitrary binary cross-classifiers, while Panagiotidis's are grounded in semantic substance. The key empirical difference is the status of P: Chomsky treats P as actively bearing [-V, -N]; Panagiotidis treats P as the default categorizer lacking both [N] and [V] (§4.3).

Interpretability distinction (§5.8): On categorizers (v, n, a), these features are interpretable — they provide the LF-legible interpretive perspective (sortal or temporal). On higher functional heads (T, C, D, etc.), these features are uninterpretable copies that serve only for Agree/selection. This formalization does not encode the interpretable/uninterpretable distinction but records which features are present, which suffices for EP consistency.

Despite the conceptual difference, the two systems produce the same four equivalence classes over categories (see chomsky_panagiotidis_agree).

hasN : Bool
hasV : Bool

Instances For

@[implicit_reducible]

instance Minimalist.instReprCategorialFeatures :

Repr CategorialFeatures

Equations

Minimalist.instReprCategorialFeatures = { reprPrec := Minimalist.instReprCategorialFeatures.repr }

def Minimalist.instReprCategorialFeatures.repr :

CategorialFeatures → ℕ → Std.Format

Equations

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

Instances For

def Minimalist.instDecidableEqCategorialFeatures.decEq (x✝ x✝¹ : CategorialFeatures) :

Decidable (x✝ = x✝¹)

Equations

Minimalist.instDecidableEqCategorialFeatures.decEq { hasN := a, hasV := a_1 } { hasN := b, hasV := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqCategorialFeatures :

DecidableEq CategorialFeatures

Equations

Minimalist.instDecidableEqCategorialFeatures = Minimalist.instDecidableEqCategorialFeatures.decEq

def Minimalist.categorialFeatures :

Cat → CategorialFeatures

Map a category to @cite{panagiotidis-2015}'s categorial features.

Categorizers (n, v, a) bear the substantive features; functional heads in the same EP inherit them (just as in Grimshaw's consistency requirement). P and its extended projection bear neither feature — P is the default case.

Equations

Minimalist.categorialFeatures Minimalist.Cat.V = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.v = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Voice = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Appl = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.T = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Foc = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Top = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Fin = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.C = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.SA = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Force = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Neg = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Mod = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Rel = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Pol = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Asp = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Evid = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.Nmlz = { hasN := false, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.N = { hasN := true, hasV := false }
Minimalist.categorialFeatures Minimalist.Cat.n = { hasN := true, hasV := false }
Minimalist.categorialFeatures Minimalist.Cat.Num = { hasN := true, hasV := false }
Minimalist.categorialFeatures Minimalist.Cat.Q = { hasN := true, hasV := false }
Minimalist.categorialFeatures Minimalist.Cat.D = { hasN := true, hasV := false }
Minimalist.categorialFeatures Minimalist.Cat.K = { hasN := true, hasV := false }
Minimalist.categorialFeatures Minimalist.Cat.A = { hasN := true, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.a = { hasN := true, hasV := true }
Minimalist.categorialFeatures Minimalist.Cat.P = { hasN := false, hasV := false }
Minimalist.categorialFeatures Minimalist.Cat.Place = { hasN := false, hasV := false }
Minimalist.categorialFeatures Minimalist.Cat.Path = { hasN := false, hasV := false }

Instances For

def Minimalist.categorialConsistent (c1 c2 : Cat) :

Bool

Consistency under Panagiotidis's system: two categories share [N]/[V] features.

Equations

Minimalist.categorialConsistent c1 c2 = (Minimalist.categorialFeatures c1 == Minimalist.categorialFeatures c2)

Instances For

theorem Minimalist.chomsky_panagiotidis_agree (c1 c2 : Cat) :

categoryConsistent c1 c2 = categorialConsistent c1 c2

Chomsky's [±V, ±N] and Panagiotidis's [N]/[V] produce the same equivalence classes over all categories. They agree on which pairs are EP-consistent.

The conceptual difference — P as [-V, -N] vs. P as default — is invisible to the consistency check: both systems group P only with itself.

structure Minimalist.ExtendedProjection :

An Extended Projection: a sequence of categories forming a projection chain with category consistency and F-value monotonicity.

The spine lists categories from lowest (lexical head) to highest (functional).

root : SyntacticObject
Root syntactic object of the EP
spine : List Cat
Categories along the spine, from lexical head (F0) upward
catConsistent : Bool
All spine categories share [±V, ±N] features
fMonotoneChain : Bool
F-values are non-decreasing along the spine

Instances For

def Minimalist.allCategoryConsistent :

List Cat → Bool

Check that a list of categories is category-consistent (all share the same [±V, ±N] features).

Equations

Minimalist.allCategoryConsistent [] = true
Minimalist.allCategoryConsistent [head] = true
Minimalist.allCategoryConsistent (c₁ :: c₂ :: rest) = (Minimalist.categoryConsistent c₁ c₂ && Minimalist.allCategoryConsistent (c₂ :: rest))

Instances For

def Minimalist.allFMonotone :

List Cat → Bool

Check that a list of categories has monotonically non-decreasing F-values.

Equations

Minimalist.allFMonotone [] = true
Minimalist.allFMonotone [head] = true
Minimalist.allFMonotone (c₁ :: c₂ :: rest) = (Minimalist.fMonotone c₁ c₂ && Minimalist.allFMonotone (c₂ :: rest))

Instances For

noncomputable def Minimalist.computeEPSpine (so : SyntacticObject) :

List (SyntacticObject × Cat)

Compute the EP spine from a syntactic object by walking the leftmost-leaf head chain (= HeadFunction.leftSpine per @cite{marcolli-chomsky-berwick-2025} §1.13). Returns pairs of (SO, Cat) from the deepest lexical head up to the root.

For a non-leftmost-headed analysis, replace the recursion's a with the daughter whose head leaf matches HeadFunction.leftSpine.outerCat so under the chosen head function, or rewrite this helper to take a HeadFunction parameter. Phase 1.0 noncomputable.

Equations

Minimalist.computeEPSpine so = Minimalist.computeEPSpinePlanar✝ (Quot.out so)

Instances For

noncomputable def Minimalist.mkExtendedProjection (so : SyntacticObject) :

ExtendedProjection

Build an ExtendedProjection from a syntactic object using the leftmost-leaf head chain.

Equations

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

Instances For

def Minimalist.ExtendedProjection.isWellFormed (ep : ExtendedProjection) :

Bool

Is this EP well-formed? (category consistent AND F-monotone)

Equations

ep.isWellFormed = (ep.catConsistent && ep.fMonotoneChain)

Instances For

def Minimalist.ExtendedProjection.family (ep : ExtendedProjection) :

Option CatFamily

The family of an EP (determined by any element of the spine).

Equations

ep.family = Option.map Minimalist.catFamily ep.spine.head?

Instances For

def Minimalist.ExtendedProjection.lexicalAnchor (ep : ExtendedProjection) :

Option Cat

The lexical anchor of an EP (the F0 head at the bottom).

Equations

ep.lexicalAnchor = Option.filter Minimalist.isLHead ep.spine.head?

Instances For

def Minimalist.ExtendedProjection.highestHead (ep : ExtendedProjection) :

Option Cat

The highest functional head in the EP.

Equations

ep.highestHead = ep.spine.getLast?

Instances For

theorem Minimalist.verbal_chain_consistent :

categoryConsistent Cat.V Cat.v = true ∧ categoryConsistent Cat.v Cat.T = true ∧ categoryConsistent Cat.T Cat.C = true

The verbal chain V → v → T → C is category-consistent: all share [+V, -N] features.

theorem Minimalist.nominal_chain_consistent :

categoryConsistent Cat.N Cat.n = true ∧ categoryConsistent Cat.n Cat.Q = true ∧ categoryConsistent Cat.Q Cat.Num = true ∧ categoryConsistent Cat.Num Cat.D = true

The nominal chain N → n → Q → Num → D is category-consistent: all have [-V, +N] features. Q (CL#, individuation) is below Num (#, counting) per @cite{borer-2005}.

theorem Minimalist.verbal_fvalues_monotone :

fValue Cat.V ≤ fValue Cat.v ∧ fValue Cat.v ≤ fValue Cat.T ∧ fValue Cat.T ≤ fValue Cat.C

F-values increase monotonically along the verbal chain: V(0) ≤ v(1) ≤ T(2) ≤ C(3).

theorem Minimalist.nominal_fvalues_monotone :

fValue Cat.N ≤ fValue Cat.n ∧ fValue Cat.n ≤ fValue Cat.Q ∧ fValue Cat.Q ≤ fValue Cat.Num ∧ fValue Cat.Num ≤ fValue Cat.D

F-values increase along the nominal chain: N(0) ≤ n(1) ≤ Q(2) ≤ Num(3) ≤ D(4). Q (individuation) is below Num (counting) per @cite{borer-2005}.

theorem Minimalist.verbal_nominal_inconsistent :

categoryConsistent Cat.V Cat.N = false

V and N are NOT category-consistent (different [±V, ±N]).

theorem Minimalist.verbal_determiner_inconsistent :

categoryConsistent Cat.V Cat.D = false

V and D are NOT category-consistent (verbal ≠ nominal).

theorem Minimalist.f0_iff_lexical (c : Cat) :

isLHead c = true ↔ c = Cat.V ∨ c = Cat.N ∨ c = Cat.A ∨ c = Cat.P

F0 is exactly the lexical heads.

theorem Minimalist.fpos_iff_not_lexical (c : Cat) :

isFHead c = true ↔ isLHead c = false

Functional heads are exactly the non-lexical heads: F1+ ↔ ¬F0.

theorem Minimalist.same_family_consistent (c1 c2 : Cat) :

catFamily c1 = catFamily c2 → categoryConsistent c1 c2 = true

Categories in the same family are category-consistent.

theorem Minimalist.full_verbal_ep_consistent :

allCategoryConsistent [Cat.V, Cat.v, Cat.T, Cat.C] = true

The full verbal EP spine [V, v, T, C] is category-consistent.

theorem Minimalist.full_verbal_ep_monotone :

allFMonotone [Cat.V, Cat.v, Cat.T, Cat.C] = true

The full verbal EP spine [V, v, T, C] is F-monotone.

theorem Minimalist.full_nominal_ep_consistent :

allCategoryConsistent [Cat.N, Cat.n, Cat.Q, Cat.Num, Cat.D] = true

The full nominal EP spine [N, n, Q, Num, D] is category-consistent.

theorem Minimalist.full_nominal_ep_monotone :

allFMonotone [Cat.N, Cat.n, Cat.Q, Cat.Num, Cat.D] = true

The full nominal EP spine [N, n, Q, Num, D] is F-monotone.

theorem Minimalist.f0_corresponds_to_head :

isLHead Cat.V = true ∧ isLHead Cat.N = true ∧ isLHead Cat.A = true ∧ isLHead Cat.P = true

F0 categories correspond to BarLevel.zero (head), F1+ categories correspond to intermediate/maximal projections. This connects Grimshaw's F-level to X-bar bar levels.

theorem Minimalist.fhead_extends_projection :

isFHead Cat.v = true ∧ isFHead Cat.n = true ∧ isFHead Cat.a = true ∧ isFHead Cat.Place = true ∧ isFHead Cat.Path = true ∧ isFHead Cat.Num = true ∧ isFHead Cat.Q = true ∧ isFHead Cat.D = true ∧ isFHead Cat.T = true ∧ isFHead Cat.C = true

Functional heads (F1+) extend the projection beyond the lexical head.

theorem Minimalist.verbal_nominal_parallel :

fValue Cat.V = fValue Cat.N ∧ fValue Cat.v = fValue Cat.n ∧ fValue Cat.T = fValue Cat.Q ∧ fValue Cat.Fin = fValue Cat.Num

The verbal and nominal spines are parallel at F0–F1: V ↔ N (lexical), v ↔ n (categorizer).

At F2–F3 the spines diverge: T (temporal specification, F2) pairs with Q (individuation, F2), while Fin (clause-typing, F3) pairs with Num (number, F3). These are structural analogs occupying the same EP zone, but their semantic functions differ. See borer_ordering_unique in Borer2005.lean for the formal argument that Q must be below Num.

def Minimalist.isCategorizer (c : Cat) :

Bool

Is this category a categorizer? Categorizers bear substantive, interpretable [N]/[V] features and combine with acategorial roots to yield categorized items.

Important: Panagiotidis (§4.5) argues categorizers are NOT functional heads — they are the only true lexical heads (roots being acategorial). Our F-value system (from @cite{grimshaw-2005}) places them at F1, which makes isFHead return true for categorizers. This reflects Grimshaw's architectural classification, not Panagiotidis's ontological claim about their nature.

Equations

Minimalist.isCategorizer Minimalist.Cat.v = true
Minimalist.isCategorizer Minimalist.Cat.n = true
Minimalist.isCategorizer Minimalist.Cat.a = true
Minimalist.isCategorizer c = false

Instances For

theorem Minimalist.categorizers_at_f1 :

fValue Cat.v = 1 ∧ fValue Cat.n = 1 ∧ fValue Cat.a = 1

All three categorizers are at F1 in @cite{grimshaw-2005}'s F-value system. @cite{panagiotidis-2015} predicts this parallelism; the F1 encoding is Grimshaw's.

theorem Minimalist.categorizer_parallel :

fValue Cat.v = fValue Cat.n ∧ fValue Cat.n = fValue Cat.a

The three categorizers are parallel: all at the same F-level.

theorem Minimalist.a_in_adjectival_family :

catFamily Cat.a = CatFamily.adjectival

The adjectival categorizer is in the adjectival family (parallel to v→verbal, n→nominal).

theorem Minimalist.adpositional_chain_consistent :

categoryConsistent Cat.P Cat.Place = true ∧ categoryConsistent Cat.Place Cat.Path = true

The adpositional chain P → Place → Path is category-consistent: all share [-V, -N] features. @cite{dendikken-2010}: PlaceP (locational) and PathP (directional) are functional projections above P.

theorem Minimalist.adpositional_fvalues_monotone :

fValue Cat.P ≤ fValue Cat.Place ∧ fValue Cat.Place ≤ fValue Cat.Path

F-values increase along the adpositional chain: P(0) ≤ Place(1) ≤ Path(2). Parallel to V(0) ≤ v(1) ≤ T(2) in the verbal domain.

theorem Minimalist.place_path_adpositional :

catFamily Cat.Place = CatFamily.adpositional ∧ catFamily Cat.Path = CatFamily.adpositional

Place and Path are in the adpositional family.

theorem Minimalist.locational_pp_wellformed :

allCategoryConsistent [Cat.P, Cat.Place] = true ∧ allFMonotone [Cat.P, Cat.Place] = true

The adpositional EP spine [P, Place] is well-formed (locational PP).

theorem Minimalist.directional_pp_wellformed :

allCategoryConsistent [Cat.P, Cat.Place, Cat.Path] = true ∧ allFMonotone [Cat.P, Cat.Place, Cat.Path] = true

The adpositional EP spine [P, Place, Path] is well-formed (directional PP). @cite{dendikken-2010}: directional PPs project PathP above PlaceP.

def Minimalist.splitCPVerbalEP :

List Cat

The verbal EP spine with @cite{rizzi-1997}'s split-CP layer: V → v → T → Fin → Foc → Top → C. Fin is the boundary between IP and CP; Foc and Top are discourse-related projections between Fin and C (= Force).

Equations

Minimalist.splitCPVerbalEP = [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T, Minimalist.Cat.Fin, Minimalist.Cat.Foc, Minimalist.Cat.Top, Minimalist.Cat.C]

Instances For

theorem Minimalist.splitCP_ep_consistent :

allCategoryConsistent splitCPVerbalEP = true

The split-CP spine is category-consistent: all heads share [+V, -N].

theorem Minimalist.splitCP_ep_monotone :

allFMonotone splitCPVerbalEP = true

The split-CP spine is F-monotone: 0 ≤ 1 ≤ 2 ≤ 3 ≤ 4 ≤ 5 ≤ 6. This is the key payoff of the fValue fix — before the fix, Fin/Foc/Top/C all had fValue 3, so any permutation would trivially pass.

theorem Minimalist.reverse_splitCP_not_monotone :

allFMonotone [Cat.Top, Cat.Foc, Cat.Fin] = false

The reverse split-CP ordering [Top, Foc, Fin] is NOT monotone. This correctly rules out pathological orderings that the collapsed fValues (all = 3) would have accepted.

def Minimalist.negVerbalEP :

List Cat

Verbal EP with NegP: V → v → Neg → T → Fin → C. Represents a clause with an IP-internal negation layer.

Equations

Minimalist.negVerbalEP = [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.Neg, Minimalist.Cat.T, Minimalist.Cat.Fin, Minimalist.Cat.C]

Instances For

theorem Minimalist.neg_verbal_ep_consistent :

allCategoryConsistent negVerbalEP = true

The verbal EP with NegP is category-consistent.

theorem Minimalist.neg_verbal_ep_monotone :

allFMonotone negVerbalEP = true

The verbal EP with NegP is F-monotone: 0 ≤ 1 ≤ 2 ≤ 2 ≤ 3 ≤ 6.

def Minimalist.fullRizziLP :

List Cat

Full Rizzi left periphery: V → v → T → Fin → Foc → Top → Force. Force is the clause-typing head when the CP is fully split.

Equations

Minimalist.fullRizziLP = [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T, Minimalist.Cat.Fin, Minimalist.Cat.Foc, Minimalist.Cat.Top, Minimalist.Cat.Force]

Instances For

theorem Minimalist.fullRizziLP_consistent :

allCategoryConsistent fullRizziLP = true

The full Rizzi left periphery is category-consistent.

theorem Minimalist.fullRizziLP_monotone :

allFMonotone fullRizziLP = true

The full Rizzi left periphery is F-monotone.

theorem Minimalist.force_equals_c_fvalue :

fValue Cat.Force = fValue Cat.C

Force and C have the same fValue (they're the same position when unsplit).

theorem Minimalist.neg_in_specification_domain :

fValue Cat.Neg = fValue Cat.T

Neg is in the specification domain (same F-level as T and Q).

theorem Minimalist.new_heads_verbal :

catFamily Cat.Force = CatFamily.verbal ∧ catFamily Cat.Neg = CatFamily.verbal ∧ catFamily Cat.Mod = CatFamily.verbal ∧ catFamily Cat.Rel = CatFamily.verbal ∧ catFamily Cat.Pol = CatFamily.verbal

New functional heads are all in the verbal family.

theorem Minimalist.nominal_functional_heads :

catFamily Cat.n = CatFamily.nominal ∧ catFamily Cat.Num = CatFamily.nominal ∧ catFamily Cat.Q = CatFamily.nominal

Nominal functional heads are in the nominal family.

structure Minimalist.ComplementSize :

The structural size of a clausal complement, determined by the highest functional head projected.

Complement size matters for tense Agree locality: a CP complement constitutes a phase boundary that blocks upward Agree for [uPAST], while a TP complement is transparent.

Also relevant for @cite{wurmbrand-2014}'s three-way infinitival classification (restructuring ≈ vP, propositional ≈ TP, full finite ≈ CP).

highestHead : Cat
The highest functional head in the complement

Instances For

def Minimalist.instDecidableEqComplementSize.decEq (x✝ x✝¹ : ComplementSize) :

Decidable (x✝ = x✝¹)

Equations

Minimalist.instDecidableEqComplementSize.decEq { highestHead := a } { highestHead := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqComplementSize :

DecidableEq ComplementSize

Equations

Minimalist.instDecidableEqComplementSize = Minimalist.instDecidableEqComplementSize.decEq

def Minimalist.instReprComplementSize.repr :

ComplementSize → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.instReprComplementSize :

Repr ComplementSize

Equations

Minimalist.instReprComplementSize = { reprPrec := Minimalist.instReprComplementSize.repr }

def Minimalist.ComplementSize.fLevel (cs : ComplementSize) :

ℕ

The F-level of a complement (derived from fValue).

Equations

cs.fLevel = Minimalist.fValue cs.highestHead

Instances For

def Minimalist.ComplementSize.isPhaseSized (cs : ComplementSize) :

Bool

A complement is phase-sized (≥ CP) if its highest head is at or above the C level in the functional sequence.

Equations

cs.isPhaseSized = decide (Minimalist.fValue Minimalist.Cat.C ≤ cs.fLevel)

Instances For

def Minimalist.ComplementSize.transparentToTenseAgree (cs : ComplementSize) :

Bool

A complement is transparent to tense Agree if it is smaller than a full CP — i.e., the highest head is below C in the fseq.

@cite{egressy-2026}: TP complements (fValue 2) are transparent; CP complements (fValue 6) are opaque.

Equations

cs.transparentToTenseAgree = decide (cs.fLevel < Minimalist.fValue Minimalist.Cat.C)

Instances For

def Minimalist.ComplementSize.vP :

Standard complement sizes.

Equations

Minimalist.ComplementSize.vP = { highestHead := Minimalist.Cat.v }

Instances For

def Minimalist.ComplementSize.tP :

Equations

Minimalist.ComplementSize.tP = { highestHead := Minimalist.Cat.T }

Instances For

def Minimalist.ComplementSize.finP :

Equations

Minimalist.ComplementSize.finP = { highestHead := Minimalist.Cat.Fin }

Instances For

def Minimalist.ComplementSize.cP :

Equations

Minimalist.ComplementSize.cP = { highestHead := Minimalist.Cat.C }

Instances For

def Minimalist.ComplementSize.forceP :

Equations

Minimalist.ComplementSize.forceP = { highestHead := Minimalist.Cat.Force }

Instances For

def Minimalist.ComplementSize.saP :

Equations

Minimalist.ComplementSize.saP = { highestHead := Minimalist.Cat.SA }

Instances For

theorem Minimalist.vP_transparent :

ComplementSize.vP.transparentToTenseAgree = true

vP complements are transparent to tense Agree.

theorem Minimalist.tP_transparent :

ComplementSize.tP.transparentToTenseAgree = true

TP complements are transparent to tense Agree.

theorem Minimalist.finP_transparent :

ComplementSize.finP.transparentToTenseAgree = true

FinP complements are transparent to tense Agree.

theorem Minimalist.cP_opaque :

ComplementSize.cP.transparentToTenseAgree = false

CP complements are opaque to tense Agree.

theorem Minimalist.forceP_opaque :

ComplementSize.forceP.transparentToTenseAgree = false

ForceP complements are opaque to tense Agree.

theorem Minimalist.saP_opaque :

ComplementSize.saP.transparentToTenseAgree = false

SAP complements are opaque to tense Agree.

theorem Minimalist.complement_size_ordering :

ComplementSize.vP.fLevel < ComplementSize.tP.fLevel ∧ ComplementSize.tP.fLevel < ComplementSize.finP.fLevel ∧ ComplementSize.finP.fLevel < ComplementSize.cP.fLevel

Size ordering: vP < TP < FinP < CP.

inductive Minimalist.ForceHead :

The seven clause-type heads in @cite{westergaard-2009}'s split-ForceP. Each represents a possible target for verb movement.

@cite{westergaard-2009} splits @cite{rizzi-1997}'s ForceP into clause-type-specific projections: DeclP, IntP, PolP, ExclP, ImpP are all "flavors of Force" in the CP domain, while FinP and WhP handle embedded contexts. This decomposition allows V2 to be treated as multiple independent micro-parameters rather than a single macro-parameter.

All seven heads are at or above FinP. The five root-clause heads (Decl, Int, Pol, Excl, Imp) are finer-grained than @cite{rizzi-1997}'s single Force head — they are all at the Force level (F6). Fin° corresponds to Cat.Fin (F3); Wh° is at the Force level (F6).

Decl : ForceHead
Int : ForceHead
Pol : ForceHead
Excl : ForceHead
Imp : ForceHead
Fin : ForceHead
Wh : ForceHead

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqForceHead :

DecidableEq ForceHead

Equations

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

@[implicit_reducible]

instance Minimalist.instReprForceHead :

Repr ForceHead

Equations

Minimalist.instReprForceHead = { reprPrec := Minimalist.instReprForceHead.repr }

def Minimalist.instReprForceHead.repr :

ForceHead → ℕ → Std.Format

Equations

Minimalist.instReprForceHead.repr Minimalist.ForceHead.Decl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.ForceHead.Decl")).group prec✝
Minimalist.instReprForceHead.repr Minimalist.ForceHead.Int prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.ForceHead.Int")).group prec✝
Minimalist.instReprForceHead.repr Minimalist.ForceHead.Pol prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.ForceHead.Pol")).group prec✝
Minimalist.instReprForceHead.repr Minimalist.ForceHead.Excl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.ForceHead.Excl")).group prec✝
Minimalist.instReprForceHead.repr Minimalist.ForceHead.Imp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.ForceHead.Imp")).group prec✝
Minimalist.instReprForceHead.repr Minimalist.ForceHead.Fin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.ForceHead.Fin")).group prec✝
Minimalist.instReprForceHead.repr Minimalist.ForceHead.Wh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.ForceHead.Wh")).group prec✝

Instances For

@[implicit_reducible]

instance Minimalist.instInhabitedForceHead :

Inhabited ForceHead

Equations

Minimalist.instInhabitedForceHead = { default := Minimalist.instInhabitedForceHead.default }

def Minimalist.instInhabitedForceHead.default :

ForceHead

Equations

Minimalist.instInhabitedForceHead.default = Minimalist.ForceHead.Decl

Instances For

@[implicit_reducible]

instance Minimalist.instFintypeForceHead :

Fintype ForceHead

Equations

Minimalist.instFintypeForceHead = { elems := { val := ↑Minimalist.ForceHead.enumList, nodup := Minimalist.ForceHead.enumList_nodup }, complete := Minimalist.instFintypeForceHead._proof_1 }

def Minimalist.ForceHead.IsRootClause :

ForceHead → Prop

A root-clause force head (in the Force domain), as opposed to a lower/embedded head (Fin, Wh).

Equations

Minimalist.ForceHead.Decl.IsRootClause = True
Minimalist.ForceHead.Int.IsRootClause = True
Minimalist.ForceHead.Pol.IsRootClause = True
Minimalist.ForceHead.Excl.IsRootClause = True
Minimalist.ForceHead.Imp.IsRootClause = True
Minimalist.ForceHead.Fin.IsRootClause = False
Minimalist.ForceHead.Wh.IsRootClause = False

Instances For

@[implicit_reducible]

instance Minimalist.instDecidablePredForceHeadIsRootClause :

DecidablePred ForceHead.IsRootClause

Equations

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

def Minimalist.ForceHead.toCat :

ForceHead → Cat

Map a ForceHead to the corresponding Cat. The five root-clause heads all map to Cat.Force (they are flavors of Force); Fin maps to Cat.Fin; Wh maps to Cat.C (embedded complementizer domain).

Equations

Instances For

theorem Minimalist.forceHead_verbal (fh : ForceHead) :

catFamily fh.toCat = CatFamily.verbal

All ForceHead values are in the verbal EP family.

@[reducible, inline]

abbrev Minimalist.V2Profile :

@cite{westergaard-2009}'s micro-parameter profile for V2: the set of clause-type heads at which verb movement is active (+) for a given language or dialect. Recast as Typology.Profile ForceHead so that fragment files can be written as set literals (e.g. {.Decl, .Int, .Pol, .Fin}) and cross-language comparison reuses the polymorphic Profile.activeCount / Profile.DiffersOnExactlyOne API.

Equations

Minimalist.V2Profile = Typology.Profile Minimalist.ForceHead

Instances For

inductive Minimalist.WhElementStatus :

The syntactic status of a wh-element: head (X°) or phrase (XP).

@cite{westergaard-2009} argues that monosyllabic wh-words (ka 'what', kem 'who', kor 'where' in the Tromsø dialect) are syntactic heads, while polysyllabic wh-constituents (korfor 'why', korsen 'how', katti 'when') are phrases. This distinction is supported by similar patterns in Italian dialects (@cite{poletto-pollock-2004}).

The distinction matters for V2: when a wh-head occupies Int°, it blocks verb movement to that position, making non-V2 possible. When a wh-phrase is in SpecIntP, Int° is free for the verb → V2 obligatory.

head : WhElementStatus
phrase : WhElementStatus

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqWhElementStatus :

DecidableEq WhElementStatus

Equations

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

def Minimalist.instReprWhElementStatus.repr :

WhElementStatus → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.instReprWhElementStatus :

Repr WhElementStatus

Equations

Minimalist.instReprWhElementStatus = { reprPrec := Minimalist.instReprWhElementStatus.repr }

def Minimalist.WhElementStatus.fromSyllableCount (n : ℕ) :

WhElementStatus

Determine wh-element status from syllable count. Monosyllabic → head; polysyllabic → phrase.

Equations

Minimalist.WhElementStatus.fromSyllableCount n = if n ≤ 1 then Minimalist.WhElementStatus.head else Minimalist.WhElementStatus.phrase

Instances For

WhElementStatus.fromSyllableCount 1 = WhElementStatus.head

theorem Minimalist.wh_mono_is_head :

Monosyllabic wh-words are heads.

WhElementStatus.fromSyllableCount 2 = WhElementStatus.phrase

theorem Minimalist.wh_poly_is_phrase :

Polysyllabic wh-words are phrases.

def Minimalist.WhBlocksMovementTo :

WhElementStatus → ForceHead → Prop

A wh-head in target position blocks verb movement to that head. Parameterized on the target ForceHead because the blocking effect is local: a monosyllabic ka head occupying Int° blocks V-to-Int°, but the same ka in an embedded relative or echo question doesn't block V-to-Decl° / V-to-Fin° / etc. Westergaard's blocking effect is specifically about the wh-question heads .Int (matrix) and .Wh (embedded).

Equations

Instances For