Feature Infrastructure for Minimalist Agree

@cite{adger-2003} @cite{chomsky-1995} @cite{chomsky-2000} @cite{chomsky-2001} @cite{alok-2020} @cite{alok-bhalla-2026} @cite{lobeck-1995} @cite{panagiotidis-2015} @cite{pollock-1989}

Phi-features, case values, and feature bundles — the shared infrastructure underlying all Agree-based operations. Extracted from Agree.lean to separate the feature types (what can be checked) from the Agree operation (how checking works) and the failure model (what happens when checking fails; see ObligatoryOperations.lean).

±Interpretable Features (@cite{chomsky-1995} Ch 4 §4.5)

The ±Interpretable distinction is orthogonal to valued/unvalued:

• +Interpretable: contributes to meaning, survives to LF. Categorial features ([N], [V], [D], [C]) and φ-features of nouns.
• –Interpretable: must be checked and deleted before LF. Case features, φ-features of T/v, strong [nominal-] features.

Interpretability is determined by the combination of feature type and host category: person on N is +Interpretable, person on T is –Interpretable. isInterpretableOn encodes this mapping.

Design Decision: PersonLevel replaces Nat

PhiFeature.person uses Features.Prominence.PersonLevel (.first |.second |.third) rather than a raw Nat. This eliminates the possibility of meaningless person values (e.g., person 47) and grounds the feature inventory in the same canonical type used across the library:

• Features.Prominence.PersonLevel — framework-agnostic person hierarchy
• PersonGeometry.DecomposedPerson — @cite{preminger-2014}'s [±participant, ±author] decomposition, now mapping from PersonLevel
• DifferentialIndexing.IndexingPersonLevel — @cite{just-2024}'s SAP/3rd binary split, bridged to PersonLevel

For unvalued (probe) features, the value is irrelevant — FeatureVal.sameType matches any .person _ against any .person _ and any .number _ against any .number _, ignoring specific values. Use .person .third and .number .sg as conventional placeholders for probes.

inductive Minimalist.PhiFeature : Type

Phi-features (agreement features).

• person : Features.Prominence.PersonLevel → PhiFeature
• number : Number → PhiFeature
• gender : ℕ → PhiFeature

def Minimalist.instReprPhiFeature.repr : PhiFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprPhiFeature : Repr PhiFeature

Equations

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

def Minimalist.instDecidableEqPhiFeature.decEq (x✝ x✝¹ : PhiFeature) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.person a) (Minimalist.PhiFeature.person b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.person a) (Minimalist.PhiFeature.number a_1) = isFalse ⋯
• Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.person a) (Minimalist.PhiFeature.gender a_1) = isFalse ⋯
• Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.number a) (Minimalist.PhiFeature.person a_1) = isFalse ⋯
• Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.number a) (Minimalist.PhiFeature.number b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.number a) (Minimalist.PhiFeature.gender a_1) = isFalse ⋯
• Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.gender a) (Minimalist.PhiFeature.person a_1) = isFalse ⋯
• Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.gender a) (Minimalist.PhiFeature.number a_1) = isFalse ⋯
• Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.gender a) (Minimalist.PhiFeature.gender b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instDecidableEqPhiFeature : DecidableEq PhiFeature

Equations

• Minimalist.instDecidableEqPhiFeature = Minimalist.instDecidableEqPhiFeature.decEq

inductive Minimalist.HonLevel : Type

Honorific level: social ordering between speaker and referent. Relational, not absolute. ⟦iHON⟧ = λx. S_i ≺ x, where ≺ encodes social hierarchy.

• nh : HonLevel
• h : HonLevel
• hh : HonLevel

def Minimalist.instReprHonLevel.repr : HonLevel → ℕ → Std.Format

Equations

• Minimalist.instReprHonLevel.repr Minimalist.HonLevel.nh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.HonLevel.nh")).group prec✝
• Minimalist.instReprHonLevel.repr Minimalist.HonLevel.h prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.HonLevel.h")).group prec✝
• Minimalist.instReprHonLevel.repr Minimalist.HonLevel.hh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.HonLevel.hh")).group prec✝

@[implicit_reducible]

instance Minimalist.instReprHonLevel : Repr HonLevel

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqHonLevel : DecidableEq HonLevel

Equations

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

inductive Minimalist.FeatureVal : Type

Feature values that can be checked via Agree

• phi : PhiFeature → FeatureVal
• case : Core.Case → FeatureVal
• wh : Bool → FeatureVal
• q : Bool → FeatureVal
• epp : Bool → FeatureVal
• tense : Bool → FeatureVal
• hon : HonLevel → FeatureVal
• finite : Bool → FeatureVal
• factive : Bool → FeatureVal
• neg : Bool → FeatureVal
• rel : Bool → FeatureVal
• oblique : Bool → FeatureVal
• ellipsis : Bool → FeatureVal
• catN : Bool → FeatureVal
• catV : Bool → FeatureVal
• foc : Bool → FeatureVal
• pol : Bool → FeatureVal
• pov : Bool → FeatureVal
• atomic : Bool → FeatureVal
• minimal : Bool → FeatureVal
• participant : Bool → FeatureVal
• author : Bool → FeatureVal

def Minimalist.instReprFeatureVal.repr : FeatureVal → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprFeatureVal : Repr FeatureVal

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqFeatureVal : DecidableEq FeatureVal

Equations

• Minimalist.instDecidableEqFeatureVal = Minimalist.instDecidableEqFeatureVal.decEq

def Minimalist.instDecidableEqFeatureVal.decEq (x✝ x✝¹ : FeatureVal) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.FeatureVal.sameType : FeatureVal → FeatureVal → Bool

Do two feature values have the same type, ignoring specific values?

This is the correct matching predicate for Agree: a probe with [uPerson] should match any goal with [Person:x], regardless of the specific person value x. In contrast, DecidableEq (==) compares both type and value, which is wrong for Agree matching where the probe carries a placeholder value.

Equations

• (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person a)).sameType (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person a_1)) = true
• (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number a)).sameType (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number a_1)) = true
• (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.gender a)).sameType (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.gender a_1)) = true
• (Minimalist.FeatureVal.phi p1).sameType (Minimalist.FeatureVal.phi p2) = false
• (Minimalist.FeatureVal.case a).sameType (Minimalist.FeatureVal.case a_1) = true
• (Minimalist.FeatureVal.wh a).sameType (Minimalist.FeatureVal.wh a_1) = true
• (Minimalist.FeatureVal.q a).sameType (Minimalist.FeatureVal.q a_1) = true
• (Minimalist.FeatureVal.epp a).sameType (Minimalist.FeatureVal.epp a_1) = true
• (Minimalist.FeatureVal.tense a).sameType (Minimalist.FeatureVal.tense a_1) = true
• (Minimalist.FeatureVal.hon a).sameType (Minimalist.FeatureVal.hon a_1) = true
• (Minimalist.FeatureVal.finite a).sameType (Minimalist.FeatureVal.finite a_1) = true
• (Minimalist.FeatureVal.factive a).sameType (Minimalist.FeatureVal.factive a_1) = true
• (Minimalist.FeatureVal.neg a).sameType (Minimalist.FeatureVal.neg a_1) = true
• (Minimalist.FeatureVal.rel a).sameType (Minimalist.FeatureVal.rel a_1) = true
• (Minimalist.FeatureVal.oblique a).sameType (Minimalist.FeatureVal.oblique a_1) = true
• (Minimalist.FeatureVal.ellipsis a).sameType (Minimalist.FeatureVal.ellipsis a_1) = true
• (Minimalist.FeatureVal.catN a).sameType (Minimalist.FeatureVal.catN a_1) = true
• (Minimalist.FeatureVal.catV a).sameType (Minimalist.FeatureVal.catV a_1) = true
• (Minimalist.FeatureVal.foc a).sameType (Minimalist.FeatureVal.foc a_1) = true
• (Minimalist.FeatureVal.pol a).sameType (Minimalist.FeatureVal.pol a_1) = true
• (Minimalist.FeatureVal.pov a).sameType (Minimalist.FeatureVal.pov a_1) = true
• (Minimalist.FeatureVal.atomic a).sameType (Minimalist.FeatureVal.atomic a_1) = true
• (Minimalist.FeatureVal.minimal a).sameType (Minimalist.FeatureVal.minimal a_1) = true
• (Minimalist.FeatureVal.participant a).sameType (Minimalist.FeatureVal.participant a_1) = true
• (Minimalist.FeatureVal.author a).sameType (Minimalist.FeatureVal.author a_1) = true
• x✝¹.sameType x✝ = false

inductive Minimalist.GramFeature : Type

A grammatical feature: either valued or unvalued.

Valued vs unvalued is about whether the feature carries a specific value (person:3) or just a type placeholder (person:_). This is orthogonal to ±Interpretable (see Interpretability below):

	+Interpretable	–Interpretable
Valued	φ of N (person:3)	—
Unvalued	—	φ of T/v, Case of N

Unvalued features act as probes; valued features can be goals. But interpretability determines whether a feature must be checked and deleted before LF — a separate question from whether it currently carries a value.

• valued : FeatureVal → GramFeature
• unvalued : FeatureVal → GramFeature

@[implicit_reducible]

instance Minimalist.instReprGramFeature : Repr GramFeature

Equations

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

def Minimalist.instReprGramFeature.repr : GramFeature → ℕ → Std.Format

Equations

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

def Minimalist.instDecidableEqGramFeature.decEq (x✝ x✝¹ : GramFeature) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqGramFeature.decEq (Minimalist.GramFeature.valued a) (Minimalist.GramFeature.valued b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalist.instDecidableEqGramFeature.decEq (Minimalist.GramFeature.valued a) (Minimalist.GramFeature.unvalued a_1) = isFalse ⋯
• Minimalist.instDecidableEqGramFeature.decEq (Minimalist.GramFeature.unvalued a) (Minimalist.GramFeature.valued a_1) = isFalse ⋯
• Minimalist.instDecidableEqGramFeature.decEq (Minimalist.GramFeature.unvalued a) (Minimalist.GramFeature.unvalued b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instDecidableEqGramFeature : DecidableEq GramFeature

Equations

• Minimalist.instDecidableEqGramFeature = Minimalist.instDecidableEqGramFeature.decEq

def Minimalist.GramFeature.isValued : GramFeature → Bool

Is this feature valued?

Equations

• (Minimalist.GramFeature.valued a).isValued = true
• (Minimalist.GramFeature.unvalued a).isValued = false

def Minimalist.GramFeature.isUnvalued : GramFeature → Bool

Is this feature unvalued (a potential probe)?

Equations

• (Minimalist.GramFeature.valued a).isUnvalued = false
• (Minimalist.GramFeature.unvalued a).isUnvalued = true

def Minimalist.GramFeature.featureType : GramFeature → FeatureVal

Get the feature type (ignoring valued/unvalued distinction)

Equations

• (Minimalist.GramFeature.valued a).featureType = a
• (Minimalist.GramFeature.unvalued a).featureType = a

def Minimalist.featuresMatch (f1 f2 : GramFeature) : Bool

Do two features match in type? (for Agree) Delegates to FeatureVal.sameType, ignoring specific values.

Equations

• Minimalist.featuresMatch f1 f2 = f1.featureType.sameType f2.featureType

@[reducible, inline]

abbrev Minimalist.FeatureBundle : Type

A feature bundle: list of grammatical features

Equations

• Minimalist.FeatureBundle = List Minimalist.GramFeature

def Minimalist.hasUnvaluedFeature (fb : FeatureBundle) (ftype : FeatureVal) : Bool

Does the bundle have an unvalued feature of a given type? Uses sameType so that e.g. [uPerson:] matches ftype [Person:].

Equations

• Minimalist.hasUnvaluedFeature fb ftype = List.any fb fun (f : Minimalist.GramFeature) => f.isUnvalued && f.featureType.sameType ftype

def Minimalist.hasValuedFeature (fb : FeatureBundle) (ftype : FeatureVal) : Bool

Does the bundle have a valued feature of a given type? Uses sameType so that e.g. [Person:3] matches ftype [Person:_].

Equations

• Minimalist.hasValuedFeature fb ftype = List.any fb fun (f : Minimalist.GramFeature) => f.isValued && f.featureType.sameType ftype

def Minimalist.getValuedFeature (fb : FeatureBundle) (ftype : FeatureVal) : Option GramFeature

Get the valued feature of a given type (if present). Uses sameType for type-level matching.

Equations

• Minimalist.getValuedFeature fb ftype = List.find? (fun (f : Minimalist.GramFeature) => f.isValued && f.featureType.sameType ftype) fb

inductive Minimalist.Interpretability : Type

Whether a feature is interpretable (contributes to LF) or uninterpretable (must be checked and deleted before LF).

This is the central distinction of @cite{chomsky-1995} Ch 4 §4.5. It is orthogonal to valued/unvalued: a feature can be interpretable but unvalued (rare), or uninterpretable but valued (never, in the standard theory). The typical pairings are:

• +Interpretable, valued: φ-features on nouns, categorial features
• –Interpretable, unvalued: φ-features on T/v, Case on nouns

AgreeSOT.lean uses Interpretability directly for tense features. GenderResolution.lean's AnnotatedFeature.interp uses Interpretability directly; CoordinateResolution.lean, AdamsonAnagnostopoulou2025.lean, and Carstens2026.lean all use it via open _root_.Minimalist.

• interpretable : Interpretability
• uninterpretable : Interpretability

def Minimalist.instReprInterpretability.repr : Interpretability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprInterpretability : Repr Interpretability

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqInterpretability : DecidableEq Interpretability

Equations

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

def Minimalist.FeatureVal.inherentInterpretability : FeatureVal → Option Interpretability

Whether a feature is inherently interpretable regardless of host.

Some features are always interpretable (categorial, honorific, factive) or always uninterpretable (Case, EPP, ellipsis). For features whose interpretability depends on host category (phi, wh, tense), see isInterpretableOn in Checking.lean.

Equations

• (Minimalist.FeatureVal.catN a).inherentInterpretability = some Minimalist.Interpretability.interpretable
• (Minimalist.FeatureVal.catV a).inherentInterpretability = some Minimalist.Interpretability.interpretable
• (Minimalist.FeatureVal.case a).inherentInterpretability = some Minimalist.Interpretability.uninterpretable
• (Minimalist.FeatureVal.epp a).inherentInterpretability = some Minimalist.Interpretability.uninterpretable
• (Minimalist.FeatureVal.ellipsis a).inherentInterpretability = some Minimalist.Interpretability.uninterpretable
• (Minimalist.FeatureVal.oblique a).inherentInterpretability = some Minimalist.Interpretability.uninterpretable
• (Minimalist.FeatureVal.hon a).inherentInterpretability = some Minimalist.Interpretability.interpretable
• (Minimalist.FeatureVal.neg a).inherentInterpretability = some Minimalist.Interpretability.interpretable
• (Minimalist.FeatureVal.factive a).inherentInterpretability = some Minimalist.Interpretability.interpretable
• (Minimalist.FeatureVal.pol a).inherentInterpretability = some Minimalist.Interpretability.interpretable
• (Minimalist.FeatureVal.pov a).inherentInterpretability = some Minimalist.Interpretability.interpretable
• x✝.inherentInterpretability = none

theorem Minimalist.case_always_uninterpretable (c : Core.Case) : (FeatureVal.case c).inherentInterpretability = some Interpretability.uninterpretable

Case is always uninterpretable.

theorem Minimalist.catN_always_interpretable (b : Bool) : (FeatureVal.catN b).inherentInterpretability = some Interpretability.interpretable

Categorial [N] is always interpretable.