`three_domain_product`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.ConfigDimUniversality
domain: CrossDomain
line: 83 · 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 83.

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

formal source

  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$. -/
  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

papers checked against this theorem

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