valence_strain_opposite
plain-language theorem explainer
The theorem states that valence equals negative strain for any qualia state. Researchers modeling consciousness as a recognition cursor cite this identity when equating pleasure with low J-cost and pain with high J-cost. The proof is a one-line term that projects the built-in identity field from the QualiaState structure.
Claim. For any qualia state $q$, the valence of $q$ equals the negative of the strain of $q$.
background
The module models consciousness as the verification cursor: past propositions are fixed, the present is the proposition under verification, and the future holds unverified candidates. Qualia supply the internal view of strain, with pleasure and pain corresponding to low and high values of the J-cost function. The QualiaState structure encodes strain as a non-negative real, valence as a real, and the identity valence = -strain as a field of the structure rather than a separate axiom.
proof idea
The proof is a one-line term wrapper that applies the valence_is_neg_strain field of the input QualiaState structure.
why it matters
This identity anchors the qualia model inside the Recognition framework by making valence identical to negative J-cost strain. It directly supports the cursor description of consciousness and precedes the TimeArrow section in the same module. The result closes the mapping from physical ledger factorization to subjective experience without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.