Feature Checking: The Derivational Lifecycle

@cite{chomsky-1995}

The four-stage lifecycle of formal features in the Minimalist Program (Ch 4 §4.5; extended with @cite{preminger-2014} §5 "derivational time bombs" and @cite{hewett-2026} Def 23):

0. Inactive: feature is present but dormant — not yet accessible to checking. Must be activated by a syntactic trigger (feature activation, @cite{hewett-2026} Def 23) before entering the checking lifecycle. Inactive –Interpretable features crash at LF.
1. Active: feature is present and accessible to computation
2. Checked (= deleted): feature has entered a checking relation; invisible at LF but still accessible to the narrow syntax
3. Erased: feature is completely removed, inaccessible to all further computation

–Interpretable features must pass through stages 1–3 (or 0–3 if initially inactive) for the derivation to converge at LF. +Interpretable features remain active (they contribute to meaning and are never deleted).

Strong Features

A strong feature is a –Interpretable feature that must be checked before Spell-Out — i.e., by an overt operation. If a strong feature survives to Spell-Out unchecked, the derivation is canceled. Strong features are the locus of the overt/covert parametric variation: English T has a strong D-feature (EPP), forcing overt subject raising; languages without overt raising lack this strong feature.

Connection to Agree

The checking lifecycle predates long-distance Agree (@cite{chomsky-2000}). In the 1995 system, checking requires a local Spec-head or head-head configuration. The post-2000 Agree mechanism in Agree.lean subsumes checking: Agree values an unvalued feature, which is equivalent to checking + deletion in one step. This module formalizes the finer-grained 1995 lifecycle, which remains relevant for:

• Distinguishing deletion (LF-invisible) from erasure (computationally inaccessible) — erasure blocks further operations on the feature
• Strong features, which interact with Spell-Out timing
• The parametric variation that allows –Interpretable features to escape erasure after checking (multiple-Spec constructions)

Activation Indices

ActivationIndex α (§ 7) formalizes ordered n-tuple activation from @cite{hewett-2026} Def 23: a feature carries a tuple of keys (c₁, …, cₙ), and each c-commanding head strips c₁ if it matches. When the tuple is empty the feature transitions from .inactive to .active. Parametric over the key type α.

def Minimalist.isInterpretableOn (fv : FeatureVal) (host : Cat) : Interpretability

Whether a feature type is interpretable on a given host category.

@cite{chomsky-1995} Ch 4: Categorial features and φ-features of nouns are +Interpretable. Case features, φ-features on functional heads (T, v, C), and EPP/strong features are –Interpretable.

This encodes the default mapping. Individual languages or analyses may override (e.g., @cite{zeijlstra-2012} treats embedded tense as uninterpretable in SOT languages).

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.isInterpretableOn fv host = match fv.inherentInterpretability with | some i => i | none => Minimalist.Interpretability.interpretable

def Minimalist.mustCheck (fv : FeatureVal) (host : Cat) : Bool

A feature must be checked before LF iff it is –Interpretable on its host.

Equations

• Minimalist.mustCheck fv host = (Minimalist.isInterpretableOn fv host == Minimalist.Interpretability.uninterpretable)

theorem Minimalist.phi_on_N_interpretable (pf : PhiFeature) : isInterpretableOn (FeatureVal.phi pf) Cat.N = Interpretability.interpretable

Phi on N is interpretable; phi on T is not.

theorem Minimalist.phi_on_T_uninterpretable (pf : PhiFeature) : isInterpretableOn (FeatureVal.phi pf) Cat.T = Interpretability.uninterpretable

inductive Minimalist.FeatureStatus : Type

The lifecycle state of a formal feature in the derivation.

Features begin .active (or .inactive if dormant) and, if –Interpretable, must reach .erased for the derivation to converge at LF.

• inactive : FeatureStatus

  Inactive: present but dormant. Not yet accessible to checking operations — must be activated first. Used for selectional features that await licensing by a specific syntactic trigger (@cite{preminger-2014} "derivational time bombs"; @cite{hewett-2026} Def 23: selectional features activated stepwise by categorizing head and template).

• active : FeatureStatus

  Active: present and accessible to all computation.

• checked : FeatureStatus

  Checked (= deleted in @cite{chomsky-1995}'s terminology): has entered a checking relation. Invisible at LF but still accessible to narrow-syntactic computation.

• erased : FeatureStatus

  Erased: completely removed. Inaccessible to all further computation, including narrow syntax.

def Minimalist.instReprFeatureStatus.repr : FeatureStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprFeatureStatus : Repr FeatureStatus

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqFeatureStatus : DecidableEq FeatureStatus

Equations

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

structure Minimalist.TrackedFeature : Type

A feature in the derivation, tracking its lifecycle state.

• val : FeatureVal
• host : Cat
• interp : Interpretability
• status : FeatureStatus

def Minimalist.instReprTrackedFeature.repr : TrackedFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprTrackedFeature : Repr TrackedFeature

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqTrackedFeature : DecidableEq TrackedFeature

Equations

• Minimalist.instDecidableEqTrackedFeature = Minimalist.instDecidableEqTrackedFeature.decEq

def Minimalist.instDecidableEqTrackedFeature.decEq (x✝ x✝¹ : TrackedFeature) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.TrackedFeature.fromHosted (fv : FeatureVal) (host : Cat) : TrackedFeature

Create a tracked feature with interpretability determined by host.

Equations

• Minimalist.TrackedFeature.fromHosted fv host = { val := fv, host := host, interp := Minimalist.isInterpretableOn fv host }

def Minimalist.TrackedFeature.check (tf : TrackedFeature) : Option TrackedFeature

Check a feature: transition from active to checked. Only –Interpretable features are checked (they enter a checking relation with a matching +Interpretable feature). Returns none if the feature is not active or is +Interpretable.

Equations

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

def Minimalist.TrackedFeature.erase (tf : TrackedFeature) : Option TrackedFeature

Erase a feature: transition from checked to erased. Erasure is possible only after checking. Once erased, the feature is computationally inaccessible.

The book allows a parametric option: a –Interpretable feature may escape erasure after checking, permitting multiple-Spec constructions (MSCs). allowEscapeErasure controls this.

Equations

• tf.erase = match tf.status with | Minimalist.FeatureStatus.checked => some { val := tf.val, host := tf.host, interp := tf.interp, status := Minimalist.FeatureStatus.erased } | x => none

def Minimalist.TrackedFeature.activate (tf : TrackedFeature) : Option TrackedFeature

Activate a dormant feature: transition from inactive to active. This models @cite{preminger-2014}'s "derivational time bombs" and @cite{hewett-2026} Def 23: a selectional feature begins dormant and is activated by a specific syntactic trigger (a categorizing head, a template-defining head, etc.). Returns none if the feature is not inactive.

Equations

• tf.activate = match tf.status with | Minimalist.FeatureStatus.inactive => some { val := tf.val, host := tf.host, interp := tf.interp } | x => none

def Minimalist.TrackedFeature.visibleAtLF (tf : TrackedFeature) : Bool

Is this feature visible at LF? +Interpretable active features are visible (they contribute meaning). Everything else — inactive, checked, erased, or –Interpretable — is not.

Equations

• tf.visibleAtLF = (tf.interp == Minimalist.Interpretability.interpretable && tf.status == Minimalist.FeatureStatus.active)

def Minimalist.TrackedFeature.accessible (tf : TrackedFeature) : Bool

Is this feature accessible to narrow-syntactic computation? Inactive, active, and checked features are accessible; erased features are not. Inactive features are accessible to Activate operations even though they cannot yet enter checking relations.

Equations

• tf.accessible = (tf.status != Minimalist.FeatureStatus.erased)

structure Minimalist.StrongFeature : Type

A strong feature must be checked before Spell-Out (overt syntax). If it survives to Spell-Out unchecked, the derivation is canceled.

Strong features are always –Interpretable. They force overt operations: the derivation cannot "wait" (Procrastinate) because the strong feature would crash at Spell-Out.

• feature : TrackedFeature
• isUninterpretable : self.feature.interp = Interpretability.uninterpretable

def Minimalist.instReprStrongFeature.repr : StrongFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprStrongFeature : Repr StrongFeature

Equations

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

def Minimalist.StrongFeature.crashesAtSpellOut (sf : StrongFeature) : Bool

Does a strong feature survive unchecked at Spell-Out? If so, the derivation is canceled. Both active (unchecked) and inactive (never activated) strong features crash.

Equations

• sf.crashesAtSpellOut = (sf.feature.status == Minimalist.FeatureStatus.active || sf.feature.status == Minimalist.FeatureStatus.inactive)

def Minimalist.convergesAtLF (features : List TrackedFeature) : Bool

A set of tracked features converges at LF iff no –Interpretable feature remains active or inactive (i.e., unchecked).

This is the Full Interpretation (FI) condition at LF: every feature present at LF must be interpretable. –Interpretable features that have been checked (deleted) are invisible at LF and satisfy FI; those that have been erased are gone entirely. Both active and inactive –Interpretable features cause a crash — inactive features should have been activated and checked before reaching LF.

Equations

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

def Minimalist.convergesAtSpellOut (features : List TrackedFeature) (isStrong : TrackedFeature → Bool) : Bool

A set of tracked features converges at Spell-Out iff no strong feature remains active or inactive.

This is weaker than LF convergence: non-strong –Interpretable features can still be active at Spell-Out (they will be checked covertly, after Spell-Out). But strong features — whether active or inactive — must be resolved before Spell-Out.

isStrong marks which features are strong (must be checked overtly).

Equations

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

theorem Minimalist.interpretable_cannot_check (tf : TrackedFeature) (h : tf.interp = Interpretability.interpretable) : tf.check = none

+Interpretable features cannot be checked: check returns none.

theorem Minimalist.check_requires_active_uninterpretable (tf result : TrackedFeature) (hc : tf.check = some result) : tf.interp = Interpretability.uninterpretable ∧ tf.status = FeatureStatus.active

Only active –Interpretable features can be checked.

theorem Minimalist.erase_requires_checked (tf result : TrackedFeature) (he : tf.erase = some result) : tf.status = FeatureStatus.checked

Only checked features can be erased.

theorem Minimalist.check_deterministic (tf r1 r2 : TrackedFeature) (h1 : tf.check = some r1) (h2 : tf.check = some r2) : r1 = r2

The lifecycle is deterministic: check always produces the same result.

theorem Minimalist.erased_cannot_check (tf : TrackedFeature) (h : tf.status = FeatureStatus.erased) : tf.check = none

Erased features cannot be checked.

theorem Minimalist.checked_cannot_recheck (tf : TrackedFeature) (h : tf.status = FeatureStatus.checked) : tf.check = none

Checked features cannot be checked again.

theorem Minimalist.active_cannot_erase (tf : TrackedFeature) (h : tf.status = FeatureStatus.active) : tf.erase = none

Active features cannot be erased (must check first).

theorem Minimalist.erased_cannot_erase (tf : TrackedFeature) (h : tf.status = FeatureStatus.erased) : tf.erase = none

Erased features cannot be erased again.

theorem Minimalist.activate_requires_inactive (tf result : TrackedFeature) (ha : tf.activate = some result) : tf.status = FeatureStatus.inactive

Only inactive features can be activated.

theorem Minimalist.active_cannot_activate (tf : TrackedFeature) (h : tf.status = FeatureStatus.active) : tf.activate = none

Active features cannot be activated (already active).

theorem Minimalist.inactive_cannot_check (tf : TrackedFeature) (h : tf.status = FeatureStatus.inactive) : tf.check = none

Inactive features cannot be checked (must activate first).

theorem Minimalist.inactive_cannot_erase (tf : TrackedFeature) (h : tf.status = FeatureStatus.inactive) : tf.erase = none

Inactive features cannot be erased.

theorem Minimalist.full_lifecycle (fv : FeatureVal) (host : Cat) (h : isInterpretableOn fv host = Interpretability.uninterpretable) : have tf := TrackedFeature.fromHosted fv host; ∃ (tf1 : TrackedFeature) (tf2 : TrackedFeature), tf.check = some tf1 ∧ tf1.erase = some tf2 ∧ tf2.status = FeatureStatus.erased

The full lifecycle: an active –Interpretable feature can be checked and then erased, reaching the terminal state.

theorem Minimalist.extended_lifecycle (fv : FeatureVal) (host : Cat) : have tf := { val := fv, host := host, interp := Interpretability.uninterpretable, status := FeatureStatus.inactive }; ∃ (tf1 : TrackedFeature) (tf2 : TrackedFeature) (tf3 : TrackedFeature), tf.activate = some tf1 ∧ tf1.check = some tf2 ∧ tf2.erase = some tf3 ∧ tf3.status = FeatureStatus.erased

The extended lifecycle: an inactive –Interpretable feature can be activated, checked, and then erased. This is the full chain for @cite{hewett-2026} Def 23 selectional features: inactive → active → checked → erased.

theorem Minimalist.checked_invisible_at_LF (tf : TrackedFeature) (h : tf.status = FeatureStatus.checked) : tf.visibleAtLF = false

Checked features are invisible at LF.

theorem Minimalist.inactive_invisible_at_LF (tf : TrackedFeature) (h : tf.status = FeatureStatus.inactive) : tf.visibleAtLF = false

Inactive features are invisible at LF.

theorem Minimalist.erased_inaccessible (tf : TrackedFeature) (h : tf.status = FeatureStatus.erased) : tf.accessible = false

Erased features are inaccessible to computation.

theorem Minimalist.inactive_accessible (tf : TrackedFeature) (h : tf.status = FeatureStatus.inactive) : tf.accessible = true

Inactive features ARE accessible to computation (they can be targeted by Activate). Only erased features are inaccessible.

theorem Minimalist.interpretable_active_visible (tf : TrackedFeature) (hi : tf.interp = Interpretability.interpretable) (hs : tf.status = FeatureStatus.active) : tf.visibleAtLF = true

+Interpretable active features are visible at LF (they contribute meaning).

theorem Minimalist.interpretable_converges (fv : FeatureVal) (host : Cat) (h : isInterpretableOn fv host = Interpretability.interpretable) : convergesAtLF [TrackedFeature.fromHosted fv host] = true

+Interpretable features never need checking — they converge as-is.

theorem Minimalist.unchecked_uninterpretable_crashes (fv : FeatureVal) (host : Cat) (h : isInterpretableOn fv host = Interpretability.uninterpretable) : convergesAtLF [TrackedFeature.fromHosted fv host] = false

An unchecked –Interpretable feature crashes at LF.

theorem Minimalist.checked_uninterpretable_converges : convergesAtLF [{ val := FeatureVal.case UD.Case.nom, host := Cat.N, interp := Interpretability.uninterpretable, status := FeatureStatus.checked }] = true

A checked –Interpretable feature does NOT crash at LF.

Ordered Activation Tuples

@cite{hewett-2026} Def 23 (adapted from @cite{merchant-2019}): a feature can be indexed by an ordered tuple of category keys (c₁, …, cₙ). Each c-commanding head bearing key k strips c₁ from the tuple if k = c₁ (matching activation). When the tuple is exhausted the feature transitions from .inactive to .active.

ActivationIndex α is parametric over the key type α — for Semitic l-selection α combines Cat and SemiticTemplate, but the mechanism generalizes to any domain where features require ordered multi-head activation (e.g., applicatives, serial verbs).

structure Minimalist.ActivationIndex (α : Type) [BEq α] : Type

An ordered tuple of activation keys. Stripping proceeds left-to-right: only the leftmost key can be matched at any derivational step.

• remaining : List α

  Keys remaining to be stripped. Empty = fully activated.

@[implicit_reducible]

instance Minimalist.instReprActivationIndex {α✝ : Type} {inst✝ : BEq α✝} [Repr α✝] : Repr (ActivationIndex α✝)

Equations

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

def Minimalist.instReprActivationIndex.repr {α✝ : Type} {inst✝ : BEq α✝} [Repr α✝] : ActivationIndex α✝ → ℕ → Std.Format

Equations

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

def Minimalist.ActivationIndex.activate {α : Type} [BEq α] (idx : ActivationIndex α) (key : α) : ActivationIndex α

Attempt to strip the leftmost key. Succeeds only if key matches the head of the tuple (matching activation). Non-matching keys and already-empty tuples are no-ops.

Equations

• idx.activate key = match idx.remaining with | k :: rest => if (k == key) = true then { remaining := rest } else idx | [] => idx

def Minimalist.ActivationIndex.isFullyActive {α : Type} [BEq α] (idx : ActivationIndex α) : Bool

Is the tuple fully stripped?

Equations

• idx.isFullyActive = idx.remaining.isEmpty

def Minimalist.ActivationIndex.toStatus {α : Type} [BEq α] (idx : ActivationIndex α) : FeatureStatus

Map activation state to the FeatureStatus lifecycle: non-empty tuples are .inactive, empty tuples are .active.

Equations

• idx.toStatus = if idx.isFullyActive = true then Minimalist.FeatureStatus.active else Minimalist.FeatureStatus.inactive

theorem Minimalist.activate_matching_strips {α : Type} [BEq α] [LawfulBEq α] (k : α) (rest : List α) : { remaining := k :: rest }.activate k = { remaining := rest }

Matching key strips the head.

theorem Minimalist.activate_nonmatching_noop {α : Type} [BEq α] [LawfulBEq α] (k₁ k₂ : α) (rest : List α) (h : k₁ ≠ k₂) : { remaining := k₁ :: rest }.activate k₂ = { remaining := k₁ :: rest }

Non-matching key is a no-op.

theorem Minimalist.empty_is_active {α : Type} [BEq α] : { remaining := [] }.isFullyActive = true

Empty tuple is fully active.

theorem Minimalist.nonempty_is_inactive {α : Type} [BEq α] (k : α) (rest : List α) : { remaining := k :: rest }.isFullyActive = false

Non-empty tuple is not fully active.

theorem Minimalist.empty_toStatus_active {α : Type} [BEq α] : { remaining := [] }.toStatus = FeatureStatus.active

Empty tuple maps to .active status.

theorem Minimalist.nonempty_toStatus_inactive {α : Type} [BEq α] (k : α) (rest : List α) : { remaining := k :: rest }.toStatus = FeatureStatus.inactive

Non-empty tuple maps to .inactive status.

theorem Minimalist.activate_empty_noop {α : Type} [BEq α] (key : α) : { remaining := [] }.activate key = { remaining := [] }

Activation on an already-empty tuple is a no-op.

theorem Minimalist.full_activation_chain {α : Type} [BEq α] [LawfulBEq α] (k₁ k₂ : α) : have idx := { remaining := [k₁, k₂] }; ((idx.activate k₁).activate k₂).toStatus = FeatureStatus.active

Full activation chain: stripping each key in order yields .active.

Connecting Agree (valuation) to Checking (lifecycle)

@cite{chomsky-2000}'s Agree subsumes the 1995 checking lifecycle: Agree values an unvalued feature, which is equivalent to checking + deletion in one step. The two formalizations operate at different levels:

• Agree.applyAgree: values probe features from goal features (feature bundles)
• TrackedFeature.check: lifecycle transition from active to checked

The bridge states: when Agree successfully values an uninterpretable feature, that feature's lifecycle also advances. If ALL uninterpretable features in a bundle are valued by Agree, the derivation converges at LF.

theorem Minimalist.agree_enables_check (fv : FeatureVal) (host : Cat) (h_uninterp : isInterpretableOn fv host = Interpretability.uninterpretable) : have tf := TrackedFeature.fromHosted fv host; tf.check.isSome = true

A feature that has been valued by Agree can be checked in the lifecycle. This connects the two formalizations: Agree valuation implies lifecycle transition is available.

theorem Minimalist.agree_then_check_converges (fv : FeatureVal) (host : Cat) (h_uninterp : isInterpretableOn fv host = Interpretability.uninterpretable) : have tf := TrackedFeature.fromHosted fv host; match tf.check with | some checked_tf => convergesAtLF [checked_tf] = true | none => False

When Agree values a feature bundle and all uninterpretable features are checked, the derivation converges at LF.

theorem Minimalist.mustCheck_resolved_by_check (fv : FeatureVal) (host : Cat) (h : mustCheck fv host = true) : have tf := TrackedFeature.fromHosted fv host; ∃ (tf' : TrackedFeature), tf.check = some tf' ∧ convergesAtLF [tf'] = true

Agree makes mustCheck features convergent: if a feature must be checked (is –Interpretable on its host), checking it resolves the convergence requirement.

theorem Minimalist.strong_feature_checked_converges (fv : FeatureVal) (host : Cat) (h_uninterp : isInterpretableOn fv host = Interpretability.uninterpretable) : have tf := TrackedFeature.fromHosted fv host; match tf.check with | some checked_tf => (convergesAtSpellOut [checked_tf] fun (x : TrackedFeature) => true) = true | none => False

A derivation converges at Spell-Out iff all strong features have been checked. This connects Checking.convergesAtSpellOut to the StrongFeature type.

theorem Minimalist.unchecked_strong_crashes (fv : FeatureVal) (host : Cat) (h_uninterp : isInterpretableOn fv host = Interpretability.uninterpretable) : (convergesAtSpellOut [TrackedFeature.fromHosted fv host] fun (x : TrackedFeature) => true) = false

An unchecked strong feature crashes at Spell-Out.