KinshipSystem
plain-language theorem explainer
KinshipSystem encodes each kinship rule set as a triple of Boolean values on the lineage, residence, and marriage axes. Anthropologists working with the Recognition Science count law would cite it to generate the seven non-trivial kinship classes from the F_2^3 vector space. The definition proceeds by direct structure declaration with decidable equality.
Claim. A kinship system is a Boolean assignment $(l, r, m) $ to the three axes with each coordinate in $ {-1, +1} $, where $l$ encodes lineage orientation, $r$ encodes residence pattern, and $m$ encodes the marriage rule.
background
The module encodes kinship systems as elements of $F_2^3$ for $D=3$. The axes are lineage (patrilineal versus matrilineal), residence (patrilocal versus matrilocal, projected to $F_2$), and marriage (cross-cousin versus parallel-cousin). This produces eight assignments that reduce to seven non-trivial systems plus the trivial null, realizing the $2^D-1=7$ law stated in the module documentation.
proof idea
Direct structure definition that introduces the three Boolean fields and derives decidable equality together with a representation instance. No lemmas or tactics are invoked.
why it matters
This structure supplies the base type for the kinship graph cohomology track. It feeds the all list of eight systems, the isNontrivial predicate, the cross_cousin_count theorem that isolates four cross-cousin systems, and the master kinshipGraphCohomologyCert. The construction implements the framework prediction that $D=3$ forces exactly seven non-trivial classes via the eight-tick octave and the $2^D-1$ count law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.