cardinalVirtuesCert
plain-language theorem explainer
The definition cardinalVirtuesCert assembles a witness for the five-virtue structure by supplying the proven cardinality of the CardinalVirtue type together with the arithmetic identity four plus one equals five. Researchers tracing ethical categories to the Recognition Science configDim parameter would cite it when matching classical virtues to the D equals five pattern. The construction is a direct record instantiation that applies two prior decidable theorems.
Claim. The definition provides an instance of the structure asserting that the cardinality of the type of cardinal virtues equals five and that four plus one equals five, with the cardinality field witnessed by the theorem establishing five virtues and the arithmetic field witnessed by the identity four plus one equals five.
background
The module treats five canonical virtues as an extension of the classical Aristotelian quartet, adding practical wisdom as the integrating fifth element to match the configDim equal to five pattern. The structure CardinalVirtuesCert encodes this requirement through two fields: one stating that the finite type of cardinal virtues has cardinality five, and one stating the natural-number equation four plus one equals five. Upstream results supply the cardinality theorem proved by decision procedure and the arithmetic identity proved by decision procedure.
proof idea
The definition is a direct structure constructor that populates the cardinality field with the theorem cardinalVirtue_count and the arithmetic field with the theorem four_plus_one.
why it matters
This definition supplies the concrete witness for the five-virtue structure, closing the link between the classical ethical quartet and the Recognition Science requirement that configDim equal five. It draws on the dimensional pattern from the broader framework where the classical four virtues are extended by one integrating element. No downstream uses are recorded, leaving open its integration into larger proofs about virtue ethics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.