love_has_unique_sigma_effect
plain-language theorem explainer
Love is the only core DREAM virtue whose sigma effect is nonzero while justice, courage, and wisdom each leave sigma unchanged. Researchers formalizing ethical generators in the Recognition Science framework cite this result when tracking how virtues modify global imbalance. The proof is a direct simplification that unfolds the explicit sigma_effect assignments in the four virtue definitions.
Claim. The sigma effect of love is nonzero while the sigma effects of justice, courage, and wisdom are each zero: $sigma_{love} neq 0 land sigma_{justice} = 0 land sigma_{courage} = 0 land sigma_{wisdom} = 0$.
background
In the Ethics.VirtueSignatures module each DREAM virtue receives a VirtueSignature record containing a name, family loadings across four families, and a sigma effect. The sigma effect measures change in global imbalance and is drawn from the sigma definition in Decision.AbileneParadox, where sigma(a) equals the gap between an agent's private preference and public vote: +1 when privately preferring stay but publicly voting go, -1 for the reverse, and 0 for truthful agents. The module states that love has a unique sigma effect as the sole mechanism for changing global imbalance while justice preserves sigma by redistributing without altering the total. Upstream definitions assign sigma_effect := -1 to love and sigma_effect := 0 to justice, courage, and wisdom.
proof idea
The proof is a one-line wrapper that applies simplification to the explicit definitions of love, justice, courage, and wisdom, directly yielding the nonzero value for love and zeros for the remaining three virtues.
why it matters
This theorem supports the claim that love is the sole virtue capable of altering sigma imbalance among the core DREAM virtues and feeds directly into the L3_scope definition in Papers.ClaimBoundaries, which outlines the E-3 section on DREAM Virtues as Ethical Generators. It aligns with the Recognition Science treatment of sigma as a measure of private-public discrepancy and underscores love's distinctive role in changing global imbalance, consistent with the framework's emphasis on recognition-theoretic structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.