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

instance Core.Number.instDecidableEqCategory : DecidableEq Category

Equations

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

instance Core.Number.instBEqCategory : BEq Category

Equations

• Core.Number.instBEqCategory = { beq := Core.Number.instBEqCategory.beq }

def Core.Number.instBEqCategory.beq : Category → Category → Bool

Equations

• Core.Number.instBEqCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Number.instReprCategory.repr : Category → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.Number.instReprCategory.repr Core.Number.Category.dual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Number.Category.dual")).group prec✝

instance Core.Number.instReprCategory : Repr Category

Equations

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

def Core.Number.Category.isDeterminate : Category → Bool

A number category is determinate iff its cardinality boundary is fixed.

Equations

• Core.Number.Category.singular.isDeterminate = true
• Core.Number.Category.dual.isDeterminate = true
• Core.Number.Category.trial.isDeterminate = true
• x✝.isDeterminate = false

def Core.Number.Category.isInSystem : Category → Bool

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

Equations

• Core.Number.Category.general.isInSystem = false
• x✝.isInSystem = true

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

Map analytical number categories to UD.Number (general has no UD equivalent).

Equations

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

def Core.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

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

theorem Core.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 Core.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.

instance Core.Number.instDecidableEqFeatures : DecidableEq Features

Equations

• Core.Number.instDecidableEqFeatures = Core.Number.instDecidableEqFeatures.decEq

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

Equations

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

instance Core.Number.instBEqFeatures : BEq Features

Equations

• Core.Number.instBEqFeatures = { beq := Core.Number.instBEqFeatures.beq }

def Core.Number.instBEqFeatures.beq : Features → Features → Bool

Equations

• Core.Number.instBEqFeatures.beq { isAtomic := a, isMinimal := a_1 } { isAtomic := b, isMinimal := b_1 } = (a == b && a_1 == b_1)
• Core.Number.instBEqFeatures.beq x✝¹ x✝ = false

def Core.Number.instReprFeatures.repr : Features → Nat → Std.Format

Equations

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

instance Core.Number.instReprFeatures : Repr Features

Equations

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

def Core.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 Core.Number.singularF : Features

Singular features: [+atomic, +minimal].

Equations

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

def Core.Number.dualF : Features

Dual features: [−atomic, +minimal].

Equations

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

def Core.Number.pluralF : Features

Plural features: [−atomic, −minimal].

Equations

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

def Core.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 Core.Number.Category.singular
• { isAtomic := false, isMinimal := true }.toCategory = some Core.Number.Category.dual
• { isAtomic := false, isMinimal := false }.toCategory = some Core.Number.Category.plural
• { isAtomic := true, isMinimal := false }.toCategory = none

def Core.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, and the rest require feature recursion or [±additive].

Equations

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

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

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

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

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

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

theorem Core.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 Core.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 Core.Number.illFormed_toCategory_none : { isAtomic := true, isMinimal := false }.toCategory = none

toCategory returns none for the ill-formed bundle.

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

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