QualiaState

formal source

 123The key insight: valence IS negative strain, not caused by it.
 124This is built into the structure, not assumed as an axiom.
 125-/
 126structure QualiaState where
 127  /-- The strain value (J). -/
 128  strain : ℝ
 129  /-- Strain is non-negative. -/
 130  strain_nonneg : 0 ≤ strain
 131  /-- The valence (pleasure/pain axis). -/
 132  valence : ℝ
 133  /-- The qualia-strain identity: valence = -strain. -/
 134  valence_is_neg_strain : valence = -strain
 135
 136/-- Create a qualia state from just strain. -/
 137def QualiaState.fromStrain (strain : ℝ) (h : 0 ≤ strain) : QualiaState := {
 138  strain := strain,
 139  strain_nonneg := h,
 140  valence := -strain,
 141  valence_is_neg_strain := rfl
 142}
 143
 144/-- Pain corresponds to high strain. -/
 145theorem pain_is_high_strain (q : QualiaState) :
 146    q.valence < 0 ↔ q.strain > 0 := by
 147  rw [q.valence_is_neg_strain]
 148  constructor
 149  · intro h; linarith
 150  · intro h; linarith
 151
 152/-- Pleasure corresponds to low/zero strain. -/
 153theorem pleasure_is_low_strain (q : QualiaState) :
 154    q.valence = 0 ↔ q.strain = 0 := by
 155  rw [q.valence_is_neg_strain]
 156  constructor