pleasure_is_low_strain
plain-language theorem explainer
The theorem states that for any qualia state, zero valence holds exactly when strain is zero. Modelers of consciousness via recognition strain cite this when treating pleasure as the zero-strain case. The proof rewrites via the built-in valence-equals-negative-strain identity then applies linear arithmetic to both directions of the biconditional.
Claim. Let $q$ be a qualia state with strain $s$ satisfying $s ≥ 0$ and valence $v = -s$. Then $v = 0$ if and only if $s = 0$.
background
A qualia state packages a non-negative real strain (the J-cost) together with a valence that is identical to negative strain by construction. The module treats consciousness as the active verification cursor whose internal view is qualia, so pleasure and pain appear as low and high values of this strain. The sole upstream dependency is the QualiaState structure definition itself, whose doc-comment notes that the valence-strain identity is built in rather than postulated as an axiom.
proof idea
The term proof first rewrites the biconditional using the valence_is_neg_strain field of the input structure, reducing the goal to -strain = 0 ↔ strain = 0. It then applies the constructor tactic to split into two implications, each discharged by the linarith tactic via elementary linear arithmetic over the reals.
why it matters
The result anchors the pleasure-pain axis inside the Recognition Science qualia model by making zero strain the precise definition of zero valence. It sits in the RRF consciousness foundation and aligns with the J-function and strain concepts appearing in the forcing chain (T5). No downstream theorems yet reference it, leaving open how the equivalence will be lifted into dynamical or multi-agent settings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.