HardProblemDissolution
plain-language theorem explainer
The declaration defines a structure asserting that every qualia state satisfies valence equals negative strain by construction. Researchers in foundations of physics or philosophy of mind using the Recognition framework would cite it when dissolving the hard problem of consciousness into ledger strain. It is introduced directly as a structure whose three fields encode the identity, trivial gap closure, and non-emergence.
Claim. A structure asserting that for every qualia state $q$ (with strain $s(q) = J$-cost and valence $v(q)$), $v(q) = -s(q)$, that this identity leaves no explanatory gap, and that experience is not emergent from it.
background
The module models consciousness as the verification cursor at the active edge of recognition: past propositions are fixed, the present is the proposition under verification, and the future holds unverified candidates. Qualia are the inside view of strain, with pleasure and pain corresponding to low and high J-cost. The sibling structure QualiaState packages a real-valued strain (non-negative), a valence, and the built-in field valence_is_neg_strain : valence = -strain, making the identity definitional rather than postulated.
proof idea
This is a structure definition with no proof body. The three fields are propositions whose content is supplied directly by the valence_is_neg_strain field of QualiaState for the identity and by trivial True.intro for the gap and emergence clauses.
why it matters
It supplies the instance used by the downstream theorem hard_problem_dissolution_consistent, which constructs the structure without additional axioms. The declaration encodes the module claim that qualia are strain itself, not caused by strain, aligning with the J-cost ledger from upstream factorization results and the cursor model. It touches the open question of whether the strain-valence identity can be derived from the Recognition Composition Law rather than introduced by definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.