0.230.584 — Core/Agreement/Controller.lean (Corbett 2006 §6.6) + parameterize MorphCategory.agreement on Controller. Anderson Ch 5 §5.2 payoff theorems direct; Bybee/Karlsson source distinctions now round-trip losslessly. ~17 consumer migrations.

Author: hawkrobe

CHANGELOG.md

@@ -4,6 +4,30 @@ The release clock (`v4.29.1`, ...) tracks Lean/mathlib compatibility and is what
 
 ## [Unreleased]
 
+### 0.230.584 — `Core/Agreement/Controller.lean` (Corbett 2006 §6.6) + parameterize `MorphCategory.agreement`
+
+The substrate gap identified at 0.230.578 (subj/obj agreement collapse blocking Anderson Ch 5 §5.2 typology) is now closed.
+
+**Substrate**:
+- `Core/Agreement/Controller.lean` — new file. `inductive Controller | subj | obj | iobj | poss | obl | defaultAgr` anchored on @cite{corbett-2006} §2.1 + §6.6. Cases derived from Hindi/Urdu rule (p. 195) + Upper Sorbian possessive controller (§2.1.4) + Italian *piove* defective controller (§2.1.3). Typological metalanguage; framework-specific projections (LFG SUBJ → Controller.subj etc.) belong in `Theories/Syntax/`.
+- `Core/Morphology/MorphRule.lean` — `MorphCategory.agreement` parameterized as `agreement (controller : Core.Agreement.Controller)`. Added `MorphCategory.IsAgreement : MorphCategory → Bool` for role-blind tests. `peripherality` updated to pattern-match `.agreement _ => 8` (Bybee bucket unchanged).
+
+**Bib**: `corbett-2006` added (Cambridge UP, ISBN 978-0-521-00170-0, DOI 10.1017/cbo9781139164306).
+
+**Anderson Ch 5 §5.2 payoff** in `Anderson2006.lean`: `doyayo_splitDoubled_subj_doubled_obj_lex_only` and `pipil_splitDoubled_subj_doubled_obj_lex_only` directly state Anderson's "subjects doubled, objects on LV only" generalization as `dist.onLex.contains (.agreement .obj) ∧ ¬ dist.onAux.contains (.agreement .obj)`. The 0.230.578 list-length workaround (fragile) is replaced. New `jakaltek_abs_on_aux_erg_on_lex` makes the abs/erg split a category-level distinction.
+
+**Bybee 1985 round-trip** in `Phenomena/Morphology/Studies/Bybee1985.lean`: `personAgr → .agreement .subj`, `personAgrObj → .agreement .obj`, `genderAgr → .agreement .subj` — Bybee's source distinctions now project losslessly. Same restoration in `HahnDegenFutrell2021.lean` (Sesotho subject vs object agreement prefix slots).
+
+**Karlsson 2017 round-trip**: Finnish possessive suffix is now `.agreement .poss` rather than collapsed onto `.agreement`.
+
+**Consumer migrations** (~17 files, mostly mechanical `.agreement → .agreement .subj`): Doyayo, Pipil, Hemba, Gorum, Jakaltek (abs/erg → obj/subj), Japanese Negation, Finnish Negation, English Verbal predicates, Karlsson2017, Bybee1985, HalleMarantz1993, HahnDegenFutrell2021, Baker1985, Anderson2006, Core/Morphology/Exponence.
+
+**Evaluated, NOT promoted** (per inspection):
+- `Fragments/Dargwa/Agreement.lean` `GenderController` (`absolutive | predicate | ergOrDat`) — case-label cases, not grammatical-relation. Genuinely a different concept; Corbett §6.6 confirms case ⊥ grammatical-relation.
+- `Fragments/Icelandic/Verbs.lean` local `AgreementTarget` (`nominativeArg | default3sg`) — case-based, not Corbett-1991 morphosyntactic-position. Name collides with `Core.AgreementTarget` only superficially.
+
+**Build**: 5677/5677 jobs green.
+
 ### 0.230.583 — Refactor `Core/AgreementTarget.lean` (mathlib-shaped) + dir move to `Core/Agreement/`
 
 Mathlib-quality cleanup of the Corbett-1991/2000/Bickel-Nichols-2001 agreement substrate, prepping for the new `Controller` axis (Corbett 2006 §6.6) landing in 0.230.584.

Linglib/Core/Agreement/Controller.lean

@@ -0,0 +1,97 @@
+/-!
+# Agreement Controller — Grammatical Role of the Controlling NP
+@cite{corbett-2006} ch 2 §2.1, ch 6 §6.6
+
+While `Core/Agreement/Target.lean` enumerates WHERE agreement morphology
+surfaces (Corbett 1991 Agreement Hierarchy), this file enumerates WHICH
+GRAMMATICAL ROLE the controlling NP plays. The two axes are orthogonal:
+a language can have subject-controlled verb agreement
+(`Controller.subj` × `AgreementTarget.verb`) and possessor-controlled
+attributive agreement (`Controller.poss` × `AgreementTarget.attributive`).
+
+## Typological labels
+
+The labels here are typological metalanguage — Comrie/Dixon S/A/P
++ grammatical-relation labels used across frameworks. Different theories
+operationalize them differently (LFG SUBJ ≠ Minimalist external argument
+≠ RG 1), but at the level of CROSS-LINGUISTIC DESCRIPTION (which is what
+`Core.Morphology.MorphCategory.agreement` records), the labels are
+reasonably consensual. Framework-specific projections
+(LFG analysis → Controller, Minimalist analysis → Controller) live in
+`Theories/Syntax/`.
+
+## Cases derived from Corbett 2006
+
+@cite{corbett-2006} §2.1 surveys controller TYPES (canonical NPs,
+defective clauses §2.1.2, weather-verb absent controllers §2.1.3,
+possessive adjectives §2.1.4, qualitative adjectives §2.1.5). Within
+canonical NP controllers, the orthogonal GRAMMATICAL-ROLE dimension
+is treated in §6.6 — Hindi/Urdu (p. 195): "if the subject is in
+the nominative, the verb agrees with it; otherwise, if the object
+is in the nominative, the verb agrees with that; otherwise the verb
+shows default agreement". This 3-way subj/obj/default rule is the
+canonical Indo-Aryan pattern; other languages fold in indirect
+objects (recipients), possessors (Upper Sorbian §2.1.4), and rarely
+obliques.
+
+## Anderson 2006 Ch 5 §5.2 motivation
+
+The substrate gap that prompted this enum: Anderson's split/doubled
+AVC typology turns on "subjects on both AUX and LV; objects only on
+LV" — a generalization unstateable when `MorphCategory.agreement`
+collapses subj/obj. Parameterizing `agreement` on `Controller`
+makes the Anderson Ch 5 typology directly Lean-checkable:
+`dist.onLex.contains (.agreement .obj) ∧ ¬ dist.onAux.contains (.agreement .obj)`.
+
+## Bybee 1985 motivation
+
+`Phenomena/Morphology/Studies/Bybee1985.lean:255-257` already encodes
+Bybee's source distinction `personAgr / personAgrObj / genderAgr` but
+collapses all three onto flat `.agreement` in the substrate projection.
+With the parametric form, the projection round-trips:
+`personAgr → .agreement .subj`, `personAgrObj → .agreement .obj`.
+
+## What's NOT here
+
+- **Case** — case-marking (nom/erg/abs/dat/...) is orthogonal to
+  grammatical role. Quirky-case subjects in Icelandic, ergative-case
+  agents in Tsakhur, etc. are case phenomena, not controller-role
+  phenomena. Case lives in `Core/Case/`.
+- **φ-features** (person, number, gender) — these are properties of
+  the CONTROLLER NP that determine agreement values. Not encoded in
+  the controller-role enum itself.
+- **Animacy / topicality / focus** — agreement *conditions* per
+  @cite{corbett-2006} ch 6, not controller-role labels.
+-/
+
+namespace Core.Agreement
+
+/-- Grammatical role of the agreement controller. Cross-linguistically
+    motivated typological labels per @cite{corbett-2006} §6.6. -/
+inductive Controller where
+  /-- Subject (S in intransitive, A in transitive). The unmarked case
+      cross-linguistically. Russian *kniga* controlling verb agreement;
+      English *he* controlling *-s*. -/
+  | subj
+  /-- Direct object (P in transitive). In ergative-absolutive systems,
+      the absolutive argument; cf. Dargwa gender-prefix agreement
+      controlled by absolutive (@cite{corbett-2006} §6.5 ex. 21-26). -/
+  | obj
+  /-- Indirect object / recipient (G in ditransitive). Some Bantu and
+      Romance dialects show recipient agreement on the verb. -/
+  | iobj
+  /-- Possessor. Hungarian possessive suffix; Upper Sorbian
+      *moj-eho muž-ow-a sotr-a* where the possessive adjective
+      controls the attributive (@cite{corbett-2006} §2.1.4). -/
+  | poss
+  /-- Oblique (rare; some Bantu locative agreement). Provided for
+      typological completeness. -/
+  | obl
+  /-- No canonical controller. Weather verbs (Italian *piove*
+      @cite{corbett-2006} §2.1.3), defective clausal/infinitival
+      controllers (§2.1.2): the target shows default agreement
+      (typically 3sg.M in IE languages). -/
+  | defaultAgr
+  deriving DecidableEq, Repr, Inhabited
+
+end Core.Agreement

Linglib/Core/Morphology/Exponence.lean

@@ -189,7 +189,7 @@ def pluralNounRuleFlat {α : Type}
 
 /-- Verb agreement -s: formal change only, semantically vacuous. -/
 def verbAgreement3sg (σ : Type) : MorphRule σ :=
-  { category := .agreement
+  { category := .agreement .subj
   , value := "3sg"
   , formRule := λ lemma_ => lemma_ ++ "s"
   , featureRule := λ f => { f with number := some .Sing, person := some .third }

Linglib/Core/Morphology/MorphRule.lean

@@ -1,4 +1,5 @@
 import Linglib.Core.Word
+import Linglib.Core.Agreement.Controller
 
 /-!
 # Morphological Infrastructure
@@ -204,12 +205,28 @@ inductive MorphCategory where
   | tense         -- past, future, present
   | mood          -- desiderative, subjunctive, imperative
   | negation      -- negation markers
-  | agreement     -- subject/object agreement, politeness
+  /-- Agreement morphology, parameterized by the grammatical role of
+      the controlling NP (`Core.Agreement.Controller`). The role
+      distinction (subj vs obj vs poss vs ...) is what allows Anderson
+      Ch 5 §5.2 split/doubled AVC typology to be Lean-checkable;
+      Bybee 1985's `personAgr / personAgrObj / genderAgr` source
+      distinctions also round-trip cleanly. See
+      `scratch/morphcategory_agreement_split_plan.md` for the design
+      rationale (0.230.578-0.230.584). -/
+  | agreement (controller : Core.Agreement.Controller)
   | nonfinite     -- nonfinite markers, interrogative/relative
   | number        -- number marking on nouns (not verb agreement)
   | degree        -- comparative/superlative on adjectives
   deriving Repr, DecidableEq
 
+/-- Predicate testing whether a `MorphCategory` is an agreement category,
+    independent of which `Controller` role parameterizes it. Used for
+    Bybee-style relevance-hierarchy code that doesn't care which role
+    triggers the agreement, only that agreement IS the category. -/
+def MorphCategory.IsAgreement : MorphCategory → Bool
+  | .agreement _ => true
+  | _ => false
+
 /-- Peripherality: numerical embedding of Bybee's relevance hierarchy
 where **higher = farther from stem = less semantically relevant**.
 
@@ -245,18 +262,18 @@ that reads these ranks):
   morphology often changes syntactic category, outside the scope
   of inflectional categories proper). -/
 def MorphCategory.peripherality : MorphCategory → Nat
-  | .stem       => 0
-  | .derivation => 1
-  | .valence    => 2
-  | .number     => 3
-  | .voice      => 3
-  | .aspect     => 4
-  | .degree     => 5
-  | .tense      => 5
-  | .mood       => 6
-  | .negation   => 7
-  | .agreement  => 8
-  | .nonfinite  => 9
+  | .stem        => 0
+  | .derivation  => 1
+  | .valence     => 2
+  | .number      => 3
+  | .voice       => 3
+  | .aspect      => 4
+  | .degree      => 5
+  | .tense       => 5
+  | .mood        => 6
+  | .negation    => 7
+  | .agreement _ => 8  -- any controller role lands at Bybee rank 8
+  | .nonfinite   => 9
 
 /-- A morpheme ordering respects the relevance hierarchy if peripherality
 is non-decreasing from stem outward (stem-adjacent first). -/

Linglib/Fragments/Doyayo/AuxiliaryVerbs.lean

@@ -53,7 +53,7 @@ def lexHeadedGloss : String := "I AUX pour-PROX 'I'm going to pour'"
     p. 120: "partially encodes person of the subject through the tone");
     LV carries TAM. -/
 def lexHeadedDistribution : InflDistribution :=
-  { onAux := [.agreement], onLex := [.tense] }
+  { onAux := [.agreement .subj], onLex := [.tense] }
 
 /-! ## Split/doubled pattern (Anderson 2006, Ch 5 ex. 128-129, pp. 222-223) -/
 
@@ -75,20 +75,13 @@ def splitDoubledGloss : String :=
   "3PL-POT 3PL-come 3PL-bite-2 'they might come bite you'"
 
 /-- Split/doubled inflection: subject agreement doubled on both
-    elements (subject category appears on AUX *and* LV); object
-    agreement appears only on LV (encoded as a second `.agreement`
-    on `onLex`). The doubled subject is what makes this split/doubled
-    rather than plain split.
-
-    Substrate gap: `MorphCategory.agreement` does not distinguish
-    subject vs object agreement — both `1` (subject) and `-mɔ`
-    (object) collapse to the same `.agreement` constructor. The
-    object-on-LV-only generalization that Anderson Ch 5 §5.2 turns
-    on can therefore not be stated at the substrate level today.
-    See `scratch/morphcategory_agreement_split_plan.md` for the
-    proposed parameterized `agreement (target : ArgRole)` extension. -/
+    elements; object agreement appears only on LV. The role-typed
+    encoding (subj vs obj) makes the Anderson Ch 5 §5.2 "objects on
+    LV only" generalization directly Lean-checkable: see
+    `Phenomena/AuxiliaryVerbs/Studies/Anderson2006.lean`. -/
 def splitDoubledDistribution : InflDistribution :=
-  { onAux := [.agreement], onLex := [.agreement, .agreement] }
+  { onAux := [.agreement .subj]
+  , onLex := [.agreement .subj, .agreement .obj] }
 
 /-! ## Primary pattern alias
 

Linglib/Fragments/English/Predicates/Verbal.lean

@@ -3518,7 +3518,7 @@ def VerbEntry.toStem {σ : Type} (v : VerbEntry) : Core.Morphology.Stem σ :=
   , baseFeatures := { valence := some (complementToValence v.complementType)
                     , vform := some .infinitive }
   , paradigm :=
-    [ { category := .agreement, value := "3sg"
+    [ { category := .agreement .subj, value := "3sg"
       , formRule := λ _ => v.form3sg
       , featureRule := λ f => { f with number := some .Sing
                                      , person := some .third

Linglib/Fragments/Finnish/Negation.lean

@@ -100,7 +100,7 @@ def connegativeRule : MorphRule Bool :=
 /-- The negative auxiliary's agreement rule: semantically vacuous,
     carries person/number agreement that would otherwise be on the main verb. -/
 def negAgreementRule (person : Nat) (number : String) : MorphRule Bool :=
-  { category := .agreement
+  { category := .agreement .subj
   , value := s!"{person}{number}"
   , formRule := fun _ =>
     match person, number with
@@ -123,7 +123,7 @@ def negAgreementRule (person : Nat) (number : String) : MorphRule Bool :=
     Uses the shared `InflDistribution` from `Core.Morphology`:
     `onAux` = negative auxiliary, `onLex` = main verb. -/
 def finnishNegDistribution : InflDistribution :=
-  { onAux := [.negation, .tense, .agreement]
+  { onAux := [.negation, .tense, .agreement .subj]
   , onLex := [.stem, .aspect] }
 
 -- ============================================================================
@@ -150,7 +150,7 @@ theorem connegative_negates : connegativeRule.semEffect true = false := rfl
     respecting Bybee's hierarchy within the neg aux word. -/
 theorem neg_aux_respects_bybee :
     MorphCategory.peripherality .negation <
-    MorphCategory.peripherality .agreement := by decide
+    MorphCategory.peripherality (.agreement .subj) := by decide
 
 
 -- ============================================================================

Linglib/Fragments/Gorum/AuxiliaryVerbs.lean

@@ -38,7 +38,7 @@ def location : String := "India"
 /-- Doubled inflection distribution: both AUX and LV are marked for
     subject agreement, tense, and affectedness (version/voice). -/
 def inflDistribution : InflDistribution :=
-  { onAux := [.agreement, .tense, .voice]
-  , onLex := [.agreement, .tense, .voice] }
+  { onAux := [.agreement .subj, .tense, .voice]
+  , onLex := [.agreement .subj, .tense, .voice] }
 
 end Fragments.Gorum.AuxiliaryVerbs

Linglib/Fragments/Hemba/AuxiliaryVerbs.lean

@@ -40,17 +40,17 @@ def gloss : String := "1PL-PST-AUX 1PL-cut-FV/IND tree"
 
 /-- Inflectional distribution: agreement doubled, tense on AUX, mood on LV. -/
 def inflDistribution : InflDistribution :=
-  { onAux := [.agreement, .tense]
-  , onLex := [.agreement, .mood] }
+  { onAux := [.agreement .subj, .tense]
+  , onLex := [.agreement .subj, .mood] }
 
 /-! ## Verification -/
 
 theorem form_nonempty : form ≠ "" := by decide
 
-/-- Agreement is doubled: it appears on both AUX and LV. -/
+/-- Agreement is doubled: subject agreement appears on both AUX and LV. -/
 theorem agreement_doubled :
-    inflDistribution.onAux.contains .agreement = true ∧
-    inflDistribution.onLex.contains .agreement = true := by
+    inflDistribution.onAux.contains (.agreement .subj) = true ∧
+    inflDistribution.onLex.contains (.agreement .subj) = true := by
   exact ⟨by decide, by decide⟩
 
 /-- Tense is split to AUX only. -/

Linglib/Fragments/Jakaltek/AuxiliaryVerbs.lean

@@ -29,13 +29,13 @@ def gloss : String := "COMPL-ABS2 ERG1-see 'I saw you'"
 def family : String := "Mayan"
 def location : String := "Guatemala"
 
-/-- Split inflection distribution: AUX hosts aspect and absolutive agreement
-    (= object in transitive); LV hosts ergative agreement (= subject in
-    transitive). Both absolutive and ergative cross-referencing are
-    `.agreement` at the `MorphCategory` level; the split is within the
-    agreement system (absolutive vs. ergative), not between category types. -/
+/-- Split inflection distribution: AUX hosts aspect and absolutive
+    agreement (= object in a transitive clause); LV hosts ergative
+    agreement (= subject in a transitive clause). The role-typed
+    `.agreement` constructor surfaces the abs/erg distinction at the
+    substrate level: `.obj` on AUX, `.subj` on LV. -/
 def inflDistribution : InflDistribution :=
-  { onAux := [.aspect, .agreement]
-  , onLex := [.agreement] }
+  { onAux := [.aspect, .agreement .obj]
+  , onLex := [.agreement .subj] }
 
 end Fragments.Jakaltek.AuxiliaryVerbs