MetaethicalPositionsCert
plain-language theorem explainer
The structure MetaethicalPositionsCert encodes the assertion that the finite type of metaethical positions has cardinality exactly five, matching the configuration dimension D=5. Philosophers or framework developers would cite it to anchor the enumeration of positions such as moral realism and error theory. The definition is a direct structural wrapper that populates the cardinality field from the Fintype instance on the inductive enumeration.
Claim. The structure MetaethicalPositionsCert consists of the field asserting that the cardinality of the finite type of metaethical positions equals five: $Fintype.card(MetaethicalPosition)=5$.
background
The module links metaethical positions to the configuration dimension D=5 in Recognition Science. The inductive type MetaethicalPosition enumerates five constructors: moralRealism, constructivism, nonCognitivism, errorTheory, and moralRelativism, each deriving DecidableEq, Repr, BEq, and Fintype to support cardinality computation. This establishes five canonical positions corresponding to configDim D=5: moral realism (cognitivist), constructivism, non-cognitivism (expressivism), error theory, and moral relativism.
proof idea
The structure is populated directly by the single field five_positions, which receives the cardinality value computed from the Fintype instance on the inductive type MetaethicalPosition. No lemmas or tactics are invoked; the definition is a one-line structural wrapper.
why it matters
This structure supplies the certificate used by the downstream metaethicalPositionsCert definition, which constructs an explicit instance via the count function. It fills the module's role of equating the philosophical enumeration to configDim D=5, consistent with the five positions listed in the module documentation. The declaration touches no open questions but supports further philosophical derivations inside the Recognition Science monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.