VirtueEffect
plain-language theorem explainer
VirtueEffect packages the effect of a virtue as a real-valued change in the imbalance measure σ together with positive multipliers for the J-bar and gap terms. Workers on the DREAM ethical framework cite the structure as the fundamental representation of virtue effects. The declaration is a bare structure definition carrying the two positivity assertions as fields.
Claim. A virtue effect is a record consisting of a real number $Δσ$ for the change in imbalance, a positive real multiplier $m_{J̄}$ for the J-bar quantity, and a positive real multiplier $m_{gap}$ for the gap quantity.
background
The Virtue Composition module supplies an algebraic model for the DREAM ethical framework in which virtues are represented by their effects on the skew measure σ. VirtueEffect is the structure that bundles the net change in σ with multipliers for the J-bar and gap quantities, the only constraints being the positivity of those multipliers. The companion definition preservesSigma identifies those effects that leave σ unchanged. The entire development is local to the module and requires no external lemmas.
proof idea
The declaration is a plain structure definition. The positivity conditions appear directly as fields of the structure and introduce no additional proof obligations.
why it matters
VirtueEffect is the carrier type for all subsequent constructions in the module. It is instantiated by loveEffect and justiceEffect, consumed by the compose operation that adds sigma changes and multiplies the multipliers, and used in the statements of composed_virtues_preserve_sigma and virtue_composition_associative. The structure therefore supplies the algebraic foundation for the claim that composed virtues preserve σ whenever each factor does.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.