Feature Recursion

[Har14a] [Har16a]

[Har14a] §4, [Har16a] 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 values form a lower set in the markedness partial order on Number (Number.instPartialOrder, Features/Number/Basic.lean): if a marked value is generated, all less-marked values it presupposes are also generated (§ 8).

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

structure Minimalist.Phi.Recursion.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 : Number.Features

  The base number features defining this region.

• base_wf : self.base.WellFormed

  The base features must be well-formed.

• base_nonatomic : self.base.isAtomic = false

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

def Minimalist.Phi.Recursion.instDecidableEqRegion.decEq (x✝ x✝¹ : Region) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.Phi.Recursion.instDecidableEqRegion : DecidableEq Region

Equations

• Minimalist.Phi.Recursion.instDecidableEqRegion = Minimalist.Phi.Recursion.instDecidableEqRegion.decEq

def Minimalist.Phi.Recursion.pluralRegion : Region

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

Equations

• Minimalist.Phi.Recursion.pluralRegion = { base := Number.pluralF, base_wf := Minimalist.Phi.Recursion.pluralRegion._proof_1, base_nonatomic := Minimalist.Phi.Recursion.pluralRegion._proof_2 }

def Minimalist.Phi.Recursion.dualRegion : Region

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

Equations

• Minimalist.Phi.Recursion.dualRegion = { base := Number.dualF, base_wf := Minimalist.Phi.Recursion.dualRegion._proof_1, base_nonatomic := Minimalist.Phi.Recursion.dualRegion._proof_2 }

structure Minimalist.Phi.Recursion.RecursiveNumber : Type

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

[Har16a] 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.

def Minimalist.Phi.Recursion.instDecidableEqRecursiveNumber.decEq (x✝ x✝¹ : RecursiveNumber) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.Phi.Recursion.instDecidableEqRecursiveNumber : DecidableEq RecursiveNumber

Equations

• Minimalist.Phi.Recursion.instDecidableEqRecursiveNumber = Minimalist.Phi.Recursion.instDecidableEqRecursiveNumber.decEq

def Minimalist.Phi.Recursion.trial : RecursiveNumber

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

Equations

• Minimalist.Phi.Recursion.trial = { region := Minimalist.Phi.Recursion.pluralRegion, isMinimalInRegion := true }

def Minimalist.Phi.Recursion.greaterPlural : RecursiveNumber

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

Equations

• Minimalist.Phi.Recursion.greaterPlural = { region := Minimalist.Phi.Recursion.pluralRegion, isMinimalInRegion := false }

def Minimalist.Phi.Recursion.unitAugmented : RecursiveNumber

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

Equations

• Minimalist.Phi.Recursion.unitAugmented = { region := Minimalist.Phi.Recursion.dualRegion, isMinimalInRegion := true }

def Minimalist.Phi.Recursion.augmented : RecursiveNumber

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

Equations

• Minimalist.Phi.Recursion.augmented = { region := Minimalist.Phi.Recursion.dualRegion, isMinimalInRegion := false }

def Minimalist.Phi.Recursion.RecursiveNumber.toNumber (r : RecursiveNumber) : Number

Map recursive features to [Cor00]'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.Phi.Recursion.trial_toNumber : trial.toNumber = Number.trial

theorem Minimalist.Phi.Recursion.greaterPlural_toNumber : greaterPlural.toNumber = Number.greaterPlural

theorem Minimalist.Phi.Recursion.unitAugmented_toNumber : unitAugmented.toNumber = Number.unitAugmented

theorem Minimalist.Phi.Recursion.augmented_toNumber : augmented.toNumber = Number.augmented

theorem Minimalist.Phi.Recursion.no_singular_recursion : ¬∃ (r : Region), r.base = 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.Phi.Recursion.recursion_yields_two (reg : Region) : { region := reg, isMinimalInRegion := true }.toNumber ≠ { region := reg, isMinimalInRegion := false }.toNumber

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

theorem Minimalist.Phi.Recursion.trial_presupposes_plural : trial.region.base = 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.Phi.Recursion.unitAug_presupposes_dual : unitAugmented.region.base = Number.dualF

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

theorem Minimalist.Phi.Recursion.recursion_presupposes_base (r : RecursiveNumber) : r.region.base.WellFormed

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

theorem Minimalist.Phi.Recursion.recursion_base_categories : trial.region.base.toNumber = some Number.plural ∧ unitAugmented.region.base.toNumber = some Number.dual

Base regions of recursive numbers map to Corbett values.

theorem Minimalist.Phi.Recursion.only_two_regions (r : Region) : r.base = Number.dualF ∨ r.base = 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.

structure Minimalist.Phi.Recursion.HarbourConfig : Type

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

[Har14a]: 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.

def Minimalist.Phi.Recursion.instDecidableEqHarbourConfig.decEq (x✝ x✝¹ : HarbourConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.Phi.Recursion.instDecidableEqHarbourConfig : DecidableEq HarbourConfig

Equations

• Minimalist.Phi.Recursion.instDecidableEqHarbourConfig = Minimalist.Phi.Recursion.instDecidableEqHarbourConfig.decEq

def Minimalist.Phi.Recursion.instReprHarbourConfig.repr : HarbourConfig → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Phi.Recursion.instReprHarbourConfig : Repr HarbourConfig

Equations

• Minimalist.Phi.Recursion.instReprHarbourConfig = { reprPrec := Minimalist.Phi.Recursion.instReprHarbourConfig.repr }

@[implicit_reducible]

instance Minimalist.Phi.Recursion.instFintypeHarbourConfig : Fintype HarbourConfig

Equations

• Minimalist.Phi.Recursion.instFintypeHarbourConfig = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × (_ : Bool) × (_ : Bool) × Bool) Minimalist.Phi.Recursion.HarbourConfig.proxyTypeEquiv

def Minimalist.Phi.Recursion.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.Phi.Recursion.HarbourConfig.categories (c : HarbourConfig) : List Number

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 (the residue remains plural)
• • [±minimal] recursion (without [±atomic]): unit augmented
• • ±additive recursion: greater paucal

Recursion on the plural region (with [±atomic]) adds .trial; the residue keeps the label .plural — [Har14a] Table 3 lists Larike as singular, dual, trial, plural (greater plural is reserved for ±additive-derived values). .augmented remains alongside .paucal and .plural when ±additive splits it; superordinates are required for the lower-set property.

Equations

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

The main impossibility theorem. [Cor00]'s implicational universals (trial → dual → plural → singular, greaterPaucal → paucal, etc.) are not stipulated constraints — they are a THEOREM of [Har16a]'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.Phi.Recursion.categories_lowerSet (c : HarbourConfig) (hw : c.wellFormed = true) (a b : Number) (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.Phi.Recursion.categories_isLowerSet (c : HarbourConfig) (hw : c.wellFormed = true) : IsLowerSet {cat : Number | c.categories.contains cat = true}

The lower set property stated via Mathlib's IsLowerSet.

theorem Minimalist.Phi.Recursion.general_not_generated (c : HarbourConfig) : c.categories.contains Number.general = false

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

theorem Minimalist.Phi.Recursion.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*}.)

The lattice-grounded feature predicates — [Har14a]'s (20) [±atomic], (21) [±minimal], (10) [±additive] as predicates over a join-semilattice, with the CUM identity for the number–aspect nexus — graduated to Features/Number/Interp.lean (Number.minimalIn, Number.additiveIn, Number.additive_subregion_is_cum).

Surface Categories and Typological Predictions

[Har14a] 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 [Har14a] 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 [Cor00], [Cys09].

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.Phi.Recursion.HarbourConfig.surfaceCategories (c : HarbourConfig) : List Number

Surface categories: the morphologically distinct number values.

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

• Augmented is removed when [±additive] (without [±atomic]) splits it into paucal + plural. The surface system is minimal/paucal/plural (Mebengokre, [Har14a] Table 3).

The resulting label sets and counts match [Har14a] Table 3.

Equations

• c.surfaceCategories = List.filter (fun (cat : Number) => !(c.hasAdditive && !c.hasAtomic && c.hasMinimal && cat == Number.augmented)) c.categories

def Minimalist.Phi.Recursion.HarbourConfig.toSystem (c : HarbourConfig) (name : String := "") : Number.System

The Number.System a configuration generates: surface values as the inventory. The empty configuration leaves Number⁰ featureless — general number ([Har14a] (24); Pirahã, Classical Chinese).

Equations

• c.toSystem name = { name := name, values := c.surfaceCategories, hasGeneral := c.surfaceCategories.isEmpty }

structure Minimalist.Phi.Recursion.Harbour2014Entry : Type

[Har14a] 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.

def Minimalist.Phi.Recursion.instReprHarbour2014Entry.repr : Harbour2014Entry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Phi.Recursion.instReprHarbour2014Entry : Repr Harbour2014Entry

Equations

• Minimalist.Phi.Recursion.instReprHarbour2014Entry = { reprPrec := Minimalist.Phi.Recursion.instReprHarbour2014Entry.repr }

def Minimalist.Phi.Recursion.harbour2014Table3 : List Harbour2014Entry

[Har14a] 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.Phi.Recursion.table3_all_wellformed : (harbour2014Table3.all fun (e : Harbour2014Entry) => e.config.wellFormed) = true

All Table 3 configs are well-formed.

theorem Minimalist.Phi.Recursion.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 [Har14a] Table 3 for each parametric setting.

theorem Minimalist.Phi.Recursion.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.Phi.Recursion.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 ([Har14a] §1).

Convexity Condition

[Har14a] §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" — [Har14a] (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 ([gaerdenfors-2004]).

Convexity here is mathlib's Set.OrdConnected: a region is convex iff it is a fixed point of ordConnectedHull (ordConnectedHull_eq_self) — the same predicate that states [Gri18]'s no-discontinuous-category condition on countability classes (Studies/Grimm2018.lean), so Harbour's and Grimm's convexity requirements are the same predicate.

Axiom of Extension

[Har14a] §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.Phi.Recursion.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).