Body-part terminology — substrate types and WALS data

@cite{wals-2013} (Chs 129, 130) @cite{brown-2013} @cite{brown-1976} @cite{andersen-1978}

Type-level enums + per-language profile struct for cross-linguistic body-part lexicalization across @cite{wals-2013} chapters 129–130 (Brown, drawing on @cite{andersen-1978} and @cite{brown-1976}). Two mereologically-related contrasts: 'hand' vs 'arm' and 'finger' vs 'hand'.

Schema

• HandArmRelation (Ch 129): one term for hand+arm, or distinct terms
• FingerHandRelation (Ch 130A): one term for finger+hand, or distinct
• BodyPartProfile: per-language bundle

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

inductive Typology.HandArmRelation : Type

Whether a language uses the same or different lexemes for 'hand' and 'arm' (WALS Ch 129, @cite{brown-2013}). Many languages use a single term covering both (e.g., Japanese te, Russian ruka); others lexically distinguish (e.g., English hand vs arm).

• identical : HandArmRelation

  The same word covers both 'hand' and 'arm'.

• different : HandArmRelation

  Distinct words for 'hand' and 'arm'.

@[implicit_reducible]

instance Typology.instDecidableEqHandArmRelation : DecidableEq HandArmRelation

Equations

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

def Typology.instReprHandArmRelation.repr : HandArmRelation → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprHandArmRelation : Repr HandArmRelation

Equations

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

inductive Typology.FingerHandRelation : Type

Whether a language uses the same or different lexemes for 'finger' and 'hand' (WALS Ch 130A, @cite{brown-2013}). Identity is rare cross- linguistically (12% of sample) and correlates with subsistence type per Ch 130B.

• identical : FingerHandRelation

  The same word covers both 'finger' and 'hand'.

• different : FingerHandRelation

  Distinct words for 'finger' and 'hand'.

@[implicit_reducible]

instance Typology.instDecidableEqFingerHandRelation : DecidableEq FingerHandRelation

Equations

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

@[implicit_reducible]

instance Typology.instReprFingerHandRelation : Repr FingerHandRelation

Equations

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

def Typology.instReprFingerHandRelation.repr : FingerHandRelation → Nat → Std.Format

Equations

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

structure Typology.BodyPartProfile : Type

A language's body-part lexicalization profile across @cite{wals-2013} Chs 129–130.

• language : String
• iso : String
• family : String
• handArm : Option HandArmRelation

  Ch 129: hand-arm relation.

• fingerHand : Option FingerHandRelation

  Ch 130A: finger-hand relation.

def Typology.instReprBodyPartProfile.repr : BodyPartProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprBodyPartProfile : Repr BodyPartProfile

Equations

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

def Typology.fromWALS129A : Data.WALS.F129A.HandAndArm → HandArmRelation

Convert WALS 129A hand-arm values into the substrate enum.

Equations

• Typology.fromWALS129A Data.WALS.F129A.HandAndArm.identical = Typology.HandArmRelation.identical
• Typology.fromWALS129A Data.WALS.F129A.HandAndArm.different = Typology.HandArmRelation.different

def Typology.fromWALS130A : Data.WALS.F130A.FingerAndHand → FingerHandRelation

Convert WALS 130A finger-hand values into the substrate enum.

Equations

• Typology.fromWALS130A Data.WALS.F130A.FingerAndHand.identical = Typology.FingerHandRelation.identical
• Typology.fromWALS130A Data.WALS.F130A.FingerAndHand.different = Typology.FingerHandRelation.different

structure Typology.HandArmCounts : Type

WALS Ch 129 distribution: hand-arm patterns (@cite{brown-2013}, n = 617).

• identical : Nat
• different : Nat

def Typology.instReprHandArmCounts.repr : HandArmCounts → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprHandArmCounts : Repr HandArmCounts

Equations

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

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

Equations

• c.total = c.identical + c.different

def Typology.walsHandArm : HandArmCounts

WALS Ch 129 counts (617 languages).

Equations

• Typology.walsHandArm = { identical := 228, different := 389 }

structure Typology.FingerHandCounts : Type

WALS Ch 130A distribution: finger-hand patterns (@cite{brown-2013}, n = 593).

• identical : Nat
• different : Nat

@[implicit_reducible]

instance Typology.instReprFingerHandCounts : Repr FingerHandCounts

Equations

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

def Typology.instReprFingerHandCounts.repr : FingerHandCounts → Nat → Std.Format

Equations

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

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

Equations

• c.total = c.identical + c.different

def Typology.walsFingerHand : FingerHandCounts

WALS Ch 130A counts (593 languages).

Equations

• Typology.walsFingerHand = { identical := 72, different := 521 }

structure Typology.FingerHandCulturalCounts : Type

WALS Ch 130B: cultural categories of languages with finger=hand identity (@cite{brown-2013}, n = 72). The classic cross-cultural correlation: hunter-gatherer societies dominate the finger=hand identity pattern.

• hunterGatherers : Nat
• farmerForagers : Nat
• fullFledgedFarmers : Nat

def Typology.instReprFingerHandCulturalCounts.repr : FingerHandCulturalCounts → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprFingerHandCulturalCounts : Repr FingerHandCulturalCounts

Equations

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

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

Equations

• c.total = c.hunterGatherers + c.farmerForagers + c.fullFledgedFarmers

def Typology.walsFingerHandCultural : FingerHandCulturalCounts

WALS Ch 130B counts (72 languages with finger=hand identity).

Equations

• Typology.walsFingerHandCultural = { hunterGatherers := 46, farmerForagers := 18, fullFledgedFarmers := 8 }

theorem Typology.hand_arm_different_majority : walsHandArm.different > walsHandArm.identical

Most languages distinguish 'hand' from 'arm': 389 of 617 (63%) have distinct terms, while 228 (37%) use a single term covering both.

theorem Typology.finger_hand_identity_rare : walsFingerHand.identical * 8 < walsFingerHand.total

Finger-hand identity is rare cross-linguistically: only 72 of 593 (~12%) of languages use one term for both. The strong default is to distinguish them.

theorem Typology.finger_hand_hunter_gatherer_majority : walsFingerHandCultural.hunterGatherers * 2 > walsFingerHandCultural.total

Among languages with finger=hand identity, hunter-gatherers dominate: 46 of 72 (~64%) — the classic Brown (1976) / Andersen (1978) correlation between subsistence and lexicalization.

theorem Typology.hunter_gatherer_dominates_farmer : walsFingerHandCultural.hunterGatherers > walsFingerHandCultural.fullFledgedFarmers * 5

Hunter-gatherers are more numerous than full-fledged farmers among finger=hand languages by a factor of ~5.7 (46 vs 8).