hardProblemStance_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the five stances from the T0-T8 forcing chain or Recognition Composition Law.
- Does not address the emergence of qualia as (Z, Θ) resonances.
- Does not compare the stances quantitatively on the phi-ladder or via the mass formula.
- Does not supply a decision procedure for assigning arbitrary theories to one of the five categories.
Lean usage
example : Fintype.card HardProblemStance = 5 := hardProblemStance_countformal statement (Lean)
29theorem hardProblemStance_count :
30 Fintype.card HardProblemStance = 5 := by decide
proof body
31