KinshipAxis
plain-language theorem explainer
KinshipAxis enumerates the three binary structural axes that classify kinship systems in the Recognition Science model. Researchers modeling cross-cultural anthropology via the F_2^3 vector space would cite it to ground the 2^D - 1 count law. The declaration is a direct inductive definition that lists lineage, residence, and marriage as the generators with no further reduction steps.
Claim. An inductive type with three constructors: lineage (patrilineal versus matrilineal), residence (patrilocal versus matrilocal, projected onto the field with two elements), and marriage (cross-cousin versus parallel-cousin).
background
The module encodes kinship systems as sign assignments in the three-dimensional vector space over the field with two elements, applying the same 2^D - 1 = 7 count law used for non-trivial structures elsewhere in Recognition Science. The axes capture lineage direction, residence pattern, and marriage rule, so that the eight possible assignments collapse to seven non-trivial systems plus the trivial null. Upstream results supply the active edge count per tick (A = 1) from IntegrationGap and the coherence energy unit from Masses.Anchor, fixing the dimensional conventions for the framework.
proof idea
The declaration is a direct inductive definition that enumerates the three axes by cases. No lemmas from the depends_on list are invoked; the structure is introduced as the generators for Boolean assignments in the module.
why it matters
This definition supplies the Q_3 basis for kinship axes, enabling the prediction of exactly seven non-trivial systems that align with Murdock's six basic types plus one syncretic case. It implements Track I1 of Plan v5 by providing the structural foundation for graph cohomology on kinship rules. The module doc states that any documented system outside these seven classes would falsify the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.