structure Minimalism.ExtendedLI : Type

Extended LI with grammatical features

This extends Harizanov's LI with Agree-relevant features. The original ⟨CAT, SEL⟩ handles selection; this adds φ, Case, etc.

• base : LexicalItem
• features : FeatureBundle

def Minimalism.instReprExtendedLI.repr : ExtendedLI → ℕ → Std.Format

Equations

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

instance Minimalism.instReprExtendedLI : Repr ExtendedLI

Equations

• Minimalism.instReprExtendedLI = { reprPrec := Minimalism.instReprExtendedLI.repr }

def Minimalism.ExtendedLI.fromSimple (cat : Cat) (sel : SelStack) (feats : FeatureBundle) : ExtendedLI

Create an extended LI from a simple LI

Equations

• Minimalism.ExtendedLI.fromSimple cat sel feats = { base := Minimalism.LexicalItem.simple cat sel, features := feats }

def Minimalism.ExtendedLI.isProbe (li : ExtendedLI) : Bool

Is this LI a probe (has unvalued features)?

Equations

• li.isProbe = List.any li.features Minimalism.GramFeature.isUnvalued

def Minimalism.ExtendedLI.isGoalFor (li : ExtendedLI) (ftype : FeatureVal) : Bool

Is this LI a potential goal for a given feature type?

Equations

• li.isGoalFor ftype = Minimalism.hasValuedFeature li.features ftype

structure Minimalism.AgreeRelation : Type

A probe-goal pair for Agree

• probe : SyntacticObject
• goal : SyntacticObject
• feature : FeatureVal
• probeFeatures : FeatureBundle
• goalFeatures : FeatureBundle

def Minimalism.AgreeRelation.probeCommands (a : AgreeRelation) (root : SyntacticObject) : Prop

The probe c-commands the goal within a given tree

Equations

• a.probeCommands root = Minimalism.cCommandsIn root a.probe a.goal

def Minimalism.AgreeRelation.goalHasFeature (a : AgreeRelation) : Bool

The goal has the relevant valued feature

Equations

• a.goalHasFeature = Minimalism.hasValuedFeature a.goalFeatures a.feature

def Minimalism.AgreeRelation.probeNeedsFeature (a : AgreeRelation) : Bool

The probe has the relevant unvalued feature

Equations

• a.probeNeedsFeature = Minimalism.hasUnvaluedFeature a.probeFeatures a.feature

def Minimalism.validAgree (a : AgreeRelation) (root : SyntacticObject) : Prop

Valid Agree: probe c-commands goal (in tree), probe has unvalued, goal has valued

Equations

• Minimalism.validAgree a root = (a.probeCommands root ∧ a.probeNeedsFeature = true ∧ a.goalHasFeature = true)

def Minimalism.intervenes (root probe x goal : SyntacticObject) (xFeatures : FeatureBundle) (ftype : FeatureVal) : Prop

X intervenes between probe and goal (within tree root) iff:

• probe c-commands X
• X c-commands goal
• X has a matching valued feature

Equations

• Minimalism.intervenes root probe x goal xFeatures ftype = (Minimalism.cCommandsIn root probe x ∧ Minimalism.cCommandsIn root x goal ∧ Minimalism.hasValuedFeature xFeatures ftype = true)

def Minimalism.closestGoal (a : AgreeRelation) (root : SyntacticObject) : Prop

Goal is the closest matching goal for probe

Equations

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

def Minimalism.valueFeature (unvalued valued : GramFeature) : Option GramFeature

Value an unvalued feature by copying from a valued one

Equations

• Minimalism.valueFeature (Minimalism.GramFeature.unvalued a) (Minimalism.GramFeature.valued v) = some (Minimalism.GramFeature.valued v)
• Minimalism.valueFeature unvalued valued = none

def Minimalism.applyAgree (probeFeats goalFeats : FeatureBundle) (ftype : FeatureVal) : Option FeatureBundle

Apply Agree: value the probe's feature from the goal. Uses sameType for matching, so a probe with [uPerson:_] will be valued by a goal with [Person:3rd] — the placeholder value is irrelevant, only the feature type matters.

Equations

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

structure Minimalism.TAgree : Type

T-Agree: T probes for φ-features on subject DP

T has [uφ], subject DP has [φ] → T gets valued φ. The .third value on person probes is a conventional placeholder — sameType ignores the specific PersonLevel value, matching any .person _ against any .person _.

• tHead : SyntacticObject
• subject : SyntacticObject
• tFeatures : FeatureBundle
• subjFeatures : FeatureBundle
• t_has_uphi : hasUnvaluedFeature self.tFeatures (FeatureVal.phi (PhiFeature.person Core.Prominence.PersonLevel.third)) = true ∨ hasUnvaluedFeature self.tFeatures (FeatureVal.phi (PhiFeature.number Number.sg)) = true
• subj_has_phi : hasValuedFeature self.subjFeatures (FeatureVal.phi (PhiFeature.person Core.Prominence.PersonLevel.third)) = true ∨ hasValuedFeature self.subjFeatures (FeatureVal.phi (PhiFeature.number Number.sg)) = true

structure Minimalism.CAgree : Type

C-Agree: C probes for [Q] feature

C has [uQ], interrogative element has [+Q] → question is licensed

• cHead : SyntacticObject
• qElement : SyntacticObject
• cFeatures : FeatureBundle
• qFeatures : FeatureBundle
• c_has_uq : hasUnvaluedFeature self.cFeatures (FeatureVal.q false) = true
• q_has_q : hasValuedFeature self.qFeatures (FeatureVal.q true) = true

def Minimalism.hasEPP (fb : FeatureBundle) : Bool

EPP triggers movement to specifier

When a head has [EPP], Agree is not enough - the goal must MOVE to the specifier position of the agreeing head.

Equations

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

def Minimalism.agreeTriggersMoveement (probeFeats : FeatureBundle) : Bool

Movement is triggered when probe has EPP

Equations

• Minimalism.agreeTriggersMoveement probeFeats = Minimalism.hasEPP probeFeats

def Minimalism.tToCTriggered (cFeats : FeatureBundle) : Bool

T-to-C movement is triggered by [uQ] + [EPP] on C

In matrix questions:

• C has [uQ, EPP]
• T has [+Q] (in some analyses) or movement satisfies EPP
• T moves to C (head movement)

Equations

• Minimalism.tToCTriggered cFeats = (Minimalism.hasUnvaluedFeature cFeats (Minimalism.FeatureVal.q false) && Minimalism.hasEPP cFeats)

def Minimalism.matrixCFeatures : FeatureBundle

Matrix C features: [uQ, EPP]

Equations

• Minimalism.matrixCFeatures = [Minimalism.GramFeature.unvalued (Minimalism.FeatureVal.q false), Minimalism.GramFeature.valued (Minimalism.FeatureVal.epp true)]

def Minimalism.embeddedCFeatures : FeatureBundle

Embedded C features: [uQ] only (satisfied by wh-movement)

Equations

• Minimalism.embeddedCFeatures = [Minimalism.GramFeature.unvalued (Minimalism.FeatureVal.q false)]

theorem Minimalism.matrix_triggers_t_to_c : tToCTriggered matrixCFeatures = true

Matrix C triggers T-to-C

theorem Minimalism.embedded_no_t_to_c : tToCTriggered embeddedCFeatures = false

Embedded C does not trigger T-to-C

def Minimalism.isActive (fb : FeatureBundle) : Bool

Is a feature bundle active? (has at least one unvalued feature)

An element is active iff it has at least one unvalued feature. Typically, DPs are active when they have unvalued Case.

Equations

• Minimalism.isActive fb = List.any fb Minimalism.GramFeature.isUnvalued

def Minimalism.needsCase (fb : FeatureBundle) : Bool

An element needs Case (has unvalued Case feature)

Equations

• Minimalism.needsCase fb = List.any fb fun (f : Minimalism.GramFeature) => f.isUnvalued && match f.featureType with | Minimalism.FeatureVal.case a => true | x => false

def Minimalism.hasCase (fb : FeatureBundle) : Bool

An element has valued Case

Equations

• Minimalism.hasCase fb = List.any fb fun (f : Minimalism.GramFeature) => f.isValued && match f.featureType with | Minimalism.FeatureVal.case a => true | x => false

theorem Minimalism.activity_via_case (fb : FeatureBundle) (h : (List.all fb fun (f : GramFeature) => match f.featureType with | FeatureVal.case a => true | x => false) = true) : isActive fb = true ↔ needsCase fb = true

Activity is typically determined by Case: A DP is active iff it lacks Case

When a feature bundle contains only Case features, the bundle is active (has unvalued features) iff it needs Case (has unvalued Case).

structure Minimalism.ActiveGoal : Type

A goal that satisfies the Activity Condition

• goal : SyntacticObject
• goalFeatures : FeatureBundle
• isActive : Minimalism.isActive self.goalFeatures = true

def Minimalism.instReprActiveGoal.repr : ActiveGoal → ℕ → Std.Format

Equations

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

instance Minimalism.instReprActiveGoal : Repr ActiveGoal

Equations

• Minimalism.instReprActiveGoal = { reprPrec := Minimalism.instReprActiveGoal.repr }

def Minimalism.mkActiveGoal (goal : SyntacticObject) (feats : FeatureBundle) : Option ActiveGoal

Create an ActiveGoal if the features are indeed active

Equations

• Minimalism.mkActiveGoal goal feats = if h : Minimalism.isActive feats = true then some { goal := goal, goalFeatures := feats, isActive := h } else none

def Minimalism.validAgreeWithActivity (a : AgreeRelation) (root : SyntacticObject) : Prop

Valid Agree with Activity Condition

Agree requires:

1. Probe c-commands goal (within tree)
2. Probe has unvalued feature
3. Goal has matching valued feature
4. Goal is ACTIVE (has some unvalued feature)

Equations

• Minimalism.validAgreeWithActivity a root = (Minimalism.validAgree a root ∧ Minimalism.isActive a.goalFeatures = true)

structure Minimalism.MultipleAgree : Type

Multiple Agree: a probe agreeing with a list of goals

• probe : SyntacticObject
• probeFeatures : FeatureBundle
• goals : List (SyntacticObject × FeatureBundle)
• feature : FeatureVal
• goalsHaveFeature : (self.goals.all fun (x : SyntacticObject × FeatureBundle) => match x with | (fst, gf) => hasValuedFeature gf self.feature) = true

def Minimalism.instReprMultipleAgree.repr : MultipleAgree → ℕ → Std.Format

Equations

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

instance Minimalism.instReprMultipleAgree : Repr MultipleAgree

Equations

• Minimalism.instReprMultipleAgree = { reprPrec := Minimalism.instReprMultipleAgree.repr }

def Minimalism.MultipleAgree.isValid (ma : MultipleAgree) (root : SyntacticObject) : Prop

Is Multiple Agree valid? Each goal must be c-commanded by probe (within tree)

Equations

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

def Minimalism.applyMultipleAgree (ma : MultipleAgree) : Option FeatureBundle

Apply Multiple Agree: value probe's feature, mark all goals

Equations

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

structure Minimalism.DefectiveElement : Type

A defective element: has some matching features but incomplete set

• so : SyntacticObject
• features : FeatureBundle
• hasPartialPhi : (List.any self.features fun (f : GramFeature) => match f.featureType with | FeatureVal.phi a => true | x => false) = true
• isDeficient : Bool

def Minimalism.instReprDefectiveElement.repr : DefectiveElement → ℕ → Std.Format

Equations

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

instance Minimalism.instReprDefectiveElement : Repr DefectiveElement

Equations

• Minimalism.instReprDefectiveElement = { reprPrec := Minimalism.instReprDefectiveElement.repr }

def Minimalism.defectivelyIntervenes (root probe x goal : SyntacticObject) (xDef : DefectiveElement) (ftype : FeatureVal) : Prop

Does X defectively intervene between probe and goal (within tree root)?

X defectively intervenes if:

• X is between probe and goal (c-command wise)
• X has matching features
• X is defective (can't be a full goal)

Equations

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

def Minimalism.validAgreeWithPIC (strength : PICStrength) (phases : List Phase) (rel : AgreeRelation) (root : SyntacticObject) : Prop

Valid Agree with Phase Impenetrability Condition.

Agree is blocked if the goal is inside a phase complement (and thus inaccessible under PIC).

Equations

• Minimalism.validAgreeWithPIC strength phases rel root = (Minimalism.validAgree rel root ∧ ¬∃ (ph : Minimalism.Phase), ph ∈ phases ∧ Minimalism.phaseImpenetrable strength ph.head rel.goal)

def Minimalism.fullAgree (strength : PICStrength) (phases : List Phase) (rel : AgreeRelation) (root : SyntacticObject) : Prop

PIC-bounded Agree with Activity Condition.

The full Agree constraint: probe c-commands goal, feature matching holds, goal is active, AND no intervening phase boundary blocks the relation.

Equations

• Minimalism.fullAgree strength phases rel root = (Minimalism.validAgreeWithActivity rel root ∧ ¬∃ (ph : Minimalism.Phase), ph ∈ phases ∧ Minimalism.phaseImpenetrable strength ph.head rel.goal)

def Minimalism.finAgreeFeatures (isFinite : Bool) : FeatureBundle

Fin-Agree: Fin probes for [±finite] on its complement (TP).

Equations

• Minimalism.finAgreeFeatures isFinite = [Minimalism.GramFeature.unvalued (Minimalism.FeatureVal.finite isFinite)]

def Minimalism.forceFinAgreeFeatures (isFactive : Bool) : FeatureBundle

Force-Fin-Agree: Force/C probes for clause-type features on Fin.

Equations

• Minimalism.forceFinAgreeFeatures isFactive = [Minimalism.GramFeature.unvalued (Minimalism.FeatureVal.factive isFactive)]

def Minimalism.negAgreeFeatures : FeatureBundle

Neg-Agree: Neg probes for [±neg], licensing sentential negation.

Equations

• Minimalism.negAgreeFeatures = [Minimalism.GramFeature.unvalued (Minimalism.FeatureVal.neg true)]

def Minimalism.relAgreeFeatures : FeatureBundle

Rel-Agree: Rel probes for [±rel], licensing relative clause formation.

Equations

• Minimalism.relAgreeFeatures = [Minimalism.GramFeature.unvalued (Minimalism.FeatureVal.rel true)]

theorem Minimalism.finite_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.finite true)) (GramFeature.valued (FeatureVal.finite true)) = true

Clause-typing features match correctly.

theorem Minimalism.factive_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.factive true)) (GramFeature.valued (FeatureVal.factive false)) = true

theorem Minimalism.neg_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.neg true)) (GramFeature.valued (FeatureVal.neg true)) = true

theorem Minimalism.rel_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.rel true)) (GramFeature.valued (FeatureVal.rel false)) = true

inductive Minimalism.SatisfactionCond : Type

How a probe's search can be terminated.

Standard Agree assumes a probe is satisfied only by finding a matching
valued feature (simple feature match). @cite{deal-2024} argues for richer
conditions to capture e.g. Mam's Infl probe, which is satisfied by
EITHER matching φ-features OR encountering transitive Voice:

**Mam example** (@cite{scott-2023}, via @cite{deal-2024}):
- Infl carries [uφ] with satisfaction [SAT: φ or Voice_TR]
- Intransitive: probe passes through (no Voice_TR) → finds S → real φ-agreement
- Transitive: probe encounters Voice_TR → satisfied without copying φ → default "∅"

This turns the Mam bridge's prose account into a computable derivation:
```
def mamInflSatisfaction : SatisfactionCond :=

.disjunctive [.featureMatch (.phi (.person.third)),.headEncounter.v] ```

• featureMatch : FeatureVal → SatisfactionCond

  Standard: probe is satisfied by finding a matching valued feature.

• disjunctive : List SatisfactionCond → SatisfactionCond

  Disjunctive: probe is satisfied by ANY of these conditions. Models @cite{deal-2024}'s interaction-based probes.

• headEncounter : Cat → SatisfactionCond

  Head encounter: probe is satisfied by encountering a head of this category, even without feature matching. The probe stops but copies no features — yielding the Elsewhere (default) exponent at PF.

instance Minimalism.instReprSatisfactionCond : Repr SatisfactionCond

Equations

• Minimalism.instReprSatisfactionCond = { reprPrec := Minimalism.instReprSatisfactionCond.repr }

partial def Minimalism.instReprSatisfactionCond.repr : SatisfactionCond → ℕ → Std.Format

def Minimalism.SatisfactionCond.isSatisfied (cond : SatisfactionCond) (fb : FeatureBundle) (ctx : Option Cat) : Bool

Check whether a satisfaction condition is met.

fb is the feature bundle of the element the probe encounters. ctx is the syntactic category of that element (if it's a head). Returns true if the probe should stop searching.

Equations

• (Minimalism.SatisfactionCond.featureMatch a).isSatisfied fb ctx = Minimalism.hasValuedFeature fb a
• (Minimalism.SatisfactionCond.disjunctive a).isSatisfied fb ctx = a.any fun (x : Minimalism.SatisfactionCond) => Minimalism.atomicSatisfied✝ x fb ctx
• (Minimalism.SatisfactionCond.headEncounter a).isSatisfied fb ctx = (ctx == some a)

def Minimalism.SatisfactionCond.copiedFeatures (cond : SatisfactionCond) (fb : FeatureBundle) (ctx : Option Cat) : Bool

Did the probe copy features, or just stop?

When satisfied by feature match, the probe copies features (→ real agreement). When satisfied by head encounter, no features are copied (→ default/Elsewhere). For disjunctive conditions, feature copying occurs iff the first satisfied condition is a feature match.

Equations

• One or more equations did not get rendered due to their size.
• (Minimalism.SatisfactionCond.featureMatch a).copiedFeatures fb ctx = Minimalism.hasValuedFeature fb a
• (Minimalism.SatisfactionCond.headEncounter a).copiedFeatures fb ctx = false

def Minimalism.mamInflSatisfaction : SatisfactionCond

Mam's Infl probe satisfaction condition: satisfied by EITHER matching φ-features OR encountering transitive Voice.

Equations

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

theorem Minimalism.mam_intransitive_satisfied : mamInflSatisfaction.isSatisfied [GramFeature.valued (FeatureVal.phi (PhiFeature.person Core.Prominence.PersonLevel.first)), GramFeature.valued (FeatureVal.phi (PhiFeature.number Number.sg))] none = true

Intransitive environment: the probe encounters a DP with φ-features (no Voice_TR in the way). Feature match is satisfied → real agreement.

theorem Minimalism.mam_transitive_satisfied : mamInflSatisfaction.isSatisfied [] (some Cat.v) = true

Transitive environment: the probe encounters Voice_TR (category.v). Head encounter is satisfied → probe stops without copying features.

theorem Minimalism.mam_transitive_no_copy : mamInflSatisfaction.copiedFeatures [] (some Cat.v) = false

In the transitive case, no features are copied — yielding default.

theorem Minimalism.mam_intransitive_copies : mamInflSatisfaction.copiedFeatures [GramFeature.valued (FeatureVal.phi (PhiFeature.person Core.Prominence.PersonLevel.first)), GramFeature.valued (FeatureVal.phi (PhiFeature.number Number.sg))] none = true

In the intransitive case, features ARE copied — yielding real agreement.