Japanese Numeral Classifier Inventory

[Aik00] [Dow96] [Sud16]

The closed inventory of Japanese numeral classifiers (josūshi 助数詞) as a finite inductive type. Properties (form, gloss, encoded semantic parameters, dimensionality, mensural-vs-sortal, default flag) are projection functions or Decidable predicates over the type, not fields on a struct.

Architectural pilot

This file is the pilot for an enum-as-source-of-truth fragment pattern (replacing the prior list-of-records pattern). Adding a classifier means adding a constructor here; the type checker propagates the addition to every projection function and every consumer that pattern-matches on Classifier. See CHANGELOG.md 0.230.179 for the rationale.

Inventory provenance

• 27 core entries from [Dow96] (UNVERIFIED: claimed to be Table 1.1 by the prior fragment file; cited tables/page numbers not cross-checked against the monograph).
• 6 extended entries from [Dow96] (UNVERIFIED: claimed to be Table 1.2; same caveat).
• 3 additional entries (rin, kumi, daasu) from [Sud16] worked examples (eq. 4 for -rin, eq. 9a for -kumi, eq. 9b for -daasu — verified against the PDF).

Bridge to legacy

Classifier.toEntry : Classifier → ClassifierEntry is the migration seam to the old NounCategorization.ClassifierEntry record type that sibling fragments (Mandarin, Shan, Chol) and Typology/ClassifierSystem still consume. Once those fragments are migrated to the same enum pattern, both this bridge and ClassifierEntry itself can be retired.

Out of scope

• Phonological allomorphy (rendaku/sokuon: ippon/sanbon/roppon for -hon, ippiki/sanbiki/roppiki for -hiki) — would belong with Phonology/.
• Native vs Sino-Japanese numeral series split (tsu selects native hitotsu/futatsu/...; Sino-classifiers select ichi/ni/san/...).
• Inventory expansion to high-frequency classifiers not in Downing's inventory (-kai 回, -bai 倍, -ban 番, -do 度, etc.).

inductive Japanese.Classifier : Type

The closed inventory of Japanese numeral classifiers. Constructors are named by Hepburn romanization, with kanji-distinct homophones disambiguated by content (e.g., kenBuilding 軒 vs kenIncident 件).

• tsu : Classifier
• nin : Classifier
• mei : Classifier
• hiki : Classifier
• tou : Classifier
• hon : Classifier
• mai : Classifier
• ko : Classifier
• satsu : Classifier
• tsubu : Classifier
• dai : Classifier
• kenBuilding : Classifier
• kenIncident : Classifier
• ki : Classifier
• ku : Classifier
• kyoku : Classifier
• mon : Classifier
• mune : Classifier
• seki : Classifier
• soku : Classifier
• soo : Classifier
• ten : Classifier
• toori : Classifier
• tsuu : Classifier
• kabu : Classifier
• shoku : Classifier
• teki : Classifier
• sao : Classifier
• wa : Classifier
• furi : Classifier
• zen : Classifier
• kyaku : Classifier
• hai : Classifier
• rin : Classifier
• kumi : Classifier
• daasu : Classifier

@[implicit_reducible]

instance Japanese.instDecidableEqClassifier : DecidableEq Classifier

Equations

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

@[implicit_reducible]

instance Japanese.instReprClassifier : Repr Classifier

Equations

• Japanese.instReprClassifier = { reprPrec := Japanese.instReprClassifier.repr }

def Japanese.instReprClassifier.repr : Classifier → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Japanese.instReprClassifier.repr Japanese.Classifier.tsu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.tsu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.nin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.nin")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.mei prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.mei")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.hiki prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.hiki")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.tou prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.tou")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.hon prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.hon")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.mai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.mai")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.ko prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.ko")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.satsu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.satsu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.tsubu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.tsubu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.dai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.dai")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.ki prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.ki")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.ku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.ku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.kyoku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.kyoku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.mon prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.mon")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.mune prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.mune")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.seki prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.seki")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.soku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.soku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.soo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.soo")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.ten prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.ten")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.toori prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.toori")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.tsuu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.tsuu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.kabu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.kabu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.shoku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.shoku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.teki prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.teki")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.sao prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.sao")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.wa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.wa")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.furi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.furi")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.zen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.zen")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.kyaku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.kyaku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.hai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.hai")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.rin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.rin")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.kumi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.kumi")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.daasu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.daasu")).group prec✝

@[implicit_reducible]

instance Japanese.instBEqClassifier : BEq Classifier

Equations

• Japanese.instBEqClassifier = { beq := Japanese.instBEqClassifier.beq }

def Japanese.instBEqClassifier.beq : Classifier → Classifier → Bool

Equations

• Japanese.instBEqClassifier.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Japanese.Classifier.core : List Classifier

The 27 core classifiers from [Dow96] (UNVERIFIED: Table 1.1).

Equations

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

def Japanese.Classifier.extended : List Classifier

The 6 extended classifiers from [Dow96] (UNVERIFIED: Table 1.2).

Equations

• Japanese.Classifier.extended = [Japanese.Classifier.sao, Japanese.Classifier.wa, Japanese.Classifier.furi, Japanese.Classifier.zen, Japanese.Classifier.kyaku, Japanese.Classifier.hai]

def Japanese.Classifier.sudoAdditions : List Classifier

The 3 additional classifiers from [Sud16]'s worked examples (eqs. 4, 9a, 9b): -rin (flowers), -kumi (pair), -daasu (dozen).

Equations

• Japanese.Classifier.sudoAdditions = [Japanese.Classifier.rin, Japanese.Classifier.kumi, Japanese.Classifier.daasu]

def Japanese.Classifier.all : List Classifier

The full inventory: Downing core ++ Downing extended ++ Sudo additions. Source-of-truth for consumer iteration (lookup, aggregations) and the Fintype instance.

Equations

• Japanese.Classifier.all = Japanese.Classifier.core ++ Japanese.Classifier.extended ++ Japanese.Classifier.sudoAdditions

theorem Japanese.Classifier.all_nodup : all.Nodup

theorem Japanese.Classifier.mem_all (c : Classifier) : c ∈ all

@[implicit_reducible]

instance Japanese.instFintypeClassifier : Fintype Classifier

Equations

• Japanese.instFintypeClassifier = { elems := Japanese.Classifier.all.toFinset, complete := Japanese.instFintypeClassifier._proof_1 }

§1: Surface form

def Japanese.Classifier.form : Classifier → String

The kanji (or hiragana, for -tsu) form of the classifier.

Equations

• Japanese.Classifier.tsu.form = "つ"
• Japanese.Classifier.nin.form = "人"
• Japanese.Classifier.mei.form = "名"
• Japanese.Classifier.hiki.form = "匹"
• Japanese.Classifier.tou.form = "頭"
• Japanese.Classifier.hon.form = "本"
• Japanese.Classifier.mai.form = "枚"
• Japanese.Classifier.ko.form = "個"
• Japanese.Classifier.satsu.form = "冊"
• Japanese.Classifier.tsubu.form = "粒"
• Japanese.Classifier.dai.form = "台"
• Japanese.Classifier.kenBuilding.form = "軒"
• Japanese.Classifier.kenIncident.form = "件"
• Japanese.Classifier.ki.form = "機"
• Japanese.Classifier.ku.form = "句"
• Japanese.Classifier.kyoku.form = "曲"
• Japanese.Classifier.mon.form = "問"
• Japanese.Classifier.mune.form = "棟"
• Japanese.Classifier.seki.form = "隻"
• Japanese.Classifier.soku.form = "足"
• Japanese.Classifier.soo.form = "艘"
• Japanese.Classifier.ten.form = "点"
• Japanese.Classifier.toori.form = "通り"
• Japanese.Classifier.tsuu.form = "通"
• Japanese.Classifier.kabu.form = "株"
• Japanese.Classifier.shoku.form = "食"
• Japanese.Classifier.teki.form = "滴"
• Japanese.Classifier.sao.form = "竿"
• Japanese.Classifier.wa.form = "羽"
• Japanese.Classifier.furi.form = "振"
• Japanese.Classifier.zen.form = "膳"
• Japanese.Classifier.kyaku.form = "脚"
• Japanese.Classifier.hai.form = "杯"
• Japanese.Classifier.rin.form = "輪"
• Japanese.Classifier.kumi.form = "組"
• Japanese.Classifier.daasu.form = "ダース"

def Japanese.Classifier.romaji : Classifier → String

Hepburn romanization of the classifier.

Equations

• Japanese.Classifier.tsu.romaji = "tsu"
• Japanese.Classifier.nin.romaji = "nin"
• Japanese.Classifier.mei.romaji = "mei"
• Japanese.Classifier.hiki.romaji = "hiki"
• Japanese.Classifier.tou.romaji = "tou"
• Japanese.Classifier.hon.romaji = "hon"
• Japanese.Classifier.mai.romaji = "mai"
• Japanese.Classifier.ko.romaji = "ko"
• Japanese.Classifier.satsu.romaji = "satsu"
• Japanese.Classifier.tsubu.romaji = "tsubu"
• Japanese.Classifier.dai.romaji = "dai"
• Japanese.Classifier.kenBuilding.romaji = "ken"
• Japanese.Classifier.kenIncident.romaji = "ken"
• Japanese.Classifier.ki.romaji = "ki"
• Japanese.Classifier.ku.romaji = "ku"
• Japanese.Classifier.kyoku.romaji = "kyoku"
• Japanese.Classifier.mon.romaji = "mon"
• Japanese.Classifier.mune.romaji = "mune"
• Japanese.Classifier.seki.romaji = "seki"
• Japanese.Classifier.soku.romaji = "soku"
• Japanese.Classifier.soo.romaji = "soo"
• Japanese.Classifier.ten.romaji = "ten"
• Japanese.Classifier.toori.romaji = "toori"
• Japanese.Classifier.tsuu.romaji = "tsuu"
• Japanese.Classifier.kabu.romaji = "kabu"
• Japanese.Classifier.shoku.romaji = "shoku"
• Japanese.Classifier.teki.romaji = "teki"
• Japanese.Classifier.sao.romaji = "sao"
• Japanese.Classifier.wa.romaji = "wa"
• Japanese.Classifier.furi.romaji = "furi"
• Japanese.Classifier.zen.romaji = "zen"
• Japanese.Classifier.kyaku.romaji = "kyaku"
• Japanese.Classifier.hai.romaji = "hai"
• Japanese.Classifier.rin.romaji = "rin"
• Japanese.Classifier.kumi.romaji = "kumi"
• Japanese.Classifier.daasu.romaji = "daasu"

def Japanese.Classifier.gloss : Classifier → String

A short English gloss describing the classifier's selection criterion.

Equations

• Japanese.Classifier.tsu.gloss = "general"
• Japanese.Classifier.nin.gloss = "person"
• Japanese.Classifier.mei.gloss = "person.formal"
• Japanese.Classifier.hiki.gloss = "small.animal"
• Japanese.Classifier.tou.gloss = "large.animal"
• Japanese.Classifier.hon.gloss = "long.thin"
• Japanese.Classifier.mai.gloss = "flat.thin"
• Japanese.Classifier.ko.gloss = "small.round"
• Japanese.Classifier.satsu.gloss = "bound.volume"
• Japanese.Classifier.tsubu.gloss = "grain"
• Japanese.Classifier.dai.gloss = "machine/vehicle"
• Japanese.Classifier.kenBuilding.gloss = "building"
• Japanese.Classifier.kenIncident.gloss = "incident"
• Japanese.Classifier.ki.gloss = "air.vehicle"
• Japanese.Classifier.ku.gloss = "poem"
• Japanese.Classifier.kyoku.gloss = "music.piece"
• Japanese.Classifier.mon.gloss = "question"
• Japanese.Classifier.mune.gloss = "building.roof"
• Japanese.Classifier.seki.gloss = "large.boat"
• Japanese.Classifier.soku.gloss = "footwear.pair"
• Japanese.Classifier.soo.gloss = "small.boat"
• Japanese.Classifier.ten.gloss = "point/item"
• Japanese.Classifier.toori.gloss = "method/way"
• Japanese.Classifier.tsuu.gloss = "letter/document"
• Japanese.Classifier.kabu.gloss = "rooted.plant"
• Japanese.Classifier.shoku.gloss = "meal"
• Japanese.Classifier.teki.gloss = "drop"
• Japanese.Classifier.sao.gloss = "pole"
• Japanese.Classifier.wa.gloss = "bird"
• Japanese.Classifier.furi.gloss = "sword"
• Japanese.Classifier.zen.gloss = "tray/chopsticks"
• Japanese.Classifier.kyaku.gloss = "legged.furniture"
• Japanese.Classifier.hai.gloss = "cupful"
• Japanese.Classifier.rin.gloss = "flower"
• Japanese.Classifier.kumi.gloss = "pair/group"
• Japanese.Classifier.daasu.gloss = "dozen"

§2: Semantic parameters and shape

def Japanese.Classifier.encodes : Classifier → List NounCategorization.SemanticParameter

The semantic parameters this classifier encodes ([Aik00] typological vocabulary).

Every constructor has an explicit arm; no fall-through. Adding a classifier requires deciding what it encodes — the type checker enforces it.

Equations

• Japanese.Classifier.tsu.encodes = []
• Japanese.Classifier.nin.encodes = [NounCategorization.SemanticParameter.humanness]
• Japanese.Classifier.mei.encodes = [NounCategorization.SemanticParameter.humanness, NounCategorization.SemanticParameter.register]
• Japanese.Classifier.hiki.encodes = [NounCategorization.SemanticParameter.animacy, NounCategorization.SemanticParameter.size]
• Japanese.Classifier.tou.encodes = [NounCategorization.SemanticParameter.animacy, NounCategorization.SemanticParameter.size]
• Japanese.Classifier.wa.encodes = [NounCategorization.SemanticParameter.animacy]
• Japanese.Classifier.hon.encodes = [NounCategorization.SemanticParameter.shape]
• Japanese.Classifier.mai.encodes = [NounCategorization.SemanticParameter.shape]
• Japanese.Classifier.ko.encodes = [NounCategorization.SemanticParameter.shape]
• Japanese.Classifier.satsu.encodes = [NounCategorization.SemanticParameter.shape]
• Japanese.Classifier.tsubu.encodes = [NounCategorization.SemanticParameter.shape]
• Japanese.Classifier.sao.encodes = [NounCategorization.SemanticParameter.shape]
• Japanese.Classifier.rin.encodes = [NounCategorization.SemanticParameter.shape, NounCategorization.SemanticParameter.boundedness]
• Japanese.Classifier.dai.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.kenBuilding.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.kenIncident.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.ki.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.ku.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.kyoku.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.mon.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.mune.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.seki.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.soku.encodes = [NounCategorization.SemanticParameter.function, NounCategorization.SemanticParameter.arrangement]
• Japanese.Classifier.soo.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.ten.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.toori.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.tsuu.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.kabu.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.furi.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.zen.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.kyaku.encodes = [NounCategorization.SemanticParameter.function]
• Japanese.Classifier.hai.encodes = [NounCategorization.SemanticParameter.quanta]
• Japanese.Classifier.shoku.encodes = [NounCategorization.SemanticParameter.quanta]
• Japanese.Classifier.teki.encodes = [NounCategorization.SemanticParameter.quanta]
• Japanese.Classifier.daasu.encodes = [NounCategorization.SemanticParameter.quanta]
• Japanese.Classifier.kumi.encodes = [NounCategorization.SemanticParameter.arrangement, NounCategorization.SemanticParameter.quanta]

def Japanese.Classifier.shapeDim : Classifier → Option NounCategorization.ShapeDimension

Shape dimensionality sub-classification per [All77]'s 1D/2D/3D scheme (cf. [Dow96]). Only meaningful when encodes includes .shape.

-rin 輪 is left as none: although it encodes shape, it tracks boundedness/ring-form (wheels, single blossoms) rather than fitting cleanly on the 1D/2D/3D axis. See encodes, where -rin carries .shape and .boundedness.

Equations

• Japanese.Classifier.hon.shapeDim = some NounCategorization.ShapeDimension.oneD
• Japanese.Classifier.sao.shapeDim = some NounCategorization.ShapeDimension.oneD
• Japanese.Classifier.mai.shapeDim = some NounCategorization.ShapeDimension.twoD
• Japanese.Classifier.satsu.shapeDim = some NounCategorization.ShapeDimension.twoD
• Japanese.Classifier.ko.shapeDim = some NounCategorization.ShapeDimension.threeD
• Japanese.Classifier.tsubu.shapeDim = some NounCategorization.ShapeDimension.threeD
• x✝.shapeDim = none

§3: Property predicates

def Japanese.Classifier.IsMensural (c : Classifier) : Prop

A classifier is mensural if it counts entities by a measure (containers, portions, drops, fixed-quantity multiples) rather than by atomic instances. -daasu ダース (← English "dozen") is mensural since it counts in fixed groups of 12.

Equations

• c.IsMensural = (c = Japanese.Classifier.hai ∨ c = Japanese.Classifier.shoku ∨ c = Japanese.Classifier.teki ∨ c = Japanese.Classifier.daasu)

@[implicit_reducible]

instance Japanese.Classifier.instDecidablePredIsMensural : DecidablePred IsMensural

Equations

• c.instDecidablePredIsMensural = Japanese.Classifier.instDecidablePredIsMensural._aux_1 c

def Japanese.Classifier.IsDefault (c : Classifier) : Prop

A classifier is the default (semantically bleached, residue) classifier of the language. Japanese: tsu.

Equations

• c.IsDefault = (c = Japanese.Classifier.tsu)

@[implicit_reducible]

instance Japanese.Classifier.instDecidablePredIsDefault : DecidablePred IsDefault

Equations

• c.instDecidablePredIsDefault = Japanese.Classifier.instDecidablePredIsDefault._aux_1 c

def Japanese.Classifier.Encodes (c : Classifier) (p : NounCategorization.SemanticParameter) : Prop

c encodes the semantic parameter p iff p ∈ c.encodes.

Equations

• c.Encodes p = (p ∈ c.encodes)

@[implicit_reducible]

instance Japanese.Classifier.instDecidableEncodes (c : Classifier) (p : NounCategorization.SemanticParameter) : Decidable (c.Encodes p)

Equations

• c.instDecidableEncodes p = Japanese.Classifier.instDecidableEncodes._aux_1 c p

§4: Lookup and aggregations

def Japanese.Classifier.defaultClassifier? : Option Classifier

The default classifier of Japanese, derived from IsDefault.

Equations

• Japanese.Classifier.defaultClassifier? = List.find? (fun (c : Japanese.Classifier) => decide c.IsDefault) Japanese.Classifier.all

def Japanese.Classifier.lookup (s : String) : Option Classifier

Lookup a classifier by surface form. Returns none if the form is not in the inventory.

Equations

• Japanese.Classifier.lookup s = List.find? (fun (c : Japanese.Classifier) => decide (c.form = s)) Japanese.Classifier.all

def Japanese.Classifier.allEncodedParams : List NounCategorization.SemanticParameter

The list of all semantic parameters encoded by some classifier in the inventory (with duplicates removed). Used by Fragments/Japanese/ClassifierSystem to compute preferredSemantics.

Equations

• Japanese.Classifier.allEncodedParams = (List.flatMap Japanese.Classifier.encodes Japanese.Classifier.all).eraseDups

§5: Bridge to legacy ClassifierEntry

Migration seam: Typology/ClassifierSystem.lean and the sibling fragments (Mandarin, Shan, Chol) still consume NounCategorization. ClassifierEntry. toEntry projects a typed Classifier back to the legacy record so cross-language aggregations continue to work during the transitional period.

def Japanese.Classifier.toEntry (c : Classifier) : NounCategorization.ClassifierEntry

Convert a typed Classifier to the legacy record. Migration-seam only; new code should consume Classifier and its projections directly.

Equations

• c.toEntry = { form := c.form, gloss := c.gloss, semantics := c.encodes, isDefault := decide c.IsDefault, isMensural := decide c.IsMensural, shapeDimension := c.shapeDim }

def Japanese.Classifier.allEntries : List NounCategorization.ClassifierEntry

The full inventory as legacy records. Bridge for typology-side code that still expects List ClassifierEntry.

Equations

• Japanese.Classifier.allEntries = List.map Japanese.Classifier.toEntry Japanese.Classifier.all

§6: Structural theorems

theorem Japanese.Classifier.inventory_size : all.length = 36

The inventory has 36 classifiers (27 Downing core + 6 Downing extended + 3 Sudo examples).

theorem Japanese.Classifier.default_eq_tsu : defaultClassifier? = some tsu

The default classifier exists and is tsu.

theorem Japanese.Classifier.isDefault_iff_tsu (c : Classifier) : c.IsDefault ↔ c = tsu

tsu is the only classifier flagged as default.

theorem Japanese.Classifier.mensural_count : (List.filter (fun (c : Classifier) => decide c.IsMensural) all).length = 4

Exactly four classifiers are mensural: hai, shoku, teki, daasu.

theorem Japanese.Classifier.specific_classifiers_have_semantics (c : Classifier) : ¬c.IsDefault → ¬c.IsMensural → c.encodes ≠ []

Every non-default sortal classifier encodes at least one semantic parameter. The default tsu is the only semantically empty classifier.

theorem Japanese.Classifier.all_dimensions_attested : (∃ (c : Classifier), c.shapeDim = some NounCategorization.ShapeDimension.oneD) ∧ (∃ (c : Classifier), c.shapeDim = some NounCategorization.ShapeDimension.twoD) ∧ ∃ (c : Classifier), c.shapeDim = some NounCategorization.ShapeDimension.threeD

All three shape dimensions are attested in the inventory.

theorem Japanese.Classifier.ken_disambiguation : kenBuilding.form ≠ kenIncident.form

軒 kenBuilding and 件 kenIncident are distinct classifiers sharing the same Hepburn romanization but differing in kanji form.

theorem Japanese.Classifier.ken_homophony : kenBuilding.romaji = kenIncident.romaji

軒 and 件 share their romanization (the homophony Downing flags).