KinshipStructureCert
plain-language theorem explainer
KinshipStructureCert certifies that the inductive enumeration of kinship systems contains exactly five elements. Cultural anthropologists mapping Recognition Science dimensions to empirical typologies would cite the certificate when linking configDim D=5 to attested kin-term systems. The definition is a direct structure packaging the Fintype cardinality fact derived from the five constructors.
Claim. A certificate structure whose field asserts that the finite cardinality of the kinship system type equals five, where the type enumerates the five canonical systems (Hawaiian, Eskimo, Iroquois, Sudanese, Omaha).
background
The module establishes that configDim D = 5 corresponds to exactly five canonical kinship-term systems: Hawaiian (generational), Eskimo (linear), Iroquois (bifurcate merging), Sudanese (descriptive), and Omaha (patrilineal crow). These are introduced as an inductive type with those five constructors, deriving Fintype, DecidableEq, and related instances to support cardinality statements. The module doc states that these exhaust the attested kin-term typologies in cultural anthropology.
proof idea
The declaration is a bare structure definition whose single field requires the cardinality of the inductive KinshipSystem type to equal five. The type derives Fintype from its five constructors, so the equality holds by the derived instance with no separate proof body or tactics required.
why it matters
This structure supplies the type for the downstream kinshipStructureCert definition that constructs the witness via the count. It anchors the anthropological application of the Recognition Science framework at configDim D=5, aligning with the forcing chain's dimensional parameters that generate discrete classifications. The module reports zero sorry or axiom, closing the enumeration for this depth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.