  37  deriving DecidableEq, Repr, BEq, Fintype
  38
  39theorem senseCount : Fintype.card Sense = 5 := by decide
  40theorem emotionCount : Fintype.card Emotion = 5 := by decide
  41theorem memorySystemCount : Fintype.card MemorySystem = 5 := by decide
  42
  43abbrev CognitiveState : Type := Sense × Emotion × MemorySystem
  44
  45theorem cognitiveStateCount : Fintype.card CognitiveState = 125 := by
  46  simp only [CognitiveState, Fintype.card_prod, senseCount, emotionCount, memorySystemCount]
  47
  48/-- Sense projection is surjective. -/
  49theorem senseProj_surj : Function.Surjective (fun s : CognitiveState => s.1) := by
  50  intro x; exact ⟨(x, Emotion.joy, MemorySystem.working), rfl⟩
  51
  52/-- Emotion projection is surjective. -/
  53theorem emotionProj_surj :
  54    Function.Surjective (fun s : CognitiveState => s.2.1) := by
  55  intro x; exact ⟨(Sense.sight, x, MemorySystem.working), rfl⟩
  56
  57/-- Memory projection is surjective. -/
  58theorem memoryProj_surj :
  59    Function.Surjective (fun s : CognitiveState => s.2.2) := by
  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 :

papers checked against this theorem

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