`linguistic_hasConfigDim5`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.ConfigDimUniversality
domain: CrossDomain
line: 54 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.ConfigDimUniversality on GitHub at line 54.

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

  51  unfold HasConfigDim5; decide
  52theorem economic_hasConfigDim5 : HasConfigDim5 EconomicCycle := by
  53  unfold HasConfigDim5; decide
  54theorem linguistic_hasConfigDim5 : HasConfigDim5 LinguisticRole := by
  55  unfold HasConfigDim5; decide
  56
  57/-! ## Cross-domain product theorems. -/
  58
  59/-- Any triple of D=5 types has a product of size 125. -/
  60theorem triple_product_125
  61    {A B C : Type} [Fintype A] [Fintype B] [Fintype C]
  62    (hA : HasConfigDim5 A) (hB : HasConfigDim5 B) (hC : HasConfigDim5 C) :
  63    Fintype.card (A × B × C) = 125 := by
  64  unfold HasConfigDim5 at hA hB hC
  65  simp [Fintype.card_prod, hA, hB, hC]
  66
  67/-- Any pair of D=5 types has a product of size 25. -/
  68theorem pair_product_25
  69    {A B : Type} [Fintype A] [Fintype B]
  70    (hA : HasConfigDim5 A) (hB : HasConfigDim5 B) :
  71    Fintype.card (A × B) = 25 := by
  72  unfold HasConfigDim5 at hA hB
  73  simp [Fintype.card_prod, hA, hB]
  74
  75/-- Two D=5 types are equicardinal (trivially, both = 5). -/
  76theorem configDim5_equicardinal
  77    {A B : Type} [Fintype A] [Fintype B]
  78    (hA : HasConfigDim5 A) (hB : HasConfigDim5 B) :
  79    Fintype.card A = Fintype.card B := by
  80  rw [hA, hB]
  81
  82/-- Concrete instance: sensory × emotion × biological = 125. -/
  83theorem three_domain_product :
  84    Fintype.card (SensoryModality × PrimaryEmotion × BiologicalState) = 125 :=

papers checked against this theorem

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