Wang & Sun (2026): Detaching Mandarin Classifiers from Nouns

@cite{wang-sun-2026} @cite{adger-2025}

Applies @cite{adger-2025}'s mereological syntax to three problems in Mandarin classifier phrases:

1. Modification: Degree-modified adjectives cannot appear between Num and Cl — predicted by dimensionality (Q is full).
2. Dislocation: [Cl-N] cannot be topicalized independently of Num — predicted by collective spell-out at Q.
3. Interpretation: 的 de changes classifier from sortal (concrete object) to mensural (abstract unit) — predicted by cross-dimensional visibility.

Key Structural Insight

Classifiers are NOT projections of nouns. They are independent syntactic objects that subjoin to Q as its 1-part. The classifier word spells out at Q (collective spell-out of the Q-Cl complementation line). This detachment from N explains all three problems.

inductive Phenomena.Classifiers.Studies.WangSun2026.GramStatus : Type

Grammaticality status for Mandarin classifier examples.

• ok : GramStatus
• marginal : GramStatus
• bad : GramStatus
• hashBad : GramStatus

instance Phenomena.Classifiers.Studies.WangSun2026.instDecidableEqGramStatus : DecidableEq GramStatus

Equations

• Phenomena.Classifiers.Studies.WangSun2026.instDecidableEqGramStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Classifiers.Studies.WangSun2026.instBEqGramStatus.beq : GramStatus → GramStatus → Bool

Equations

• Phenomena.Classifiers.Studies.WangSun2026.instBEqGramStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Classifiers.Studies.WangSun2026.instBEqGramStatus : BEq GramStatus

Equations

• Phenomena.Classifiers.Studies.WangSun2026.instBEqGramStatus = { beq := Phenomena.Classifiers.Studies.WangSun2026.instBEqGramStatus.beq }

instance Phenomena.Classifiers.Studies.WangSun2026.instReprGramStatus : Repr GramStatus

Equations

• Phenomena.Classifiers.Studies.WangSun2026.instReprGramStatus = { reprPrec := Phenomena.Classifiers.Studies.WangSun2026.instReprGramStatus.repr }

def Phenomena.Classifiers.Studies.WangSun2026.instReprGramStatus.repr : GramStatus → ℕ → Std.Format

Equations

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

structure Phenomena.Classifiers.Studies.WangSun2026.ClDatum : Type

• mandarin : String
• gloss : String
• translation : String
• status : GramStatus

def Phenomena.Classifiers.Studies.WangSun2026.instReprClDatum.repr : ClDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Classifiers.Studies.WangSun2026.instReprClDatum : Repr ClDatum

Equations

• Phenomena.Classifiers.Studies.WangSun2026.instReprClDatum = { reprPrec := Phenomena.Classifiers.Studies.WangSun2026.instReprClDatum.repr }

Problem 1: Modification restrictions

def Phenomena.Classifiers.Studies.WangSun2026.ex4c : ClDatum

(4c) *yī hěn cōngmíng de gè xuéshēng — degree adj before Cl: bad.

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.ex8a : ClDatum

(8a) yī gè cōngmíng (de) xuéshēng — adj after Cl: ok.

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.ex29a : ClDatum

(29a) *yī hěn dà (de) zhāng zhuōzi — degree adj between Num and Cl: bad.

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.ex29b : ClDatum

(29b) yī dà zhāng zhuōzi — bare size adj before Cl: ok (included in Q spell-out).

Equations

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

Problem 1b: Modification IS possible after Cl

def Phenomena.Classifiers.Studies.WangSun2026.ex28a : ClDatum

(28a) yī zhāng hěn dà de zhuōzi — degree adj after Cl: ok.

Equations

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

Problem 2: Dislocation restrictions

def Phenomena.Classifiers.Studies.WangSun2026.ex5c : ClDatum

(5c) *Gè píngguǒ, Zhāngsān chī-le sān — [Cl-N] topicalized, Num stranded: bad.

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.ex13b : ClDatum

(13b) Píngguǒ, Zhāngsān chī-le sān gè — N topicalized alone: ok.

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.ex14a : ClDatum

(14a) *Sān gè, Zhāngsān chī-le píngguǒ — [Num-Cl] without N: bad.

Equations

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

Wh-island effects (§5)

def Phenomena.Classifiers.Studies.WangSun2026.ex39a : ClDatum

(39a) Zhāngsān mǎi-le jǐ zhāng hěn dà de zhuōzi? — wh-numeral before Cl: ok.

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.ex39b : ClDatum

(39b) *Zhāngsān mǎi-le hěn dà de jǐ zhāng zhuōzi? — wh-numeral after Mod: bad.

Equations

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

Problem 3: Interpretation change with 的 de

def Phenomena.Classifiers.Studies.WangSun2026.ex33a : ClDatum

(33a) sān bēi jiǔ — no de: "three glasses of liquor" (real glasses).

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.ex33b : ClDatum

(33b) sān bēi de jiǔ — with de: "three glassfuls of liquor" (abstract).

Equations

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

(26b): yī zhāng zhuōzi "a table"

```
D
  @Q: zhāng        ← Q and Cl collectively spell out
    Num: yī    Cl
                 N: zhuōzi
```
Parthood: N <₁ Cl <₁ Q, Num <₂ Q, Q <₁ D. 

def Phenomena.Classifiers.Studies.WangSun2026.basic_N : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.basic_N = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.N

def Phenomena.Classifiers.Studies.WangSun2026.basic_Cl : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.basic_Cl = MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.Cl Phenomena.Classifiers.Studies.WangSun2026.basic_N

def Phenomena.Classifiers.Studies.WangSun2026.basic_Num : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.basic_Num = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Num

def Phenomena.Classifiers.Studies.WangSun2026.basic_Q : MereologicalSyntax.SynObj

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.basic_D : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.basic_D = MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.D Phenomena.Classifiers.Studies.WangSun2026.basic_Q

(34a): sān bēi jiǔ "three glasses of liquor" — without 的

Same topology as (26b). Cl is in D's 1-part chain → visible → sortal. 

def Phenomena.Classifiers.Studies.WangSun2026.noDe_N : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.noDe_N = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.N

def Phenomena.Classifiers.Studies.WangSun2026.noDe_Cl : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.noDe_Cl = MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.Cl Phenomena.Classifiers.Studies.WangSun2026.noDe_N

def Phenomena.Classifiers.Studies.WangSun2026.noDe_Num : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.noDe_Num = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Num

def Phenomena.Classifiers.Studies.WangSun2026.noDe_Q : MereologicalSyntax.SynObj

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.noDe_D : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.noDe_D = MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.D Phenomena.Classifiers.Studies.WangSun2026.noDe_Q

(34b): sān bēi de jiǔ "three glassfuls of liquor" — with 的

的 *de* is the spell-out of Mod. Q subjoins to Mod as 1-part;
Mod then subjoins to D as 2-part. N subjoins directly to D
as 1-part — NOT to Cl (contrast with noDe where N <₁ Cl).
```
D
  N: jiǔ         Mod: de
                    @Q: bēi
                      Cl    Num: sān
```
Parthood: Cl <₁ Q, Num <₂ Q, Q <₁ Mod, N <₁ D, Mod <₂ D.
Cl is NOT in D's 1-part chain → invisible → mensural. 

def Phenomena.Classifiers.Studies.WangSun2026.de_Cl : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.de_Cl = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Cl

def Phenomena.Classifiers.Studies.WangSun2026.de_Num : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.de_Num = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Num

def Phenomena.Classifiers.Studies.WangSun2026.de_Q : MereologicalSyntax.SynObj

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.de_Mod : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.de_Mod = MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.Mod Phenomena.Classifiers.Studies.WangSun2026.de_Q

def Phenomena.Classifiers.Studies.WangSun2026.de_N : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.de_N = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.N

def Phenomena.Classifiers.Studies.WangSun2026.de_D : MereologicalSyntax.SynObj

Equations

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

(27b): hěn dà de "very big"

```
Mod
  @Deg: dà-de
    A          Adv: hěn
```
A <₁ Deg, Adv <₂ Deg, Deg <₁ Mod. Mod spells out *de* at its node;
Deg spells out the adjective *dà* collectively with A. 

def Phenomena.Classifiers.Studies.WangSun2026.modPhrase_A : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.modPhrase_A = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.A

def Phenomena.Classifiers.Studies.WangSun2026.modPhrase_Adv : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.modPhrase_Adv = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Adv

def Phenomena.Classifiers.Studies.WangSun2026.modPhrase_Deg : MereologicalSyntax.SynObj

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.modPhrase : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.modPhrase = MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.Mod Phenomena.Classifiers.Studies.WangSun2026.modPhrase_Deg

(28c): yī zhāng hěn dà de zhuōzi "a very big table"

Mod adjoins as 2-part of Cl (Cl has only N as 1-part, so it has room).
```
D
  @Q: zhāng
    Num: yī    Cl
                 N: zhuōzi    Mod
                                @Deg: dà-de
                                  A    Adv: hěn
```
Parthood: A <₁ Deg, Adv <₂ Deg, Deg <₁ Mod, N <₁ Cl, Mod <₂ Cl,
          Cl <₁ Q, Num <₂ Q, Q <₁ D. 

def Phenomena.Classifiers.Studies.WangSun2026.postCl_N : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.postCl_N = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.N

def Phenomena.Classifiers.Studies.WangSun2026.postCl_Cl : MereologicalSyntax.SynObj

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.postCl_Num : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.postCl_Num = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Num

def Phenomena.Classifiers.Studies.WangSun2026.postCl_Q : MereologicalSyntax.SynObj

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.postCl_D : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.postCl_D = MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.D Phenomena.Classifiers.Studies.WangSun2026.postCl_Q

(32b): hěn dà de yī zhāng zhuōzi "a very big table" — pre-DP modifier

Mod adjoins as 2-part of D (D has only Q as 1-part, so it has room).
Contrast with (28c) where Mod is 2-part of Cl. Same structure
blocks wh-extraction in (39b): D is full, Num cannot subjoin.
```
D
  @Q: zhāng      Mod: de
    Num: yī  Cl     @Deg: dà-de
               N      A    Adv: hěn
```
Parthood: N <₁ Cl <₁ Q, Num <₂ Q, Q <₁ D, Mod <₂ D. 

def Phenomena.Classifiers.Studies.WangSun2026.preDp_D : MereologicalSyntax.SynObj

Equations

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

(45b): sān kē "three (CL)" — measure phrase without N

Classifier independent of noun: Cl has no N subjoined.
```
@PRED: duō
  Deg
    Q          A
    Num: sān   Cl: kē
```
Cl <₁ Q, Num <₂ Q, Q <₁ Deg, A <₂ Deg, Deg <₁ Pred. 

def Phenomena.Classifiers.Studies.WangSun2026.meas_Cl : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.meas_Cl = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Cl

def Phenomena.Classifiers.Studies.WangSun2026.meas_Num : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.meas_Num = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Num

def Phenomena.Classifiers.Studies.WangSun2026.meas_Q : MereologicalSyntax.SynObj

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.meas_A : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.meas_A = MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.A

def Phenomena.Classifiers.Studies.WangSun2026.meas_Deg : MereologicalSyntax.SynObj

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.meas_Pred : MereologicalSyntax.SynObj

Equations

• Phenomena.Classifiers.Studies.WangSun2026.meas_Pred = MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.Pred Phenomena.Classifiers.Studies.WangSun2026.meas_Deg

Prediction 1: Q is full — no modifier can intervene

Q has both a 1-part (Cl) and a 2-part (Num). By Dimensionality,
no further subjunction to Q is possible. This derives the ban on
degree-modified adjectives between Num and Cl (examples 4c, 29a). 

theorem Phenomena.Classifiers.Studies.WangSun2026.q_is_full : basic_Q.isFull = true

theorem Phenomena.Classifiers.Studies.WangSun2026.cannot_subjoin_to_q : MereologicalSyntax.subjoin (MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Mod) basic_Q = none

theorem Phenomena.Classifiers.Studies.WangSun2026.cl_has_room : basic_Cl.isFull = false

Cl has only N as 1-part — it has room for Mod as 2-part.

theorem Phenomena.Classifiers.Studies.WangSun2026.modification_contrast : basic_Cl.isFull = false ∧ basic_Q.isFull = true

The modification contrast: Mod CAN be 2-part of Cl (has room) but CANNOT be part of Q (full). This derives (28a) vs (29a).

theorem Phenomena.Classifiers.Studies.WangSun2026.postCl_cl_still_visible : MereologicalSyntax.labelInOnePartChain MereologicalSyntax.MLabel.Cl postCl_D = true

(28c): post-Cl modification preserves Cl visibility from D. Adding Mod as Cl's 2-part does not disrupt the 1-part chain D → Q → Cl, so the classifier retains its sortal reading.

Prediction 1b: Classifier independence from nouns

(45b) shows a classifier with no N subjoined — the classifier
functions as a measure phrase in a degree construction. 

theorem Phenomena.Classifiers.Studies.WangSun2026.meas_cl_has_no_noun : MereologicalSyntax.SynObj.containsLabel MereologicalSyntax.MLabel.N meas_Cl = false

Cl has no N as subpart in (45b): classifier is structurally independent of nouns.

theorem Phenomena.Classifiers.Studies.WangSun2026.meas_cl_visible : MereologicalSyntax.labelInOnePartChain MereologicalSyntax.MLabel.Cl meas_Pred = true

Cl is still in Pred's 1-part chain despite having no N.

Prediction 2: Cl spells out at Q

Q's complementation line (1-part chain) includes both Q and Cl.
The classifier word is realized at Q via collective spell-out.
Extracting the classifier therefore means extracting Q, which also
contains Num as 2-part — [Cl-N] cannot topicalize without Num
(examples 5c, 14a). 

theorem Phenomena.Classifiers.Studies.WangSun2026.q_compline : basic_Q.compLine = [MereologicalSyntax.MLabel.Q, MereologicalSyntax.MLabel.Cl, MereologicalSyntax.MLabel.N]

theorem Phenomena.Classifiers.Studies.WangSun2026.cl_in_q_spellout : basic_Q.compLine.contains MereologicalSyntax.MLabel.Cl = true

theorem Phenomena.Classifiers.Studies.WangSun2026.q_contains_both : MereologicalSyntax.SynObj.containsLabel MereologicalSyntax.MLabel.Cl basic_Q = true ∧ MereologicalSyntax.SynObj.containsLabel MereologicalSyntax.MLabel.Num basic_Q = true

Q contains both Cl and Num: extracting Q extracts both.

Prediction 3: 的 de changes Cl visibility from D

**Without 的**: Cl <₁ Q <₁ D — within-dimension transitivity applies.
Cl is in D's 1-part chain, so Cl's semantic content (sortal meaning,
e.g., "real glass") contributes to D's referential interpretation.

**With 的**: Cl <₁ Q <₁ Mod ∧₂ D — cross-dimension path. Cl is NOT
in D's 1-part chain (D's 1-part chain goes through N only). Cl's
content is invisible to D → abstract measure reading ("glassful"). 

theorem Phenomena.Classifiers.Studies.WangSun2026.cl_visible_without_de : MereologicalSyntax.labelInOnePartChain MereologicalSyntax.MLabel.Cl noDe_D = true

theorem Phenomena.Classifiers.Studies.WangSun2026.cl_invisible_with_de : MereologicalSyntax.labelInOnePartChain MereologicalSyntax.MLabel.Cl de_D = false

theorem Phenomena.Classifiers.Studies.WangSun2026.de_changes_visibility : MereologicalSyntax.labelInOnePartChain MereologicalSyntax.MLabel.Cl noDe_D = true ∧ MereologicalSyntax.labelInOnePartChain MereologicalSyntax.MLabel.Cl de_D = false

The de contrast: same classifier, different visibility.

Prediction 3b: 的 detaches N from Cl

The key structural difference: without 的, N is 1-part of Cl
(N <₁ Cl); with 的, Cl is bare (no N) and N is directly 1-part
of D (N <₁ D). This is NOT movement — it is a different
derivation path (different subjunction targets). 

theorem Phenomena.Classifiers.Studies.WangSun2026.noDe_n_inside_cl : noDe_Cl.onePart = some noDe_N

Without 的: N is inside Cl (N <₁ Cl).

theorem Phenomena.Classifiers.Studies.WangSun2026.de_cl_is_bare : de_Cl.onePart = none

With 的: Cl is bare — no N subjoined to it.

Prediction 3c: Two modifier positions

Post-Cl (28c): Mod <₂ Cl. D has only Q as 1-part (not full).
Pre-DP (32b): Mod <₂ D. D is full (Q + Mod).
Both are grammatical, but the pre-DP structure blocks
wh-movement because D is full (see Prediction 5). 

theorem Phenomena.Classifiers.Studies.WangSun2026.preDp_D_is_full : preDp_D.isFull = true

Pre-DP modifier: D is full.

theorem Phenomena.Classifiers.Studies.WangSun2026.postCl_D_not_full : postCl_D.isFull = false

Post-Cl modifier: D is NOT full (only Q as 1-part).

Prediction 4: N is always visible from D

Regardless of 的, N is always directly in D's 1-part chain:
without 的, N <₁ Cl <₁ Q <₁ D; with 的, N <₁ D.
The noun's denotation always contributes to the referent. 

theorem Phenomena.Classifiers.Studies.WangSun2026.n_visible_without_de : MereologicalSyntax.labelInOnePartChain MereologicalSyntax.MLabel.N noDe_D = true

theorem Phenomena.Classifiers.Studies.WangSun2026.n_visible_with_de : MereologicalSyntax.labelInOnePartChain MereologicalSyntax.MLabel.N de_D = true

Prediction 5: Wh-island via dimensionality (§5)

In (39a), D has only Q as 1-part (no Mod). D is not full, so
Num (the wh-phrase jǐ) can subjoin to D as its 2-part — the
intermediate step needed for wh-movement to C.

In (39b), Mod is 2-part of D (pre-nominal modifier). D is full.
Num cannot subjoin to D → wh-movement is blocked. 

theorem Phenomena.Classifiers.Studies.WangSun2026.wh_ok_without_mod : (MereologicalSyntax.subjoin (MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Num) (MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.D basic_Q)).isSome = true

(39a): D without Mod has room — Num can subjoin.

theorem Phenomena.Classifiers.Studies.WangSun2026.wh_blocked_with_mod : (MereologicalSyntax.subjoin (MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Num) (MereologicalSyntax.SynObj.sub₁₂ MereologicalSyntax.MLabel.D basic_Q modPhrase)).isSome = false

(39b): D with Mod is full — Num blocked.

theorem Phenomena.Classifiers.Studies.WangSun2026.wh_dimensionality_contrast : (MereologicalSyntax.subjoin (MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Num) (MereologicalSyntax.SynObj.sub₁ MereologicalSyntax.MLabel.D basic_Q)).isSome = true ∧ (MereologicalSyntax.subjoin (MereologicalSyntax.SynObj.leaf MereologicalSyntax.MLabel.Num) (MereologicalSyntax.SynObj.sub₁₂ MereologicalSyntax.MLabel.D basic_Q modPhrase)).isSome = false

The wh-island contrast: same Q, different D dimensionality.

inductive Phenomena.Classifiers.Studies.WangSun2026.ClReading : Type

Reading of a classifier determined by its structural visibility from D. When Cl is in D's 1-part chain, the classifier denotes a concrete object (sortal). When invisible, it denotes an abstract unit (mensural).

• sortal : ClReading
• mensural : ClReading

instance Phenomena.Classifiers.Studies.WangSun2026.instDecidableEqClReading : DecidableEq ClReading

Equations

• Phenomena.Classifiers.Studies.WangSun2026.instDecidableEqClReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Classifiers.Studies.WangSun2026.instBEqClReading : BEq ClReading

Equations

• Phenomena.Classifiers.Studies.WangSun2026.instBEqClReading = { beq := Phenomena.Classifiers.Studies.WangSun2026.instBEqClReading.beq }

def Phenomena.Classifiers.Studies.WangSun2026.instBEqClReading.beq : ClReading → ClReading → Bool

Equations

• Phenomena.Classifiers.Studies.WangSun2026.instBEqClReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Classifiers.Studies.WangSun2026.instReprClReading : Repr ClReading

Equations

• Phenomena.Classifiers.Studies.WangSun2026.instReprClReading = { reprPrec := Phenomena.Classifiers.Studies.WangSun2026.instReprClReading.repr }

def Phenomena.Classifiers.Studies.WangSun2026.instReprClReading.repr : ClReading → ℕ → Std.Format

Equations

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

def Phenomena.Classifiers.Studies.WangSun2026.classifierReading (d : MereologicalSyntax.SynObj) : ClReading

Equations

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

theorem Phenomena.Classifiers.Studies.WangSun2026.noDe_is_sortal : classifierReading noDe_D = ClReading.sortal

theorem Phenomena.Classifiers.Studies.WangSun2026.de_is_mensural : classifierReading de_D = ClReading.mensural

theorem Phenomena.Classifiers.Studies.WangSun2026.both_positions_sortal : classifierReading postCl_D = ClReading.sortal ∧ classifierReading preDp_D = ClReading.sortal

Both modifier positions (post-Cl and pre-DP) preserve Cl visibility from D, so the classifier retains its sortal reading regardless of where Mod attaches.

theorem Phenomena.Classifiers.Studies.WangSun2026.bei_can_be_mensural : Fragments.Mandarin.Classifiers.bei.isMensural = true

杯 bēi (glass) is the classifier in examples (33)–(34). It has isMensural = true, indicating it CAN function as a measure phrase. Whether it DOES have a mensural reading is determined by the structure (§4 above), not by the lexical entry alone.

theorem Phenomena.Classifiers.Studies.WangSun2026.zhang_is_sortal : Fragments.Mandarin.Classifiers.zhang.isMensural = false

张 zhāng (flat surface) is the classifier in the basic structure (26b) and modification examples (28)–(29). It is a pure sortal classifier — not lexically mensural.

theorem Phenomena.Classifiers.Studies.WangSun2026.ge_is_default : Fragments.Mandarin.Classifiers.ge.isDefault = true

个 gè (general) is the default classifier in the dislocation examples (5c), (13b), (14a).

Both @cite{borer-2005} and @cite{wang-sun-2026} place Q below D and above N in the nominal spine, and both treat classifiers as independent of nouns. The mereological analysis adds a structural explanation for the 的-contrast that Borer's theory does not directly address: without 的, the classifier is visible to D (sortal); with 的, it is invisible (mensural).

theorem Phenomena.Classifiers.Studies.WangSun2026.noDe_matches_borer_spine : noDe_D.compLine = [MereologicalSyntax.MLabel.D, MereologicalSyntax.MLabel.Q, MereologicalSyntax.MLabel.Cl, MereologicalSyntax.MLabel.N]

The 1-part chain from D (without 的) follows the ordering D → Q → Cl → N. Two differences from @cite{borer-2005}'s EP (D → Num → Q → n → N): (1) n (categorizer) is absent in the mereological analysis; (2) Num is Q's 2-part here (outside the 1-part chain), whereas Borer places Num above Q in the spine. Both frameworks agree on D > Q > N ordering and on Q as the individuation locus.

theorem Phenomena.Classifiers.Studies.WangSun2026.q_is_individuation_locus : noDe_D.compLine.contains MereologicalSyntax.MLabel.Q = true

Q is the individuation locus in both frameworks. Borer: Q hosts CL#/Div, converting CUM → QUA. Wang & Sun: Cl subjoins to Q as 1-part; Q spells out the classifier.

theorem Phenomena.Classifiers.Studies.WangSun2026.bei_end_to_end : Fragments.Mandarin.Classifiers.bei.isMensural = true ∧ classifierReading noDe_D = ClReading.sortal ∧ classifierReading de_D = ClReading.mensural ∧ noDe_D.compLine = [MereologicalSyntax.MLabel.D, MereologicalSyntax.MLabel.Q, MereologicalSyntax.MLabel.Cl, MereologicalSyntax.MLabel.N]

End-to-end argumentation for 杯 bēi:

1. Fragment: bēi has mensural affordance (isMensural = true)
2. Without 的: Cl visible from D → sortal reading (real glass)
3. With 的: Cl invisible from D → mensural reading (glassful)
4. Without-的 spine matches @cite{borer-2005}'s nominal EP

theorem Phenomena.Classifiers.Studies.WangSun2026.modification_end_to_end : basic_Cl.isFull = false ∧ basic_Q.isFull = true ∧ classifierReading postCl_D = ClReading.sortal

End-to-end for modification: Cl has room for Mod (derives 28c), Q is full (blocks 29a), and post-Cl modification preserves Cl visibility from D (sortal reading maintained).

The structural predictions in §§ 3–5 determine syntactic visibility. This section connects visibility to @cite{borer-2005}'s mereological semantics via the bridge in Interpretation.lean: visible Cl → QUA (count/sortal); invisible Cl → root preserved (mass/mensural).

theorem Phenomena.Classifiers.Studies.WangSun2026.noDe_is_qua {α : Type u_1} [SemilatticeSup α] (P : α → Prop) : Mereology.QUA (MereologicalSyntax.nominalDenotation noDe_D P)

Without 的: Cl visible → denotation is individuated → QUA.

theorem Phenomena.Classifiers.Studies.WangSun2026.de_preserves_root {α : Type u_1} [SemilatticeSup α] (P : α → Prop) : MereologicalSyntax.nominalDenotation de_D P = P

With 的: Cl invisible → denotation equals the root predicate.

theorem Phenomena.Classifiers.Studies.WangSun2026.de_is_cum {α : Type u_1} [SemilatticeSup α] (P : α → Prop) (hc : Mereology.CUM P) : Mereology.CUM (MereologicalSyntax.nominalDenotation de_D P)

With 的 and a cumulative root: denotation is CUM (mass/mensural).

theorem Phenomena.Classifiers.Studies.WangSun2026.bei_semantic_contrast {α : Type u_1} [SemilatticeSup α] (P : α → Prop) (hc : Mereology.CUM P) : Mereology.QUA (MereologicalSyntax.nominalDenotation noDe_D P) ∧ Mereology.CUM (MereologicalSyntax.nominalDenotation de_D P)

End-to-end 的-contrast: same root, different structure, opposite mereological properties.

End-to-end argumentation connecting three independent theories:

1. **@cite{chierchia-1998}**: Mandarin is [+arg, -pred] → nouns are
   kind-denoting → bare nouns are arguments → classifiers required.
2. **@cite{borer-2005}**: Roots denote cumulative (CUM) predicates.
   The Q head hosts individuation (Div), converting CUM → QUA.
   Classifiers spell out at Q.
3. **@cite{wang-sun-2026}**: Mereological syntax determines whether
   Cl is visible from D via 1-part chain transitivity. Visible Cl → QUA
   (sortal); invisible Cl → CUM (mensural). The particle 的 changes
   dimensional attachment, toggling visibility.

The CUM P hypothesis in `bei_semantic_contrast` IS Borer's thesis
instantiated for Chierchia's [+arg, -pred] languages: root predicates
are cumulative because they denote kind-level extensions (closed under
join). 

theorem Phenomena.Classifiers.Studies.WangSun2026.mandarin_needs_classifiers : Fragments.Mandarin.Nouns.mandarinMapping = Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.argOnly

Mandarin's NMP is [+arg, -pred]: nouns denote kinds, requiring classifiers for counting. This is the typological precondition for the entire mereological analysis.

theorem Phenomena.Classifiers.Studies.WangSun2026.full_chain {α : Type u_1} [SemilatticeSup α] (P : α → Prop) (hc : Mereology.CUM P) : Fragments.Mandarin.Nouns.mandarinMapping = Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.argOnly ∧ Fragments.Mandarin.Classifiers.bei.isMensural = true ∧ MereologicalSyntax.individuates noDe_D = true ∧ MereologicalSyntax.individuates de_D = false ∧ Mereology.QUA (MereologicalSyntax.nominalDenotation noDe_D P) ∧ Mereology.CUM (MereologicalSyntax.nominalDenotation de_D P)

The Chierchia–Borer–Wang&Sun chain for 杯 bēi:

1. Mandarin NMP = argOnly → classifiers required (Chierchia)
2. bēi has mensural affordance (Fragment)
3. Without 的: Cl visible → QUA (Borer + Wang&Sun)
4. With 的: Cl invisible → CUM under Borer's thesis
5. Same root, opposite mereological properties (Interpretation)