Number — the Harbour feature decomposition and its lattice grounding

[Har14a] [Lin83]

Binary feature decomposition of the number values ([Har14a]):

• [±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]), but with an asymmetry worth marking: number's filter is a theorem of the lattice semantics (the grounding sections below — atoms are minimal; [Har16a] ch. 9.5 notes the odd cooccurrence is contradictory for ±atomic "by the logic of the system"), whereas person's filter is a descriptive convention the same chapter rejects. See Features/ContainmentPair.lean.

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; Syntax/Minimalist/Phi/Recursion.lean). The approximative numbers require the additional feature [±additive] (§ on the additive feature below).

Main declarations

• Number.Features — the [±atomic, ±minimal] bundle, with the containment filter Features.WellFormed and the ContainmentPairLike presentation unifying it with the person skeleton (featuresEquiv : Features ≃ ContainmentPair).
• Number.latticeToFeatures — classify a lattice element as singular/dual/plural by its position.
• Number.isJoinCompleteIn / Number.isRegionJoinComplete — the [±additive] feature ([Har14a]): join-completeness within a region.
• Number.dualPredOnLattice — ⟦DUAL⟧ as a predicate modifier ([JBG+25]), grounded in the feature decomposition by dualPredOnLattice_eq_via_features.

The feature bundle

structure Number.Features : Type

Bivalent 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 cut by the containment filter (WellFormed): an atom is necessarily a minimal element of any lattice region (a theorem of the semantics — §8).

• isAtomic : Bool

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

• isMinimal : Bool

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

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

Equations

• Number.instDecidableEqFeatures.decEq { isAtomic := a, isMinimal := a_1 } { isAtomic := b, isMinimal := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Number.instDecidableEqFeatures : DecidableEq Features

Equations

• Number.instDecidableEqFeatures = Number.instDecidableEqFeatures.decEq

@[implicit_reducible]

instance Number.instReprFeatures : Repr Features

Equations

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

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

Equations

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

@[implicit_reducible]

instance Number.instFintypeFeatures : Fintype Features

Equations

• Number.instFintypeFeatures = Fintype.ofEquiv ((_ : Bool) × Bool) Number.Features.proxyTypeEquiv

def Number.singularF : Features

Singular features: [+atomic, +minimal].

Equations

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

def Number.dualF : Features

Dual features: [−atomic, +minimal].

Equations

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

def Number.pluralF : Features

Plural features: [−atomic, −minimal].

Equations

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

Features ↔ value bridge

def Number.Features.toNumber : Features → Option Number

Map a feature bundle to the number value it realizes.

The three well-formed base bundles map to three of [Cor00]'s values. 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 }.toNumber = some Number.singular
• { isAtomic := false, isMinimal := true }.toNumber = some Number.dual
• { isAtomic := false, isMinimal := false }.toNumber = some Number.plural
• { isAtomic := true, isMinimal := false }.toNumber = none

def Number.Features.ofNumber : Number → Option Features

Map a number value to its base feature bundle (partial).

Only the three values 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

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

The ContainmentPairLike presentation

def Number.featuresEquiv : Features ≃ Features.ContainmentPair

The [±atomic, ±minimal] decomposition is carrier-equivalent to the containment pair: outer = minimal, inner = atomic. The containment [+atomic] → [+minimal] maps to [+inner] → [+outer], unifying the structure with person features — one edge of the φ-feature iso-web (phiKernelEquiv, Studies/Harbour2016.lean).

Equations

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

@[implicit_reducible]

instance Number.instContainmentPairLikeFeatures : Features.ContainmentPairLike Features

Equations

• Number.instContainmentPairLikeFeatures = Features.ContainmentPairLike.ofEquiv Number.featuresEquiv

@[simp]

theorem Number.singular_is_maximal : Features.ContainmentPairLike.toPair singularF = Features.ContainmentPair.maximal

The three canonical number values land on the three well-formed cells.

@[simp]

theorem Number.dual_is_intermediate : Features.ContainmentPairLike.toPair dualF = Features.ContainmentPair.intermediate

@[simp]

theorem Number.plural_is_minimal : Features.ContainmentPairLike.toPair pluralF = Features.ContainmentPair.minimal

@[reducible, inline]

abbrev Number.Features.WellFormed (nf : Features) : Prop

Well-formedness: [+atomic] → [+minimal] — an atom is necessarily a minimal element. Inherited from ContainmentPair.WellFormed through the presentation; for number this filter is a theorem of the lattice semantics (§8), not a stipulation.

Equations

• nf.WellFormed = Features.ContainmentPairLike.WellFormed nf

theorem Number.no_fourth_base_number (a b c d : Features) : a.WellFormed → b.WellFormed → c.WellFormed → d.WellFormed → a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → False

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

Verification

@[simp]

theorem Number.singular_wellFormed : singularF.WellFormed

@[simp]

theorem Number.dual_wellFormed : dualF.WellFormed

@[simp]

theorem Number.plural_wellFormed : pluralF.WellFormed

theorem Number.illFormed_only : ¬{ isAtomic := true, isMinimal := false }.WellFormed

The filtered combination [+atomic, −minimal] is the only one that violates containment.

theorem Number.card_wellFormed : Fintype.card { nf : Features // nf.WellFormed } = 3

Exactly 3 well-formed feature combinations (= 3 base numbers) — the carrier count of the containment chain (ContainmentPair.card_wellFormed).

theorem Number.roundtrip_ofNumber_toNumber : ([singularF, dualF, pluralF].all fun (f : Features) => f.toNumber.bind Features.ofNumber == some f) = true

Round-trip: ofNumber ∘ toNumber = some for all well-formed features.

theorem Number.illFormed_toNumber_none : { isAtomic := true, isMinimal := false }.toNumber = none

toNumber returns none for the filtered bundle.

theorem Number.atomic_implies_minimal (f : Features) : f.WellFormed → 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.

[Lin83] models the domain of individuals as a join-semilattice ⟨D, ⊔⟩. Number categories correspond to the lattice predicates of Features/Number/Interp.lean:

• singular = domain-minimal elements (the atoms),
• dual = minimal non-atoms (minimalNonAtomIn),
• plural = the rest.

The containment [+atomic] → [+minimal] is a theorem of lattice theory (Number.singular_subset_minimal), not a stipulation. On finite carriers the predicates are decidable (instances in Interp.lean), so every concrete classification below is kernel-checked by decide: domains are Finset (Fin n) powerset lattices with join = union. Minimality is domain-relative (minimalIn (· ∈ domain)), agreeing with the global Mereology.Atom when the domain is downward closed in D⁺.

def Number.minimalNonAtomIn {D : Type u_1} [SemilatticeSup D] (domain : D → Prop) : D → Prop

The minimal non-atoms of domain: minimal among its non-minimal elements — the dual's region ([Har14a] [−atomic, +minimal]).

Equations

• Number.minimalNonAtomIn domain = Number.minimalIn fun (y : D) => domain y ∧ ¬Number.minimalIn domain y

theorem Number.not_minimalIn_of_minimalNonAtomIn {D : Type u_1} [SemilatticeSup D] {domain : D → Prop} {x : D} (h : minimalNonAtomIn domain x) : ¬minimalIn domain x

A minimal non-atom is not domain-minimal.

def Number.RegionAdditive {D : Type u_1} [SemilatticeSup D] (Q : D → Prop) : Prop

A region is join-complete: every element is [+additive] in it — Mereology.CUM restricted to the region ([Har14a] (11), complement completeness).

Equations

• Number.RegionAdditive Q = ∀ (x : D), Q x → Number.additiveIn Q x

@[implicit_reducible]

instance Number.instDecidableMinimalNonAtomInOfDecidablePred {D : Type u_1} [SemilatticeSup D] [Fintype D] [DecidableEq D] [DecidableLE D] {domain : D → Prop} [DecidablePred domain] (x : D) : Decidable (minimalNonAtomIn domain x)

Equations

• Number.instDecidableMinimalNonAtomInOfDecidablePred x = id inferInstance

@[implicit_reducible]

instance Number.instDecidableRegionAdditiveOfDecidablePred {D : Type u_1} [SemilatticeSup D] [Fintype D] {Q : D → Prop} [DecidablePred Q] : Decidable (RegionAdditive Q)

Equations

• Number.instDecidableRegionAdditiveOfDecidablePred = id inferInstance

def Number.latticeToFeatures {D : Type u_1} [SemilatticeSup D] [Fintype D] [DecidableEq D] [DecidableLE D] (domain : D → Prop) [DecidablePred domain] (x : D) : Features

Classify a lattice element by position: domain-minimal → singular, minimal non-atom → dual, otherwise → plural.

Equations

• Number.latticeToFeatures domain x = if Number.minimalIn domain x then Number.singularF else if Number.minimalNonAtomIn domain x then Number.dualF else Number.pluralF

theorem Number.latticeToFeatures_wellFormed {D : Type u_1} [SemilatticeSup D] [Fintype D] [DecidableEq D] [DecidableLE D] (domain : D → Prop) [DecidablePred domain] (x : D) : (latticeToFeatures domain x).WellFormed

Every branch of latticeToFeatures produces a well-formed bundle: [+atomic] → [+minimal] holds by construction.

Powerset lattice examples

theorem Number.ex_atom_is_singular : latticeToFeatures Number.ps2✝ {0} = singularF

theorem Number.ex_atom_is_singular' : latticeToFeatures Number.ps2✝ {1} = singularF

theorem Number.ex_pair_is_dual : latticeToFeatures Number.ps2✝ {0, 1} = dualF

def Number.ps3 (s : Finset (Fin 3)) : Prop

The 3-atom powerset domain: nonempty subsets of Fin 3. Pairs are minimal non-atoms → dual; the triple is non-minimal → plural (the 2-atom domain has a single non-atom and cannot show the split).

Equations

• Number.ps3 s = s.Nonempty

@[implicit_reducible]

instance Number.instDecidablePredFinsetFinOfNatNatPs3 : DecidablePred ps3

Equations

• Number.instDecidablePredFinsetFinOfNatNatPs3 s = Number.instDecidablePredFinsetFinOfNatNatPs3._aux_1 s

theorem Number.ps3_atom_is_singular : latticeToFeatures ps3 {0} = singularF

theorem Number.ps3_pair_is_dual : latticeToFeatures ps3 {0, 1} = dualF

theorem Number.ps3_pair_is_dual' : latticeToFeatures ps3 {0, 2} = dualF

theorem Number.ps3_triple_is_plural : latticeToFeatures ps3 {0, 1, 2} = pluralF

The additive feature

[Har14a]

[±additive] is the third number feature, characterizing join-completeness within a lattice region (Number.additiveIn). 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 (RegionAdditive).
• Fungibility ((12)): the boundary must be permutation-invariant (horizontal cuts by cardinality, not identity of atoms) — which is why the regions below are defined by Finset.card.

Connection to CUM: [+additive] IS cumulativity restricted to a subregion (Number.additive_subregion_is_cum). The link between number and aspect/telicity ([Har14a] §4.4) runs through exactly this connection: mass nouns satisfy [+additive] (cumulative), count nouns [−additive] (quantized).

theorem Number.ps3_nonAtoms_joinComplete : RegionAdditive fun (s : Finset (Fin 3)) => 2 ≤ s.card

With 3 atoms the entire non-atomic region is join-complete: [±additive] is vacuous — a paucal/plural split needs a richer lattice.

theorem Number.ps5_paucal_not_joinComplete : ¬RegionAdditive fun (s : Finset (Fin 5)) => 2 ≤ s.card ∧ s.card ≤ 3

The "paucal" region of the 5-atom powerset (2–3 atoms) is NOT join-complete: {0,1} ⊔ {2,3} has four atoms and escapes the region.

theorem Number.ps5_plural_joinComplete : RegionAdditive fun (s : Finset (Fin 5)) => 4 ≤ s.card

The "plural" region (≥ 4 atoms) IS join-complete: joining two large sums stays large. Satisfies complement completeness ([Har14a] (11)).

theorem Number.ps5_additive_asymmetry : (RegionAdditive fun (s : Finset (Fin 5)) => 4 ≤ s.card) ∧ ¬RegionAdditive fun (s : Finset (Fin 5)) => 2 ≤ s.card ∧ s.card ≤ 3

The paucal/plural asymmetry: the [+additive] region is join-complete, the [−additive] region is not — the formal content of the approximative number distinction ([Har14a] §3).

DUAL as predicate modifier

[JBG+25]

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" (minimalNonAtomIn). The bridge is therefore a one-line composition: restrict 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 Studies/JereticEtAl2025.lean.

def Number.dualPredOnLattice {D : Type u_1} [SemilatticeSup D] (domain P : D → Prop) (x : D) : Prop

⟦DUAL⟧ as a predicate modifier on a join-semilattice domain ([JBG+25] eq 39): P x, and x has exactly two atomic parts — i.e. is a minimal non-atom of the domain.

Equations

• Number.dualPredOnLattice domain P x = (P x ∧ Number.minimalNonAtomIn domain x)

@[implicit_reducible]

instance Number.instDecidableDualPredOnLatticeOfFintypeOfDecidableEqOfDecidableLEOfDecidablePred {D : Type u_1} [SemilatticeSup D] {domain P : D → Prop} [Fintype D] [DecidableEq D] [DecidableLE D] [DecidablePred domain] [DecidablePred P] (x : D) : Decidable (dualPredOnLattice domain P x)

Equations

• Number.instDecidableDualPredOnLatticeOfFintypeOfDecidableEqOfDecidableLEOfDecidablePred x = Number.instDecidableDualPredOnLatticeOfFintypeOfDecidableEqOfDecidableLEOfDecidablePred._aux_1 x

theorem Number.dualPredOnLattice_refines {D : Type u_1} [SemilatticeSup D] {domain P : D → Prop} {x : D} (h : dualPredOnLattice domain P x) : P x

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

theorem Number.dualPredOnLattice_eq_via_features {D : Type u_1} [SemilatticeSup D] [Fintype D] [DecidableEq D] [DecidableLE D] (domain : D → Prop) [DecidablePred domain] (P : D → Prop) (x : D) : dualPredOnLattice domain P x ↔ P x ∧ latticeToFeatures domain x = dualF

Bridge: the dual lattice predicate IS the condition latticeToFeatures uses to assign dualF, so dualPredOnLattice factors as P x ∧ latticeToFeatures … x = dualF. DUAL is not a separate primitive but the same condition that classifies a lattice element as [−atomic, +minimal] ([JBG+25] eq 39).

theorem Number.ps3_dual_pairs_satisfy : dualPredOnLattice ps3 (fun (x : Finset (Fin 3)) => True) {0, 1} ∧ dualPredOnLattice ps3 (fun (x : Finset (Fin 3)) => True) {0, 2} ∧ dualPredOnLattice ps3 (fun (x : Finset (Fin 3)) => True) {1, 2}

On the 3-atom powerset, the dual reading of the trivial property selects the three pairs and excludes the triple.

theorem Number.ps3_dual_triple_excluded : ¬dualPredOnLattice ps3 (fun (x : Finset (Fin 3)) => True) {0, 1, 2}

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