CardinalVirtue
plain-language theorem explainer
The inductive definition introduces the type of five cardinal virtues as an enumeration extending the classical Aristotelian four with practical wisdom to match the configDim = 5 structure in Recognition Science. RS ethicists would cite it when grounding virtue theory in the forced dimension count. The declaration is a direct inductive type with automatically derived decidability and finiteness instances.
Claim. The inductive type of cardinal virtues consists of the five constructors prudence, justice, fortitude, temperance, and practical wisdom.
background
The module sets configDim to 5 to accommodate the five cardinal virtues, extending the classical Aristotelian quartet (prudence, justice, fortitude, temperance) by adding practical wisdom as the integrating fifth element. This matches the D = 5 pattern stated in the module documentation for the Recognition Science view of ethics.
proof idea
The declaration is a direct inductive definition with five constructors and no proof body. It derives the DecidableEq, Repr, BEq, and Fintype instances automatically via the deriving clause.
why it matters
This definition supplies the type used by the downstream theorem cardinalVirtue_count establishing Fintype.card CardinalVirtue = 5 and by the structure CardinalVirtuesCert certifying the five_virtues count together with the four-plus-one decomposition. It grounds the classical virtues in the RS configDim = 5 pattern described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.