VirtueSignature
plain-language theorem explainer
VirtueSignature supplies the data structure for encoding a DREAM virtue's Born-profile in the Recognition Science ethics module. It consists of a string name, a function assigning real loadings to each of four families, and a real sigma effect that records direct impact on global imbalance. Researchers modeling ethical decision making cite this structure to define concrete virtues such as love. The declaration is a bare structure introduction with no computational content or lemmas.
Claim. A virtue signature consists of a string name, a function $f : [4] → ℝ$ giving loadings on the four families, and a real number $σ$ recording the sigma effect on global imbalance.
background
The Ethics.VirtueSignatures module introduces Born-profile signatures for the 14 DREAM virtues. Each signature is a pattern of loadings across four families together with a sigma effect that tracks how the virtue alters global imbalance σ. The upstream sigma definition from the AbileneParadox module treats σ as the gap between private preference and public vote: +1 when an agent privately prefers stay but publicly votes go, and -1 for the reverse.
proof idea
The declaration is a direct structure definition that introduces the three fields name, family_loading, and sigma_effect with no tactics, reductions, or lemma applications.
why it matters
VirtueSignature is the common type underlying all virtue definitions and theorems in the module, including love, justice, courage, wisdom, non_love_preserves_sigma, and sigma_effect_well_defined. It implements the Born-profile signatures described in the module documentation and extends the sigma concept from decision theory into ethical modeling within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.