Color-term typology — substrate types and WALS data

@cite{wals-2013} (Chs 132–135) @cite{berlin-kay-1969} @cite{kay-maffi-2013}

Type-level enums + per-language profile struct for cross-linguistic color naming across @cite{wals-2013} chapters 132–135 (Kay & Maffi: number of basic color categories; green/blue and red/yellow boundary patterns), plus WALS distribution data and the principal cross-linguistic generalizations from the Berlin & Kay tradition.

Schema

• NonDerivedColorCount (Ch 132): number of non-derived basic color categories
• BasicColorCount (Ch 133): total number of basic color categories
• GreenBlueRelation (Ch 134): green/blue boundary (the classic grue distinction)
• RedYellowRelation (Ch 135): red/yellow boundary
• ColorProfile: per-language bundle (all four chapters)

Per-language data lives in Fragments/{Lang}/Color.lean.

inductive Typology.NonDerivedColorCount : Type

Number of non-derived basic color categories (WALS Ch 132, @cite{kay-maffi-2013}). Ranges from 3 to 6 along the Berlin & Kay sequence; transitional half-values represent languages with one composite category undergoing splitting.

• three : NonDerivedColorCount
• threeHalf : NonDerivedColorCount
• four : NonDerivedColorCount
• fourHalf : NonDerivedColorCount
• five : NonDerivedColorCount
• fiveHalf : NonDerivedColorCount
• six : NonDerivedColorCount

@[implicit_reducible]

instance Typology.instDecidableEqNonDerivedColorCount : DecidableEq NonDerivedColorCount

Equations

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

def Typology.instReprNonDerivedColorCount.repr : NonDerivedColorCount → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprNonDerivedColorCount : Repr NonDerivedColorCount

Equations

• Typology.instReprNonDerivedColorCount = { reprPrec := Typology.instReprNonDerivedColorCount.repr }

inductive Typology.BasicColorCount : Type

Total number of basic color categories including derived ones (WALS Ch 133, @cite{kay-maffi-2013}). Ranges from 3–4 (minimal systems) to 11 (maximal, e.g., English, Russian).

• v3to4 : BasicColorCount
• v4to5 : BasicColorCount
• v6to6h : BasicColorCount
• v7to7h : BasicColorCount
• v8to8h : BasicColorCount
• v9to10 : BasicColorCount
• v11 : BasicColorCount

@[implicit_reducible]

instance Typology.instDecidableEqBasicColorCount : DecidableEq BasicColorCount

Equations

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

@[implicit_reducible]

instance Typology.instReprBasicColorCount : Repr BasicColorCount

Equations

• Typology.instReprBasicColorCount = { reprPrec := Typology.instReprBasicColorCount.repr }

def Typology.instReprBasicColorCount.repr : BasicColorCount → Nat → Std.Format

Equations

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

inductive Typology.GreenBlueRelation : Type

How a language treats the green-blue region of color space (WALS Ch 134, @cite{kay-maffi-2013}). The classic grue / green-blue composite distinction, with several other composite patterns (with black, with yellow).

• distinct : GreenBlueRelation

  Separate terms for green and blue.

• merged : GreenBlueRelation

  A single grue term covering both green and blue.

• blackGreenBlue : GreenBlueRelation

  A single term covering black, green, and blue.

• blackBlueVsGreen : GreenBlueRelation

  Black/blue merged, green separate.

• yellowGreenBlue : GreenBlueRelation

  Yellow, green, blue all merged.

• yellowGreenVsBlue : GreenBlueRelation

  Yellow/green merged, blue separate.

• noTerm : GreenBlueRelation

  No green or blue term at all.

@[implicit_reducible]

instance Typology.instDecidableEqGreenBlueRelation : DecidableEq GreenBlueRelation

Equations

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

def Typology.instReprGreenBlueRelation.repr : GreenBlueRelation → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprGreenBlueRelation : Repr GreenBlueRelation

Equations

• Typology.instReprGreenBlueRelation = { reprPrec := Typology.instReprGreenBlueRelation.repr }

inductive Typology.RedYellowRelation : Type

How a language treats the red-yellow region of color space (WALS Ch 135, @cite{kay-maffi-2013}).

• distinct : RedYellowRelation

  Separate terms for red and yellow.

• merged : RedYellowRelation

  A single term covering both red and yellow.

• yellowGreenBlueVsRed : RedYellowRelation

  Yellow/green/blue merged, vs red.

• yellowGreenVsRed : RedYellowRelation

  Yellow/green merged, vs red.

• noTerm : RedYellowRelation

  No red or yellow term at all.

@[implicit_reducible]

instance Typology.instDecidableEqRedYellowRelation : DecidableEq RedYellowRelation

Equations

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

def Typology.instReprRedYellowRelation.repr : RedYellowRelation → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprRedYellowRelation : Repr RedYellowRelation

Equations

• Typology.instReprRedYellowRelation = { reprPrec := Typology.instReprRedYellowRelation.repr }

structure Typology.ColorProfile : Type

A language's color-naming profile across @cite{wals-2013} Chs 132–135. Coverage is sparse (~120 languages); fields are optional.

• language : String
• iso : String
• family : String
• nonDerived : Option NonDerivedColorCount

  Ch 132: non-derived basic color categories.

• basic : Option BasicColorCount

  Ch 133: total basic color categories.

• greenBlue : Option GreenBlueRelation

  Ch 134: green-blue relation.

• redYellow : Option RedYellowRelation

  Ch 135: red-yellow relation.

def Typology.instReprColorProfile.repr : ColorProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprColorProfile : Repr ColorProfile

Equations

• Typology.instReprColorProfile = { reprPrec := Typology.instReprColorProfile.repr }

def Typology.fromWALS132A : Data.WALS.F132A.NumberOfNonDerivedBasicColourCategories → NonDerivedColorCount

Convert WALS 132A non-derived-color-count values into the substrate enum.

Equations

• Typology.fromWALS132A Data.WALS.F132A.NumberOfNonDerivedBasicColourCategories.v3 = Typology.NonDerivedColorCount.three
• Typology.fromWALS132A Data.WALS.F132A.NumberOfNonDerivedBasicColourCategories.v35 = Typology.NonDerivedColorCount.threeHalf
• Typology.fromWALS132A Data.WALS.F132A.NumberOfNonDerivedBasicColourCategories.v4 = Typology.NonDerivedColorCount.four
• Typology.fromWALS132A Data.WALS.F132A.NumberOfNonDerivedBasicColourCategories.v45 = Typology.NonDerivedColorCount.fourHalf
• Typology.fromWALS132A Data.WALS.F132A.NumberOfNonDerivedBasicColourCategories.v5 = Typology.NonDerivedColorCount.five
• Typology.fromWALS132A Data.WALS.F132A.NumberOfNonDerivedBasicColourCategories.v55 = Typology.NonDerivedColorCount.fiveHalf
• Typology.fromWALS132A Data.WALS.F132A.NumberOfNonDerivedBasicColourCategories.v6 = Typology.NonDerivedColorCount.six

def Typology.fromWALS133A : Data.WALS.F133A.NumberOfBasicColourCategories → BasicColorCount

Convert WALS 133A basic-color-count values into the substrate enum.

Equations

• Typology.fromWALS133A Data.WALS.F133A.NumberOfBasicColourCategories.v34 = Typology.BasicColorCount.v3to4
• Typology.fromWALS133A Data.WALS.F133A.NumberOfBasicColourCategories.v4555 = Typology.BasicColorCount.v4to5
• Typology.fromWALS133A Data.WALS.F133A.NumberOfBasicColourCategories.v665 = Typology.BasicColorCount.v6to6h
• Typology.fromWALS133A Data.WALS.F133A.NumberOfBasicColourCategories.v775 = Typology.BasicColorCount.v7to7h
• Typology.fromWALS133A Data.WALS.F133A.NumberOfBasicColourCategories.v885 = Typology.BasicColorCount.v8to8h
• Typology.fromWALS133A Data.WALS.F133A.NumberOfBasicColourCategories.v910 = Typology.BasicColorCount.v9to10
• Typology.fromWALS133A Data.WALS.F133A.NumberOfBasicColourCategories.v11 = Typology.BasicColorCount.v11

def Typology.fromWALS134A : Data.WALS.F134A.GreenAndBlue → GreenBlueRelation

Convert WALS 134A green-blue values into the substrate enum.

Equations

• Typology.fromWALS134A Data.WALS.F134A.GreenAndBlue.greenVsBlue = Typology.GreenBlueRelation.distinct
• Typology.fromWALS134A Data.WALS.F134A.GreenAndBlue.greenBlue = Typology.GreenBlueRelation.merged
• Typology.fromWALS134A Data.WALS.F134A.GreenAndBlue.blackGreenBlue = Typology.GreenBlueRelation.blackGreenBlue
• Typology.fromWALS134A Data.WALS.F134A.GreenAndBlue.blackBlueVsGreen = Typology.GreenBlueRelation.blackBlueVsGreen
• Typology.fromWALS134A Data.WALS.F134A.GreenAndBlue.yellowGreenBlue = Typology.GreenBlueRelation.yellowGreenBlue
• Typology.fromWALS134A Data.WALS.F134A.GreenAndBlue.yellowGreenVsBlue = Typology.GreenBlueRelation.yellowGreenVsBlue
• Typology.fromWALS134A Data.WALS.F134A.GreenAndBlue.none = Typology.GreenBlueRelation.noTerm

def Typology.fromWALS135A : Data.WALS.F135A.RedAndYellow → RedYellowRelation

Convert WALS 135A red-yellow values into the substrate enum.

Equations

• Typology.fromWALS135A Data.WALS.F135A.RedAndYellow.redVsYellow = Typology.RedYellowRelation.distinct
• Typology.fromWALS135A Data.WALS.F135A.RedAndYellow.redYellow = Typology.RedYellowRelation.merged
• Typology.fromWALS135A Data.WALS.F135A.RedAndYellow.yellowGreenBlueVsRed = Typology.RedYellowRelation.yellowGreenBlueVsRed
• Typology.fromWALS135A Data.WALS.F135A.RedAndYellow.yellowGreenVsRed = Typology.RedYellowRelation.yellowGreenVsRed
• Typology.fromWALS135A Data.WALS.F135A.RedAndYellow.none = Typology.RedYellowRelation.noTerm

structure Typology.GreenBlueCounts : Type

WALS Ch 134 distribution: green-blue boundary patterns (@cite{kay-maffi-2013}, n = 120).

• distinct : Nat
• merged : Nat
• other : Nat

@[implicit_reducible]

instance Typology.instReprGreenBlueCounts : Repr GreenBlueCounts

Equations

• Typology.instReprGreenBlueCounts = { reprPrec := Typology.instReprGreenBlueCounts.repr }

def Typology.instReprGreenBlueCounts.repr : GreenBlueCounts → Nat → Std.Format

Equations

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

def Typology.GreenBlueCounts.total (c : GreenBlueCounts) : Nat

Equations

• c.total = c.distinct + c.merged + c.other

def Typology.walsGreenBlue : GreenBlueCounts

WALS Ch 134 counts (120 languages).

Equations

• Typology.walsGreenBlue = { distinct := 30, merged := 68, other := 22 }

structure Typology.RedYellowCounts : Type

WALS Ch 135 distribution: red-yellow boundary patterns (@cite{kay-maffi-2013}, n = 120).

• distinct : Nat
• merged : Nat
• other : Nat

def Typology.instReprRedYellowCounts.repr : RedYellowCounts → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprRedYellowCounts : Repr RedYellowCounts

Equations

• Typology.instReprRedYellowCounts = { reprPrec := Typology.instReprRedYellowCounts.repr }

def Typology.RedYellowCounts.total (c : RedYellowCounts) : Nat

Equations

• c.total = c.distinct + c.merged + c.other

def Typology.walsRedYellow : RedYellowCounts

WALS Ch 135 counts (120 languages).

Equations

• Typology.walsRedYellow = { distinct := 98, merged := 15, other := 7 }

theorem Typology.grue_majority : walsGreenBlue.merged > walsGreenBlue.distinct

The grue pattern (merged green/blue) is the majority for the green-blue dimension (68 of 120 = 57%), more than double the distinct-terms pattern (30). Berlin & Kay's classic finding: mid-evolution color systems collapse green and blue.

theorem Typology.red_yellow_usually_distinct : walsRedYellow.distinct * 5 > walsRedYellow.total * 4

Red and yellow are almost always distinguished: 98 of 120 = 82% of languages have separate terms. The red/yellow split appears very early in the Berlin & Kay sequence.

theorem Typology.red_yellow_merger_rarer_than_grue : walsGreenBlue.merged > walsRedYellow.merged

Red/yellow merger is rare (15 languages) — much rarer than green/blue merger (68). The Berlin & Kay sequence predicts this asymmetry: red appears before any blue/green term.