cross_cousin_count
plain-language theorem explainer
Exactly four of the eight kinship systems defined by Boolean assignments to lineage, residence, and marriage axes admit cross-cousin marriage. Mathematical anthropologists modeling Murdock and Lévi-Strauss classifications via F_2^3 structures would cite this count. The proof is a one-line decision procedure that evaluates the filter length on the enumerated list of systems.
Claim. Let $K$ be the complete list of eight kinship systems, each a triple of Boolean values for the lineage, residence, and marriage axes. Then the number of systems $k$ in $K$ with marriage axis true is exactly four: $|{k in K mid k.marriage = true}| = 4$.
background
A KinshipSystem is a structure with three Boolean fields: lineage, residence, and marriage. The definition KinshipSystem.all enumerates all eight possible assignments in F_2^3, including the trivial all-false case. The predicate isCrossCousin holds exactly when the marriage field is true, marking systems that conserve the lineage axis across generations.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the concrete list KinshipSystem.all filtered by isCrossCousin, confirming the length equals 4 by exhaustive evaluation of the eight elements.
why it matters
This supplies the cross-cousin count for the master certificate KinshipGraphCohomologyCert and the combined statement kinship_one_statement. It realizes the half-space prediction for the marriage axis inside the 2^3 - 1 = 7 non-trivial systems, consistent with T8 (D = 3) from the UnifiedForcingChain and the eight-tick octave. Downstream theorems cross_cousin_half and kinship_one_statement invoke it directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.