  60  intro x; exact ⟨(Sense.sight, Emotion.joy, x), rfl⟩
  61
  62/-- Non-reducibility: the product is strictly larger than any single factor. -/
  63theorem notCollapsedToSense : Fintype.card CognitiveState > Fintype.card Sense := by
  64  rw [cognitiveStateCount, senseCount]; decide
  65
  66theorem notCollapsedToEmotion :
  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

papers checked against this theorem

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