murdock_count
plain-language theorem explainer
The count of non-trivial kinship systems, each a Boolean triple on lineage, residence, and marriage axes, equals exactly seven. Anthropologists working with Murdock's classification would cite the result to connect empirical types to the Recognition Science 2^D - 1 law at D = 3. The proof reduces the claim to the length of the filtered nontrivial list and evaluates the arithmetic.
Claim. Let a kinship system be a triple of Boolean values, one for each of the lineage, residence, and marriage axes. The number of such systems with at least one true component equals $2^3 - 1$.
background
KinshipSystem is the structure with three Boolean fields lineage, residence, and marriage, each an axis assignment in {-1, +1} projected to Bool. The nontrivial list is formed by filtering the full list of eight possible assignments to retain only those with at least one true field, excluding the all-false trivial case. The module places this construction inside Recognition Science track I1, where the same 2^D - 1 count law applied to the kinship-axis Q3 structure at D = 3 yields seven classes asserted to match Murdock's six basic types plus one syncretic form.
proof idea
The proof is a one-line wrapper that rewrites the target length using the nontrivial_length theorem, which already establishes the filtered list has length 7, then applies norm_num to confirm 2^3 - 1 evaluates to 7.
why it matters
The declaration supplies the murdock field inside kinshipGraphCohomologyCert and is conjoined inside kinship_one_statement. It realizes the 7-class theorem stated in the module documentation, which applies the 2^D - 1 count law from the Recognition Science framework at D = 3 (T8). This step links the kinship graph cohomology construction to the eight-tick octave and spatial dimension forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.