Coordinate Agreement Resolution #

@cite{corbett-2000} @cite{adamson-anagnostopoulou-2025} @cite{carstens-2026} @cite{harbour-2014} @cite{link-1983}

When DPs are conjoined, &P must bear phi-features for agreement. Each phi-dimension resolves conjuncts' features using a distinct operation:

Number (@cite{corbett-2000} §6.3, @cite{harbour-2014}): mereological join — canonically sg + sg → du (atom ⊔ atom = pair), coarsened to the available categories in the target number system (du → pl in {sg, pl} systems like English)
Gender (@cite{adamson-anagnostopoulou-2025}, @cite{carstens-2026}): intersection — shared i-features survive (via GenderResolution.resolve)
Person (@cite{noyer-1997}): hierarchy — most marked person wins

Despite different operations, all three share a common architecture:

Percolation: only i(nterpretable) features enter resolution
Resolution: apply the dimension-specific operation
Default: if resolution yields nothing, apply a language-specific default

A key structural asymmetry: number and person resolution always succeed (conjoined DPs always have some number and person), while gender resolution can fail (empty intersection → language-specific default).

Number resolution — lattice grounding #

Number resolution is derived from the join-semilattice of individuals (@cite{link-1983}) via @cite{harbour-2014}'s feature geometry:

canonicalResolve computes the finest category from the lattice join
coarsenTo maps it to the available categories in a number system
numberResolveIn composes the two

Relation to existing modules #

FeatureRecursion.lean: HarbourConfig.surfaceCategories provides the set of available number categories. numberResolveConfig composes canonical resolution with coarsening to a Harbour configuration.
GenderResolution.lean: compositional endpoint for gender resolution.
Corbett2000.lean: defines semanticResolve (= canonicalResolve without the MIN/AUG branch, coarsened inline).
Carstens2026.lean: instantiates the Bantu gender system and connects all three resolution levels.

source

structure Minimalist.Agreement.CoordinateResolution.ResolutionOp (F : Type) :

Type

A resolution operation for a single phi-feature dimension.

Person and number each have their own algebraic structure for combining feature values from conjoined DPs. Gender uses GenderResolution.resolve directly (multi-feature intersection).

resolve f₁ f₂ combines two percolated (interpretable) feature values and returns the resolved value, or none if resolution fails.

resolve : F → F → Option F

Instances For

Lattice-Grounded Number Resolution #

@cite{harbour-2014} @cite{corbett-2000} @cite{link-1983}

Number resolution for conjoined DPs is grounded in the join-semilattice of individuals (@cite{link-1983}). The referent of "X and Y" is the mereological sum x ⊔ y, and the sum's number category is determined by its lattice position (@cite{harbour-2014} §4):

atom ⊔ atom (disjoint) = pair → dual ([−atomic, +minimal])
atom ⊔ pair (disjoint) = triple → trial (minimal in plural region)
pair ⊔ pair (disjoint) = 4+ → greater plural (non-minimal in plural)
anything ⊔ non-minimal non-atom = non-minimal → plural

This CANONICAL resolution gives the finest possible category. Languages then coarsen the result to their available categories:

In a {sg, pl} system (English): du coarsens to pl → sg + sg → pl
In a {sg, du, pl} system (Slovene): du is available → sg + sg → du
In a {sg, du, trial, greaterPl} system: sg + du → trial

The coarsening is the formal content of @cite{corbett-2000} §6.3: "the result depends on which number values the language has."

source

def Minimalist.Agreement.CoordinateResolution.canonicalResolve (a b : Features.Number.Category) :

Features.Number.Category

Canonical number resolution: the finest category for the mereological sum of two referents, derived from two lattice-theoretic principles (@cite{harbour-2014}):

Cardinality addition (for determinate categories): |A ⊔ B| = |A| + |B| for disjoint referent sets A, B. The sum is mapped back to the finest determinate category via Category.fromCard.
- sg(1) + sg(1) = 2 → du
- sg(1) + du(2) = 3 → trial
- du(2) + du(2) = 4 → greaterPlural
MIN/AUG lattice join (for [±minimal] systems without [±atomic]): In a 2-level lattice {minimal, augmented}, the join of any two distinct elements exceeds the minimal. Since coordination requires disjoint referents, the result is always augmented.
Catch-all: Categories without exact cardinality or MIN/AUG membership (plural, paucal, greaterPlural, etc.) resolve to plural — the default non-singular category.

Equations

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

Instances For

source

theorem Minimalist.Agreement.CoordinateResolution.canonical_comm (a b : Features.Number.Category) :

canonicalResolve a b = canonicalResolve b a

Canonical resolution is commutative: x ⊔ y = y ⊔ x.

source

def Minimalist.Agreement.CoordinateResolution.coarsenTo (system : List Features.Number.Category) (c : Features.Number.Category) :

Features.Number.Category

Coarsen a category to the nearest available one in a number system.

Categories not present in the system map to their semantic superordinate — the broader category whose referents include the absent category's referents.

Equations

One or more equations did not get rendered due to their size.
Minimalist.Agreement.CoordinateResolution.coarsenTo system c = if system.contains c = true then c else c

Instances For

source

def Minimalist.Agreement.CoordinateResolution.numberResolveIn (system : List Features.Number.Category) (a b : Features.Number.Category) :

Option Features.Number.Category

System-parameterized number resolution: canonical lattice join, coarsened to the available categories in the target system.

This derives resolution rules from two independent components:

Lattice join: sg + sg → du (canonical)
Coarsening: du → pl in a {sg, pl} system

Equations

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

Instances For

source

def Minimalist.Agreement.CoordinateResolution.numberOp (system : List Features.Number.Category) :

ResolutionOp Features.Number.Category

Number resolution operation for a given number system.

Equations

Minimalist.Agreement.CoordinateResolution.numberOp system = { resolve := Minimalist.Agreement.CoordinateResolution.numberResolveIn system }

Instances For

source

def Minimalist.Agreement.CoordinateResolution.numberResolveConfig (c : FeatureRecursion.HarbourConfig) (a b : Features.Number.Category) :

Option Features.Number.Category

numberResolveIn with the system from a HarbourConfig.

Equations

Minimalist.Agreement.CoordinateResolution.numberResolveConfig c a b = Minimalist.Agreement.CoordinateResolution.numberResolveIn c.surfaceCategories a b

Instances For

The canonical resolution is verified against a concrete 3-atom powerset lattice. Atoms: {a}=1, {b}=2, {c}=4. Pairs: {a,b}=3, {a,c}=5, {b,c}=6. Triple: {a,b,c}=7. Join = bitwise OR.

`Features.Number.latticeToFeatures` classifies elements by lattice
position: atoms → singular, minimal non-atoms → dual, non-minimal
non-atoms → plural.

source

theorem Minimalist.Agreement.CoordinateResolution.lattice_atom_join_dual :

Features.Number.latticeToFeatures Features.Number.bitmaskJoin Features.Number.ps3Domain (Features.Number.bitmaskJoin 1 2) = Features.Number.dualF

Atom 1 ⊔ Atom 2 = 3, which is dual (minimal non-atom). Lattice grounding: canonicalResolve sg sg = du.

source

theorem Minimalist.Agreement.CoordinateResolution.lattice_atom_pair_plural :

Features.Number.latticeToFeatures Features.Number.bitmaskJoin Features.Number.ps3Domain (Features.Number.bitmaskJoin 4 3) = Features.Number.pluralF

Atom 4 ⊔ Pair 3 = 7, which is plural (non-minimal non-atom). Lattice grounding: canonicalResolve sg du = trial (plural in base system, trial with recursion).

source

theorem Minimalist.Agreement.CoordinateResolution.lattice_grounding_agrees :

Features.Number.latticeToFeatures Features.Number.bitmaskJoin Features.Number.ps3Domain (Features.Number.bitmaskJoin 1 2) = Features.Number.dualF ∧ Features.Number.latticeToFeatures Features.Number.bitmaskJoin Features.Number.ps3Domain (Features.Number.bitmaskJoin 4 3) = Features.Number.pluralF

The derived canonicalResolve agrees with the powerset lattice: join in the concrete lattice, then classify via latticeToFeatures, matches canonicalResolve applied to the classified inputs.

atom(1) is singular, atom(2) is singular → join=3 is dual
atom(1) is singular, pair(6) is dual → join=7 is plural (= trial with recursion)

This is the structural proof that canonicalResolve is the lattice join pushed through latticeToFeatures, not a stipulation.

source

theorem Minimalist.Agreement.CoordinateResolution.resolve_sgpl_sg_sg :

numberResolveIn [Features.Number.Category.singular, Features.Number.Category.plural] Features.Number.Category.singular Features.Number.Category.singular = some Features.Number.Category.plural

In a {sg, pl} system (English): sg + sg → pl. Canonical du coarsened to plural.

source

theorem Minimalist.Agreement.CoordinateResolution.resolve_sgdupl_sg_sg :

numberResolveIn [Features.Number.Category.singular, Features.Number.Category.dual, Features.Number.Category.plural] Features.Number.Category.singular Features.Number.Category.singular = some Features.Number.Category.dual

In a {sg, du, pl} system (Slovene): sg + sg → du. Canonical du is available, no coarsening.

source

theorem Minimalist.Agreement.CoordinateResolution.resolve_sgdupl_sg_du :

In a {sg, du, pl} system: sg + du → pl (triple = plural without recursion).

source

theorem Minimalist.Agreement.CoordinateResolution.resolve_larike_sg_du :

numberResolveIn [Features.Number.Category.singular, Features.Number.Category.dual, Features.Number.Category.plural, Features.Number.Category.trial, Features.Number.Category.greaterPlural] Features.Number.Category.singular Features.Number.Category.dual = some Features.Number.Category.trial

In a {sg, du, trial, greaterPl} system (Larike): sg + du → trial.

source

theorem Minimalist.Agreement.CoordinateResolution.resolve_larike_sg_sg :

In a {sg, du, trial, greaterPl} system: sg + sg → du.

source

theorem Minimalist.Agreement.CoordinateResolution.resolve_minAug_min_min :

numberResolveIn [Features.Number.Category.minimal, Features.Number.Category.augmented] Features.Number.Category.minimal Features.Number.Category.minimal = some Features.Number.Category.augmented

In a {min, aug} system (Winnebago): min + min → aug.

Resolution Closure #

Number resolution is closed under every well-formed number system generated by @cite{harbour-2014}'s feature recursion: for any two categories a, b in a system S, the resolved category coarsenTo S (canonicalResolve a b) is also in S.

This is a non-trivial structural property — canonicalResolve can produce categories not in the target system (e.g., du from sg + sg in a {sg, pl} system), but coarsenTo always maps the result back to an available category. The theorem verifies this for all 15 Table 3 entries (12 distinct configs, covering 2–5 value systems).

source

theorem Minimalist.Agreement.CoordinateResolution.resolution_closure_table3 :

(FeatureRecursion.harbour2014Table3.all fun (entry : FeatureRecursion.Harbour2014Entry) => have sys := entry.config.surfaceCategories; sys.all fun (a : Features.Number.Category) => sys.all fun (b : Features.Number.Category) => sys.contains (coarsenTo sys (canonicalResolve a b))) = true

Resolution closure: for every Harbour 2014 Table 3 system, resolving any two categories from the system produces a category in the system.

source

def Minimalist.Agreement.CoordinateResolution.personResolve :

Features.Prominence.PersonLevel → Features.Prominence.PersonLevel → Option Features.Prominence.PersonLevel

Person resolution: most marked wins (@cite{noyer-1997}).

1st > 2nd > 3rd. The person with the higher prominence rank determines the resolved person on &P. This follows from person features being privative: [+participant] subsumes [−participant], and [+author] subsumes [−author]. Resolution always succeeds.

Equations

Instances For

source

def Minimalist.Agreement.CoordinateResolution.personOp :

ResolutionOp Features.Prominence.PersonLevel

Person resolution operation.

Equations

Minimalist.Agreement.CoordinateResolution.personOp = { resolve := Minimalist.Agreement.CoordinateResolution.personResolve }

Instances For

source

def Minimalist.Agreement.CoordinateResolution.percolate {F : Type} (a : GenderResolution.AnnotatedFeature F) :

Option F

Percolation: extract the feature value iff interpretable.

u-features are excluded from the resolution calculus (@cite{adamson-anagnostopoulou-2025}, @cite{carstens-2026}).

Equations

Minimalist.Agreement.CoordinateResolution.percolate a = if (a.interp == Minimalist.Interpretability.interpretable) = true then some a.value else none

Instances For

source

def Minimalist.Agreement.CoordinateResolution.resolveAnnotated {F : Type} (op : ResolutionOp F) (a b : GenderResolution.AnnotatedFeature F) :

Option F

Resolve two annotated features: percolate, then apply the operation.

Both features must be interpretable for resolution to proceed. If either is uninterpretable, resolution yields none (default).

Equations

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

Instances For

source

theorem Minimalist.Agreement.CoordinateResolution.number_total (system : List Features.Number.Category) (a b : Features.Number.Category) :

(numberResolveIn system a b).isSome = true

Number resolution always succeeds for any system.

source

theorem Minimalist.Agreement.CoordinateResolution.person_total (p₁ p₂ : Features.Prominence.PersonLevel) :

(personResolve p₁ p₂).isSome = true

Person resolution always succeeds.

source

theorem Minimalist.Agreement.CoordinateResolution.gender_singleton_iff_match {G : Type} [BEq G] [LawfulBEq G] (g₁ g₂ : G) :

(GenderResolution.resolve [{ value := g₁, interp := Interpretability.interpretable }] [{ value := g₂, interp := Interpretability.interpretable }]).isSome = (g₁ == g₂)

Gender resolution with singleton interpretable bundles succeeds iff features match — the only dimension that can fail, triggering default agreement.

source

theorem Minimalist.Agreement.CoordinateResolution.number_comm (system : List Features.Number.Category) (a b : Features.Number.Category) :

numberResolveIn system a b = numberResolveIn system b a

Number resolution is commutative for any system.

source

theorem Minimalist.Agreement.CoordinateResolution.person_comm (p₁ p₂ : Features.Prominence.PersonLevel) :

personResolve p₁ p₂ = personResolve p₂ p₁

Person resolution is commutative (both directions yield max).

source

theorem Minimalist.Agreement.CoordinateResolution.gender_only_fallible :

(∀ (system : List Features.Number.Category) (a b : Features.Number.Category), (numberResolveIn system a b).isSome = true) ∧ (∀ (p₁ p₂ : Features.Prominence.PersonLevel), (personResolve p₁ p₂).isSome = true) ∧ ∃ (g₁ : GenderResolution.FeatureBundle Bool) (g₂ : GenderResolution.FeatureBundle Bool), (GenderResolution.resolve g₁ g₂).isSome = false

The structural asymmetry: number and person always resolve successfully, but gender can fail. This explains why default agreement is a gender phenomenon, not a number or person one.

source

structure Minimalist.Agreement.CoordinateResolution.PhiBundle (G : Type) :

Type

A phi-feature bundle for a single conjunct DP.