Grammatical number — the canonical value space

[Cor00] [Har14a] [Gre63] [Cys09]

Number is the canonical grammatical-number type: [Cor00]'s analytical inventory of number values, the vocabulary in which systems, agreement, resolution, and semantics are stated. The UD tagset (UD.Number) is the realization vocabulary — the surface morphology a value projects to via Number.toUD (the analogue of Pronoun.toWord) and is ingested from via Number.fromUD at the corpus boundary. Values UD cannot tag (general, minimal, augmented, unitAugmented) realize as none; conversely UD.Number.Inv/.Coll/.Count are morphological form-categories that are not values of the count-number system, and have no Number preimage. The quadral is deliberately excluded: [Cor00] reanalyzes apparent quadrals (Sursurunga, Tangga) as paucals.

Values are classified along two orthogonal dimensions ([Cor00]):

• System membership: general 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).

Main declarations

• Number — the analytical value inventory ([Cor00] Ch 2).
• Number.toUD / Number.fromUD — realization to / ingestion from UD.Number.
• Number.instPartialOrder — the markedness order: a ≤ b iff every system containing b also contains a (the implicational hierarchy of [Gre63] and [Cor00] §2.3, derived as a lower-set theorem from [Har14a]'s feature geometry in Syntax/Minimalist/Phi/Recursion.lean).
• Number.System — a language's number-value inventory ([Cor00] §2.3), with the implicational universals as decidable predicates and their conjunction System.WellFormed.
• Number.Stage — [Cys09]'s N1–N4 number-opposition stages, a LinearOrder.

Implementation notes

The [Har14a] feature decomposition and its lattice grounding live in Features/Number/Decomposition.lean; coordinate resolution in Features/Number/Resolve.lean; the HasNumber capability mixin in Features/Number/Capabilities.lean.

inductive Number : Type

Grammatical number: [Cor00]'s analytical inventory of number values. The canonical type — UD.Number is its surface realization vocabulary (Number.toUD/Number.fromUD).

• general : Number

  Non-committal to cardinality; outside the number system (Bayso lúban 'lion(s)', Japanese inu 'dog(s)'). Not to be conflated with non-countability: a general form is a value-noncommittal form of a noun that has number, whereas a non-countable noun lacks the contrast altogether — a countability-class fact, not a number value ([Gri18]; Studies/Grimm2018.lean).

• singular : Number

  Exactly one ([+atomic, +minimal]).

• dual : Number

  Exactly two ([−atomic, +minimal]).

• trial : Number

  Exactly three (recursive [+minimal] on the plural region).

• paucal : Number

  A few — indeterminate boundary ([−additive]).

• plural : Number

  More than one — the residual value ([−atomic] or [+additive]).

• greaterPaucal : Number

  Indeterminate, larger than paucal (recursive [−additive]).

• greaterPlural : Number

  Abundance / totality (recursive [−minimal] on the plural region).

• minimal : Number

  [+minimal] without [±atomic] — atoms and minimal non-atoms; distinct from singular.

• augmented : Number

  [−minimal] without [±atomic] — the complement of minimal.

• unitAugmented : Number

  Recursive [+minimal] on the augmented region — minimal non-minimal; distinct from dual.

• globalPlural : Number

  Recursive [+additive] on a [+additive] region (tentative in [Har14a]).

@[implicit_reducible]

instance instDecidableEqNumber : DecidableEq Number

Equations

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

def instReprNumber.repr : Number → ℕ → Std.Format

Equations

• instReprNumber.repr Number.general prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.general")).group prec✝
• instReprNumber.repr Number.singular prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.singular")).group prec✝
• instReprNumber.repr Number.dual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.dual")).group prec✝
• instReprNumber.repr Number.trial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.trial")).group prec✝
• instReprNumber.repr Number.paucal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.paucal")).group prec✝
• instReprNumber.repr Number.plural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.plural")).group prec✝
• instReprNumber.repr Number.greaterPaucal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.greaterPaucal")).group prec✝
• instReprNumber.repr Number.greaterPlural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.greaterPlural")).group prec✝
• instReprNumber.repr Number.minimal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.minimal")).group prec✝
• instReprNumber.repr Number.augmented prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.augmented")).group prec✝
• instReprNumber.repr Number.unitAugmented prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.unitAugmented")).group prec✝
• instReprNumber.repr Number.globalPlural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.globalPlural")).group prec✝

@[implicit_reducible]

instance instReprNumber : Repr Number

Equations

• instReprNumber = { reprPrec := instReprNumber.repr }

@[implicit_reducible]

instance instFintypeNumber : Fintype Number

Equations

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

Classification predicates

def Number.isDeterminate : Number → Prop

A number value is determinate iff its cardinality boundary is fixed. Minimal and unit augmented are indeterminate: they depend on the composition of the group, not a fixed cardinality.

Equations

• Number.singular.isDeterminate = True
• Number.dual.isDeterminate = True
• Number.trial.isDeterminate = True
• x✝.isDeterminate = False

@[implicit_reducible]

instance Number.instDecidablePredIsDeterminate : DecidablePred isDeterminate

Equations

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

def Number.isInSystem : Number → Prop

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

Equations

• Number.general.isInSystem = False
• x✝.isInSystem = True

@[implicit_reducible]

instance Number.instDecidablePredIsInSystem : DecidablePred isInSystem

Equations

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

def Number.exactCard : Number → Option ℕ

Exact referent-set cardinality for determinate number values.

Singular denotes exactly 1 individual (atom), dual exactly 2 (pair), trial exactly 3 (triple). All other values have indeterminate or context-dependent cardinality and return none.

Used by Number.resolve to derive coordinate resolution from cardinality addition: |A ⊔ B| = |A| + |B| for disjoint sets.

Equations

• Number.singular.exactCard = some 1
• Number.dual.exactCard = some 2
• Number.trial.exactCard = some 3
• x✝.exactCard = none

def Number.isMinAug : Number → Prop

Whether a value belongs to the [±minimal] number system (without [±atomic]). In such systems, minimal = atoms ∪ minimal non-atoms, and augmented = everything else.

Equations

• Number.minimal.isMinAug = True
• Number.augmented.isMinAug = True
• x✝.isMinAug = False

@[implicit_reducible]

instance Number.instDecidablePredIsMinAug : DecidablePred isMinAug

Equations

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

def Number.fromCard : ℕ → Number

Map a referent-set cardinality back to the finest determinate value. 1 → singular, 2 → dual, 3 → trial; sums of 4+ have no determinate value and fall to the residual plural (greater plural is an abundance value in [Cor00]'s sense, not "four or more").

Equations

• Number.fromCard 1 = Number.singular
• Number.fromCard 2 = Number.dual
• Number.fromCard 3 = Number.trial
• Number.fromCard x✝ = Number.plural

theorem Number.fromCard_singular : fromCard 1 = singular

fromCard inverts exactCard for determinate values.

theorem Number.fromCard_dual : fromCard 2 = dual

theorem Number.fromCard_trial : fromCard 3 = trial

Realization: the UD bridge

def Number.toUD : Number → Option UD.Number

Realize a number value as a UD morphological tag (general has no UD equivalent; minimal, augmented, and unit augmented cannot be tagged).

Equations

• Number.general.toUD = none
• Number.singular.toUD = some UD.Number.Sing
• Number.dual.toUD = some UD.Number.Dual
• Number.trial.toUD = some UD.Number.Tri
• Number.paucal.toUD = some UD.Number.Pauc
• Number.plural.toUD = some UD.Number.Plur
• Number.greaterPaucal.toUD = some UD.Number.Grpa
• Number.greaterPlural.toUD = some UD.Number.Grpl
• Number.minimal.toUD = none
• Number.augmented.toUD = none
• Number.unitAugmented.toUD = none
• Number.globalPlural.toUD = none

def Number.fromUD : UD.Number → Option Number

Ingest a UD morphological tag as a number value (partial).

Seven core values round-trip cleanly. Three UD tags 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

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

theorem Number.roundtrip_fromUD_toUD (v : Number) : v ∈ [singular, dual, trial, paucal, plural, greaterPaucal, greaterPlural] → v.toUD.bind fromUD = some v

Round-trip: fromUD ∘ toUD = id for all in-system values with a UD tag.

The markedness order

a ≤ b means b presupposes a: every number system containing b also contains a — the implicational hierarchy of [Gre63] and [Cor00] §2.3. The order is derived, not stipulated: the values generated by any well-formed Harbour configuration form a lower set in this order (Minimalist.Phi.Recursion.categories_isLowerSet, from [Har14a]'s feature geometry).

Three independent branches:

[±atomic] branch:    trial    greaterPlural
                       |        /
                      dual     /
                       |      /
                   singular  /
                       |    /
                    plural

[±minimal] branch:       unitAugmented
                              |
                          augmented
                              |
                           minimal

Approximative branch:    greaterPaucal    globalPlural
                              |               |
                            paucal          plural

The [±atomic] branch and [±minimal] branch are independent: singular and minimal never cooccur. Plural spans both. general is isolated (incomparable with all in-system values).

This typological order is one of three markedness notions on number and must not be conflated with the others: the specification order on the Harbour decomposition (Features.ContainmentPair.specLevel: sg > du > pl, linear) and semantic markedness ([Sau03], which rides on specification). On the sg/pl pair the two orders disagree — here sg and pl are incomparable; under specification sg > pl.

def Number.markednessLE (a b : Number) : Prop

The markedness ordering on number values.

Equations

• Number.singular.markednessLE Number.dual = (Number.singular = Number.dual ∨ True)
• Number.singular.markednessLE Number.trial = (Number.singular = Number.trial ∨ True)
• Number.plural.markednessLE Number.singular = (Number.plural = Number.singular ∨ True)
• Number.plural.markednessLE Number.dual = (Number.plural = Number.dual ∨ True)
• Number.plural.markednessLE Number.trial = (Number.plural = Number.trial ∨ True)
• Number.plural.markednessLE Number.greaterPlural = (Number.plural = Number.greaterPlural ∨ True)
• Number.dual.markednessLE Number.trial = (Number.dual = Number.trial ∨ True)
• Number.plural.markednessLE Number.paucal = (Number.plural = Number.paucal ∨ True)
• Number.plural.markednessLE Number.greaterPaucal = (Number.plural = Number.greaterPaucal ∨ True)
• Number.paucal.markednessLE Number.greaterPaucal = (Number.paucal = Number.greaterPaucal ∨ True)
• Number.minimal.markednessLE Number.augmented = (Number.minimal = Number.augmented ∨ True)
• Number.minimal.markednessLE Number.unitAugmented = (Number.minimal = Number.unitAugmented ∨ True)
• Number.augmented.markednessLE Number.unitAugmented = (Number.augmented = Number.unitAugmented ∨ True)
• Number.plural.markednessLE Number.globalPlural = (Number.plural = Number.globalPlural ∨ True)
• a.markednessLE b = (a = b ∨ False)

@[implicit_reducible]

instance Number.instLE : LE Number

Equations

• Number.instLE = { le := Number.markednessLE }

@[implicit_reducible]

instance Number.instDecidableRelLe : DecidableRel fun (x1 x2 : Number) => x1 ≤ x2

Equations

• a.instDecidableRelLe b = a.instDecidableMarkednessLE b

@[implicit_reducible]

instance Number.instPartialOrder : PartialOrder Number

Equations

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

Number opposition stages ([Cys09], Fig 10.8)

inductive Number.Stage : Type

Number opposition stages ([Cys09], Fig 10.8): a coarsening of the number values into a four-step hierarchy of typological richness, from no number marking (N1) to full number marking with restricted groups (N3/N4). Linearly ordered by richness.

• N1 : Stage

  Undifferentiated number marking (singular = group unmarked).

• N2 : Stage

  Singular vs group (basic number opposition).

• N3 : Stage

  Restricted group (dual/trial) distinguished from unrestricted.

• N4 : Stage

  Small group (paucal) additionally distinguished.

@[implicit_reducible]

instance Number.instDecidableEqStage : DecidableEq Stage

Equations

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

def Number.instReprStage.repr : Stage → ℕ → Std.Format

Equations

• Number.instReprStage.repr Number.Stage.N1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.Stage.N1")).group prec✝
• Number.instReprStage.repr Number.Stage.N2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.Stage.N2")).group prec✝
• Number.instReprStage.repr Number.Stage.N3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.Stage.N3")).group prec✝
• Number.instReprStage.repr Number.Stage.N4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.Stage.N4")).group prec✝

@[implicit_reducible]

instance Number.instReprStage : Repr Stage

Equations

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

def Number.Stage.toNat : Stage → ℕ

Numeric embedding into ℕ preserving the richness order.

Equations

• Number.Stage.N1.toNat = 0
• Number.Stage.N2.toNat = 1
• Number.Stage.N3.toNat = 2
• Number.Stage.N4.toNat = 3

@[implicit_reducible]

instance Number.Stage.instLinearOrder : LinearOrder Stage

Equations

• Number.Stage.instLinearOrder = LinearOrder.lift' Number.Stage.toNat Number.Stage.instLinearOrder._proof_1

theorem Number.Stage.toNat_le_toNat {a b : Stage} : a ≤ b ↔ a.toNat ≤ b.toNat

The order on Stage is the toNat order.

Number systems ([Cor00] §2.3)

structure Number.System : Type

A number system: the values available in a language, which are obligatory vs facultative, and whether general number exists ([Cor00] §2.3). Per-language instances live with the studies and Fragments that record them.

• name : String
• values : List Number

  Values available within the number system.

• hasGeneral : Bool

  Whether the language has general number (a form outside the system).

• facultative : List Number

  Values whose use is optional (facultative).

@[implicit_reducible]

instance Number.instDecidableEqSystem : DecidableEq System

Equations

• Number.instDecidableEqSystem = Number.instDecidableEqSystem.decEq

def Number.instDecidableEqSystem.decEq (x✝ x✝¹ : System) : Decidable (x✝ = x✝¹)

Equations

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

def Number.System.size (ns : System) : ℕ

Number of values in the system.

Equations

• ns.size = ns.values.length

def Number.System.IsObligatory (ns : System) (v : Number) : Prop

Whether a value is obligatory (present and not facultative).

Equations

• ns.IsObligatory v = (v ∈ ns.values ∧ v ∉ ns.facultative)

@[implicit_reducible]

instance Number.System.instDecidableIsObligatory (ns : System) (v : Number) : Decidable (ns.IsObligatory v)

Equations

• ns.instDecidableIsObligatory v = id inferInstance

Implicational universals ([Gre63], [Cor00] §2.3.1)

def Number.System.TrialImpliesDual (ns : System) : Prop

Trial implies dual ([Har14a] Table 1: TR → DU).

Equations

• ns.TrialImpliesDual = (Number.trial ∈ ns.values → Number.dual ∈ ns.values)

def Number.System.DualImpliesSingular (ns : System) : Prop

Dual implies singular ([Har14a] Table 1: DU → SG).

Equations

• ns.DualImpliesSingular = (Number.dual ∈ ns.values → Number.singular ∈ ns.values)

def Number.System.SingularImpliesPlural (ns : System) : Prop

Singular implies plural ([Har14a] Table 1: SG → PL).

Equations

• ns.SingularImpliesPlural = (Number.singular ∈ ns.values → Number.plural ∈ ns.values)

def Number.System.DualImpliesPlural (ns : System) : Prop

Dual implies plural ([Gre66], [Cor00] §2.3.1; the composition of DU → SG and SG → PL).

Equations

• ns.DualImpliesPlural = (Number.dual ∈ ns.values → Number.plural ∈ ns.values)

def Number.System.MinimalImpliesAugmentedOrPlural (ns : System) : Prop

Minimal implies augmented or plural ([Har14a] Table 1: MIN → AUG/PL).

Equations

• ns.MinimalImpliesAugmentedOrPlural = (Number.minimal ∈ ns.values → Number.augmented ∈ ns.values ∨ Number.plural ∈ ns.values)

def Number.System.PaucalImpliesPlural (ns : System) : Prop

Paucal implies plural ([Har14a] Table 1: PC → PL).

Equations

• ns.PaucalImpliesPlural = (Number.paucal ∈ ns.values → Number.plural ∈ ns.values)

def Number.System.GreaterPaucalImpliesPaucal (ns : System) : Prop

Greater paucal implies paucal ([Har14a] Table 1: GR.PC → PC).

Equations

• ns.GreaterPaucalImpliesPaucal = (Number.greaterPaucal ∈ ns.values → Number.paucal ∈ ns.values)

def Number.System.GreaterPluralImpliesPluralOrAugmented (ns : System) : Prop

Greater plural implies plural or augmented ([Har14a] Table 1: GR.PL → PL/AUG) — disjunctive, so it is a System predicate, not a markedness-order edge.

Equations

• ns.GreaterPluralImpliesPluralOrAugmented = (Number.greaterPlural ∈ ns.values → Number.plural ∈ ns.values ∨ Number.augmented ∈ ns.values)

def Number.System.PluralImpliesSingularOrMinimal (ns : System) : Prop

Plural implies singular or minimal ([Har14a] Table 1: PL → SG/MIN). Plural requires a "base" value — either singular (from [±atomic]) or minimal (from [±minimal]).

Equations

• ns.PluralImpliesSingularOrMinimal = (Number.plural ∈ ns.values → Number.singular ∈ ns.values ∨ Number.minimal ∈ ns.values)

def Number.System.AugmentedImpliesMinimal (ns : System) : Prop

Augmented implies minimal ([Har14a] Table 1: AUG → MIN).

Equations

• ns.AugmentedImpliesMinimal = (Number.augmented ∈ ns.values → Number.minimal ∈ ns.values)

def Number.System.UnitAugImpliesAugmented (ns : System) : Prop

Unit augmented implies augmented ([Har14a] Table 1: U.AUG → AUG).

Equations

• ns.UnitAugImpliesAugmented = (Number.unitAugmented ∈ ns.values → Number.augmented ∈ ns.values)

@[implicit_reducible]

instance Number.System.instDecidableTrialImpliesDual (ns : System) : Decidable ns.TrialImpliesDual

Equations

• ns.instDecidableTrialImpliesDual = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidableDualImpliesSingular (ns : System) : Decidable ns.DualImpliesSingular

Equations

• ns.instDecidableDualImpliesSingular = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidableSingularImpliesPlural (ns : System) : Decidable ns.SingularImpliesPlural

Equations

• ns.instDecidableSingularImpliesPlural = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidableDualImpliesPlural (ns : System) : Decidable ns.DualImpliesPlural

Equations

• ns.instDecidableDualImpliesPlural = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidableMinimalImpliesAugmentedOrPlural (ns : System) : Decidable ns.MinimalImpliesAugmentedOrPlural

Equations

• ns.instDecidableMinimalImpliesAugmentedOrPlural = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidablePaucalImpliesPlural (ns : System) : Decidable ns.PaucalImpliesPlural

Equations

• ns.instDecidablePaucalImpliesPlural = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidableGreaterPaucalImpliesPaucal (ns : System) : Decidable ns.GreaterPaucalImpliesPaucal

Equations

• ns.instDecidableGreaterPaucalImpliesPaucal = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidableGreaterPluralImpliesPluralOrAugmented (ns : System) : Decidable ns.GreaterPluralImpliesPluralOrAugmented

Equations

• ns.instDecidableGreaterPluralImpliesPluralOrAugmented = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidablePluralImpliesSingularOrMinimal (ns : System) : Decidable ns.PluralImpliesSingularOrMinimal

Equations

• ns.instDecidablePluralImpliesSingularOrMinimal = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidableAugmentedImpliesMinimal (ns : System) : Decidable ns.AugmentedImpliesMinimal

Equations

• ns.instDecidableAugmentedImpliesMinimal = id inferInstance

@[implicit_reducible]

instance Number.System.instDecidableUnitAugImpliesAugmented (ns : System) : Decidable ns.UnitAugImpliesAugmented

Equations

• ns.instDecidableUnitAugImpliesAugmented = id inferInstance

def Number.System.WellFormed (ns : System) : Prop

A well-formed number system satisfies all implicational universals ([Har14a] Table 1). Any Fragment-recorded system discharges this by decide.

Equations

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

@[implicit_reducible]

instance Number.System.instDecidableWellFormed (ns : System) : Decidable ns.WellFormed

Equations

• ns.instDecidableWellFormed = id inferInstance

def Number.System.toStage (ns : System) : Stage

The [Cys09] stage a system realizes, by value count: 0–1 values → N1 (undifferentiated), 2 → N2 (basic opposition), 3 → N3 (restricted group), 4+ → N4 (paucal additionally).

Equations

• ns.toStage = match ns.size with | 0 => Number.Stage.N1 | 1 => Number.Stage.N1 | 2 => Number.Stage.N2 | 3 => Number.Stage.N3 | x => Number.Stage.N4