Systemic_ne_Facilitative
plain-language theorem explainer
The result establishes that the category containing justice, temperance and humility is distinct from the category containing forgiveness, gratitude, courage, hope and creativity. A researcher checking the non-redundancy of the fourteen virtue signatures would cite this fact when confirming the catalogue remains complete after any single removal. The argument is a one-line wrapper that assumes equality and obtains a contradiction by case analysis on the inductive constructors.
Claim. Within the inductive classification of ethical transformation types, the category for justice, temperance and humility is not identical to the category for forgiveness, gratitude, courage, hope and creativity: $C_{sys} ≠ C_{fac}$.
background
The module proves structural and combinatorial properties of the fourteen virtue effect signatures: they are pairwise distinct, removing any one breaks the completeness condition, and each is absent from the reduced list. The four categories are defined by an inductive type whose constructors group the virtues as follows: relational for love, compassion and sacrifice; systemic for justice, temperance and humility; temporal for wisdom, patience and prudence; facilitative for forgiveness, gratitude, courage, hope and creativity. All distinctions rely only on the decidable equality derived from this inductive definition and on standard foundational axioms.
proof idea
The proof is a one-line wrapper. It introduces the assumed equality hypothesis and immediately applies case analysis on the two distinct constructors, yielding an immediate contradiction.
why it matters
This theorem supplies one of the pairwise inequalities required to establish that the fourteen signatures are distinct and non-redundant. It therefore contributes directly to the module's stated goal of verifying the structural completeness and minimality of the catalogue. No downstream results depend on it yet, and it touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.