kinship_one_statement
plain-language theorem explainer
The declaration asserts that the non-trivial kinship systems over three Boolean axes number exactly seven, equivalently 2 cubed minus one, while exactly four of the eight total systems allow cross-cousin marriage. Structural anthropologists and researchers extending Murdock's typology would reference this result to ground the count law in the Recognition framework. The proof is a single term that assembles the nontrivial length lemma, the Murdock count theorem, and the cross-cousin count theorem.
Claim. Let $S$ be the set of all kinship systems, each an assignment of Boolean values to the lineage, residence, and marriage axes. Then the number of non-trivial systems equals 7, which equals $2^3-1$, and the number of systems admitting cross-cousin marriage equals 4.
background
KinshipSystem is a structure that assigns Boolean values to three axes: lineage, residence, and marriage. The module encodes kinship rules as elements of the vector space $F_2^3$, so that the eight possible assignments collapse to seven non-trivial systems plus the trivial null. The upstream definition all enumerates the explicit list of eight systems. The lemma nontrivial_length computes the length of the non-trivial subset. The theorem murdock_count proves this length equals $2^3-1$, matching Murdock's six basic types plus the syncretic seventh. The theorem cross_cousin_count shows that exactly four systems satisfy the predicate isCrossCousin, defined by the marriage axis being true.
proof idea
The proof is a one-line term that packages the three lemmas nontrivial_length, murdock_count, and cross_cousin_count into the required conjunction.
why it matters
This statement consolidates the count results for the kinship graph cohomology track and confirms the $2^D-1$ law for $D=3$ spatial dimensions from the forcing chain (T8). It aligns with the eight-tick octave structure (T7) and supplies the structural basis for Murdock's classification inside the Recognition Science derivation from the J-cost functional equation. No downstream uses are recorded, leaving open its integration into larger models of cultural evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.