HardProblemStance
plain-language theorem explainer
HardProblemStance enumerates the five canonical positions on Chalmers' hard problem of consciousness. A philosopher of mind or foundations physicist working in Recognition Science would cite the enumeration to classify responses to the explanatory gap before introducing the framework's recognition-coupling ontology. The definition is a direct inductive listing of constructors with derived decidable equality and finite-type instances.
Claim. The inductive type whose elements are the five stances on the hard problem: eliminativism, type-A materialism (reductive), type-B materialism (a-posteriori identity), dualism (property or substance), and panpsychism or neutral monism.
background
The module sets the hard problem equal to configDim D = 5 and lists the five classical stances as the exhaustive set of responses to the gap between physical description and qualia. Recognition Science treats recognition coupling as the ontic ground from which qualia arise as (Z, Θ) resonances, placing the framework outside the four classical options. The inductive type supplies the finite carrier set required by the downstream cardinality statement.
proof idea
The declaration is the inductive definition that introduces the five named constructors and automatically derives DecidableEq, Repr, BEq, and Fintype instances.
why it matters
It supplies the enumeration consumed by HardProblemCert (which asserts Fintype.card = 5) and by the decide-based count theorem. The module positions Recognition Science as a fifth-type view in which recognition coupling grounds qualia without reduction to any of the listed stances, directly tying the enumeration to the configDim D = 5 landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.