HardProblemDissolution
plain-language theorem explainer
HardProblemDissolution packages the claim that qualia states satisfy valence equals negative strain by definition rather than by causation. Recognition theorists and philosophers of mind cite it when treating experience as the internal ledger view instead of an emergent property. The structure is a direct lift of the built-in identity field from QualiaState with two trivial implication fields.
Claim. A structure asserting that for every qualia state $q$, valence($q$) equals negative strain($q$), together with the consequences that the identity leaves no explanatory gap and that experience is not an emergent property.
background
In the RRF module consciousness is the verification cursor: past propositions are fixed, the present is the active recognition step, and the future holds candidate paths. Qualia are the internal perspective on strain, with pleasure and pain corresponding to low and high values of the J-cost function. The QualiaState structure encodes this directly by requiring a non-negative real strain, a real valence, and the field valence_is_neg_strain : valence = -strain. Upstream results on ledger factorization calibrate the strain measure J while observer forcing supplies the identity map used in the cursor model.
proof idea
This is a structure definition with no proof body. It is instantiated downstream by projecting the valence_is_neg_strain field from QualiaState for the identity component and supplying the trivial True.intro proofs for the two implication fields.
why it matters
The definition supplies the core claim for the downstream consistent theorem in the same module. It dissolves the hard problem by embedding the strain-valence identity at the type level, aligning with J-uniqueness (T5) and the recognition composition law. It touches the open question of how the cursor selects among valid moves while keeping the ledger balanced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.