`configDimUniversalityCert`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.ConfigDimUniversality on GitHub at line 115.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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

papers checked against this theorem

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