Number

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

Two components of the number API:

§ 1–3: Number Categories (@cite{corbett-2000}). Eight analytical number values organized along two orthogonal dimensions:

• System membership: general number is outside the number system (a form non-committal to cardinality); all others are within it.
• Determinacy: values whose cardinality boundary is fixed (singular=1, dual=2, trial=3) vs those whose boundary varies by context (paucal ≈ 2–6, greater plural ≈ abundance).

§ 4–6: Number Features (@cite{harbour-2014}). Binary feature decomposition:

• [±atomic]: whether the referent is an atom (singleton) or a non-atom (plurality). Singular is [+atomic]; dual and plural are [−atomic].
• [±minimal]: whether the referent is a minimal element of the relevant lattice region. Singular and dual are [+minimal]; plural is [−minimal].

These features form a containment hierarchy: [+atomic] → [+minimal]. An atom is necessarily a minimal element of any lattice region it belongs to.

This containment parallels person features: [+author] → [+participant].

The three well-formed combinations yield the three basic number values:

• singular: [+atomic, +minimal] — atoms (singletons)
• dual: [−atomic, +minimal] — minimal non-atoms (pairs)
• plural: [−atomic, −minimal] — non-minimal non-atoms (triads and up)

Trial, unit augmented, and augmented arise from feature recursion (reapplying [±minimal] to subregions), which is theory-layer material. The approximative numbers (paucal, greater paucal, greater plural) require the additional feature [±additive], also theory-layer.

The full typological machinery (number systems, animacy profiles, agreement hierarchy, language data) remains in Phenomena/Agreement/Studies/Corbett2000.lean.

inductive Features.Number.Category : Type

Number categories in @cite{corbett-2000}'s inventory.

Two orthogonal classifications:

• System membership: general is outside the number system; all others are within it.
• Determinacy: values whose cardinality boundary is fixed (singular=1, dual=2, trial=3) vs those whose boundary varies by context (paucal ≈ 2–6, greater plural ≈ all/abundance).

• general : Category
• singular : Category
• dual : Category
• trial : Category
• paucal : Category
• plural : Category
• greaterPaucal : Category
• greaterPlural : Category
• minimal : Category
• augmented : Category
• unitAugmented : Category
• globalPlural : Category

@[implicit_reducible]

instance Features.Number.instDecidableEqCategory : DecidableEq Category

Equations

• Features.Number.instDecidableEqCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Number.instReprCategory : Repr Category

Equations

• Features.Number.instReprCategory = { reprPrec := Features.Number.instReprCategory.repr }

def Features.Number.instReprCategory.repr : Category → ℕ → Std.Format

Equations

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

def Features.Number.Category.isDeterminate : Category → Prop

A number category is determinate iff its cardinality boundary is fixed. Minimal and unit augmented are indeterminate: they depend on the composition of the group, not a fixed cardinality.

Equations

• Features.Number.Category.singular.isDeterminate = True
• Features.Number.Category.dual.isDeterminate = True
• Features.Number.Category.trial.isDeterminate = True
• x✝.isDeterminate = False

@[implicit_reducible]

instance Features.Number.Category.instDecidablePredIsDeterminate : DecidablePred isDeterminate

Equations

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

def Features.Number.Category.isInSystem : Category → Prop

A number category participates in the number system (is not general).

Equations

• Features.Number.Category.general.isInSystem = False
• x✝.isInSystem = True

@[implicit_reducible]

instance Features.Number.Category.instDecidablePredIsInSystem : DecidablePred isInSystem

Equations

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

def Features.Number.Category.exactCard : Category → Option ℕ

Exact referent-set cardinality for determinate number categories.

Singular denotes exactly 1 individual (atom), dual exactly 2 (pair), trial exactly 3 (triple). All other categories — plural, paucal, greaterPlural, minimal, augmented — have indeterminate or context-dependent cardinality and return none.

Used by CoordinateResolution.canonicalResolve to derive resolution from cardinality addition: |A ⊔ B| = |A| + |B| for disjoint sets.

Equations

• Features.Number.Category.singular.exactCard = some 1
• Features.Number.Category.dual.exactCard = some 2
• Features.Number.Category.trial.exactCard = some 3
• x✝.exactCard = none

def Features.Number.Category.isMinAug : Category → Prop

Whether a category belongs to the [±minimal] number system (without [±atomic]). In such systems, minimal = atoms ∪ minimal non-atoms, and augmented = everything else. Returns none for categories outside the MIN/AUG system.

Equations

• Features.Number.Category.minimal.isMinAug = True
• Features.Number.Category.augmented.isMinAug = True
• x✝.isMinAug = False

@[implicit_reducible]

instance Features.Number.Category.instDecidablePredIsMinAug : DecidablePred isMinAug

Equations

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

def Features.Number.Category.fromCard : ℕ → Category

Map a referent-set cardinality back to the finest determinate category. 1 → singular, 2 → dual, 3 → trial, 4+ → greaterPlural.

Equations

• Features.Number.Category.fromCard 1 = Features.Number.Category.singular
• Features.Number.Category.fromCard 2 = Features.Number.Category.dual
• Features.Number.Category.fromCard 3 = Features.Number.Category.trial
• Features.Number.Category.fromCard x✝ = Features.Number.Category.greaterPlural

theorem Features.Number.Category.fromCard_singular : fromCard 1 = singular

fromCard inverts exactCard for determinate categories.

theorem Features.Number.Category.fromCard_dual : fromCard 2 = dual

theorem Features.Number.Category.fromCard_trial : fromCard 3 = trial

def Features.Number.Category.toUD : Category → Option UD.Number

Map analytical number categories to UD.Number (general has no UD equivalent). Minimal, augmented, unit augmented, and global plural have no UD representation.

Equations

• Features.Number.Category.general.toUD = none
• Features.Number.Category.singular.toUD = some UD.Number.Sing
• Features.Number.Category.dual.toUD = some UD.Number.Dual
• Features.Number.Category.trial.toUD = some UD.Number.Tri
• Features.Number.Category.paucal.toUD = some UD.Number.Pauc
• Features.Number.Category.plural.toUD = some UD.Number.Plur
• Features.Number.Category.greaterPaucal.toUD = some UD.Number.Grpa
• Features.Number.Category.greaterPlural.toUD = some UD.Number.Grpl
• Features.Number.Category.minimal.toUD = none
• Features.Number.Category.augmented.toUD = none
• Features.Number.Category.unitAugmented.toUD = none
• Features.Number.Category.globalPlural.toUD = none

def Features.Number.Category.fromUD : UD.Number → Option Category

Map UD.Number to analytical number categories (partial).

Seven core categories round-trip cleanly. Three UD values have no analytical equivalent:

• Inv (inverse number): marks the unexpected number for a given noun — plural for some nouns, singular for others. Not a fixed cardinality.
• Coll (collective): denotes a group-as-unit (Russian листва 'foliage'), distinct from general number which is non-committal to cardinality.
• Count (count form): a special form after numerals (Hungarian, Welsh), not equivalent to singular (exactly one).

Equations

• Features.Number.Category.fromUD UD.Number.Sing = some Features.Number.Category.singular
• Features.Number.Category.fromUD UD.Number.Plur = some Features.Number.Category.plural
• Features.Number.Category.fromUD UD.Number.Dual = some Features.Number.Category.dual
• Features.Number.Category.fromUD UD.Number.Tri = some Features.Number.Category.trial
• Features.Number.Category.fromUD UD.Number.Pauc = some Features.Number.Category.paucal
• Features.Number.Category.fromUD UD.Number.Grpa = some Features.Number.Category.greaterPaucal
• Features.Number.Category.fromUD UD.Number.Grpl = some Features.Number.Category.greaterPlural
• Features.Number.Category.fromUD UD.Number.Inv = none
• Features.Number.Category.fromUD UD.Number.Coll = none
• Features.Number.Category.fromUD UD.Number.Count = none

theorem Features.Number.roundtrip_fromUD_toUD : ([Category.singular, Category.dual, Category.trial, Category.paucal, Category.plural, Category.greaterPaucal, Category.greaterPlural].all fun (v : Category) => v.toUD.bind Category.fromUD == some v) = true

Round-trip: fromUD ∘ toUD = id for all in-system categories.

structure Features.Number.Features : Type

Binary number features: [±atomic, ±minimal].

These two features suffice for the three basic number distinctions:

• singular: [+atomic, +minimal]
• dual: [−atomic, +minimal]
• plural: [−atomic, −minimal]

The fourth combination [+atomic, −minimal] is ill-formed: an atom is necessarily a minimal element of any lattice region.

• isAtomic : Bool

  [+atomic]: referent is an atom (singleton individual).

• isMinimal : Bool

  [+minimal]: referent is a minimal element of the relevant lattice region.

@[implicit_reducible]

instance Features.Number.instDecidableEqFeatures : DecidableEq Features

Equations

• Features.Number.instDecidableEqFeatures = Features.Number.instDecidableEqFeatures.decEq

def Features.Number.instDecidableEqFeatures.decEq (x✝ x✝¹ : Features) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Features.Number.instReprFeatures : Repr Features

Equations

• Features.Number.instReprFeatures = { reprPrec := Features.Number.instReprFeatures.repr }

def Features.Number.instReprFeatures.repr : Features → ℕ → Std.Format

Equations

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

def Features.Number.Features.wellFormed (nf : Features) : Bool

Well-formedness: [+atomic] → [+minimal]. An atom (singleton) is necessarily a minimal element.

Equations

• nf.wellFormed = (!nf.isAtomic || nf.isMinimal)

def Features.Number.singularF : Features

Singular features: [+atomic, +minimal].

Equations

• Features.Number.singularF = { isAtomic := true, isMinimal := true }

def Features.Number.dualF : Features

Dual features: [−atomic, +minimal].

Equations

• Features.Number.dualF = { isAtomic := false, isMinimal := true }

def Features.Number.pluralF : Features

Plural features: [−atomic, −minimal].

Equations

• Features.Number.pluralF = { isAtomic := false, isMinimal := false }

def Features.Number.Features.toCategory : Features → Option Category

Map number features to Corbett's analytical number categories.

The three well-formed base feature bundles map to three of @cite{corbett-2000}'s eight categories. The remaining (trial, paucal, etc.) arise from feature recursion and [±additive], which require compositional machinery beyond the base feature pair.

Equations

• { isAtomic := true, isMinimal := true }.toCategory = some Features.Number.Category.singular
• { isAtomic := false, isMinimal := true }.toCategory = some Features.Number.Category.dual
• { isAtomic := false, isMinimal := false }.toCategory = some Features.Number.Category.plural
• { isAtomic := true, isMinimal := false }.toCategory = none

def Features.Number.Features.fromCategory : Category → Option Features

Map Corbett's number categories to base features (partial).

Only the three categories derivable from the base [±atomic, ±minimal] system have feature equivalents. Trial, paucal, minimal, augmented, and the rest require feature recursion, [±additive], or different feature activation patterns.

Equations

• Features.Number.Features.fromCategory Features.Number.Category.singular = some Features.Number.singularF
• Features.Number.Features.fromCategory Features.Number.Category.dual = some Features.Number.dualF
• Features.Number.Features.fromCategory Features.Number.Category.plural = some Features.Number.pluralF
• Features.Number.Features.fromCategory x✝ = none

@[implicit_reducible]

instance Features.Number.instPhiFeaturesFeatures : PhiFeatures Features

Number features are a PhiFeatures instance: outer = isMinimal, inner = isAtomic.

The containment [+atomic] → [+minimal] maps to PrivativePair's [+inner] → [+outer], unifying the structure with person features. All shared properties are inherited by construction.

Equations

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

@[simp]

theorem Features.Number.singular_is_maximal : PhiFeatures.toPair singularF = PrivativePair.maximal

The three canonical number values map to the three PrivativePair cells.

@[simp]

theorem Features.Number.dual_is_intermediate : PhiFeatures.toPair dualF = PrivativePair.intermediate

@[simp]

theorem Features.Number.plural_is_minimal : PhiFeatures.toPair pluralF = PrivativePair.minimal

theorem Features.Number.no_fourth_base_number (a b c d : Features) : a.wellFormed = true → b.wellFormed = true → c.wellFormed = true → d.wellFormed = true → a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → False

No 4-way base number distinction (inherited from PhiFeatures).

@[simp]

theorem Features.Number.singular_wellFormed : singularF.wellFormed = true

@[simp]

theorem Features.Number.dual_wellFormed : dualF.wellFormed = true

@[simp]

theorem Features.Number.plural_wellFormed : pluralF.wellFormed = true

theorem Features.Number.illFormed_only : { isAtomic := true, isMinimal := false }.wellFormed = false

The ill-formed combination [+atomic, −minimal] is the only combination that violates well-formedness.

theorem Features.Number.exactly_three_wellFormed : (List.filter Features.wellFormed [{ isAtomic := true, isMinimal := true }, { isAtomic := true, isMinimal := false }, { isAtomic := false, isMinimal := true }, { isAtomic := false, isMinimal := false }]).length = 3

There are exactly 3 well-formed feature combinations (= 3 base numbers).

theorem Features.Number.roundtrip_fromCategory_toCategory : ([singularF, dualF, pluralF].all fun (f : Features) => f.toCategory.bind Features.fromCategory == some f) = true

Round-trip: fromCategory ∘ toCategory = some for all well-formed features.

theorem Features.Number.illFormed_toCategory_none : { isAtomic := true, isMinimal := false }.toCategory = none

toCategory returns none for the ill-formed bundle.

theorem Features.Number.atomic_implies_minimal (f : Features) (hw : f.wellFormed = true) : f.isAtomic = true → f.isMinimal = true

Containment: [+atomic] → [+minimal] for all well-formed features.

Lattice-Theoretic Grounding

Number features grounded in a join-semilattice of individuals.

@cite{link-1983} models the domain of individuals as a join-semilattice ⟨D, ⊔⟩. Number categories correspond to lattice predicates:

• singular = atoms (no proper part)
• dual = minimal non-atoms (join of exactly 2 atoms)
• plural = non-minimal non-atoms

The containment [+atomic] → [+minimal] is a theorem of lattice theory, not a stipulation: atoms have no proper parts, so they are trivially minimal in any sublattice region (Mereology.Atom).

The decidable functions isAtom and isMinimalNonAtom are parameterized by a join operation and a finite domain, making the lattice-theoretic grounding computationally verifiable. They are the Bool counterparts of Mereology.Atom and minimality-in-region.

def Features.Number.bitmaskJoin (a b : ℕ) : ℕ

Powerset lattice join (bitwise OR). Atoms are powers of 2; sums are bitwise OR of their atoms. Used across §§8–10 and by CoordinateResolution for lattice verification.

Equations

• Features.Number.bitmaskJoin a b = a.lor b

def Features.Number.isAtom {D : Type} [DecidableEq D] (join : D → D → D) (domain : List D) (x : D) : Bool

An element is an atom in a domain under the join-induced ordering: x ∈ domain and no element other than x is below it. Decidable counterpart of Mereology.Atom (∀ y, y ≤ x → y = x), parameterized by a concrete join operation and finite domain.

Equations

• Features.Number.isAtom join domain x = (domain.contains x && domain.all fun (y : D) => y == x || !Features.Number.joinLE✝ join y x)

def Features.Number.isMinimalNonAtom {D : Type} [DecidableEq D] (join : D → D → D) (domain : List D) (x : D) : Bool

An element is a minimal non-atom: not an atom, and no non-atom in the domain is strictly below it in the join-induced ordering. For number: minimal non-atoms are duals (pairs of exactly 2 atoms). Non-minimal non-atoms are plurals (groups of 3+).

Equations

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

def Features.Number.latticeToFeatures {D : Type} [DecidableEq D] (join : D → D → D) (domain : List D) (x : D) : Features

Convert lattice membership to number features using join structure. Atoms → singular, minimal non-atoms → dual, others → plural.

Equations

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

theorem Features.Number.latticeToFeatures_wellFormed {D : Type} [DecidableEq D] (join : D → D → D) (domain : List D) (x : D) : (latticeToFeatures join domain x).wellFormed = true

Containment follows from lattice structure: atoms always get [+minimal], so [+atomic] → [+minimal] holds by construction. Every branch of latticeToFeatures produces a well-formed bundle.

theorem Features.Number.ex_atom_is_singular : latticeToFeatures bitmaskJoin Features.Number.ps2Domain✝ 1 = singularF

theorem Features.Number.ex_atom_is_singular' : latticeToFeatures bitmaskJoin Features.Number.ps2Domain✝ 2 = singularF

theorem Features.Number.ex_pair_is_dual : latticeToFeatures bitmaskJoin Features.Number.ps2Domain✝ 3 = dualF

def Features.Number.ps3Domain : List ℕ

Powerset lattice with 3 atoms: {0}=1, {1}=2, {2}=4. Pairs (3,5,6) are minimal non-atoms → dual. Triple (7) is non-minimal non-atom → plural. This demonstrates that isMinimalNonAtom correctly distinguishes duals from plurals in a non-trivial lattice (the 2-atom domain above has only one non-atom and cannot show this).

Equations

• Features.Number.ps3Domain = [1, 2, 4, 3, 5, 6, 7]

theorem Features.Number.ps3_atom_is_singular : latticeToFeatures bitmaskJoin ps3Domain 1 = singularF

theorem Features.Number.ps3_pair_is_dual : latticeToFeatures bitmaskJoin ps3Domain 3 = dualF

theorem Features.Number.ps3_pair_is_dual' : latticeToFeatures bitmaskJoin ps3Domain 5 = dualF

theorem Features.Number.ps3_triple_is_plural : latticeToFeatures bitmaskJoin ps3Domain 7 = pluralF

The Additive Feature

@cite{harbour-2014}

[±additive] is the third number feature, characterizing join-completeness within a lattice region. Applied to the non-atomic region, it separates:

• [+additive] = "abundance" (plural/greater plural) — join-complete
• [−additive] = "paucity" (paucal/greater paucal) — not join-complete

The boundary is fixed by sociosemantic convention, subject to:

• Complement completeness ((11)): the [+additive] subregion must be join-complete.
• Fungibility ((12)): the boundary must be permutation-invariant (horizontal cuts by cardinality, not identity of atoms).

Connection to CUM: [+additive] IS cumulativity restricted to a subregion. The link between number and aspect/telicity (@cite{harbour-2014} §4.4) runs through exactly this connection: mass nouns satisfy [+additive] (cumulative), count nouns satisfy [−additive] (quantized).

def Features.Number.isJoinCompleteIn {D : Type} [DecidableEq D] (join : D → D → D) (region : List D) (x : D) : Bool

An element is join-complete in a region under a given join operation. @cite{harbour-2014} (10): +additive ⟺ x ∈ Q ∧ ∀y ∈ Q, x ⊔ y ∈ Q.

Equations

• Features.Number.isJoinCompleteIn join region x = (region.contains x && region.all fun (y : D) => region.contains (join x y))

def Features.Number.isRegionJoinComplete {D : Type} [DecidableEq D] (join : D → D → D) (region : List D) : Bool

A region is globally join-complete: every element is [+additive]. Decidable counterpart of Mereology.CUM restricted to the region: CUM(Q) ⇔ ∀x,y ∈ Q, x ⊔ y ∈ Q.

Equations

• Features.Number.isRegionJoinComplete join region = region.all fun (x : D) => Features.Number.isJoinCompleteIn join region x

Powerset Lattice Examples

Paucal vs plural on a powerset lattice (join = bitwise OR). Atoms encoded as powers of 2; sums as bitwise OR of their atoms.

With 3 atoms, the non-atomic region is entirely join-complete, so [±additive] draws no distinction — paucal requires a richer lattice.

With 5 atoms, the "paucal" region (2–3 atoms) is NOT join-complete: two small sums can join to exceed "a few." The "plural" region (≥ 4 atoms) IS join-complete, satisfying complement completeness.

theorem Features.Number.ps3_nonAtoms_joinComplete : isRegionJoinComplete bitmaskJoin Features.Number.ps3NonAtoms✝ = true

With 3 atoms, the entire non-atomic region is join-complete. [±additive] is vacuous — no paucal/plural split possible.

theorem Features.Number.ps5_paucal_not_joinComplete : isRegionJoinComplete bitmaskJoin Features.Number.ps5Paucal✝ = false

The paucal region is NOT join-complete: {0,1}=3 ⊔ {2,3}=12 = {0,1,2,3}=15 has 4 atoms and escapes the region.

theorem Features.Number.ps5_plural_joinComplete : isRegionJoinComplete bitmaskJoin Features.Number.ps5Plural✝ = true

The plural region IS join-complete: joining two large sums stays large. Satisfies complement completeness (@cite{harbour-2014} (11)).

theorem Features.Number.ps5_additive_asymmetry : isRegionJoinComplete bitmaskJoin Features.Number.ps5Plural✝ = true ∧ isRegionJoinComplete bitmaskJoin Features.Number.ps5Paucal✝ = false

The paucal/plural asymmetry: the [+additive] region is join-complete, the [−additive] region is not. This is the formal content of the approximative number distinction (@cite{harbour-2014} §3).

DUAL as predicate modifier

@cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025}

The paper proposes (eq 39 in §4.2.1, derived from Harbour features in §8 eq 98b) that the core concept DUAL has a predicate-modification semantics:

⟦DUAL⟧ = λP.λx. P(x) ∧ |{y : atom(y) ∧ y ⊑ x}| = 2

In a join-semilattice, "exactly 2 atomic parts below x" coincides with "x is a minimal non-atom" — already formalized as isMinimalNonAtom. The bridge is therefore a one-line composition: filter P by the dual lattice predicate.

This connects the Harbour feature bundle dualF = ⟨isAtomic := false, isMinimal := true⟩ to the predicate modifier required by the paper's Indirect Alternative analysis: les deux lexicalizes the predicate modifier dualPredOnLattice _ _ verres ('cup'), which is what blocks tous les NP.dual. See Phenomena/Presupposition/Studies/JereticEtAl2025.lean.

def Features.Number.dualPredOnLattice {D : Type} [DecidableEq D] (join : D → D → D) (domain : List D) (P : D → Bool) (x : D) : Bool

⟦DUAL⟧ as a predicate modifier on a join-semilattice domain (@cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025} eq 39).

Given a property P over individuals and an element x, dualPredOnLattice holds of x iff P x and x has exactly 2 atomic parts. The latter is witnessed by isMinimalNonAtom, since in a join-semilattice the minimal non-atoms are precisely the joins of two atoms.

Equations

• Features.Number.dualPredOnLattice join domain P x = (P x && Features.Number.isMinimalNonAtom join domain x)

theorem Features.Number.dualPredOnLattice_refines {D : Type} [DecidableEq D] (join : D → D → D) (domain : List D) (P : D → Bool) (x : D) : dualPredOnLattice join domain P x = true → P x = true

dualPredOnLattice P strictly refines P: the dual reading of P is a subset of P.

theorem Features.Number.dualPredOnLattice_iff {D : Type} [DecidableEq D] (join : D → D → D) (domain : List D) (P : D → Bool) (x : D) : dualPredOnLattice join domain P x = true ↔ P x = true ∧ isMinimalNonAtom join domain x = true

The dual reading of a property holds of x iff P x and x is a minimal non-atom in the domain.

theorem Features.Number.not_atom_of_isMinimalNonAtom {D : Type} [DecidableEq D] (join : D → D → D) (domain : List D) (x : D) (h : isMinimalNonAtom join domain x = true) : isAtom join domain x = false

An element classified as a minimal non-atom is, by construction, not an atom. This is a structural fact about isMinimalNonAtom: it filters to the non-atom region of the domain before testing minimality.

theorem Features.Number.dualPredOnLattice_eq_via_features {D : Type} [DecidableEq D] (join : D → D → D) (domain : List D) (P : D → Bool) (x : D) : dualPredOnLattice join domain P x = true ↔ P x = true ∧ latticeToFeatures join domain x = dualF

Bridge: the lattice predicate isMinimalNonAtom IS the condition latticeToFeatures uses to assign dualF. So dualPredOnLattice factors as P x ∧ latticeToFeatures … x = dualF.

This grounds the paper's predicate-modifier semantics (@cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025} eq 39) in the existing Harbour feature decomposition (Number.lean §§4-5): DUAL is not a separate primitive but the same conditions used to classify a lattice element as [−atomic, +minimal].

theorem Features.Number.ps3_dual_pairs_satisfy : dualPredOnLattice bitmaskJoin ps3Domain (fun (x : ℕ) => true) 3 = true ∧ dualPredOnLattice bitmaskJoin ps3Domain (fun (x : ℕ) => true) 5 = true ∧ dualPredOnLattice bitmaskJoin ps3Domain (fun (x : ℕ) => true) 6 = true

On the 3-atom powerset, the dual reading of "is a non-atom" selects the three pairs (3, 5, 6) and excludes the triple (7).

theorem Features.Number.ps3_dual_triple_excluded : dualPredOnLattice bitmaskJoin ps3Domain (fun (x : ℕ) => true) 7 = false

Triples (≥3 atomic parts) fail the dual predicate.

inductive Features.Number.NumberStage : Type

Number opposition stages (@cite{cysouw-2009}, Fig 10.8). A coarsening over the eight @cite{corbett-2000} number values into a four-step hierarchy of typological "richness", from no number marking (N₁) to full number marking with restricted groups (N₃/N₄).

Used by both @cite{cysouw-2009} (paradigmatic person-marking) and @cite{corbett-2000} (NumberSystem.toNumberStage bridge in Phenomena/Agreement/Studies/Corbett2000.lean).

• N1 : NumberStage

  Undifferentiated number marking (singular = group unmarked).

• N2 : NumberStage

  Singular vs group (basic number opposition).

• N3 : NumberStage

  Restricted group (dual/trial) distinguished from unrestricted.

• N4 : NumberStage

  Small group (paucal) additionally distinguished.

@[implicit_reducible]

instance Features.Number.instDecidableEqNumberStage : DecidableEq NumberStage

Equations

• Features.Number.instDecidableEqNumberStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Number.instReprNumberStage : Repr NumberStage

Equations

• Features.Number.instReprNumberStage = { reprPrec := Features.Number.instReprNumberStage.repr }

def Features.Number.instReprNumberStage.repr : NumberStage → ℕ → Std.Format

Equations

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