Number resolution

[Cor00] [Har14a] [Lin83]

The single canonical number-resolution operation: when two number-bearing referents combine (conjoined DPs, resolved agreement), the result is derived from the join-semilattice of individuals ([Lin83]) via [Har14a]'s feature geometry, then coarsened to the values the language's number system makes available — the formal content of [Cor00] §6.3: "the result depends on which number values the language has."

• Number.resolve computes the finest value for the mereological sum (sg ⊔ sg → du: atom ⊔ atom = pair).
• Number.coarsenTo maps it to an available value (du → pl in a {sg, pl} system like English).
• Number.resolveIn composes the two; Number.System.resolve is the system-typed entry point.

Consumers: Studies/Carstens2026.lean calls resolveIn as the number dimension of its coordinate φ-resolution; Studies/Corbett2000.lean states the book's resolution data over its language systems.

Canonical resolution

def Number.resolve (a b : Number) : Number

Canonical number resolution: the finest value for the mereological sum of two referents, derived from two lattice-theoretic principles. The resolution data are [Cor00] §6.3 (resolved dual in Slovene/Sorbian); the value lattice they are derived from is [Lin83]/[Har14a]:

1. Cardinality addition (for determinate values): |A ⊔ B| = |A| + |B| for disjoint referent sets A, B. The sum is mapped back to the finest determinate value via Number.fromCard.

   • sg(1) + sg(1) = 2 → du
   • sg(1) + du(2) = 3 → trial
   • du(2) + du(2) = 4 → plural (no determinate value for sums ≥ 4)

2. 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.

3. Catch-all: values without exact cardinality or MIN/AUG membership (plural, paucal, greaterPlural, etc.) resolve to plural — the default non-singular value.

Equations

• a.resolve b = match a.exactCard, b.exactCard with | some na, some nb => Number.fromCard (na + nb) | x, x_1 => if a.isMinAug ∧ b.isMinAug then Number.augmented else Number.plural

theorem Number.resolve_comm (a b : Number) : a.resolve b = b.resolve a

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

theorem Number.resolve_assoc (a b c : Number) : (a.resolve b).resolve c = a.resolve (b.resolve c)

Canonical resolution is associative: sums of three or more referents resolve the same under any bracketing (cardinalities ≥ 4 all collapse to the residual plural, which absorbs).

Coarsening to a system

def Number.coarsenTo (system : List Number) (c : Number) : Number

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

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

The superordinate map is hand-specified: it is not monotone in the markedness order (Number.instPartialOrder), whose direction is implicational (b presupposes a), not referent-containment. By construction it returns a value in system (or the input unchanged), so resolveIn is closed over every [Har14a] Table 3 system.

Equations

• One or more equations did not get rendered due to their size.
• Number.coarsenTo system Number.augmented = if system.contains Number.augmented = true then Number.augmented else if system.contains Number.plural = true then Number.plural else Number.augmented
• Number.coarsenTo system c = if system.contains c = true then c else c

def Number.resolveIn (system : List Number) (a b : Number) : Number

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

This derives resolution rules from two independent components:

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

Equations

• Number.resolveIn system a b = Number.coarsenTo system (a.resolve b)

theorem Number.resolveIn_comm (system : List Number) (a b : Number) : resolveIn system a b = resolveIn system b a

System-parameterized resolution is commutative.

def Number.System.resolve (ns : System) (a b : Number) : Number

Resolution typed by a Number.System: resolve in the system's values.

Equations

• ns.resolve a b = Number.resolveIn ns.values a b

Lattice verification

The canonical resolution is verified against the 3-atom powerset lattice (Number.ps3: nonempty subsets of Fin 3, join = union). Number.latticeToFeatures classifies elements by lattice position; resolve is the union pushed through the classification.

theorem Number.lattice_atom_join_dual : latticeToFeatures ps3 ({0} ∪ {1}) = dualF

Atom ⊔ atom is a pair, which is dual (minimal non-atom). Lattice grounding: resolve sg sg = du.

theorem Number.lattice_atom_pair_plural : latticeToFeatures ps3 ({2} ∪ {0, 1}) = pluralF

Atom ⊔ pair is the triple, which is plural (non-minimal non-atom). Lattice grounding: resolve sg du = trial (plural in the base system, trial with recursion).

theorem Number.lattice_grounding_agrees : latticeToFeatures ps3 ({0} ∪ {1}) = dualF ∧ latticeToFeatures ps3 ({2} ∪ {0, 1}) = pluralF

The derived resolve agrees with the powerset lattice: join in the concrete lattice, then classify via latticeToFeatures, matches resolve applied to the classified inputs — the structural proof that resolve is the lattice join pushed through the classification, not a stipulation.

System-dependent predictions

theorem Number.resolve_sgpl_sg_sg : resolveIn [singular, plural] singular singular = plural

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

theorem Number.resolve_sgdupl_sg_sg : resolveIn [singular, dual, plural] singular singular = dual

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

theorem Number.resolve_sgdupl_sg_du : resolveIn [singular, dual, plural] singular dual = plural

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

theorem Number.resolve_larike_sg_du : resolveIn [singular, dual, plural, trial, greaterPlural] singular dual = trial

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

theorem Number.resolve_larike_sg_sg : resolveIn [singular, dual, plural, trial, greaterPlural] singular singular = dual

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

theorem Number.resolve_minAug_min_min : resolveIn [minimal, augmented] minimal minimal = augmented

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