sig_ne_of_cat_ne
plain-language theorem explainer
Signatures with different virtue categories cannot be identical. Researchers establishing the distinctness of the fourteen-signature catalogue cite this to separate the four classes before addressing intra-category indices. The argument is a one-line wrapper that assumes equality of signatures, extracts equality of categories, and derives a contradiction by case analysis.
Claim. If two effect signatures $s_1$ and $s_2$ satisfy $s_1$.category ≠ $s_2$.category, then $s_1$ ≠ $s_2$.
background
EffectSignature is a structure consisting of a VirtueCategory together with a natural-number index. VirtueCategory is an inductive type with four constructors: Relational, Systemic, Temporal, and Facilitative. The module proves that the fourteen listed signatures are pairwise distinct and that the list satisfies a minimality condition under removal.
proof idea
This is a one-line wrapper. It introduces the assumption that the two signatures are equal, applies the given category inequality, performs case analysis on that equality, and closes with reflexivity to obtain the contradiction.
why it matters
The result separates signatures across the four virtue categories and thereby supports the module's proof that the fourteen signatures are distinct and non-redundant. It belongs to the category-orthogonality section and relies only on standard foundational axioms. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.