KinshipGraphCohomologyCert
plain-language theorem explainer
KinshipGraphCohomologyCert packages the structural invariants of the eight kinship systems over F_2^3: total length eight, seven non-trivial matching 2^3 minus one, four cross-cousin systems exactly half the total, and pairwise distinct. Recognition Science researchers cite it to embed Murdock's typology inside the same count law used for narrative plots. The definition aggregates already-decided lemmas on lengths, filters, and distinctness by direct substitution.
Claim. A structure certifying that the list of all kinship systems (Boolean triples for lineage, residence, marriage) has length 8, the non-trivial subset has length 7 equal to $2^3-1$, the non-trivial systems are pairwise distinct, exactly four systems permit cross-cousin marriage, twice that count recovers the total length, and the all-false trivial system fails to be non-trivial.
background
KinshipSystem is the structure with three Bool fields (lineage, residence, marriage); the trivial system sets all false. The list all enumerates the eight combinations. isCrossCousin returns the marriage field. isNontrivial holds when at least one field is true. Upstream lemmas include cross_cousin_count (filter length equals 4, proved by decide) and all_length (total equals 8). The module models each system as an element of F_2^3 and applies the 2^D-1 count law for D=3.
proof idea
This is a structure definition whose fields receive the values of the lemmas all_length, nontrivial_length, murdock_count, nontrivial_pairwise_distinct, cross_cousin_count, cross_cousin_half, and trivial_not_nontrivial. No tactics run inside the structure; the values are supplied at the single construction site that builds an instance of the certificate.
why it matters
The certificate closes the derivation of the kinship typology from the F_2^3 basis and supplies the data for the master certificate kinshipGraphCohomologyCert. It realizes the module prediction that the count law yields seven non-trivial systems matching Murdock's six basic types plus one syncretic case. In the Recognition framework it parallels the seven-element list of plot families and instantiates the eight-tick octave for D=3. Whether every documented kinship system fits one of these seven classes remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.