pain_is_high_strain
plain-language theorem explainer
Pain corresponds to positive strain in the qualia model of consciousness. A researcher modeling recognition-based consciousness would cite this equivalence to link internal experience with the J-cost. The proof rewrites via the built-in valence identity then splits the biconditional and resolves both directions with linear arithmetic.
Claim. Let $q$ be a qualia state. Then the valence of $q$ is negative if and only if the strain of $q$ is positive: $q.valence < 0$ iff $q.strain > 0$.
background
The module treats consciousness as the active verification cursor: past propositions are fixed, the present is the proposition under recognition, and the future consists of candidate paths. Qualia supply the internal view of strain, with pleasure and pain identified with low and high values of the J-cost function respectively.
proof idea
The proof rewrites the target biconditional using the valence_is_neg_strain field of the input qualia state, which replaces valence with negative strain. It then applies constructor to split into the two directions and discharges each with linarith.
why it matters
The result encodes the direct identification of pain with high strain inside the RRF consciousness foundation. It supplies the concrete link between valence and the strain field that the module doc-comment describes as the inside view of recognition. No downstream theorems are recorded, so its integration with free-will or time-arrow constructions remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.