Adjective Agreement Paradigms

Theory-neutral substrate for which φ/κ-features are morphologically realized on adjectives in each syntactic position (predicative vs. attributive). This is the data layer of the Modification Agreement Generalization ([AZ25d]); the theory-specific analysis (the Attr head, the direct-vs-mediated modification route) lives in Studies/AlexeyenkoZeijlstra2025.lean.

Formerly Syntax/Minimalist/Modification.lean's MAGFeatureType/AdjAgreementEntry — relocated here so the per-language Fragments/*/AdjAgreement.lean files import theory-neutral substrate rather than Minimalist theory.

inductive Agreement.AgrFeature : Type

An agreement feature realized on an adjective: a φ-feature (person/number/gender) or a κ-feature (case).

• person : Person → AgrFeature
• number : Number → AgrFeature
• gender : ℕ → AgrFeature
• kappa : Case → AgrFeature

@[implicit_reducible]

instance Agreement.instDecidableEqAgrFeature : DecidableEq AgrFeature

Equations

• Agreement.instDecidableEqAgrFeature = Agreement.instDecidableEqAgrFeature.decEq

def Agreement.instDecidableEqAgrFeature.decEq (x✝ x✝¹ : AgrFeature) : Decidable (x✝ = x✝¹)

Equations

• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.person a) (Agreement.AgrFeature.person b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.person a) (Agreement.AgrFeature.number a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.person a) (Agreement.AgrFeature.gender a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.person a) (Agreement.AgrFeature.kappa a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.number a) (Agreement.AgrFeature.person a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.number a) (Agreement.AgrFeature.number b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.number a) (Agreement.AgrFeature.gender a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.number a) (Agreement.AgrFeature.kappa a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.gender a) (Agreement.AgrFeature.person a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.gender a) (Agreement.AgrFeature.number a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.gender a) (Agreement.AgrFeature.gender b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.gender a) (Agreement.AgrFeature.kappa a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.kappa a) (Agreement.AgrFeature.person a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.kappa a) (Agreement.AgrFeature.number a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.kappa a) (Agreement.AgrFeature.gender a_1) = isFalse ⋯
• Agreement.instDecidableEqAgrFeature.decEq (Agreement.AgrFeature.kappa a) (Agreement.AgrFeature.kappa b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Agreement.instReprAgrFeature.repr : AgrFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Agreement.instReprAgrFeature : Repr AgrFeature

Equations

• Agreement.instReprAgrFeature = { reprPrec := Agreement.instReprAgrFeature.repr }

structure Agreement.AdjAgreementEntry : Type

An adjective agreement entry: the features morphologically realized on predicative vs. attributive adjectives, and all φ/κ-features available in the DP.

• predFeatures : List AgrFeature

  Features realized on predicative adjectives.

• attrFeatures : List AgrFeature

  Features realized on attributive adjectives.

• dpFeatures : List AgrFeature

  All φ/κ-features available in the DP of this language.

@[implicit_reducible]

instance Agreement.instReprAdjAgreementEntry : Repr AdjAgreementEntry

Equations

• Agreement.instReprAdjAgreementEntry = { reprPrec := Agreement.instReprAdjAgreementEntry.repr }

def Agreement.instReprAdjAgreementEntry.repr : AdjAgreementEntry → ℕ → Std.Format

Equations

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

def Agreement.AdjAgreementEntry.sameAgreement (e : AdjAgreementEntry) : Bool

Predicative and attributive adjectives realize the same agreement ([AZ25d] MAG (34a), clause 1).

Equations

• e.sameAgreement = (e.predFeatures.length == e.attrFeatures.length && e.attrFeatures.all fun (x : Agreement.AgrFeature) => e.predFeatures.contains x)

def Agreement.AdjAgreementEntry.phiKappaComplete (e : AdjAgreementEntry) : Bool

Attributive adjectives realize every DP φ/κ-feature ([AZ25d] MAG (34a), clause 2).

Equations

• e.phiKappaComplete = e.dpFeatures.all fun (x : Agreement.AgrFeature) => e.attrFeatures.contains x