theorem
proved
notCollapsedToMemory
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.CrossDomain.CognitiveStateSpace on GitHub at line 70.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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)
97 memory_surj : Function.Surjective (fun s : CognitiveState => s.2.2)
98 irreducible_1 : Fintype.card CognitiveState > Fintype.card Sense
99 irreducible_2 : Fintype.card CognitiveState > Fintype.card Emotion
100 irreducible_3 : Fintype.card CognitiveState > Fintype.card MemorySystem