SignatureSetComplete
plain-language theorem explainer
SignatureSetComplete defines the predicate on lists of effect signatures that holds exactly when the list has length 14 and contains no duplicates. Researchers formalizing the minimality of the virtue catalogue cite this predicate to state that the canonical list satisfies completeness. The definition is introduced as a direct conjunction of length equality and the Nodup property with no auxiliary lemmas.
Claim. A list $s$ of effect signatures is complete when its length equals 14 and its elements are pairwise distinct: $|s|=14$ and Nodup$(s)$.
background
EffectSignature is the structure that pairs a VirtueCategory with a natural-number index inside that category. The module proves combinatorial properties of the fixed catalogue of fourteen such signatures: they remain distinct, and deletion of any one violates the completeness condition. These are purely structural facts about the signature list rather than claims about semantic independence of the underlying virtue transforms.
proof idea
The declaration is a direct definition that conjoins the length check with the Nodup predicate. No lemmas or tactics are invoked; the predicate is supplied for later theorems to reference.
why it matters
The predicate is the central definition referenced by signatures_complete (which asserts the full list meets it), signatures_non_redundant (which shows erasure of any entry breaks it), and virtue_signatures_minimality_complete (which packages both minimality and completeness). It supplies the formal statement of the fourteen-element catalogue whose independence properties are asserted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.