pair_product_25

formal source

  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 :=
  85  triple_product_125 sensory_hasConfigDim5 emotion_hasConfigDim5 biological_hasConfigDim5
  86
  87/-- All five domains together: 5^5 = 3125. -/
  88theorem five_domain_product :
  89    Fintype.card (SensoryModality × PrimaryEmotion × BiologicalState ×
  90                  EconomicCycle × LinguisticRole) = 3125 := by
  91  have hs : Fintype.card SensoryModality = 5 := sensory_hasConfigDim5
  92  have he : Fintype.card PrimaryEmotion = 5 := emotion_hasConfigDim5
  93  have hb : Fintype.card BiologicalState = 5 := biological_hasConfigDim5
  94  have hc : Fintype.card EconomicCycle = 5 := economic_hasConfigDim5
  95  have hl : Fintype.card LinguisticRole = 5 := linguistic_hasConfigDim5
  96  simp [Fintype.card_prod, hs, he, hb, hc, hl]
  97
  98/-- $5^5 = 3125$. -/