SignatureSetMinimal
plain-language theorem explainer
The predicate requiring a list of effect signatures to contain no duplicates supports proofs that the virtue catalogue is minimal. Researchers establishing non-redundancy of the 14 signatures cite this condition when showing that the full list satisfies distinctness while any proper sublist fails completeness. The definition is introduced as a direct abbreviation of the standard list noduplicate property.
Claim. A list $S$ of effect signatures, each pairing a virtue category with a natural-number index, satisfies the minimality predicate if and only if all members of $S$ are pairwise distinct.
background
The module on virtue independence and minimality shows that the 14 effect signatures are distinct and that removing any one breaks the completeness condition. An effect signature is defined as a structure with a virtue category field and a natural-number index field, equipped with decidable equality. This supplies the combinatorial setting for statements about lists of such signatures.
proof idea
The definition is a one-line abbreviation that equates the predicate on an input list directly to the standard noduplicate condition.
why it matters
It is invoked by the theorem all_signatures_minimal, which asserts the full list satisfies the predicate, and by the combined statement virtue_signatures_minimality_complete that packages minimality, completeness, and non-redundancy. The predicate therefore anchors the module's explicit proofs that the catalogue has no internal repetition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.