kinshipSystem_count
plain-language theorem explainer
The theorem establishes that the inductive type KinshipSystem has exactly five elements. Mathematical anthropologists modeling cross-cultural terminologies would cite it to confirm the exhaustive enumeration of attested systems. The proof is a one-line wrapper that applies the decide tactic to the automatically derived Fintype instance.
Claim. The set of kinship systems has cardinality five: $|$Hawaiian, Eskimo, Iroquois, Sudanese, Omaha$| = 5$.
background
In this module kinship systems are formalized as an inductive type whose five constructors are the canonical typologies: Hawaiian (generational), Eskimo (linear), Iroquois (bifurcate merging), Sudanese (descriptive), and Omaha (patrilineal crow). The module states that these exhaust the attested kin-term typologies in cultural anthropology and ties the count to configDim D = 5. An upstream structure in KinshipGraphCohomology instead represents a kinship system as a Boolean triple on the axes of lineage, residence, and marriage.
proof idea
The proof is a one-line wrapper that invokes the decide tactic, which evaluates the Fintype.card instance derived from the inductive definition with its five constructors.
why it matters
The result populates the five_systems field of the downstream KinshipStructureCert definition, certifying the typology inside the Recognition Science anthropology layer. It extends the core forcing chain (T0-T8) by fixing configDim = 5 for kinship structures while preserving the zero-sorry status of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.