hopeSignature
plain-language theorem explainer
hopeSignature assigns the Facilitative category with index 3 to the virtue of hope. Researchers verifying the 14-element catalogue in the Ethics.Virtues.Independence module cite it when checking completeness of allSignatures. The definition is a direct structure constructor application with no further computation.
Claim. The effect signature for hope is the pair consisting of the Facilitative category and the natural number 3, where an effect signature is a structure with a VirtueCategory value and an index in the naturals.
background
The module proves that the 14 virtue effect signatures are distinct, non-redundant, and mutually independent as structural properties of the catalogue. EffectSignature is the structure with fields category : VirtueCategory and index : ℕ. The local setting is the explicit verification of the 14-element completeness condition using only standard foundational axioms.
proof idea
Direct definition that applies the structure constructor to the Facilitative category and the literal 3.
why it matters
Supplies one entry in the allSignatures list that establishes the 14-element completeness condition. The module doc states these are combinatorial properties of the signature catalogue, not semantic independence of the transforms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.