QualiaState
plain-language theorem explainer
QualiaState encodes strain as a non-negative real paired with valence fixed to its negation, making the identity definitional rather than emergent. Researchers addressing the hard problem of consciousness cite it to treat qualia as the internal view of J-cost in the RRF cursor model. The definition is a four-field structure plus a constructor that directly assigns the negation and discharges the equality by reflexivity.
Claim. A qualia state consists of a strain value $s$ with $0 ≤ s$ and a valence value $v$ satisfying $v = -s$.
background
The RRF module models consciousness as the active verification cursor separating verified past propositions from unverified future candidates. Qualia supply the internal perspective on strain, with pleasure identified as low J-cost via the Berlyne function (1 minus normalized J-cost) and pain as high strain. Upstream results include the identity event at minimum J-cost, the collision-free property of empirical programs, and the reduction of seven axioms to four structural conditions plus definitional facts.
proof idea
QualiaState is introduced as a structure with four fields: strain, its non-negativity witness, valence, and the equality valence = -strain. The fromStrain constructor populates the fields by direct assignment and uses reflexivity to discharge the equality field.
why it matters
The structure supplies the identity field required by HardProblemDissolution to assert that qualia are strain itself rather than caused by it, thereby closing the explanatory gap. It directly supports the downstream theorems pain_is_high_strain, pleasure_is_low_strain, and valence_strain_opposite. The construction aligns with the J-uniqueness step in the forcing chain and the recognition composition law by treating valence as the signed strain without additional axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.