allSignatures
plain-language theorem explainer
allSignatures supplies the explicit 14-element list that serves as the fixed catalogue of virtue effect signatures for the entire independence module. Researchers establishing combinatorial properties of virtues cite this list when invoking distinctness, length, or minimality results. The definition is a direct enumeration of the fourteen pre-defined signatures, each constructed as a category-index pair.
Claim. Let $S$ be the list of fourteen effect signatures, where each signature is a pair consisting of a virtue category and a natural-number index within that category. The list $S$ is defined to contain the signatures for love, compassion, sacrifice, justice, temperance, humility, wisdom, patience, prudence, forgiveness, gratitude, courage, hope, and creativity.
background
The module establishes structural properties of a catalogue of virtue effect signatures. An EffectSignature is a structure consisting of a VirtueCategory together with a natural-number index inside that category. The module proves that the fourteen signatures are distinct, that removing any one destroys completeness, and that each signature is absent from the list obtained by erasing it. All proofs rely only on standard axioms and explicit computation; no compiler-trust axioms are used.
proof idea
The definition is a direct enumeration of the fourteen individually declared signatures. No tactics or lemmas are applied; the body simply lists loveSignature through creativitySignature in order.
why it matters
This definition supplies the concrete list on which every independence and completeness theorem in the module depends. It is invoked by all_signatures_distinct to establish noduplication, by allSignatures_length to fix the cardinality at 14, and by signatures_complete, all_signatures_minimal, and all_virtues_independent to prove the catalogue is minimal and non-redundant. The list therefore anchors the combinatorial claims that the fourteen signatures form a minimal complete set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.