CardinalVirtuesCert
plain-language theorem explainer
The structure packages a certificate that exactly five cardinal virtues exist by pairing the finite cardinality of an explicit enumeration with the arithmetic identity four plus one equals five. A Recognition Science philosopher extending classical ethics to the configuration dimension would cite it to align virtues with the five-fold pattern. The definition is a bare structure declaration that assembles these two facts directly.
Claim. A structure certifying that the finite type of cardinal virtues has cardinality 5, where the virtues are the five constructors prudence, justice, fortitude, temperance and practical wisdom, together with the equation $4 + 1 = 5$.
background
The module examines cardinal virtues in Recognition Science by extending the classical Aristotelian four with practical wisdom to reach five, matching the configuration dimension D = 5. The inductive type enumerates precisely these five virtues. An upstream theorem records the arithmetic identity four plus one equals five and interprets it as the classical quartet plus the integrating fifth.
proof idea
The declaration is a direct structure definition that specifies the two fields: the cardinality of the virtues type and the arithmetic identity. It inherits the inductive enumeration and the decide proof of the upstream arithmetic result without applying further tactics or lemmas.
why it matters
This structure is instantiated by the downstream definition that constructs the certificate for use throughout the philosophy module. It supplies the ethical extension of the configDim pattern, aligning the five virtues with the five-fold structure noted in the module documentation. The construction touches the broader question of how Recognition Science maps configuration dimensions onto classical categories.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.