KinshipSystem
KinshipSystem enumerates the five attested kinship-term systems in cultural anthropology as an inductive type. Modelers of kinship graphs under configDim D = 5 cite it to classify term typologies and populate certificates. The declaration is a direct inductive enumeration whose deriving clauses supply decidability and finiteness automatically.
claimThe set of canonical kinship systems consists of the five elements Hawaiian (generational), Eskimo (linear), Iroquois (bifurcate merging), Sudanese (descriptive), and Omaha (patrilineal crow).
background
The module introduces five canonical kinship-term systems tied to configuration dimension 5. Module documentation states these exhaust the attested kin-term typologies in cultural anthropology, with Hawaiian generational, Eskimo linear, Iroquois bifurcate merging, Sudanese descriptive, and Omaha patrilineal crow. Upstream, the KinshipSystem structure from KinshipGraphCohomology defines a kinship system as a Boolean assignment to three axes (lineage, residence, marriage), each taking values in {-1, +1}. This inductive type supplies the named instances that label the Boolean assignments appearing in downstream lists and certificates.
proof idea
The declaration is the inductive definition itself, introducing five constructors with no proof obligations. The deriving clauses for DecidableEq, Repr, BEq, and Fintype are discharged automatically by Lean.
why it matters in Recognition Science
This definition supplies the concrete systems used by downstream results including cross_cousin_count, cross_cousin_half, isCrossCousin, and the master certificate kinshipGraphCohomologyCert. It realizes the configDim = 5 constraint, linking attested anthropological data to the Recognition framework's dimensional forcing steps. The zero-axiom status closes the enumeration required for the cohomology certificate.
scope and limits
- Does not claim these five systems are the only mathematically possible Boolean assignments to the three axes.
- Does not derive the specific system names from the J-cost function or phi-ladder.
- Does not address non-attested or hypothetical kinship systems outside the attested typologies.
- Does not prove a bijection between the named systems and all 8 possible axis assignments.
formal statement (Lean)
18inductive KinshipSystem where
19 | hawaiian
20 | eskimo
21 | iroquois
22 | sudanese
23 | omaha
24 deriving DecidableEq, Repr, BEq, Fintype
25