loveEffect
plain-language theorem explainer
The love virtue effect supplies concrete parameters inside the VirtueEffect structure: zero sigma change together with jbar and gap multipliers of 0.8 and 1.5. Researchers working on the DREAM ethical framework cite this definition when they verify that composed virtues preserve the skew parameter sigma. The definition is a direct record construction whose two positivity obligations are discharged by norm_num.
Claim. The effect of the love virtue is the structure satisfying $sigma_change = 0$, $bar{j}_multiplier = 0.8$, $gap_multiplier = 1.5$, with proofs that both multipliers are positive.
background
VirtueEffect is a structure that records how one virtue alters the skew parameter sigma, scales the average jbar, and scales the gap, together with proofs that the two scaling factors are positive. The VirtueComposition module models sequential application of virtues as algebraic composition of these records and proves that sigma preservation is closed under such composition. This supplies the algebraic foundation for the DREAM ethical framework.
proof idea
The definition directly assembles the VirtueEffect record with the supplied numeric values and invokes norm_num on the two positivity fields.
why it matters
This definition is invoked by the theorem that shows the composition of the love and justice effects preserves sigma. It thereby supplies one concrete instance to the algebraic foundation for the DREAM ethical framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.