The feature decomposition of number

Harbour decomposes the three basic number values into two features, [±atomic] and [±minimal]. A bundle is the set of its positive features, and it passes the containment filter when they form a lower set of the chain minimal < atomic, so the three values are the chain's initial segments. For number the filter follows from the semantics: an atom is minimal in every region excluding the null individual (Number.singular_subset_minimal), so [+atomic, −minimal] corresponds to no number, as Harbour observes. Lattice elements are classified by the regions of Harbour's features (Semantics/Plurality/Number.lean).

Main definitions

• Number.Feature, Number.Features: the two features and their bundles, with Features.toNumber and Features.ofNumber relating bundles to Number.
• Number.latticeToFeatures: the bundle a lattice element realizes in a region, singular on its atoms, dual on its minimal non-atoms, plural otherwise.
• Number.dualPredOnLattice: the dual as a predicate modifier.

Main results

• Number.card_wellFormed: exactly three bundles pass the containment filter.
• Number.toNumber_isSome_iff, Number.ofNumber_toNumber, Number.toNumber_ofNumber: bundles and values correspond on those cells.
• Number.latticeToFeatures_wellFormed: classification never produces the filtered cell.
• Number.dualPredOnLattice_iff: the dual predicate modifier is the restriction to elements classified dualF.

Implementation notes

Harbour argues that the features are bivalent, a privative encoding collapsing values such as unit augmented and minimal; a bundle here is the set of positive values of a bivalent valuation, the negative values being its complement. The examples use the powerset lattice Finset (Fin n) on its nonempty subsets, whose atoms are the singletons.

References

• [Har14a], §5.1, p. 213
• [Har16a], §9.5, pp. 222–223
• [Lin83]
• [JBG+25], §4.2.1, §8

The feature bundle

inductive Number.Feature : Type

Harbour's two number features, atomicity depending on minimality.

• minimal : Feature

  [minimal] holds of a referent minimal in its region.

• atomic : Feature

  [atomic] holds of an atom.

@[instance_reducible]

instance Number.instDecidableEqFeature : DecidableEq Feature

Equations

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

def Number.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

• Number.instReprFeature.repr Number.Feature.minimal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.Feature.minimal")).group prec✝
• Number.instReprFeature.repr Number.Feature.atomic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.Feature.atomic")).group prec✝

@[instance_reducible]

instance Number.instReprFeature : Repr Feature

Equations

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

@[instance_reducible]

instance Number.instFintypeFeature : Fintype Feature

Equations

• Number.instFintypeFeature = { elems := { val := ↑Number.Feature.enumList, nodup := Number.Feature.enumList_nodup }, complete := Number.instFintypeFeature._proof_1 }

def Number.Feature.rank : Feature → Fin 2

Feature.rank places minimal below atomic on the dependency chain.

Equations

• Number.Feature.minimal.rank = 0
• Number.Feature.atomic.rank = 1

@[instance_reducible]

instance Number.instLinearOrderFeature : LinearOrder Feature

Equations

• Number.instLinearOrderFeature = LinearOrder.lift' Number.Feature.rank Number.instLinearOrderFeature._proof_1

@[instance_reducible]

instance Number.instLocallyFiniteOrderBotFeature : LocallyFiniteOrderBot Feature

Equations

• Number.instLocallyFiniteOrderBotFeature = Fintype.toLocallyFiniteOrderBot

@[reducible, inline]

abbrev Number.Features : Type

A number feature bundle is the set of its positive features.

Equations

• Number.Features = Finset Number.Feature

def Number.singularF : Features

The singular is [+atomic, +minimal], the whole chain.

Equations

• Number.singularF = Finset.Iic Number.Feature.atomic

def Number.dualF : Features

The dual is [−atomic, +minimal], the chain below atomic.

Equations

• Number.dualF = Finset.Iic Number.Feature.minimal

def Number.pluralF : Features

The plural is [−atomic, −minimal], the empty bundle.

Equations

• Number.pluralF = ∅

theorem Number.singularF_eq : singularF = {Feature.minimal, Feature.atomic}

theorem Number.dualF_eq : dualF = {Feature.minimal}

def Number.Features.toNumber (f : Features) : Option Number

The number value a bundle realizes; the ill-formed [+atomic, −minimal] realizes none.

Equations

• f.toNumber = if Number.Feature.atomic ∈ f then if Number.Feature.minimal ∈ f then some Number.singular else none else if Number.Feature.minimal ∈ f then some Number.dual else some Number.plural

def Number.Features.ofNumber : Number → Option Features

The bundle of a basic number value; the values that need feature recursion or additivity have none.

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

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

Exactly three bundles pass the containment filter, the three basic number values.

theorem Number.toNumber_isSome_iff (f : Features) : f.toNumber.isSome = true ↔ IsLowerSet ↑f

theorem Number.ofNumber_toNumber (f : Features) : IsLowerSet ↑f → f.toNumber.bind Features.ofNumber = some f

theorem Number.toNumber_ofNumber (n : Number) (f : Features) : Features.ofNumber n = some f → f.toNumber = some n

Classification by lattice position

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

A lattice element realizes, in the region P, the singular on the atoms of P, the dual on its minimal non-atoms, and the plural on the rest.

Equations

• Number.latticeToFeatures P x = if Number.atomsOf P x then Number.singularF else if Number.dualOf P x then Number.dualF else Number.pluralF

theorem Number.latticeToFeatures_wellFormed {D : Type u_1} [SemilatticeSup D] [Fintype D] [DecidableLE D] (P : D → Prop) [DecidablePred P] (x : D) : IsLowerSet ↑(latticeToFeatures P x)

Classification never produces the ill-formed cell.

@[reducible, inline]

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

The dual as a predicate modifier holds of x when P x and x has exactly two atomic parts, being a minimal non-atom of the region domain ([JBG+25] (39)).

Equations

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

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

The dual predicate modifier is the restriction of P to the elements classified dualF.

The powerset lattice

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

The nonempty subsets of Fin 3, a lattice with three atoms.

Equations

• Number.ps3 s = s.Nonempty

@[instance_reducible]

instance Number.instDecidablePredFinsetFinOfNatNatPs3 : DecidablePred ps3

Equations

• Number.instDecidablePredFinsetFinOfNatNatPs3 s = { decide := decide (∃ a ∈ s, true = true), reflects_decide := ⋯ }