pith. machine review for the scientific record. sign in
def definition def or abbrev

cognitiveStateSpaceCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 104def cognitiveStateSpaceCert : CognitiveStateSpaceCert where
 105  product_count := cognitiveStateCount

proof body

Definition body.

 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

depends on (9)

Lean names referenced from this declaration's body.