ConfigDimUniversalityCert

formal source

  98/-- $5^5 = 3125$. -/
  99theorem fivePowFive : (5 : ℕ)^5 = 3125 := by decide
 100
 101structure ConfigDimUniversalityCert where
 102  sensory_5 : HasConfigDim5 SensoryModality
 103  emotion_5 : HasConfigDim5 PrimaryEmotion
 104  biological_5 : HasConfigDim5 BiologicalState
 105  economic_5 : HasConfigDim5 EconomicCycle
 106  linguistic_5 : HasConfigDim5 LinguisticRole
 107  triple_125 : ∀ (A B C : Type) [Fintype A] [Fintype B] [Fintype C],
 108    HasConfigDim5 A → HasConfigDim5 B → HasConfigDim5 C →
 109    Fintype.card (A × B × C) = 125
 110  five_domain_3125 :
 111    Fintype.card (SensoryModality × PrimaryEmotion × BiologicalState ×
 112                  EconomicCycle × LinguisticRole) = 3125
 113  five_pow_five : (5 : ℕ)^5 = 3125
 114
 115def configDimUniversalityCert : ConfigDimUniversalityCert where
 116  sensory_5 := sensory_hasConfigDim5
 117  emotion_5 := emotion_hasConfigDim5
 118  biological_5 := biological_hasConfigDim5
 119  economic_5 := economic_hasConfigDim5
 120  linguistic_5 := linguistic_hasConfigDim5
 121  triple_125 := fun _ _ _ _ _ _ => triple_product_125
 122  five_domain_3125 := five_domain_product
 123  five_pow_five := fivePowFive
 124
 125end IndisputableMonolith.CrossDomain.ConfigDimUniversality