Little, Moroney & Royer (2022)

@cite{little-moroney-royer-2022}

Classifiers can be for numerals or nouns: Two strategies for numeral modification. Glossa 7(1). 1–35.

Core Claim

Numeral classifiers form a heterogeneous class. Two families of theories — classifier-for-numeral (CLF-for-NUM) and classifier-for-noun (CLF-for-N) — are both correct, but for different languages:

• Ch'ol (Mayan): CLF-for-NUM — the classifier is a measure function required by the numeral.
• Shan (Kra-Dai): CLF-for-N — the classifier atomizes the noun denotation so the numeral can count.

Four Predictions (Table 8)

The two strategies make divergent predictions about classifier distribution:

1. (num) Variation in whether a numeral requires a CLF → CLF-for-NUM
2. (noun) Variation in whether a noun requires a CLF → CLF-for-N
3. (noun) CLF found beyond numerals (quantifiers, demonstratives) → CLF-for-N
4. (num) CLF appears in counting (no noun present) → CLF-for-NUM

Ch'ol shows predictions 1 and 4; Shan shows predictions 2 and 3.

Semantic Equivalence

Despite different derivational strategies, both languages derive the same meaning for "two dogs": {ab, ac, bc} — the set of pluralities of two dogs.

Architectural Note

CLF-for-NUM is formalized using Mereology.QMOD — the measure function Finset.card produces a quantized predicate (clfForNum_qua). CLF-for-N is formalized directly as atom-pair selection: ∃ d₁ d₂, d₁ ≠ d₂ ∧ s = {d₁, d₂}. The ClassifierStrategy enum in Typology captures the typological parameter.

Note: Mereology.atomize cannot be applied to Finset Dog directly because Finset has ∅ as a bottom element — Mereology.Atom (no proper part) is only satisfied by ∅, so atomize(DOGS) would be empty. The CLF-for-N semantics is instead formalized at the element level: singletons {d} are the atoms, and clfForNounSem selects 2-element unions of distinct atoms. The extensional equivalence (derivations_extensionally_equal) bridges the two via Finset.card_eq_two.

def LittleMoroneyRoyer2022.chol : Typology.NounCategorizationSystem

Ch'ol noun categorization system: numeral classifier, CLF-for-NUM. @cite{bale-coon-2014} @cite{bale-et-al-2019}

Key properties:

• Classifiers are bound to the numeral (suffixes)
• Only Mayan-based numerals (1–6) take classifiers; Spanish loans do not
• Classifiers appear in counting contexts (no noun)
• Plural marking -ob co-occurs with classifiers (ex. 30)
• Classifiers are ungrammatical with quantifiers, demonstratives, modifiers (ex. 19)

Equations

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

def LittleMoroneyRoyer2022.shan : Typology.NounCategorizationSystem

Shan noun categorization system: numeral classifier, CLF-for-N. @cite{moroney-2021}

Key properties:

• Classifiers are free morphemes derived from nominal elements
• All numerals uniformly require classifiers (no idiosyncrasies)
• Classifiers appear with quantifiers, demonstratives, relative clauses (ex. 42)
• Classifiers degraded/unacceptable in counting contexts (exs. 48–49)
• No plural–classifier co-occurrence

Equations

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

structure LittleMoroneyRoyer2022.Predictions : Type

The four distributional predictions from the CLF-for-NUM vs CLF-for-N distinction (Table 2/7/8).

• numeralIdiosyncrasies : Bool

  Prediction 1: Idiosyncrasies in whether a numeral requires a CLF. Expected for CLF-for-NUM (measure function may be built into numeral).

• nounIdiosyncrasies : Bool

  Prediction 2: Idiosyncrasies in whether a noun requires a CLF. Expected for CLF-for-N (some nouns may already denote atoms).

• clfBeyondNumerals : Bool

  Prediction 3: CLF found with the noun beyond numerals (quantifiers, demonstratives, relative clauses). Expected for CLF-for-N (CLF is for the noun, not the numeral).

• clfInCounting : Bool

  Prediction 4: CLF appears in counting contexts (no noun present). Expected for CLF-for-NUM (CLF is required by the numeral itself).

def LittleMoroneyRoyer2022.instReprPredictions.repr : Predictions → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instReprPredictions : Repr Predictions

Equations

• LittleMoroneyRoyer2022.instReprPredictions = { reprPrec := LittleMoroneyRoyer2022.instReprPredictions.repr }

def LittleMoroneyRoyer2022.instBEqPredictions.beq : Predictions → Predictions → Bool

Equations

• One or more equations did not get rendered due to their size.
• LittleMoroneyRoyer2022.instBEqPredictions.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instBEqPredictions : BEq Predictions

Equations

• LittleMoroneyRoyer2022.instBEqPredictions = { beq := LittleMoroneyRoyer2022.instBEqPredictions.beq }

def LittleMoroneyRoyer2022.instDecidableEqPredictions.decEq (x✝ x✝¹ : Predictions) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instDecidableEqPredictions : DecidableEq Predictions

Equations

• LittleMoroneyRoyer2022.instDecidableEqPredictions = LittleMoroneyRoyer2022.instDecidableEqPredictions.decEq

def LittleMoroneyRoyer2022.clfForNumPredictions : Predictions

Expected predictions for CLF-for-NUM languages.

Equations

• LittleMoroneyRoyer2022.clfForNumPredictions = { numeralIdiosyncrasies := true, nounIdiosyncrasies := false, clfBeyondNumerals := false, clfInCounting := true }

def LittleMoroneyRoyer2022.clfForNounPredictions : Predictions

Expected predictions for CLF-for-N languages.

Equations

• LittleMoroneyRoyer2022.clfForNounPredictions = { numeralIdiosyncrasies := false, nounIdiosyncrasies := true, clfBeyondNumerals := true, clfInCounting := false }

def LittleMoroneyRoyer2022.sudoBlockingPredictions : Predictions

Expected predictions for languages whose classifier system is the @cite{sudo-2016} blocking strategy: classifier semantics live with numerals, not nouns; the silent ∪-operator that lifts numerals to predicates is blocked by the lexical presence of classifiers.

LMR's diagnostic battery applied to Sudo's framework:

• numeralIdiosyncrasies = false: ∪ is uniformly blocked across all numerals; no per-numeral variation (contrast Ch'ol Mayan-vs- Spanish split, which Sudo's framework does not predict).
• nounIdiosyncrasies = false: explanation lives in numerals, not nouns; uniform across the noun lexicon.
• clfBeyondNumerals = false: classifiers exist to lift numerals to predicate type; they appear with numerals, not beyond them (contrast LMR's CLF-for-N prediction).
• clfInCounting = true: the ∩-operator (Sudo eq. 24) maps the numeral+CL property back to type-n, so number-predicate uses like juu-ni-nin-da "the number is twelve people" (Sudo eq. 22a) are well-formed (contrast LMR's CLF-for-N prediction).

Equations

• LittleMoroneyRoyer2022.sudoBlockingPredictions = { numeralIdiosyncrasies := false, nounIdiosyncrasies := false, clfBeyondNumerals := false, clfInCounting := true }

def LittleMoroneyRoyer2022.predictionsOf : Typology.ClassifierStrategy → Predictions

Derive LMR's distributional predictions from any classifier strategy. This is the paper's core claim for .forNumeral and .forNoun; extended here to .sudoBlocking per @cite{sudo-2016}'s analysis.

Equations

• LittleMoroneyRoyer2022.predictionsOf Typology.ClassifierStrategy.forNumeral = LittleMoroneyRoyer2022.clfForNumPredictions
• LittleMoroneyRoyer2022.predictionsOf Typology.ClassifierStrategy.forNoun = LittleMoroneyRoyer2022.clfForNounPredictions
• LittleMoroneyRoyer2022.predictionsOf Typology.ClassifierStrategy.sudoBlocking = LittleMoroneyRoyer2022.sudoBlockingPredictions

§2b: LMR's per-language strategy assignments

@cite{little-moroney-royer-2022} assigns Ch'ol the CLF-for-NUM strategy and Shan the CLF-for-N strategy. They are consistent with the @cite{chierchia-1998} CLF-for-N assignment for Mandarin/Japanese (LMR treat Sinitic and Japonic as CLF-for-N). Per-language assignments live here (in this study file) rather than on NounCategorizationSystem.

def LittleMoroneyRoyer2022.cholStrategy : Typology.ClassifierStrategy

LMR's strategy assignment for Ch'ol: classifier is a measure function required by the numeral.

Equations

• LittleMoroneyRoyer2022.cholStrategy = Typology.ClassifierStrategy.forNumeral

def LittleMoroneyRoyer2022.shanStrategy : Typology.ClassifierStrategy

LMR's strategy assignment for Shan: classifier atomizes the noun denotation.

Equations

• LittleMoroneyRoyer2022.shanStrategy = Typology.ClassifierStrategy.forNoun

def LittleMoroneyRoyer2022.cholPredictions : Predictions

Ch'ol predictions derived from LMR's CLF-for-NUM assignment.

Equations

• LittleMoroneyRoyer2022.cholPredictions = LittleMoroneyRoyer2022.predictionsOf LittleMoroneyRoyer2022.cholStrategy

def LittleMoroneyRoyer2022.shanPredictions : Predictions

Shan predictions derived from LMR's CLF-for-N assignment.

Equations

• LittleMoroneyRoyer2022.shanPredictions = LittleMoroneyRoyer2022.predictionsOf LittleMoroneyRoyer2022.shanStrategy

theorem LittleMoroneyRoyer2022.profiles_distinct : clfForNumPredictions ≠ clfForNounPredictions

The CLF-for-NUM and CLF-for-N profiles are distinct — the two LMR strategies make genuinely different predictions on all four diagnostics.

theorem LittleMoroneyRoyer2022.chol_predictions_from_strategy : predictionsOf cholStrategy = cholPredictions

Ch'ol predictions follow from LMR's strategy assignment via predictionsOf.

theorem LittleMoroneyRoyer2022.shan_predictions_from_strategy : predictionsOf shanStrategy = shanPredictions

Shan predictions follow from LMR's strategy assignment via predictionsOf.

theorem LittleMoroneyRoyer2022.chierchia_sudo_diverge_on_predictions : predictionsOf NMP.japaneseStrategy ≠ predictionsOf Sudo2016.japaneseStrategy

@cite{chierchia-1998} and @cite{sudo-2016} disagree on Japanese's classifier strategy: Chierchia assigns .forNoun, Sudo assigns .sudoBlocking. Run through LMR's diagnostic battery, the two strategies make divergent empirical predictions:

theorem LittleMoroneyRoyer2022.clfInCounting_distinguishes_chierchia_from_sudo : (predictionsOf NMP.japaneseStrategy).clfInCounting = false ∧ (predictionsOf Sudo2016.japaneseStrategy).clfInCounting = true

The empirical wedge: under LMR's diagnostics, Chierchia's .forNoun and Sudo's .sudoBlocking agree on numeralIdiosyncrasies = false but diverge on the other three. The most decisive disagreement is clfInCounting: Sudo predicts true (citing eq. 22a — juu-ni-nin-da "the number is twelve people" is well-formed via the ∩-operator), Chierchia predicts false. Japanese empirically exhibits the Sudo pattern on this diagnostic.

theorem LittleMoroneyRoyer2022.clfBeyondNumerals_distinguishes_chierchia_from_sudo : (predictionsOf NMP.japaneseStrategy).clfBeyondNumerals = true ∧ (predictionsOf Sudo2016.japaneseStrategy).clfBeyondNumerals = false

Symmetric divergence on clfBeyondNumerals: Chierchia predicts true (CLF appears with quantifiers, demonstratives, relative clauses independent of numerals); Sudo predicts false (CLF exists for numerals, not beyond them).

structure LittleMoroneyRoyer2022.ClfDatum : Type

Grammaticality judgments for Ch'ol classifier distribution (§3.1, §4). Each datum records whether a CLF appears in a given syntactic context.

• language : String
• context : String
• clfPresent : Bool
• grammatical : Bool

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instReprClfDatum : Repr ClfDatum

Equations

• LittleMoroneyRoyer2022.instReprClfDatum = { reprPrec := LittleMoroneyRoyer2022.instReprClfDatum.repr }

def LittleMoroneyRoyer2022.instReprClfDatum.repr : ClfDatum → ℕ → Std.Format

Equations

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

def LittleMoroneyRoyer2022.cholData : List ClfDatum

Ch'ol: CLF only with numerals and interrogative jay- 'how many'.

Equations

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

def LittleMoroneyRoyer2022.shanData : List ClfDatum

Shan: CLF with numerals, quantifiers, demonstratives, relative clauses.

Equations

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

theorem LittleMoroneyRoyer2022.greenberg_refined_by_strategy : cholStrategy = Typology.ClassifierStrategy.forNumeral ∧ chol.PluralClfCooccur ∧ shanStrategy = Typology.ClassifierStrategy.forNoun ∧ ¬shan.PluralClfCooccur

@cite{little-moroney-royer-2022} §3.4 refine @cite{greenberg-1972}'s complementarity universal. The original says numeral classifiers and obligatory number marking are in complementary distribution. The refinement: this holds for CLF-for-N (where CLF and PL occupy the same functional projection) but not for CLF-for-NUM (where CLF is in a separate projection and can co-occur with PL).

Ch'ol (CLF-for-NUM): cha'-tyikil wiñik-ob 'two-CLF men-PL' (ex. 30) Shan (CLF-for-N): *mǎa sǎam tǒ khǎw 'three CLF dogs PL' (unattested)

theorem LittleMoroneyRoyer2022.clf_beyond_numerals_tracks_scopes : (chol.scopes.any fun (x : Typology.CategorizationScope) => x != Typology.CategorizationScope.numeralNP) = false ∧ (shan.scopes.any fun (x : Typology.CategorizationScope) => x != Typology.CategorizationScope.numeralNP) = true

Prediction 3 (CLF beyond numerals) is derived from the system's scopes. CLF-for-N classifiers serve the noun, so they appear wherever the noun needs individuation — not just with numerals.

def LittleMoroneyRoyer2022.cholTree : Core.Tree.Tree Unit String

Ch'ol constituency (51): numeral and classifier form a constituent. [[cha'-kojty]_NumCLF [ts'i']_N] The numeral cha' first combines with the classifier -kojty to form a measure phrase, which then applies to the noun ts'i' 'dog'.

Equations

• LittleMoroneyRoyer2022.cholTree = ((Core.Tree.Tree.leaf "cha'").bin (Core.Tree.Tree.leaf "kojty")).bin (Core.Tree.Tree.leaf "ts'i'")

def LittleMoroneyRoyer2022.shanTree : Core.Tree.Tree Unit String

Shan constituency (52): classifier and noun form a constituent. [[sǒŋ]_Num [[tǒ]_CLF [mǎa]_N]] The classifier tǒ first combines with the noun mǎa 'dog' to atomize it, then the numeral sǒŋ 'two' selects a 2-element sum.

Equations

• LittleMoroneyRoyer2022.shanTree = (Core.Tree.Tree.leaf "sǒŋ").bin ((Core.Tree.Tree.leaf "tǒ").bin (Core.Tree.Tree.leaf "mǎa"))

theorem LittleMoroneyRoyer2022.constituency_differs : (cholTree != shanTree) = true

The two derivation trees have different constituency despite both being binary branching over three terminals. In Ch'ol, the left daughter of the root is complex (Num+CLF); in Shan, the right daughter is complex (CLF+N).

This structural difference is what generates the four distributional predictions: if Num+CLF is a constituent, the classifier is part of the numeral's semantics and appears wherever the numeral appears (counting, number reference). If CLF+N is a constituent, the classifier is part of the noun's semantics and appears wherever the noun needs individuation (quantifiers, demonstratives).

theorem LittleMoroneyRoyer2022.same_size : cholTree.size = shanTree.size

Both trees have the same size (5 nodes each: 2 internal + 3 terminals). The difference is purely structural — which pairs branch together.

inductive LittleMoroneyRoyer2022.Dog : Type

A finite domain of three atomic dogs: a, b, c.

• a : Dog
• b : Dog
• c : Dog

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instDecidableEqDog : DecidableEq Dog

Equations

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

def LittleMoroneyRoyer2022.instReprDog.repr : Dog → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instReprDog : Repr Dog

Equations

• LittleMoroneyRoyer2022.instReprDog = { reprPrec := LittleMoroneyRoyer2022.instReprDog.repr }

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instFintypeDog : Fintype Dog

Equations

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

def LittleMoroneyRoyer2022.clfForNumSem (s : Finset Dog) : Prop

CLF-for-NUM derivation: Mereology.QMOD applied to the dog domain. ⟦two-CLF⟧ = λP. QMOD(P, μ#, 2) where μ# = Finset.card. This uses Mereology.QMOD from Core/Mereology.lean: QMOD(R, μ, n) = λx. R(x) ∧ μ(x) = n

Equations

• LittleMoroneyRoyer2022.clfForNumSem s = Mereology.QMOD (fun (x : Finset LittleMoroneyRoyer2022.Dog) => x.Nonempty) Finset.card 2 s

def LittleMoroneyRoyer2022.clfForNounSem (s : Finset Dog) : Prop

CLF-for-N derivation: atomize, then count. ⟦CLF⟧(⟦DOGS⟧) restricts to atoms (singletons), then ⟦TWO⟧ selects 2-element sums from the atomized set. The result: s is the union of exactly two distinct atoms.

Equations

• LittleMoroneyRoyer2022.clfForNounSem s = ∃ (d₁ : LittleMoroneyRoyer2022.Dog) (d₂ : LittleMoroneyRoyer2022.Dog), d₁ ≠ d₂ ∧ s = {d₁, d₂}

theorem LittleMoroneyRoyer2022.derivations_extensionally_equal (s : Finset Dog) : clfForNumSem s ↔ clfForNounSem s

The two derivation strategies are extensionally equivalent: QMOD(DOGS, μ#, 2) = {s | ∃ d₁ d₂, d₁ ≠ d₂ ∧ s = {d₁, d₂}}. This is the paper's key semantic result (§5): despite different compositional paths, both strategies produce the same denotation for "two dogs."

The CLF-for-NUM path uses the measure constraint directly (QMOD); the CLF-for-N path atomizes then forms 2-element sums. Finset.card_eq_two provides the bridge: a finset has cardinality 2 iff it's a pair of distinct elements.

theorem LittleMoroneyRoyer2022.dogs_cum : Mereology.CUM fun (x : Finset Dog) => x.Nonempty

The full dog predicate (Nonempty) is cumulative: the union of two dog-pluralities is a dog-plurality. Mereology.CUM applied to Finset Dog with ⊔ = ∪.

Cumulativity is what forces classifier languages to need a classifier: counting over a CUM predicate is undefined until it's quantized. CLF-for-NUM uses QMOD to quantize directly; CLF-for-N atomizes first.

theorem LittleMoroneyRoyer2022.clfForNum_qua : Mereology.QUA clfForNumSem

CLF-for-NUM creates a quantized predicate via QMOD: no proper subset of a 2-element set also has 2 elements.

Proof: y ⊂ x implies |y| < |x| (Finset.card_lt_card), but both have card 2 — contradiction. This mirrors the general Mereology.extMeasure_qua pattern (QMOD by any extensive measure produces QUA), instantiated directly for Finset.card.

theorem LittleMoroneyRoyer2022.clfForNoun_qua : Mereology.QUA clfForNounSem

CLF-for-N also creates a quantized predicate: no proper subset of a pair of distinct dogs is also a pair of distinct dogs. Both strategies convert CUM predicates to QUA predicates — this is the semantic function of classifiers regardless of strategy.

Proof: if y ⊂ x and both satisfy clfForNounSem, then by derivations_extensionally_equal, both have card 2. But y ⊂ x implies |y| < |x| — contradiction.

theorem LittleMoroneyRoyer2022.both_strategies_quantize : Mereology.QUA clfForNumSem ∧ Mereology.QUA clfForNounSem

Both strategies quantize: the semantic function of classifiers is to turn CUM predicates into QUA predicates, enabling counting.

theorem LittleMoroneyRoyer2022.ab_satisfies : clfForNumSem {Dog.a, Dog.b}

Concrete witness: {a, b} is a two-dog plurality.

theorem LittleMoroneyRoyer2022.ac_satisfies : clfForNumSem {Dog.a, Dog.c}

Concrete witness: {a, c} is a two-dog plurality.

theorem LittleMoroneyRoyer2022.bc_satisfies : clfForNumSem {Dog.b, Dog.c}

Concrete witness: {b, c} is a two-dog plurality.

theorem LittleMoroneyRoyer2022.singleton_excluded (d : Dog) : ¬clfForNumSem {d}

Singletons are not two-dog pluralities: the measure constraint excludes them. This is why CLF-for-N atomization alone doesn't suffice — the numeral still needs to select the right cardinality.

theorem LittleMoroneyRoyer2022.triple_excluded : ¬clfForNumSem {Dog.a, Dog.b, Dog.c}

The triple is not a two-dog plurality: QMOD excludes oversized sums.

def LittleMoroneyRoyer2022.allSystemsWithCholShan : List Typology.NounCategorizationSystem

Extended system list including Ch'ol and Shan.

Equations

• LittleMoroneyRoyer2022.allSystemsWithCholShan = Aikhenvald2000.allSystems ++ [LittleMoroneyRoyer2022.chol, LittleMoroneyRoyer2022.shan]

theorem LittleMoroneyRoyer2022.same_aikhenvald_different_strategy : chol.classifierType = shan.classifierType ∧ cholStrategy ≠ shanStrategy

Ch'ol and Shan are both numeral classifier systems in Aikhenvald's typology, but have different classifier strategies. They agree on Aikhenvald's morphosyntactic classification but differ on the semantic level — illustrating that ClassifierType is too coarse to capture the CLF-for-NUM vs CLF-for-N distinction.

theorem LittleMoroneyRoyer2022.sample_no_agreement_with_chol_shan (s : Typology.NounCategorizationSystem) : s ∈ allSystemsWithCholShan → Typology.NounCategorizationSystem.isClassifierType s.classifierType = true → ¬s.HasAgreement

Sample-restricted: in the 7-language Aikhenvald sample plus Ch'ol and Shan, every classifier-type language lacks agreement.

theorem LittleMoroneyRoyer2022.shan_agrees_with_chierchia_clf_for_noun : shanStrategy = NMP.mandarinStrategy ∧ shanStrategy = NMP.japaneseStrategy

@cite{chierchia-1998}'s NMP predicts CLF-for-N for [+arg, -pred] languages (Mandarin, Japanese). Shan is also CLF-for-N per @cite{little-moroney-royer-2022}, despite being Kra-Dai not Sino-Tibetan — the strategy is independent of the NMP parameter. Ch'ol is CLF-for-NUM, which @cite{chierchia-1998} does not predict (Ch'ol is not a [+arg, -pred] language in the NMP typology).

This connects the two classifier study files: Chierchia predicts the strategy for Mandarin/Japanese; Little et al. provide the diagnostic framework that confirms it and extends it to new languages.

theorem LittleMoroneyRoyer2022.chol_differs_from_chierchia_languages : cholStrategy ≠ NMP.mandarinStrategy

Ch'ol's CLF-for-NUM strategy differs from the Chierchia-predicted CLF-for-N found in Mandarin and Japanese. This is the paper's main typological contribution: not all numeral classifier languages use the same semantic strategy.

theorem LittleMoroneyRoyer2022.strategy_dispatch_forNoun : Semantics.Classifier.classifierDenot Typology.ClassifierStrategy.forNoun (fun (x : Finset Dog) => True) (fun (x : Finset Dog) => 0) 0 = Semantics.Classifier.clfForNoun fun (x : Finset Dog) => True

The unified classifierDenot correctly dispatches based on strategy.

• CLF-for-N → clfForNoun (= atomize)
• CLF-for-NUM → clfForNum (= QMOD)

This confirms that the typological enum in Typology is structurally connected to semantic content, not just a label.

theorem LittleMoroneyRoyer2022.clfForNum_agrees_with_local (s : Finset Dog) : clfForNumSem s ↔ Mereology.QMOD (fun (x : Finset Dog) => x.Nonempty) Finset.card 2 s

The local clfForNumSem IS QMOD from Core.Mereology: both compute R(x) ∧ μ(x) = n with μ = Finset.card and n = 2. The unified clfForNum specializes QMOD to ℚ; the local definition uses ℕ directly. Both reduce to QMOD.