HardProblemCert
plain-language theorem explainer
The HardProblemCert structure encodes the assertion that exactly five stances exist toward Chalmers' hard problem of consciousness. Philosophers of mind engaging Recognition Science would cite it to mark the framework's fifth position, where recognition coupling grounds qualia as (Z, Θ) resonances. The declaration is a bare structure definition whose single field requires the Fintype cardinality of the enumerated stance type to equal five.
Claim. Let $S$ be the finite set of stances toward Chalmers' hard problem of consciousness. The certificate asserts that the cardinality of $S$ equals five, where $S$ consists of eliminativism, type-A materialism, type-B materialism, dualism, and panpsychism or neutral monism.
background
Recognition Science treats the hard problem as having configDim D = 5. The module enumerates five canonical stances: eliminativism, type-A materialism (reductive), type-B materialism (a-posteriori identity), dualism (property or substance), and panpsychism/neutral-monism. Recognition Science occupies the fifth stance by taking recognition coupling as the ontic ground, with qualia emerging as (Z, Θ) resonances not reducible to the classical four positions without loss.
proof idea
This is a structure definition containing one field. The field directly states that the Fintype cardinality of the stance inductive type equals five. No lemmas, tactics, or reductions are applied; the declaration simply packages the cardinality constraint as a named structure.
why it matters
The definition supplies the structural anchor for the module's treatment of the hard problem, feeding the concrete instance hardProblemCert. It formalizes the claim that Recognition Science adds a distinct fifth stance beyond the classical quartet, consistent with the framework's ontic grounding in recognition coupling. The construction touches the open question of how (Z, Θ) resonances close the explanatory gap left by the four standard positions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.