`cross_cousin_half`

proved

show as: view math explainer →

module: IndisputableMonolith.Anthropology.KinshipGraphCohomology
domain: Anthropology
line: 122 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Anthropology.KinshipGraphCohomology on GitHub at line 122.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 119    (KinshipSystem.all.filter isCrossCousin).length = 4 := by decide
 120
 121/-- The 4 cross-cousin systems are exactly half. -/
 122theorem cross_cousin_half :
 123    2 * (KinshipSystem.all.filter isCrossCousin).length =
 124    KinshipSystem.all.length := by
 125  rw [cross_cousin_count, KinshipSystem.all_length]
 126
 127/-! ## §4. Master certificate -/
 128
 129structure KinshipGraphCohomologyCert where
 130  all_count : KinshipSystem.all.length = 8
 131  nontrivial_count : KinshipSystem.nontrivial.length = 7
 132  murdock : KinshipSystem.nontrivial.length = 2 ^ 3 - 1
 133  pairwise_distinct : KinshipSystem.nontrivial.Nodup
 134  cross_cousin_count : (KinshipSystem.all.filter isCrossCousin).length = 4
 135  cross_cousin_half :
 136    2 * (KinshipSystem.all.filter isCrossCousin).length = KinshipSystem.all.length
 137  trivial_excluded : ¬ KinshipSystem.isNontrivial KinshipSystem.trivial
 138
 139def kinshipGraphCohomologyCert : KinshipGraphCohomologyCert where
 140  all_count := KinshipSystem.all_length
 141  nontrivial_count := KinshipSystem.nontrivial_length
 142  murdock := murdock_count
 143  pairwise_distinct := nontrivial_pairwise_distinct
 144  cross_cousin_count := cross_cousin_count
 145  cross_cousin_half := cross_cousin_half
 146  trivial_excluded := KinshipSystem.trivial_not_nontrivial
 147
 148/-- **KINSHIP ONE-STATEMENT.** The number of non-trivial kinship-axis
 149systems is `2^3 - 1 = 7` (Murdock's six basic types plus the
 150syncretic seventh), with cross-cousin marriage admitted by exactly
 151half the axis space. -/
 152theorem kinship_one_statement :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.