IndisputableMonolith.Anthropology.KinshipStructuresFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Kinship Structures from configDim — Anthropology Depth
   6
   7Five canonical kinship-term systems (= configDim D = 5):
   8  Hawaiian (generational), Eskimo (linear), Iroquois (bifurcate merging),
   9  Sudanese (descriptive), Omaha (patrilineal crow).
  10
  11These exhaust the attested kin-term typologies in cultural anthropology.
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith.Anthropology.KinshipStructuresFromConfigDim
  17
  18inductive KinshipSystem where
  19  | hawaiian
  20  | eskimo
  21  | iroquois
  22  | sudanese
  23  | omaha
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem kinshipSystem_count : Fintype.card KinshipSystem = 5 := by decide
  27
  28structure KinshipStructureCert where
  29  five_systems : Fintype.card KinshipSystem = 5
  30
  31def kinshipStructureCert : KinshipStructureCert where
  32  five_systems := kinshipSystem_count
  33
  34end IndisputableMonolith.Anthropology.KinshipStructuresFromConfigDim
  35