Feature Recursion

@cite{harbour-2014} @cite{harbour-2016}

@cite{harbour-2014} §4, @cite{harbour-2016} Ch 6: extended number categories beyond the base three (singular, dual, plural) arise from feature recursion — reapplying [±minimal] to sublattice regions of the base [±atomic, ±minimal] partition.

The Mechanism

The base partition divides the lattice of individual sums into three regions:

• Singular [+atomic, +minimal]: atoms (singletons)
• Dual [−atomic, +minimal]: minimal non-atoms (pairs)
• Plural [−atomic, −minimal]: non-minimal non-atoms (groups of 3+)

Feature recursion reapplies [±minimal] to a non-singleton region, splitting it in two. This operation is constrained:

• Only [±minimal] can recurse (not [±atomic])
• The target region must have non-trivial lattice structure — atoms are singletons and cannot be further partitioned

Derived Categories

Recursion on plural (the [−atomic, −minimal] region) yields:

• Trial [+minimalR]: the minimal elements of the plural region (groups of exactly 3)
• Greater plural [−minimalR]: non-minimal plurals (groups of 4+)

Recursion on non-singular (the [−atomic] region, before the base [±minimal] split) yields:

• Unit augmented [+minimalR]: the minimal non-singulars (pairs)
• Augmented [−minimalR]: non-minimal non-singulars (groups of 3+)

Implicational Universals as a Lower Set

The implicational universals (trial → dual → plural → singular, etc.) are not stipulated — they are a theorem of the feature geometry. The generated categories form a lower set in the markedness partial order on Category: if a marked category is generated, all less-marked categories it presupposes are also generated (§ 8).

This is a lattice-theoretic property: the partial order on categories is the presupposition ordering, and the IsLowerSet formulation (Mathlib) captures all implicational universals in a single statement.

structure Minimalist.Agreement.FeatureRecursion.Region : Type

A region of the number lattice eligible for recursion.

Only non-atomic ([−atomic]) regions have internal lattice structure that supports a meaningful [±minimal] split. Atoms are singletons and cannot be further partitioned.

• base : Features.Number.Features

  The base number features defining this region.

• base_wf : self.base.wellFormed = true

  The base features must be well-formed.

• base_nonatomic : self.base.isAtomic = false

  The region must be non-atomic: atoms cannot be recursed.

@[implicit_reducible]

instance Minimalist.Agreement.FeatureRecursion.instDecidableEqRegion : DecidableEq Region

Equations

• Minimalist.Agreement.FeatureRecursion.instDecidableEqRegion = Minimalist.Agreement.FeatureRecursion.instDecidableEqRegion.decEq

def Minimalist.Agreement.FeatureRecursion.instDecidableEqRegion.decEq (x✝ x✝¹ : Region) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.Agreement.FeatureRecursion.pluralRegion : Region

The plural region: [−atomic, −minimal]. Groups of 3 or more.

Equations

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

def Minimalist.Agreement.FeatureRecursion.dualRegion : Region

The non-singular (dual) region: [−atomic, +minimal]. Minimal non-atoms (pairs).

Equations

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

structure Minimalist.Agreement.FeatureRecursion.RecursiveNumber : Type

A recursive number category: one application of [±minimal] within a base region.

@cite{harbour-2016} Ch 6: reapplying [±minimal] to a sublattice region splits it into a minimal and non-minimal subregion, yielding two new number categories from one base category.

• region : Region

  The target region for recursion.

• isMinimalInRegion : Bool

  [±minimal] within the target region.

@[implicit_reducible]

instance Minimalist.Agreement.FeatureRecursion.instDecidableEqRecursiveNumber : DecidableEq RecursiveNumber

Equations

• Minimalist.Agreement.FeatureRecursion.instDecidableEqRecursiveNumber = Minimalist.Agreement.FeatureRecursion.instDecidableEqRecursiveNumber.decEq

def Minimalist.Agreement.FeatureRecursion.instDecidableEqRecursiveNumber.decEq (x✝ x✝¹ : RecursiveNumber) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.Agreement.FeatureRecursion.trial : RecursiveNumber

Trial: minimal element of the plural region. The smallest groups of 3+ = groups of exactly 3.

Equations

• Minimalist.Agreement.FeatureRecursion.trial = { region := Minimalist.Agreement.FeatureRecursion.pluralRegion, isMinimalInRegion := true }

def Minimalist.Agreement.FeatureRecursion.greaterPlural : RecursiveNumber

Greater plural: non-minimal element of the plural region. Groups of 4+.

Equations

• Minimalist.Agreement.FeatureRecursion.greaterPlural = { region := Minimalist.Agreement.FeatureRecursion.pluralRegion, isMinimalInRegion := false }

def Minimalist.Agreement.FeatureRecursion.unitAugmented : RecursiveNumber

Unit augmented: minimal element of the non-singular region. The smallest non-singulars = pairs.

Equations

• Minimalist.Agreement.FeatureRecursion.unitAugmented = { region := Minimalist.Agreement.FeatureRecursion.dualRegion, isMinimalInRegion := true }

def Minimalist.Agreement.FeatureRecursion.augmented : RecursiveNumber

Augmented: non-minimal element of the non-singular region. Non-singulars that are not minimal = groups of 3+.

Equations

• Minimalist.Agreement.FeatureRecursion.augmented = { region := Minimalist.Agreement.FeatureRecursion.dualRegion, isMinimalInRegion := false }

def Minimalist.Agreement.FeatureRecursion.RecursiveNumber.toCategory (r : RecursiveNumber) : Features.Number.Category

Map recursive features to @cite{corbett-2000}'s number categories.

Recursion target determines the category:

• On the plural region ([−atomic, −minimal]): trial / greater plural
• On the non-singular region ([−atomic, +minimal]): unit augmented / augmented

Equations

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

theorem Minimalist.Agreement.FeatureRecursion.trial_toCategory : trial.toCategory = Features.Number.Category.trial

theorem Minimalist.Agreement.FeatureRecursion.greaterPlural_toCategory : greaterPlural.toCategory = Features.Number.Category.greaterPlural

theorem Minimalist.Agreement.FeatureRecursion.unitAugmented_toCategory : unitAugmented.toCategory = Features.Number.Category.unitAugmented

theorem Minimalist.Agreement.FeatureRecursion.augmented_toCategory : augmented.toCategory = Features.Number.Category.augmented

theorem Minimalist.Agreement.FeatureRecursion.no_singular_recursion : ¬∃ (r : Region), r.base = Features.Number.singularF

Recursion on singular is impossible: [+atomic] regions cannot be further partitioned because they're singletons.

This explains why no language has a "sub-singular" category: the singular region contains only atoms, which have no internal lattice structure to split via [±minimal].

theorem Minimalist.Agreement.FeatureRecursion.recursion_yields_two (reg : Region) : { region := reg, isMinimalInRegion := true }.toCategory ≠ { region := reg, isMinimalInRegion := false }.toCategory

Each recursion yields exactly 2 new categories: the [+minimal] and [−minimal] subregions are always distinct.

theorem Minimalist.Agreement.FeatureRecursion.trial_presupposes_plural : trial.region.base = Features.Number.pluralF

Trial presupposes plural: the plural region must exist (i.e., the base partition must include [−atomic, −minimal]) for trial to arise from recursion on it.

theorem Minimalist.Agreement.FeatureRecursion.unitAug_presupposes_dual : unitAugmented.region.base = Features.Number.dualF

Unit augmented presupposes dual: the non-singular region must exist for unit augmented to arise from recursion on it.

theorem Minimalist.Agreement.FeatureRecursion.recursion_presupposes_base (r : RecursiveNumber) : r.region.base.wellFormed = true

The base partition is a prerequisite for any recursion: every recursive category's base region is a well-formed base number.

theorem Minimalist.Agreement.FeatureRecursion.recursion_base_categories : trial.region.base.toCategory = some Features.Number.Category.plural ∧ unitAugmented.region.base.toCategory = some Features.Number.Category.dual

Base categories of recursive numbers map to Corbett categories.

theorem Minimalist.Agreement.FeatureRecursion.only_two_regions (r : Region) : r.base = Features.Number.dualF ∨ r.base = Features.Number.pluralF

There are exactly two recursion-eligible regions: the dual region ([−atomic, +minimal]) and the plural region ([−atomic, −minimal]).

The singular region ([+atomic, +minimal]) is excluded by base_nonatomic, and the ill-formed [+atomic, −minimal] is excluded by base_wf.

The markedness ordering on number categories, derived from @cite{harbour-2014}'s feature geometry and @cite{corbett-2000}'s implicational hierarchy. a ≤ b means b presupposes a: every number system containing b also contains a.

Three independent branches:
```
[±atomic] branch:        trial   greaterPlural
                           \        /
                            dual
                           /    \
                     singular    plural

[±minimal] branch:       unitAugmented
                              |
                          augmented
                              |
                           minimal

Approximative branch:    greaterPaucal    globalPlural
                              |               |
                            paucal          plural
```
The [±atomic] branch (singular, dual, trial, greaterPlural) and
[±minimal] branch (minimal, augmented, unitAugmented) are INDEPENDENT:
singular and minimal never cooccur; they arise from different feature
activations. Plural spans both branches: it appears in [±atomic]
systems as [−atomic] and in [±additive, ±minimal] systems as [+additive].

`general` is isolated (incomparable with all in-system categories). 

def Minimalist.Agreement.FeatureRecursion.markednessLE (a b : Features.Number.Category) : Bool

The markedness ordering on number categories as a decidable relation.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Agreement.FeatureRecursion.markednessLE Features.Number.Category.singular Features.Number.Category.dual = (Features.Number.Category.singular == Features.Number.Category.dual || true)
• Minimalist.Agreement.FeatureRecursion.markednessLE Features.Number.Category.singular Features.Number.Category.trial = (Features.Number.Category.singular == Features.Number.Category.trial || true)
• Minimalist.Agreement.FeatureRecursion.markednessLE Features.Number.Category.plural Features.Number.Category.dual = (Features.Number.Category.plural == Features.Number.Category.dual || true)
• Minimalist.Agreement.FeatureRecursion.markednessLE Features.Number.Category.plural Features.Number.Category.trial = (Features.Number.Category.plural == Features.Number.Category.trial || true)
• Minimalist.Agreement.FeatureRecursion.markednessLE Features.Number.Category.dual Features.Number.Category.trial = (Features.Number.Category.dual == Features.Number.Category.trial || true)
• Minimalist.Agreement.FeatureRecursion.markednessLE Features.Number.Category.plural Features.Number.Category.paucal = (Features.Number.Category.plural == Features.Number.Category.paucal || true)
• Minimalist.Agreement.FeatureRecursion.markednessLE a b = (a == b || false)

@[implicit_reducible]

instance Minimalist.Agreement.FeatureRecursion.instLECategory : LE Features.Number.Category

Equations

• Minimalist.Agreement.FeatureRecursion.instLECategory = { le := fun (a b : Features.Number.Category) => Minimalist.Agreement.FeatureRecursion.markednessLE a b = true }

@[implicit_reducible]

instance Minimalist.Agreement.FeatureRecursion.instDecidableRelCategoryLe : DecidableRel fun (a b : Features.Number.Category) => a ≤ b

Equations

• Minimalist.Agreement.FeatureRecursion.instDecidableRelCategoryLe a b = inferInstance

@[implicit_reducible]

instance Minimalist.Agreement.FeatureRecursion.instFintypeCategory : Fintype Features.Number.Category

Equations

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

@[implicit_reducible]

instance Minimalist.Agreement.FeatureRecursion.instPartialOrderCategory : PartialOrder Features.Number.Category

Equations

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

structure Minimalist.Agreement.FeatureRecursion.HarbourConfig : Type

A Harbour number configuration: which features and operations are active.

@cite{harbour-2014}: every attested number system can be described by activating a subset of these 5 parameters. The 2⁵ = 32 logically possible configurations reduce to 16 well-formed ones after applying the feature activation prerequisites.

• hasAtomic : Bool

  Whether [±atomic] is active.

• hasMinimal : Bool

  Whether [±minimal] is active.

• hasAdditive : Bool

  Whether [±additive] is active.

• recurseOnPlural : Bool

  Whether [±minimal] recurses on the plural region.

• recurseOnAdditive : Bool

  Whether [±additive] recurses (splitting paucal into paucal + greater paucal). Marked * on [±additive] in Table 3.

@[implicit_reducible]

instance Minimalist.Agreement.FeatureRecursion.instDecidableEqHarbourConfig : DecidableEq HarbourConfig

Equations

• Minimalist.Agreement.FeatureRecursion.instDecidableEqHarbourConfig = Minimalist.Agreement.FeatureRecursion.instDecidableEqHarbourConfig.decEq

def Minimalist.Agreement.FeatureRecursion.instDecidableEqHarbourConfig.decEq (x✝ x✝¹ : HarbourConfig) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.Agreement.FeatureRecursion.instReprHarbourConfig.repr : HarbourConfig → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Agreement.FeatureRecursion.instReprHarbourConfig : Repr HarbourConfig

Equations

• Minimalist.Agreement.FeatureRecursion.instReprHarbourConfig = { reprPrec := Minimalist.Agreement.FeatureRecursion.instReprHarbourConfig.repr }

def Minimalist.Agreement.FeatureRecursion.HarbourConfig.wellFormed (c : HarbourConfig) : Bool

Well-formedness: feature activation prerequisites.

1. [±minimal] recursion requires [±minimal] — the feature must be active for recursion to have a target region. When [±atomic] is also active, recursion targets the plural region (→ trial, greater plural); without [±atomic], it targets the augmented region (→ unit augmented).
2. [±additive] requires at least one base feature ([±atomic] or [±minimal]) to define the region it operates on. Without a base partition, [±additive] has no non-trivial region to split.
3. [±additive] recursion requires [±additive] to be active.

Equations

• c.wellFormed = ((!c.recurseOnPlural || c.hasMinimal) && (!c.hasAdditive || c.hasAtomic || c.hasMinimal) && (!c.recurseOnAdditive || c.hasAdditive))

def Minimalist.Agreement.FeatureRecursion.HarbourConfig.categories (c : HarbourConfig) : List Features.Number.Category

The number categories generated by a Harbour configuration.

Features are activated cumulatively, and each activation adds categories to the system:

• [±atomic] alone: singular vs non-singular (= plural)
• [±minimal] alone: minimal vs non-minimal (= augmented)
• [±atomic] + [±minimal]: singular, dual, plural (the base partition)
• • [±minimal] recursion (with [±atomic]): trial, greater plural
• • [±minimal] recursion (without [±atomic]): unit augmented
• • ±additive recursion: greater paucal

The list includes superordinate categories (e.g., .plural remains alongside .trial and .greaterPlural when recursion is active, and .augmented remains alongside .paucal and .plural). This is required for the lower-set property.

Equations

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

The main impossibility theorem. @cite{corbett-2000}'s implicational universals (trial → dual → plural → singular, greaterPaucal → paucal, etc.) are not stipulated constraints — they are a THEOREM of @cite{harbour-2016}'s feature geometry.

The categories generated by any well-formed Harbour configuration form
a **lower set** (`IsLowerSet`) in the markedness partial order. This
single theorem subsumes ALL implicational universals: if a category is
generated, everything it presupposes is also generated.

The proof is exhaustive: 4 Bool parameters × 8² category pairs,
verified by `decide` after case-splitting. 

theorem Minimalist.Agreement.FeatureRecursion.categories_lowerSet (c : HarbourConfig) (hw : c.wellFormed = true) (a b : Features.Number.Category) (hab : a ≤ b) (hb : c.categories.contains b = true) : c.categories.contains a = true

The categories generated by any well-formed Harbour configuration form a lower set in the markedness partial order: if b is generated and a ≤ b, then a is also generated.

theorem Minimalist.Agreement.FeatureRecursion.categories_isLowerSet (c : HarbourConfig) (hw : c.wellFormed = true) : IsLowerSet {cat : Features.Number.Category | c.categories.contains cat = true}

The lower set property stated via Mathlib's IsLowerSet.

theorem Minimalist.Agreement.FeatureRecursion.general_not_generated (c : HarbourConfig) : c.categories.contains Features.Number.Category.general = false

General number is outside the Harbour feature system entirely: no configuration generates it.

theorem Minimalist.Agreement.FeatureRecursion.sixteen_wellformed_configs : have allConfigs := List.flatMap (fun (a : Bool) => List.flatMap (fun (m : Bool) => List.flatMap (fun (d : Bool) => List.flatMap (fun (r : Bool) => List.map (fun (ra : Bool) => { hasAtomic := a, hasMinimal := m, hasAdditive := d, recurseOnPlural := r, recurseOnAdditive := ra }) [false, true]) [false, true]) [false, true]) [false, true]) [false, true]; (List.filter HarbourConfig.wellFormed allConfigs).length = 16

Exactly 16 of the 32 logically possible configurations are well-formed. (Previously 13 when [±minimal] recursion required [±atomic]; relaxing to require only [±minimal] adds 3 configs: {±minimal*}, {±additive, ±minimal*}, {±additive*, ±minimal*}.)

Lattice-Grounded Feature Predicates

@cite{harbour-2014}

The three number features are predicates on a join-semilattice of individuals:

• (20) [±atomic] = λx. (¬)atom(x) — IS Mereology.Atom
• (21) [±minimal] = λP λx. (¬)∃y(P(y) ∧ y ⊏ x), presupposing P(x)
• (10) [±additive] = λP λx. (¬)∀y(Q(y) → Q(x ⊔ y)), presupposing Q(x)

[+additive] IS cumulativity restricted to a subregion: the set of [+additive] elements is CUM. This connects number to aspect/telicity (@cite{harbour-2014} §4.4): mass nouns satisfy [+additive], telic predicates satisfy [−additive].

def Minimalist.Agreement.FeatureRecursion.minimalInPred {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (x : D) : Prop

[+minimal] in region P: x is a minimal element of P under ≤. @cite{harbour-2014} (21): x has no proper P-part below it.

Equations

• Minimalist.Agreement.FeatureRecursion.minimalInPred P x = (P x ∧ ∀ (y : D), P y → y ≤ x → y = x)

def Minimalist.Agreement.FeatureRecursion.additiveInPred {D : Type u_1} [SemilatticeSup D] (Q : D → Prop) (x : D) : Prop

[+additive] in region Q: x is join-complete in Q. @cite{harbour-2014} (10): ∀y ∈ Q, x ⊔ y ∈ Q.

Equations

• Minimalist.Agreement.FeatureRecursion.additiveInPred Q x = (Q x ∧ ∀ (y : D), Q y → Q (x ⊔ y))

theorem Minimalist.Agreement.FeatureRecursion.additive_region_cum {D : Type u_1} [SemilatticeSup D] (Q : D → Prop) (x y : D) (hx : additiveInPred Q x) (hy : additiveInPred Q y) : additiveInPred Q (x ⊔ y)

The [+additive] region is CUM: joining two [+additive] elements gives another [+additive] element.

This is the formal link between number and aspect/telicity (@cite{harbour-2014} §4.4): mass nouns are [+additive] (cumulative), telic predicates are [−additive] (quantized), and the features governing both are the same.

theorem Minimalist.Agreement.FeatureRecursion.atoms_all_minimal {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (hAllAtoms : ∀ (x : D), P x → Mereology.Atom x) (x : D) (hPx : P x) : minimalInPred P x

Atoms are trivially minimal in any region containing them. Grounding of [+atomic] → [+minimal] in lattice theory: atoms have no proper parts, so they are minimal everywhere.

Consequence for recursion (@cite{harbour-2014} §4.2): [±minimal] applied to a region of atoms selects ALL of them ([+minimal]) or NONE ([−minimal] = ∅). Feature recursion on an all-atom region adds no information, which is why [±atomic] cannot undergo meaningful feature recursion.

theorem Minimalist.Agreement.FeatureRecursion.atoms_no_nonminimal {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (hAllAtoms : ∀ (x : D), P x → Mereology.Atom x) (x : D) : ¬(P x ∧ ¬minimalInPred P x)

The [−minimal] complement of an all-atom region is empty: no atom fails to be minimal. This is the formal reason [±atomic] cannot recurse (@cite{harbour-2014} §4.2).

theorem Minimalist.Agreement.FeatureRecursion.additive_subregion_is_cum {D : Type u_1} [SemilatticeSup D] (Q : D → Prop) : Mereology.CUM fun (x : D) => additiveInPred Q x

The [+additive] subregion is cumulative (Mereology.CUM). This is the formal content of @cite{harbour-2014} §4.4: [+additive] IS cumulativity restricted to a subregion. The number-aspect connection runs through exactly this identity: mass nouns are [+additive] (CUM), telic predicates are [−additive] (not CUM).

Surface Categories and Typological Predictions

@cite{harbour-2014} Table 3

categories includes superordinate categories that have been split by recursion or [±additive]. For example, {±minimal*, ±atomic} generates [sg, du, pl, trial, greaterPl], but the surface system is sg/du/trial/greaterPl (4 values) — plural has been split into trial + greater plural and is no longer a distinct morphological category.

surfaceCategories removes these split superordinates to match the observable number distinctions. The resulting counts match @cite{harbour-2014} Table 3 exactly.

The parameter space — feature activation ({±atomic}, {±minimal}, {±additive}) and feature recursion (* = reapplication) — generates a typology of number systems. Each parametric setting predicts a specific inventory of number values matching @cite{corbett-2000}, @cite{cysouw-2009}.

Key predictions:

• Trial and unit augmented are the highest exact numbers attainable without numerals (bounded by the axiom of extension, (27)).
• A language may have at most two approximative numbers (e.g. paucal + greater paucal, from [±additive] + recursion).
• Three unattested parameter settings ({±additive, ±minimal*}, {±additive*, ±minimal}, {±additive*, ±minimal*, ±atomic}) have plausible explanations for their absence.

def Minimalist.Agreement.FeatureRecursion.HarbourConfig.surfaceCategories (c : HarbourConfig) : List Features.Number.Category

Surface categories: the morphologically distinct number values.

Unlike categories (which includes superordinates for the lower-set property), this removes categories that have been split into subcategories by recursion or [±additive]:

• Plural is removed when [±minimal] recursion (with [±atomic]) splits it into trial + greater plural. The surface "plural" IS greater plural (groups of 4+).
• Augmented is removed when [±additive] (without [±atomic]) splits it into paucal + plural. The surface system is minimal/paucal/plural.

The resulting counts match @cite{harbour-2014} Table 3 exactly.

Equations

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

structure Minimalist.Agreement.FeatureRecursion.Harbour2014Entry : Type

@cite{harbour-2014} Table 3 entry: a HarbourConfig connected to the predicted system size and an example language.

• config : HarbourConfig

  The feature activation and recursion parameters.

• numValues : ℕ

  Number of distinct surface values in the system.

• language : String

  Example language.

@[implicit_reducible]

instance Minimalist.Agreement.FeatureRecursion.instReprHarbour2014Entry : Repr Harbour2014Entry

Equations

• Minimalist.Agreement.FeatureRecursion.instReprHarbour2014Entry = { reprPrec := Minimalist.Agreement.FeatureRecursion.instReprHarbour2014Entry.repr }

def Minimalist.Agreement.FeatureRecursion.instReprHarbour2014Entry.repr : Harbour2014Entry → ℕ → Std.Format

Equations

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

def Minimalist.Agreement.FeatureRecursion.harbour2014Table3 : List Harbour2014Entry

@cite{harbour-2014} Table 3: typology of number systems. 15 attested parametric settings (12 distinct configs) generating 0–5 value systems. Subscripted entries share the same config but exemplify different languages.

Equations

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

theorem Minimalist.Agreement.FeatureRecursion.table3_all_wellformed : (harbour2014Table3.all fun (e : Harbour2014Entry) => e.config.wellFormed) = true

All Table 3 configs are well-formed.

theorem Minimalist.Agreement.FeatureRecursion.table3_counts_match : (harbour2014Table3.all fun (e : Harbour2014Entry) => decide (e.config.surfaceCategories.length = e.numValues)) = true

Surface category counts match Table 3's predictions.

This is the key verification theorem: the generative mechanism (HarbourConfig → categories → surfaceCategories) produces exactly the number of morphologically distinct values predicted by @cite{harbour-2014} Table 3 for each parametric setting.

theorem Minimalist.Agreement.FeatureRecursion.max_system_size : (harbour2014Table3.all fun (e : Harbour2014Entry) => decide (e.numValues ≤ 5)) = true

No system has more than 5 surface values (Table 3).

theorem Minimalist.Agreement.FeatureRecursion.min_system_size : (harbour2014Table3.all fun (e : Harbour2014Entry) => decide (e.numValues = 0 ∨ e.numValues ≥ 2)) = true

All nonempty systems have at least 2 values: number is inherently contrastive (@cite{harbour-2014} §1).

Convexity Condition

@cite{harbour-2014} §4.5, (32)

The convexity condition explains why {±additive} alone is NOT a legitimate number system. A lattice region L is convex iff for any a, b ∈ L and a ≤ c ≤ b, c ∈ L (no "gaps" — @cite{harbour-2014} (33)).

For first and second person, [±additive] applied without [±atomic] or [±minimal] produces a nonconvex cut: between the [+additive] first-person atom (the speaker, closed under join with itself) and any [+additive] first-person plural, there must lie a [−additive] first-person paucal. This nonconvex cut violates the general requirement that basic meanings be convex (@cite{gaerdenfors-2004}).

The formalization connects to Mereology.convexClosure (Core/Mereology.lean §13): a nonconvex region under convexClosure strictly expands, witnessing elements that "should" be in the region but aren't.

def Minimalist.Agreement.FeatureRecursion.isConvex {D : Type u_1} [PartialOrder D] (L : Set D) : Prop

A region is convex in a lattice: between any two members, all intermediaries are also members. @cite{harbour-2014} (33).

Equations

• Minimalist.Agreement.FeatureRecursion.isConvex L = ∀ (a b c : D), a ∈ L → b ∈ L → a ≤ c → c ≤ b → c ∈ L

theorem Minimalist.Agreement.FeatureRecursion.convex_iff_closure_eq {D : Type u_1} [PartialOrder D] (L : Set D) : isConvex L ↔ Mereology.convexClosure L = L

Convex regions are fixed points of convex closure: Conv(L) = L.

Axiom of Extension

@cite{harbour-2014} §4.2, (27)

The axiom of extension ({a, a} = {a}) from set theory caps the complexity of number feature specifications. Since feature bundles are SETS, repeating a feature value has no effect: [+F −F] is the maximum specification that a single feature F can achieve. This means [+F −F] = {+F, −F}, and adding more copies ([+F −F −F]) just gives {+F, −F} again.

Consequence: trial and unit augmented are the highest exact numbers attainable without numerals. A "quadral" would require [+minimal −minimal −minimal −atomic] = {+minimal, −minimal, −atomic} = [+minimal −minimal −atomic] = trial. The axiom prevents going beyond trial.

This is formalized as a theorem about Finset: the deduplication of a feature value list has at most 2 elements for any single feature.

theorem Minimalist.Agreement.FeatureRecursion.axiom_of_extension_binary : Finset.univ.card = 2

The axiom of extension limits a single binary feature to at most 2 distinct values: {+F} and/or {−F}. Repeating a value adds nothing.

Stated via Fintype.card Bool = 2: any binary feature has exactly 2 possible values, so no specification of a single feature can produce more than 2 distinctions. This is why trial (3 atoms) is the maximum exact number: it requires [+minimal −minimal −atomic], which uses 2 features × 2 values = at most 4 distinctions (but [+atomic] and [+minimal] overlap, giving only 3).