prudenceSignature
plain-language theorem explainer
Prudence receives the temporal category paired with index 2 inside the catalogue of virtue effect signatures. Researchers enumerating the full set of 14 signatures for independence and completeness arguments cite this entry. The definition is introduced by direct construction of the category-index pair.
Claim. The prudence signature is the effect signature whose category is temporal and whose index is the natural number 2.
background
The module establishes that the 14 virtue effect signatures are distinct, non-redundant, and mutually independent as structural properties of the catalogue. An effect signature is a pair consisting of a virtue category and a natural number index. The definition supplies the prudence entry that appears in the complete list of signatures.
proof idea
The definition constructs the signature directly as the pair of the temporal category and the index 2. No lemmas or tactics are invoked; it is a one-line definition.
why it matters
This definition is referenced by the allSignatures list that enumerates the complete set of 14 virtues. It supports the module's explicit proofs that the signatures remain distinct after any single removal. The module restricts itself to standard foundational axioms and avoids compiler-trust axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.