structure
definition
CognitiveStateSpaceCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CrossDomain.CognitiveStateSpace on GitHub at line 93.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
101 irreducible_pair : Fintype.card CognitiveState >
102 Fintype.card (Sense × Emotion)
103
104def cognitiveStateSpaceCert : CognitiveStateSpaceCert where
105 product_count := cognitiveStateCount
106 sense_surj := senseProj_surj
107 emotion_surj := emotionProj_surj
108 memory_surj := memoryProj_surj
109 irreducible_1 := notCollapsedToSense
110 irreducible_2 := notCollapsedToEmotion
111 irreducible_3 := notCollapsedToMemory
112 irreducible_pair := notCollapsedToPair1
113
114end IndisputableMonolith.CrossDomain.CognitiveStateSpace