def
definition
HasConfigDim5
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CrossDomain.ConfigDimUniversality on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
19namespace IndisputableMonolith.CrossDomain.ConfigDimUniversality
20
21/-- A type has configDim D = 5 iff it is finite with cardinality 5. -/
22def HasConfigDim5 (T : Type) [Fintype T] : Prop := Fintype.card T = 5
23
24/-! ## Five canonical D=5 domains (fresh local inductives, self-contained). -/
25
26inductive SensoryModality where
27 | sight | hearing | touch | smell | taste
28 deriving DecidableEq, Repr, BEq, Fintype
29
30inductive PrimaryEmotion where
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