`notCollapsedToPair3`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.CognitiveStateSpace on GitHub at line 87.

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

  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
 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.