`BiologicalState`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.ConfigDimUniversality on GitHub at line 34.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  31  | joy | sadness | fear | anger | disgust
  32  deriving DecidableEq, Repr, BEq, Fintype
  33
  34inductive BiologicalState where
  35  | embryonic | developmental | mature | aging | senescent
  36  deriving DecidableEq, Repr, BEq, Fintype
  37
  38inductive EconomicCycle where
  39  | recession | recovery | expansion | peak | contraction
  40  deriving DecidableEq, Repr, BEq, Fintype
  41
  42inductive LinguisticRole where
  43  | subject | verb | object | modifier | complement
  44  deriving DecidableEq, Repr, BEq, Fintype
  45
  46theorem sensory_hasConfigDim5 : HasConfigDim5 SensoryModality := by
  47  unfold HasConfigDim5; decide
  48theorem emotion_hasConfigDim5 : HasConfigDim5 PrimaryEmotion := by
  49  unfold HasConfigDim5; decide
  50theorem biological_hasConfigDim5 : HasConfigDim5 BiologicalState := by
  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

papers checked against this theorem

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