Linearization of Complex Modifiers: (Dis)obeying the Head-Final Filter

[AZ25d]

The Head-Final Filter (HFF, Williams 1982) states that prenominal modifiers must not contain post-head material. [AZ25d] show that the HFF both overgenerates (Greek and Russian allow A–XP–N) and undergenerates (Basque and Chácobo display mirror-HFF effects).

They propose the Modifier-Noun Adjacency Generalization (MAG) (34): an XP can intervene between N and its modifying adjective A only if

(a) A has an overt agreement marker that is also present on the predicative form of A and specified for all φ/κ-features in the DP, or (b) A has an overt attributive marker morphophonologically independent of A (adjectival clitic or free word) or forming a morphophonological unit with N.

The MAG is derived from two independent factors:

1. Feature composition (§5.1): φ/κ-completeness of adjectives determines whether an attributivizer is needed for modification
2. Morphophonological status of Attr (§5.2): affixal Attr must be adjacent to its host (ICP, [AN04a]), while clitic/free-word Attr imposes no adjacency

We formalize the MAG as a decision procedure matching the paper's decision trees (44)/(45), encode 24 languages from Table 3, and verify that the MAG correctly predicts all of them while the HFF fails for 11. Bridge theorems connect to WALS F87A and Minimalist feature infrastructure.

[AN04a]'s ICP — used by AZ 2025 §5.2 as the morphophonological factor of the MAG. Was previously in Morphology/ Core/ICP.lean; relocated 0.230.455 (sole consumer is this study file).

The ICP constrains the phonological realization of affixes: an affix must take as its phonological host the head of the phrase it selects. Affixes are always linearly adjacent to their syntactic selectee.

When the attributivizer (Attr) is realized as an affix, the ICP forces it to be adjacent to the adjective head A — dependents of A (PPs, CPs, AdvPs) cannot linearly intervene between A and N. When Attr is a clitic or free word, the ICP does not apply. For null affixes, the Affix Continuity Constraint (Ackema-Neeleman §70) extends the ICP.

The Attr head and modification routes ([AZ25d] §5)

Formerly Syntax/Minimalist/Modification.lean — relocated here as this paper's own analysis (it had a single consumer, this study). The theory-neutral substrate it used (MAGFeatureType/AdjAgreementEntry) is now Syntax/Agreement/AdjAgreement.lean, imported theory-neutrally by the Fragments/*/AdjAgreement files.

inductive AlexeyenkoZeijlstra2025.AttrStatus : Type

Morphophonological status of the attributivizer (Attr head, §5.2). Determines whether Attr imposes linear adjacency with the adjective.

• affix : AttrStatus
• clitic : AttrStatus
• freeWord : AttrStatus
• null : AttrStatus

@[implicit_reducible]

instance AlexeyenkoZeijlstra2025.instDecidableEqAttrStatus : DecidableEq AttrStatus

Equations

• AlexeyenkoZeijlstra2025.instDecidableEqAttrStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AlexeyenkoZeijlstra2025.instReprAttrStatus : Repr AttrStatus

Equations

• AlexeyenkoZeijlstra2025.instReprAttrStatus = { reprPrec := AlexeyenkoZeijlstra2025.instReprAttrStatus.repr }

def AlexeyenkoZeijlstra2025.instReprAttrStatus.repr : AttrStatus → ℕ → Std.Format

Equations

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

inductive AlexeyenkoZeijlstra2025.AdjPosition : Type

Position of attributive adjectives relative to the modified noun.

• prenominal : AdjPosition
• postnominal : AdjPosition
• both : AdjPosition

@[implicit_reducible]

instance AlexeyenkoZeijlstra2025.instDecidableEqAdjPosition : DecidableEq AdjPosition

Equations

• AlexeyenkoZeijlstra2025.instDecidableEqAdjPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AlexeyenkoZeijlstra2025.instReprAdjPosition.repr : AdjPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlexeyenkoZeijlstra2025.instReprAdjPosition : Repr AdjPosition

Equations

• AlexeyenkoZeijlstra2025.instReprAdjPosition = { reprPrec := AlexeyenkoZeijlstra2025.instReprAdjPosition.repr }

structure AlexeyenkoZeijlstra2025.AdjMorphProfile : Type

Morphosyntactic profile of adjectives in a language — the MAG (34) factors: agreement identity (pred = attr), φ/κ-completeness, and the attributivizer's status.

• adjPosition : AdjPosition
• apDirection : HeadDirection
• predAttrSameAgreement : Bool
• agreementPhiKappaComplete : Bool
• attrStatus : AttrStatus

def AlexeyenkoZeijlstra2025.instDecidableEqAdjMorphProfile.decEq (x✝ x✝¹ : AdjMorphProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance AlexeyenkoZeijlstra2025.instDecidableEqAdjMorphProfile : DecidableEq AdjMorphProfile

Equations

• AlexeyenkoZeijlstra2025.instDecidableEqAdjMorphProfile = AlexeyenkoZeijlstra2025.instDecidableEqAdjMorphProfile.decEq

def AlexeyenkoZeijlstra2025.instReprAdjMorphProfile.repr : AdjMorphProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlexeyenkoZeijlstra2025.instReprAdjMorphProfile : Repr AdjMorphProfile

Equations

• AlexeyenkoZeijlstra2025.instReprAdjMorphProfile = { reprPrec := AlexeyenkoZeijlstra2025.instReprAdjMorphProfile.repr }

inductive AlexeyenkoZeijlstra2025.ModificationRoute : Type

The two routes to nominal modification (§5.1): direct (adjective carries [N, uN]) vs attrMediated (an Attr head converts features).

• direct : ModificationRoute
• attrMediated : ModificationRoute

@[implicit_reducible]

instance AlexeyenkoZeijlstra2025.instDecidableEqModificationRoute : DecidableEq ModificationRoute

Equations

• AlexeyenkoZeijlstra2025.instDecidableEqModificationRoute x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AlexeyenkoZeijlstra2025.instReprModificationRoute : Repr ModificationRoute

Equations

• AlexeyenkoZeijlstra2025.instReprModificationRoute = { reprPrec := AlexeyenkoZeijlstra2025.instReprModificationRoute.repr }

def AlexeyenkoZeijlstra2025.instReprModificationRoute.repr : ModificationRoute → ℕ → Std.Format

Equations

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

def AlexeyenkoZeijlstra2025.modificationRoute (prof : AdjMorphProfile) : ModificationRoute

φ/κ-complete languages modify directly; all others require an Attr head.

Equations

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

theorem AlexeyenkoZeijlstra2025.phiKappaComplete_implies_direct (prof : AdjMorphProfile) (hSame : prof.predAttrSameAgreement = true) (hComplete : prof.agreementPhiKappaComplete = true) : modificationRoute prof = ModificationRoute.direct

φ/κ-complete languages use direct modification.

theorem AlexeyenkoZeijlstra2025.predNeAttr_implies_attrMediated (prof : AdjMorphProfile) (h : prof.predAttrSameAgreement = false) : modificationRoute prof = ModificationRoute.attrMediated

Languages with pred ≠ attr require Attr.

theorem AlexeyenkoZeijlstra2025.incomplete_implies_attrMediated (prof : AdjMorphProfile) (h : prof.agreementPhiKappaComplete = false) : modificationRoute prof = ModificationRoute.attrMediated

Languages with incomplete φ/κ require Attr.

def AlexeyenkoZeijlstra2025.morphStatusToAttrStatus : Morphology.MorphStatus → AttrStatus

Map the framework-agnostic MorphStatus (Zwicky-Pullum clitic-affix cline) to the MAG's AttrStatus: affixes impose adjacency, clitics are independent.

Equations

• AlexeyenkoZeijlstra2025.morphStatusToAttrStatus Morphology.MorphStatus.freeWord = AlexeyenkoZeijlstra2025.AttrStatus.freeWord
• AlexeyenkoZeijlstra2025.morphStatusToAttrStatus Morphology.MorphStatus.simpleClitic = AlexeyenkoZeijlstra2025.AttrStatus.clitic
• AlexeyenkoZeijlstra2025.morphStatusToAttrStatus Morphology.MorphStatus.specialClitic = AlexeyenkoZeijlstra2025.AttrStatus.clitic
• AlexeyenkoZeijlstra2025.morphStatusToAttrStatus Morphology.MorphStatus.inflAffix = AlexeyenkoZeijlstra2025.AttrStatus.affix
• AlexeyenkoZeijlstra2025.morphStatusToAttrStatus Morphology.MorphStatus.derivAffix = AlexeyenkoZeijlstra2025.AttrStatus.affix

def Morphology.ICP.imposesAdjacency : AlexeyenkoZeijlstra2025.AttrStatus → Bool

Does the morphophonological status of Attr impose adjacency between Attr and the adjective head? The ICP applies to affixes (overt and null); clitics and free words are not constrained.

Equations

• Morphology.ICP.imposesAdjacency AlexeyenkoZeijlstra2025.AttrStatus.affix = true
• Morphology.ICP.imposesAdjacency AlexeyenkoZeijlstra2025.AttrStatus.null = true
• Morphology.ICP.imposesAdjacency AlexeyenkoZeijlstra2025.AttrStatus.clitic = false
• Morphology.ICP.imposesAdjacency AlexeyenkoZeijlstra2025.AttrStatus.freeWord = false

def Morphology.ICP.icpBlocksIntervention (status : AlexeyenkoZeijlstra2025.AttrStatus) : Bool

When adjacency is imposed, dependents of A cannot intervene between A and the modified N. This is the morphophonological factor of the MAG.

Equations

• Morphology.ICP.icpBlocksIntervention status = Morphology.ICP.imposesAdjacency status

theorem Morphology.ICP.affix_blocks : icpBlocksIntervention AlexeyenkoZeijlstra2025.AttrStatus.affix = true

theorem Morphology.ICP.null_blocks : icpBlocksIntervention AlexeyenkoZeijlstra2025.AttrStatus.null = true

theorem Morphology.ICP.clitic_permits : icpBlocksIntervention AlexeyenkoZeijlstra2025.AttrStatus.clitic = false

theorem Morphology.ICP.freeWord_permits : icpBlocksIntervention AlexeyenkoZeijlstra2025.AttrStatus.freeWord = false

theorem Morphology.ICP.magCondB_is_not_icp (status : AlexeyenkoZeijlstra2025.AttrStatus) : (match status with | AlexeyenkoZeijlstra2025.AttrStatus.clitic => true | AlexeyenkoZeijlstra2025.AttrStatus.freeWord => true | AlexeyenkoZeijlstra2025.AttrStatus.affix => false | AlexeyenkoZeijlstra2025.AttrStatus.null => false) = !icpBlocksIntervention status

MAG condition (b) is exactly the negation of ICP adjacency.

def AlexeyenkoZeijlstra2025.interventionGeometryExists (prof : AdjMorphProfile) : Bool

Does the combination of adjective position and AP-internal direction create a configuration where XP could intervene between A and N? Prenominal A–XP–N requires head-initial AP; postnominal N–XP–A requires head-final AP. This is the prerequisite checked at the top of both decision trees (44) and (45).

Equations

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

def AlexeyenkoZeijlstra2025.magConditionA (prof : AdjMorphProfile) : Bool

MAG condition (a) (34a): adjectives have identical, fully specified φ/κ-agreement in both predicative and attributive use.

Equations

• AlexeyenkoZeijlstra2025.magConditionA prof = (prof.predAttrSameAgreement && prof.agreementPhiKappaComplete)

def AlexeyenkoZeijlstra2025.magConditionB (prof : AdjMorphProfile) : Bool

MAG condition (b) (34b): the attributivizer is morphophonologically independent of the adjective.

Equations

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

def AlexeyenkoZeijlstra2025.magLicensesIntervention (prof : AdjMorphProfile) : Bool

MAG licensing: does the language's morphosyntax permit intervention when geometry supports it? Disjunction of conditions (a) and (b).

Equations

• AlexeyenkoZeijlstra2025.magLicensesIntervention prof = (AlexeyenkoZeijlstra2025.magConditionA prof || AlexeyenkoZeijlstra2025.magConditionB prof)

def AlexeyenkoZeijlstra2025.interventionPredicted (prof : AdjMorphProfile) : Bool

MAG prediction: intervention is observed iff geometry exists AND MAG conditions license it.

Equations

• AlexeyenkoZeijlstra2025.interventionPredicted prof = (AlexeyenkoZeijlstra2025.interventionGeometryExists prof && AlexeyenkoZeijlstra2025.magLicensesIntervention prof)

def AlexeyenkoZeijlstra2025.prenominalTree (prof : AdjMorphProfile) : Bool

Decision tree (44), p. 24: Is A–XP–N possible in prenominal APs?

1. Is AP-internal order head-initial (A–XP)? NO → trivially HFF (Japanese)
2. Are pred & attr φ/κ-complete? YES → intervention OK (Greek)
3. Is Attr a clitic/free word? YES → intervention OK (Tagalog) NO → adjacency forced (German, English)

Equations

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

def AlexeyenkoZeijlstra2025.postnominalTree (prof : AdjMorphProfile) : Bool

Decision tree (45), p. 25: Is N–XP–A possible in postnominal APs? Mirror of (44).

Equations

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

theorem AlexeyenkoZeijlstra2025.decisionTrees_equiv_mag (prof : AdjMorphProfile) : interventionPredicted prof = match prof.adjPosition with | AdjPosition.prenominal => prenominalTree prof | AdjPosition.postnominal => postnominalTree prof | AdjPosition.both => prenominalTree prof || postnominalTree prof

The decision trees are equivalent to interventionPredicted.

def AlexeyenkoZeijlstra2025.greek : AdjMorphProfile

Greek: pred & attr identically inflected for gender, number, case (37). Both are fully φ/κ-specified. MAG(a).

Equations

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

def AlexeyenkoZeijlstra2025.russian : AdjMorphProfile

Russian: long forms fully φ/κ-marked; used in both pred & attr positions. Short forms are pred-only and irrelevant (Table 4). (24), (39). MAG(a).

Equations

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

def AlexeyenkoZeijlstra2025.bulgarian : AdjMorphProfile

Bulgarian: affixal agreement, pred & attr identical for φ/κ. MAG(a).

Equations

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

def AlexeyenkoZeijlstra2025.polish : AdjMorphProfile

Polish: fully inflected pred & attr, like Russian. MAG(a).

Equations

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

def AlexeyenkoZeijlstra2025.lithuanian : AdjMorphProfile

Lithuanian: affixal φ/κ-agreement on pred & attr alike. MAG(a).

Equations

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

def AlexeyenkoZeijlstra2025.latin : AdjMorphProfile

Latin: full φ/κ-marking (gender, number, case) in both pred and attr uses. Both pre- and postnominal. (35). MAG(a).

Equations

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

def AlexeyenkoZeijlstra2025.mandarin : AdjMorphProfile

Mandarin: no φ-agreement; attributivizer 的 (de) cliticizes to AP. (26). MAG(b).

Equations

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

def AlexeyenkoZeijlstra2025.tagalog : AdjMorphProfile

Tagalog: no φ-agreement; attributivizer -ng/na is a clitic. Both pre- and postnominal. (27). MAG(b).

Equations

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

def AlexeyenkoZeijlstra2025.german : AdjMorphProfile

German: pred adjectives bare, attr carry agreement affix (38, 60–63). predAttrSameAgreement = false (pred bare, attr inflected).

Equations

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

def AlexeyenkoZeijlstra2025.english : AdjMorphProfile

English: no overt agreement on adjectives. Null Attr evidenced by distributional parallels with Dutch (§5.2.3). (71).

Equations

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

def AlexeyenkoZeijlstra2025.dutch : AdjMorphProfile

Dutch: attr schwa -e (overt) or null (indef neut sg), both affixal. Pred adjectives bare (64). (65)–(68), Table 6.

Equations

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

def AlexeyenkoZeijlstra2025.icelandic : AdjMorphProfile

Icelandic: strong/weak distinction. Pred = strong only; attr = strong (indef) or weak (def). Attr forms carry definiteness features absent from pred forms → pred ≠ attr. (40)–(42), Table 5.

Equations

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

def AlexeyenkoZeijlstra2025.serboCroatian : AdjMorphProfile

Serbo-Croatian: short (pred only) vs long (pred/attr, definiteness). Attr long forms encode definiteness absent from short pred forms → pred ≠ attr featurally. (21), (43).

Equations

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

def AlexeyenkoZeijlstra2025.hungarian : AdjMorphProfile

Hungarian: bare pred adjectives, no overt attr agreement. (18).

Equations

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

def AlexeyenkoZeijlstra2025.georgian : AdjMorphProfile

Georgian: HFF-obeying, null Attr. (17).

Equations

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

def AlexeyenkoZeijlstra2025.armenian : AdjMorphProfile

Armenian (Modern Eastern): HFF-obeying, null Attr. (20).

Equations

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

def AlexeyenkoZeijlstra2025.italian : AdjMorphProfile

Italian: postnominal primary, head-initial APs → no N–XP–A geometry. φ-agreement (gender, number) but no κ (case) on adjectives → agreementPhiKappaComplete = false. (36), (72).

Equations

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

def AlexeyenkoZeijlstra2025.japanese : AdjMorphProfile

Japanese: strictly head-final APs → no post-head material to create A–XP–N geometry. Trivially HFF-obeying (§2.2).

Equations

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

def AlexeyenkoZeijlstra2025.basque : AdjMorphProfile

Basque: postnominal, head-final. Complex attr APs blocked; must use relative clause with -en. (3), (28).

Equations

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

def AlexeyenkoZeijlstra2025.chacobo : AdjMorphProfile

Chácobo (Panoan): postnominal, head-final. Complex attr APs impossible; relativize with =ka(to) instead. (29).

Equations

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

def AlexeyenkoZeijlstra2025.easternOromo : AdjMorphProfile

Eastern Oromo: postnominal, head-final. Complex attr APs blocked; must use dependent clause marker. (30).

Equations

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

def AlexeyenkoZeijlstra2025.farsi : AdjMorphProfile

Farsi: postnominal, head-final. Ezafe cliticizes to NP (33). MAG(b).

Equations

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

def AlexeyenkoZeijlstra2025.atong : AdjMorphProfile

Atong (Sino-Tibetan): postnominal, head-final. Clitic attributivizer =gaba/=aw. (32). MAG(b).

Equations

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

def AlexeyenkoZeijlstra2025.kalaallisut : AdjMorphProfile

Kalaallisut (West Greenlandic): postnominal, head-final. Full affixal φ/κ-agreement; pred & attr identically specified. (31). MAG(a).

Equations

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

structure AlexeyenkoZeijlstra2025.InterventionDatum : Type

• name : String
• profile : AdjMorphProfile
• observed : Bool

@[implicit_reducible]

instance AlexeyenkoZeijlstra2025.instReprInterventionDatum : Repr InterventionDatum

Equations

• AlexeyenkoZeijlstra2025.instReprInterventionDatum = { reprPrec := AlexeyenkoZeijlstra2025.instReprInterventionDatum.repr }

def AlexeyenkoZeijlstra2025.instReprInterventionDatum.repr : InterventionDatum → ℕ → Std.Format

Equations

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

def AlexeyenkoZeijlstra2025.table3 : List InterventionDatum

Equations

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

def AlexeyenkoZeijlstra2025.magCorrect (d : InterventionDatum) : Bool

Equations

• AlexeyenkoZeijlstra2025.magCorrect d = (AlexeyenkoZeijlstra2025.interventionPredicted d.profile == d.observed)

theorem AlexeyenkoZeijlstra2025.mag_predicts_all : table3.all magCorrect = true

The MAG correctly predicts all 24 languages in Table 3.

theorem AlexeyenkoZeijlstra2025.mag_greek : interventionPredicted greek = true

theorem AlexeyenkoZeijlstra2025.mag_russian : interventionPredicted russian = true

theorem AlexeyenkoZeijlstra2025.mag_bulgarian : interventionPredicted bulgarian = true

theorem AlexeyenkoZeijlstra2025.mag_polish : interventionPredicted polish = true

theorem AlexeyenkoZeijlstra2025.mag_lithuanian : interventionPredicted lithuanian = true

theorem AlexeyenkoZeijlstra2025.mag_latin : interventionPredicted latin = true

theorem AlexeyenkoZeijlstra2025.mag_mandarin : interventionPredicted mandarin = true

theorem AlexeyenkoZeijlstra2025.mag_tagalog : interventionPredicted tagalog = true

theorem AlexeyenkoZeijlstra2025.mag_german : interventionPredicted german = false

theorem AlexeyenkoZeijlstra2025.mag_english : interventionPredicted english = false

theorem AlexeyenkoZeijlstra2025.mag_dutch : interventionPredicted dutch = false

theorem AlexeyenkoZeijlstra2025.mag_icelandic : interventionPredicted icelandic = false

theorem AlexeyenkoZeijlstra2025.mag_serboCroatian : interventionPredicted serboCroatian = false

theorem AlexeyenkoZeijlstra2025.mag_hungarian : interventionPredicted hungarian = false

theorem AlexeyenkoZeijlstra2025.mag_georgian : interventionPredicted georgian = false

theorem AlexeyenkoZeijlstra2025.mag_armenian : interventionPredicted armenian = false

theorem AlexeyenkoZeijlstra2025.mag_italian : interventionPredicted italian = false

theorem AlexeyenkoZeijlstra2025.mag_japanese : interventionPredicted japanese = false

theorem AlexeyenkoZeijlstra2025.mag_basque : interventionPredicted basque = false

theorem AlexeyenkoZeijlstra2025.mag_chacobo : interventionPredicted chacobo = false

theorem AlexeyenkoZeijlstra2025.mag_easternOromo : interventionPredicted easternOromo = false

theorem AlexeyenkoZeijlstra2025.mag_farsi : interventionPredicted farsi = true

theorem AlexeyenkoZeijlstra2025.mag_atong : interventionPredicted atong = true

theorem AlexeyenkoZeijlstra2025.mag_kalaallisut : interventionPredicted kalaallisut = true

theorem AlexeyenkoZeijlstra2025.greek_uses_condA : magConditionA greek = true ∧ magConditionB greek = false

Greek uses MAG(a) alone: φ/κ-complete, no clitic Attr.

theorem AlexeyenkoZeijlstra2025.mandarin_uses_condB : magConditionA mandarin = false ∧ magConditionB mandarin = true

Mandarin uses MAG(b) alone: clitic 的, no φ/κ-agreement.

theorem AlexeyenkoZeijlstra2025.kalaallisut_uses_condA : magConditionA kalaallisut = true ∧ magConditionB kalaallisut = false

Kalaallisut uses MAG(a) alone despite affixal Attr: φ/κ-complete agreement overrides affix adjacency.

theorem AlexeyenkoZeijlstra2025.german_fails_both : magConditionA german = false ∧ magConditionB german = false

German fails BOTH conditions: pred ≠ attr AND Attr is affix.

theorem AlexeyenkoZeijlstra2025.condA_failure_modes : german.predAttrSameAgreement = false ∧ italian.predAttrSameAgreement = true ∧ italian.agreementPhiKappaComplete = false

MAG(a) failure modes are distinct. German fails because pred ≠ attr (clause 1); Italian fails because agreement is not κ-complete (clause 2, no case on adjectives). Both have geometry.

def AlexeyenkoZeijlstra2025.hffWrong (d : InterventionDatum) : Bool

Languages where geometry exists but intervention IS observed — exactly those satisfying MAG(a) or MAG(b). The HFF (+ mirror) incorrectly blocks all of them.

Equations

• AlexeyenkoZeijlstra2025.hffWrong d = (AlexeyenkoZeijlstra2025.interventionGeometryExists d.profile && d.observed)

theorem AlexeyenkoZeijlstra2025.hff_wrong_count : (List.filter hffWrong table3).length = 11

theorem AlexeyenkoZeijlstra2025.mag_correct_count : (List.filter magCorrect table3).length = 24

theorem AlexeyenkoZeijlstra2025.hff_overgenerates_greek : interventionGeometryExists greek = true ∧ interventionPredicted greek = true

HFF overgenerates for Greek: blocks A–XP–N but it is observed.

theorem AlexeyenkoZeijlstra2025.hff_overgenerates_mandarin : interventionGeometryExists mandarin = true ∧ interventionPredicted mandarin = true

HFF overgenerates for Mandarin: clitic 的 licenses A–XP–N.

theorem AlexeyenkoZeijlstra2025.hff_undergenerates_basque : interventionGeometryExists basque = true ∧ interventionPredicted basque = false

HFF undergenerates for Basque: mirror-HFF effects exist but the original HFF cannot state them (postnominal APs).

def AlexeyenkoZeijlstra2025.english_enough : AdjMorphProfile

English "enough" (15)–(16): a genuine HFF exception. Post-adjectival degree modifier that CAN precede the noun: "a tall enough guy." In the MAG analysis, DegP headed by "enough" intervenes between Attr and A; this is possible because null Attr (when DegP heads the extended AP) attaches to DegP, not A (69b).

Equations

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

theorem AlexeyenkoZeijlstra2025.greek_fragment_sameAgreement : Greek.StandardModern.AdjAgreement.entry.sameAgreement = true

Greek: fragment entry confirms pred = attr agreement.

theorem AlexeyenkoZeijlstra2025.greek_fragment_phiKappaComplete : Greek.StandardModern.AdjAgreement.entry.phiKappaComplete = true

Greek: fragment entry confirms φ/κ-completeness.

theorem AlexeyenkoZeijlstra2025.greek_profile_consistent_pred : greek.predAttrSameAgreement = Greek.StandardModern.AdjAgreement.entry.sameAgreement

Greek profile is consistent with fragment: pred = attr.

theorem AlexeyenkoZeijlstra2025.greek_profile_consistent_phikappa : greek.agreementPhiKappaComplete = Greek.StandardModern.AdjAgreement.entry.phiKappaComplete

Greek profile is consistent with fragment: φ/κ-complete.

theorem AlexeyenkoZeijlstra2025.german_fragment_not_sameAgreement : German.AdjAgreement.entry.sameAgreement = false

German: fragment entry confirms pred ≠ attr.

theorem AlexeyenkoZeijlstra2025.german_profile_consistent_pred : german.predAttrSameAgreement = German.AdjAgreement.entry.sameAgreement

German profile is consistent with fragment.

theorem AlexeyenkoZeijlstra2025.russian_fragment_sameAgreement : Russian.AdjAgreement.entry.sameAgreement = true

Russian: fragment confirms pred = attr (long forms identical).

theorem AlexeyenkoZeijlstra2025.russian_profile_consistent_pred : russian.predAttrSameAgreement = Russian.AdjAgreement.entry.sameAgreement

Russian profile is consistent with fragment.

theorem AlexeyenkoZeijlstra2025.italian_fragment_sameAgreement : Italian.AdjAgreement.entry.sameAgreement = true

Italian: fragment confirms pred = attr (both carry φ).

theorem AlexeyenkoZeijlstra2025.italian_fragment_not_phiKappaComplete : Italian.AdjAgreement.entry.phiKappaComplete = false

Italian: fragment confirms NOT φ/κ-complete (no case).

theorem AlexeyenkoZeijlstra2025.italian_profile_consistent_pred : italian.predAttrSameAgreement = Italian.AdjAgreement.entry.sameAgreement

Italian profile is consistent with fragment: pred = attr.

theorem AlexeyenkoZeijlstra2025.italian_profile_consistent_phikappa : italian.agreementPhiKappaComplete = Italian.AdjAgreement.entry.phiKappaComplete

Italian profile is consistent with fragment: NOT φ/κ-complete.

theorem AlexeyenkoZeijlstra2025.greek_direct_mod : modificationRoute greek = ModificationRoute.direct

Greek uses direct modification (no Attr needed).

theorem AlexeyenkoZeijlstra2025.german_attr_mediated : modificationRoute german = ModificationRoute.attrMediated

German uses Attr-mediated modification.

theorem AlexeyenkoZeijlstra2025.mandarin_attr_mediated : modificationRoute mandarin = ModificationRoute.attrMediated

Mandarin uses Attr-mediated modification (clitic 的).

theorem AlexeyenkoZeijlstra2025.italian_attr_mediated : modificationRoute italian = ModificationRoute.attrMediated

Italian uses Attr-mediated modification (null Attr for κ).

theorem AlexeyenkoZeijlstra2025.kalaallisut_direct_mod : modificationRoute kalaallisut = ModificationRoute.direct

Kalaallisut uses direct modification despite affixal Attr: φ/κ-complete agreement means Attr is not needed structurally.

theorem AlexeyenkoZeijlstra2025.german_icp_blocks : Morphology.ICP.icpBlocksIntervention german.attrStatus = true

German: affixal Attr → ICP blocks intervention.

theorem AlexeyenkoZeijlstra2025.english_icp_blocks : Morphology.ICP.icpBlocksIntervention english.attrStatus = true

English: null Attr → ICP blocks intervention.

theorem AlexeyenkoZeijlstra2025.mandarin_icp_permits : Morphology.ICP.icpBlocksIntervention mandarin.attrStatus = false

Mandarin: clitic 的 → ICP does NOT block.

theorem AlexeyenkoZeijlstra2025.farsi_icp_permits : Morphology.ICP.icpBlocksIntervention farsi.attrStatus = false

Farsi: clitic ezafe → ICP does NOT block.

theorem AlexeyenkoZeijlstra2025.mag_factors_orthogonal : modificationRoute greek = ModificationRoute.direct ∧ Morphology.ICP.icpBlocksIntervention greek.attrStatus = true ∧ modificationRoute mandarin = ModificationRoute.attrMediated ∧ Morphology.ICP.icpBlocksIntervention mandarin.attrStatus = false ∧ modificationRoute german = ModificationRoute.attrMediated ∧ Morphology.ICP.icpBlocksIntervention german.attrStatus = true

The two MAG conditions are orthogonal to the two theory-layer mechanisms. Condition (a) = direct modification route; ICP blocking = morphophonological factor of condition (b).

def AlexeyenkoZeijlstra2025.walsOrder (code : String) : Option Data.WALS.F87A.AdjectiveNounOrder

Equations

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

def AlexeyenkoZeijlstra2025.walsToPosition : Data.WALS.F87A.AdjectiveNounOrder → AdjPosition

Equations

• AlexeyenkoZeijlstra2025.walsToPosition Data.WALS.F87A.AdjectiveNounOrder.adjectiveNoun = AlexeyenkoZeijlstra2025.AdjPosition.prenominal
• AlexeyenkoZeijlstra2025.walsToPosition Data.WALS.F87A.AdjectiveNounOrder.nounAdjective = AlexeyenkoZeijlstra2025.AdjPosition.postnominal
• AlexeyenkoZeijlstra2025.walsToPosition Data.WALS.F87A.AdjectiveNounOrder.noDominantOrder = AlexeyenkoZeijlstra2025.AdjPosition.both
• AlexeyenkoZeijlstra2025.walsToPosition Data.WALS.F87A.AdjectiveNounOrder.onlyInternallyHeadedRelativeClauses = AlexeyenkoZeijlstra2025.AdjPosition.both

def AlexeyenkoZeijlstra2025.walsConsistent (code : String) (prof : AdjMorphProfile) : Bool

Equations

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

theorem AlexeyenkoZeijlstra2025.wals_greek : walsConsistent "grk" greek = true

theorem AlexeyenkoZeijlstra2025.wals_russian : walsConsistent "rus" russian = true

theorem AlexeyenkoZeijlstra2025.wals_german : walsConsistent "ger" german = true

theorem AlexeyenkoZeijlstra2025.wals_mandarin : walsConsistent "mnd" mandarin = true

theorem AlexeyenkoZeijlstra2025.wals_basque : walsConsistent "bsq" basque = true

theorem AlexeyenkoZeijlstra2025.wals_hungarian : walsConsistent "hun" hungarian = true

theorem AlexeyenkoZeijlstra2025.wals_italian : walsConsistent "ita" italian = true

theorem AlexeyenkoZeijlstra2025.wals_farsi : walsConsistent "prs" farsi = true

theorem AlexeyenkoZeijlstra2025.wals_tagalog : walsConsistent "tag" tagalog = true