creativitySignature
plain-language theorem explainer
creativitySignature assigns the creativity virtue the effect signature consisting of the Facilitative category and index 4. Researchers enumerating the 14-virtue catalogue cite it when verifying distinctness and completeness in the Independence module. The definition is a direct constructor application to the EffectSignature structure.
Claim. The creativity signature is the effect signature with category facilitative and index 4, written as the pair consisting of the facilitative category and the natural number 4, where EffectSignature is the structure with fields category : VirtueCategory and index : ℕ.
background
The Ethics.Virtues.Independence module proves that the 14 virtue effect signatures are distinct, non-redundant, and mutually independent as structural properties of the catalogue. EffectSignature is defined as the structure pairing a VirtueCategory with a natural number index, described in its doc-comment as 'Effect signature: category plus within-category index'. This definition places creativity in the Facilitative category at index 4 within that structure. The module relies only on standard axioms such as propext and Quot.sound for its proofs.
proof idea
The definition is a one-line constructor application that supplies the Facilitative category and the index 4 directly to the EffectSignature structure. No lemmas are invoked and no tactics are used.
why it matters
This definition populates the allSignatures list that enumerates the full set of 14 signatures to enable the module's proofs of distinctness and minimality. It completes the catalogue entry for creativity and supports the combinatorial independence claims stated in the module doc-comment. The module addresses structural properties of the signature list rather than direct connections to the forcing chain or recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.