isCrossCousin
plain-language theorem explainer
The definition projects the marriage Boolean from a KinshipSystem structure to mark whether cross-cousin marriage is permitted. Anthropologists working with Lévi-Strauss exchange rules cite this selector when partitioning the eight axis assignments. It is a direct field accessor with no further computation.
Claim. For a kinship system $k$ given by a triple of Booleans (lineage, residence, marriage), the cross-cousin indicator equals the marriage component, true precisely when cross-cousin unions are allowed.
background
KinshipSystem is a structure that assigns a Boolean value to each of three axes: lineage (patrilineal versus matrilineal), residence (patrilocal versus matrilocal), and marriage (cross-cousin versus parallel-cousin). The module encodes these assignments as elements of the vector space over F_2 of dimension 3, so that the full set of systems has cardinality 8 and the non-trivial subset has cardinality 7. This construction follows the Recognition Science count law 2^D - 1 for D = 3 and matches the six basic Murdock types plus one syncretic case.
proof idea
One-line field projection that extracts the marriage component of the KinshipSystem structure.
why it matters
The definition supplies the predicate required by the downstream theorems cross_cousin_count and kinship_one_statement, which establish that exactly four of the eight systems admit cross-cousin marriage. It thereby completes the axis decomposition for the kinship graph cohomology and anchors the anthropological count to the eight-tick octave and D = 3. The result also records the σ-conservation property that distinguishes cross-cousin from parallel-cousin rules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.