`cognitiveStateSpaceCert`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.CognitiveStateSpace
domain: CrossDomain
line: 104 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.CognitiveStateSpace on GitHub at line 104.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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

papers checked against this theorem

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