kinshipStructureCert
plain-language theorem explainer
This definition supplies a certificate asserting that exactly five kinship systems are recognized in the anthropological record. Researchers mapping cultural structures onto Recognition Science's configuration dimension would reference it to align empirical typologies with the five-dimensional space. It is realized as a direct one-line assignment of the pre-proven cardinality result into the structure field.
Claim. The certificate satisfies $Fintype.card(KinshipSystem) = 5$, where $KinshipSystem$ enumerates the five attested typologies.
background
The module states that five canonical kinship-term systems exhaust the attested typologies in cultural anthropology: Hawaiian (generational), Eskimo (linear), Iroquois (bifurcate merging), Sudanese (descriptive), and Omaha (patrilineal crow). These are tied to configDim D = 5. KinshipStructureCert is the structure whose sole field requires the cardinality of KinshipSystem to equal 5. The upstream theorem kinshipSystem_count establishes this equality by direct computation.
proof idea
One-line wrapper that populates the five_systems field of KinshipStructureCert by direct reference to the theorem kinshipSystem_count.
why it matters
This definition certifies the exhaustion of kinship typologies at five systems, aligning with the five-dimensional configuration space in Recognition Science. It provides the anthropological grounding for the configDim parameter. No parent theorems are listed in the used-by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.