theorem
proved
notCollapsedToEmotion
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CrossDomain.CognitiveStateSpace on GitHub at line 66.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
63theorem notCollapsedToSense : Fintype.card CognitiveState > Fintype.card Sense := by
64 rw [cognitiveStateCount, senseCount]; decide
65
66theorem notCollapsedToEmotion :
67 Fintype.card CognitiveState > Fintype.card Emotion := by
68 rw [cognitiveStateCount, emotionCount]; decide
69
70theorem notCollapsedToMemory :
71 Fintype.card CognitiveState > Fintype.card MemorySystem := by
72 rw [cognitiveStateCount, memorySystemCount]; decide
73
74/-- The product is strictly larger than any pairwise factor too. -/
75theorem notCollapsedToPair1 :
76 Fintype.card CognitiveState > Fintype.card (Sense × Emotion) := by
77 have h : Fintype.card (Sense × Emotion) = 25 := by
78 simp only [Fintype.card_prod, senseCount, emotionCount]
79 rw [cognitiveStateCount, h]; decide
80
81theorem notCollapsedToPair2 :
82 Fintype.card CognitiveState > Fintype.card (Sense × MemorySystem) := by
83 have h : Fintype.card (Sense × MemorySystem) = 25 := by
84 simp only [Fintype.card_prod, senseCount, memorySystemCount]
85 rw [cognitiveStateCount, h]; decide
86
87theorem notCollapsedToPair3 :
88 Fintype.card CognitiveState > Fintype.card (Emotion × MemorySystem) := by
89 have h : Fintype.card (Emotion × MemorySystem) = 25 := by
90 simp only [Fintype.card_prod, emotionCount, memorySystemCount]
91 rw [cognitiveStateCount, h]; decide
92
93structure CognitiveStateSpaceCert where
94 product_count : Fintype.card CognitiveState = 125
95 sense_surj : Function.Surjective (fun s : CognitiveState => s.1)
96 emotion_surj : Function.Surjective (fun s : CognitiveState => s.2.1)