hardProblemStance_count
plain-language theorem explainer
The theorem asserts that the inductive type enumerating stances toward Chalmers's hard problem has finite cardinality exactly five. Philosophers of mind working inside Recognition Science cite this count when mapping eliminativism, type-A and type-B materialism, dualism, and panpsychism/neutral monism onto the framework's recognition-coupling ontology. The proof is a one-line wrapper that invokes the decide tactic on the derived Fintype instance.
Claim. The finite set of stances toward Chalmers's hard problem of consciousness has cardinality five: $|S| = 5$, where $S$ consists of eliminativism, type-A materialism, type-B materialism, dualism, and panpsychism/neutral monism.
background
The module defines HardProblemStance as an inductive type whose five constructors are eliminativism, typeAMaterialism, typeBMaterialism, dualism, and panpsychismNeutralMonism, each deriving DecidableEq, Repr, BEq, and Fintype. The module documentation states that these are the five canonical positions toward Chalmers's hard problem (configDim D = 5) and that Recognition Science occupies a distinct fifth-type view in which recognition coupling is the ontic ground and qualia emerge as (Z, Θ) resonances. The sole upstream dependency is the inductive definition itself.
proof idea
The proof is a one-line wrapper that applies the decide tactic. Because the inductive type derives Fintype, the tactic reduces the equality Fintype.card HardProblemStance = 5 to a direct enumeration of the five constructors.
why it matters
The result supplies the five_stances field of the downstream hardProblemCert definition, thereby anchoring the module's structural claim that RS occupies a position beyond the four classical stances. It directly implements the module's assertion of five canonical stances and the statement that recognition coupling provides the additional ontic type. No open scaffolding or unresolved questions are indicated in the surrounding declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.