preservesSigma
plain-language theorem explainer
preservesSigma is the predicate asserting that a VirtueEffect produces no net change in the skew parameter σ. Researchers working on the DREAM ethical framework cite it when showing that the set of sigma-preserving effects is closed under composition. The definition is realized by direct equality to the sigma_change field of the input structure.
Claim. A virtue effect $v$ preserves the skew parameter $σ$ precisely when the recorded change in skew is zero.
background
The module models virtues as effects on a skew parameter $σ$ together with scaling factors. A VirtueEffect record consists of a real number for the change in $σ$, two positive real multipliers for jbar and gap, and proofs that those multipliers are positive. Composition of effects is defined so that the composite sigma change is the sum of the individual changes. The module documentation states that this construction supplies the algebraic foundation for the DREAM ethical framework.
proof idea
The definition is a direct field access returning the proposition that the sigma change component equals zero. No lemmas or tactics are applied.
why it matters
The predicate supplies the hypothesis in the theorem that sigma-preserving effects are closed under composition. It is also used to verify that the specific composition of the love and justice effects preserves sigma. In this way the definition anchors the claim that sequential application of virtues maintains balance in the DREAM framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.