cross_cousin_half
plain-language theorem explainer
The theorem establishes that exactly half of the eight kinship systems permit cross-cousin marriage. Researchers modeling structural kinship rules via Boolean assignments to three axes would cite this to verify the predicted partition between cross and parallel systems. The proof is a one-line wrapper that substitutes the precomputed counts of four cross-cousin systems and eight total systems.
Claim. Let $K$ be the set of all eight kinship systems, each a Boolean triple on the lineage, residence, and marriage axes. Let $C$ be the subset where the marriage axis is true. Then $2 |C| = |K|$.
background
Kinship systems are encoded as Boolean assignments to three axes in $F_2^3$: lineage (patrilineal vs matrilineal), residence (projected to binary), and marriage (cross-cousin vs parallel-cousin). The module lists all eight assignments and isolates the seven non-trivial ones via the $2^D-1=7$ count law for $D=3$. The predicate isCrossCousin selects those with marriage axis true, which the upstream cross_cousin_count theorem shows number exactly four.
proof idea
The proof is a one-line wrapper that rewrites the left side via the cross_cousin_count theorem (filtered length equals 4) and the right side via the all_length theorem (total length equals 8).
why it matters
This populates the cross_cousin_count field inside the KinshipGraphCohomologyCert structure that collects all structural invariants for the anthropology track. It realizes the $2^D-1=7$ prediction for $D=3$ derived from the forcing chain (T8) and confirms the balance required by the Recognition Composition Law applied to the kinship-axis $Q_3$ structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.