module module moderate

`IndisputableMonolith.Anthropology.KinshipGraphCohomology`

This module defines the three structural axes of kinship systems within Recognition Science: lineage, residence, and marriage. Researchers modeling social networks or extending graph cohomology to anthropology would cite these definitions. The module supplies basic types, predicates for trivial and nontrivial systems, and length properties as pure definitions with no proof obligations.

claimKinship axes form an inductive type with three constructors: lineage, residence, marriage. A kinship system is a structure over these axes equipped with predicates trivial and nontrivial together with length functions on the axes.

background

Recognition Science imports the fundamental time quantum τ₀ = 1 tick from Constants and cost structures from the Cost module to ground its extensions. This anthropology module introduces KinshipAxis and KinshipSystem to encode the three structural axes of lineage, residence, and marriage for graph-cohomology analysis. Sibling definitions supply predicates such as isNontrivial, all_length, and nontrivial_pairwise_distinct that classify systems by axis occupancy.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the base objects for KinshipGraphCohomology constructions in Recognition Science. It directly encodes the three structural axes stated in the module documentation and provides the classification lemmas required by downstream graph-cohomology work.

scope and limits

Does not model concrete cultural kinship data.
Does not compute cohomology groups or invariants.
Does not link axes to physical constants beyond the imported τ₀ and cost primitives.
Does not address forcing-chain steps T0-T8 or the Recognition Composition Law.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (17)

inductive KinshipAxis L43
structure KinshipSystem L51
def trivial L60
def isNontrivial L63
theorem trivial_not_nontrivial L67
def all L73
theorem all_length L83
def nontrivial L86
theorem nontrivial_length L89
theorem murdock_count L98
theorem nontrivial_pairwise_distinct L104
def isCrossCousin L113
theorem cross_cousin_count L118
theorem cross_cousin_half L122
structure KinshipGraphCohomologyCert L129
def kinshipGraphCohomologyCert L139
theorem kinship_one_statement L152