Qin 2025: canonical and non-canonical roots

[Qin25]

The canonical-typology space of roots over the formal base definition of Morphology/Root/Basic.lean: four canonicity criteria (Table 1) — C1 boundness, C2 positional flexibility, C3 phonological richness, C4 meaning lexicality — spanning a 16-cell space anchored by the canonical root, with Fig. 1's tiers counting the ways of failing k criteria. The Mandarin case study classifies 122 morphemes in the space; flagship rows here run from canonical 厂 chǎng to the maximally non-canonical toneless 边 -bian and 个 -ge (tonelessness diagnosing phonological deficiency in a tone language).

The paper's -fer case makes the base definition's formal character exact: -fer is a morphological core despite "lacking identifiable meaning" — the roothood judgment is "formal-based", not semantic (fer_core; the contentfulness-gated alternative it contrasts with is Studies/Haspelmath2025Root.lean).

Main results

• fer_core — -fer is a morphological core with no semantic input.
• Row, Row.violations, Row.IsCanonical — the four-criterion space; space_card, tier_card — Fig. 1's 16 cells and binomial tiers.
• chang, bu, ba, xing, bian, ge — Mandarin rows with their paper-assigned judgments (mandarin_tiers).

The -fer witness

def Qin2025.re : Morphology.Morph

The bound prefix of refer.

Equations

• Qin2025.re = Morphology.Morph.pref "re"

def Qin2025.fer : Morphology.Morph

-fer, a bound root with no identifiable meaning.

Equations

• Qin2025.fer = Morphology.Morph.root "fer"

def Qin2025.con : Morphology.Morph

The bound prefix of confer.

Equations

• Qin2025.con = Morphology.Morph.pref "con"

def Qin2025.ferWords : List (List Morphology.Morph)

The mini-fragment: refer and confer, both free forms, primary since neither re-, con-, nor -fer is free.

Equations

• Qin2025.ferWords = [[Qin2025.re, Qin2025.fer], [Qin2025.con, Qin2025.fer]]

theorem Qin2025.fer_core : fer.IsCoreIn ferWords ferWords

-fer is a morphological core: it occurs in the primary word refer.

The four criteria and the theoretical space

structure Qin2025.Row : Type

A morpheme's judgment on the four canonicity criteria (Table 1), as the survey's classification outcomes: C1 free, C2 positionally flexible, C3 phonologically rich, C4 lexical in meaning.

• c1 : Bool

  C1: free rather than bound.

• c2 : Bool

  C2: positionally flexible rather than fixed.

• c3 : Bool

  C3: phonologically rich rather than deficient.

• c4 : Bool

  C4: lexical rather than less lexical in meaning.

@[implicit_reducible]

instance Qin2025.instDecidableEqRow : DecidableEq Row

Equations

• Qin2025.instDecidableEqRow = Qin2025.instDecidableEqRow.decEq

def Qin2025.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def Qin2025.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Qin2025.instReprRow : Repr Row

Equations

• Qin2025.instReprRow = { reprPrec := Qin2025.instReprRow.repr }

@[implicit_reducible]

instance Qin2025.instFintypeRow : Fintype Row

Equations

• Qin2025.instFintypeRow = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × (_ : Bool) × Bool) Qin2025.Row.proxyTypeEquiv

def Qin2025.Row.violations (r : Row) : ℕ

The number of criteria a row fails — its distance from the canonical point.

Equations

• r.violations = (((if r.c1 = true then 0 else 1) + if r.c2 = true then 0 else 1) + if r.c3 = true then 0 else 1) + if r.c4 = true then 0 else 1

def Qin2025.Row.IsCanonical (r : Row) : Prop

A canonical root satisfies all four criteria.

Equations

• r.IsCanonical = (r.violations = 0)

@[implicit_reducible]

instance Qin2025.instDecidableIsCanonical (r : Row) : Decidable r.IsCanonical

Equations

• Qin2025.instDecidableIsCanonical r = Qin2025.instDecidableIsCanonical._aux_1 r

theorem Qin2025.space_card : Fintype.card Row = 16

The theoretical space of roots has 16 cells (Fig. 1).

theorem Qin2025.tier_card (k : Fin 5) : {r : Row | r.violations = ↑k}.card = Nat.choose 4 ↑k

Fig. 1's tiers: 4.choose k ways to fail exactly k criteria — "there are 15 different ways for an instance to be non-canonical, while only one way for an instance to be canonical".

Mandarin rows (§4, appendix)

Judgments transcribed from the case study; glosses from the paper.

def Qin2025.chang : Row

厂 chǎng 'a factory': free, flexible (fúzhuang-chǎng ~ chǎng-shang), toned, fully referential — canonical.

Equations

• Qin2025.chang = { c1 := true, c2 := true, c3 := true, c4 := true }

def Qin2025.bu : Row

不 bù 'generalized negation': deviates on C4 alone.

Equations

• Qin2025.bu = { c1 := true, c2 := true, c3 := true, c4 := false }

def Qin2025.ba : Row

霸 -bà 'a person outstanding in a field': bound and positionally fixed.

Equations

• Qin2025.ba = { c1 := false, c2 := false, c3 := true, c4 := true }

def Qin2025.xing : Row

性 -xìng 'to form nouns or adjectives indicating a property': bound, fixed, and schematic in meaning.

Equations

• Qin2025.xing = { c1 := false, c2 := false, c3 := true, c4 := false }

def Qin2025.bian : Row

边 -bian 'indicating locality': bound, fixed, toneless, adding almost no meaning.

Equations

• Qin2025.bian = { c1 := false, c2 := false, c3 := false, c4 := false }

def Qin2025.ge : Row

个 -ge 'used after a demonstrative pronoun': like -bian, meeting none of the criteria.

Equations

• Qin2025.ge = { c1 := false, c2 := false, c3 := false, c4 := false }

theorem Qin2025.mandarin_tiers : chang.IsCanonical ∧ bu.violations = 1 ∧ ba.violations = 2 ∧ xing.violations = 3 ∧ bian.violations = 4 ∧ ge.violations = 4

The five Mandarin tiers, from canonical 厂 chǎng to the maximally non-canonical 边 -bian and 个 -ge.