EffectSignature
plain-language theorem explainer
EffectSignature is the record type pairing one of four virtue categories with a natural-number index. Virtue independence proofs cite it to enumerate the fourteen signatures without semantic overlap. The declaration is a direct structure with derived decidable equality and representation.
Claim. An effect signature is a pair $(C, n)$ where $C$ is a virtue category (relational, systemic, temporal, or facilitative) and $n$ is a natural number indexing the member within that category.
background
The module proves combinatorial properties of a fixed catalogue of fourteen virtue effect signatures: they are distinct, non-redundant, and mutually independent under removal. VirtueCategory is the inductive type whose four constructors label the groups: Relational (love, compassion, sacrifice), Systemic (justice, temperance, humility), Temporal (wisdom, patience, prudence), and Facilitative (forgiveness, gratitude, courage, hope, creativity). EffectSignature attaches an index to each category so that each of the fourteen signatures receives a unique pair.
proof idea
The declaration is a direct structure definition that introduces the two fields category and index and derives the DecidableEq and Repr instances.
why it matters
EffectSignature supplies the uniform type for the list allSignatures and for each concrete constructor such as compassionSignature and courageSignature. It therefore anchors the downstream proofs that the fourteen-element catalogue is minimal and complete. The module treats these signatures as purely structural objects, independent of any semantic reading of the underlying ethical transforms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.