love_composed_with_justice
plain-language theorem explainer
The theorem shows that the sequential composition of the love effect and justice effect leaves the sigma invariant unchanged. Modelers of sequential virtue application in the DREAM framework cite the result to confirm that zero-sigma virtues remain balanced under composition. The proof is a direct unfolding of the four definitions followed by arithmetic normalization.
Claim. If the love effect has sigma change zero and the justice effect has sigma change zero, then the composed effect also has sigma change zero.
background
VirtueEffect is a record that stores a sigma change (skew or imbalance), a jbar multiplier, and a gap multiplier. preservesSigma holds exactly when the sigma change component equals zero. The compose operation adds the two sigma changes and multiplies the corresponding multipliers, with positivity proofs carried along.
proof idea
The proof unfolds preservesSigma, compose, loveEffect, and justiceEffect, then applies norm_num to verify that the summed sigma change is zero.
why it matters
The result supplies a concrete verification that sigma-preserving virtues remain sigma-preserving under composition, thereby supporting the algebraic foundation for the DREAM ethical framework stated in the module documentation. It instantiates the general composition rule for the specific pair of love and justice effects. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.