composed_virtues_preserve_sigma
plain-language theorem explainer
If two virtue effects each have zero sigma change, their sequential composition also has zero sigma change. Researchers modeling compound ethical effects in the DREAM framework cite this to guarantee invariance under composition. The proof is a one-line wrapper that unfolds the definitions of preservesSigma and compose then simplifies with the two hypotheses.
Claim. Let $v_1$ and $v_2$ be virtue effects. If $v_1$ satisfies $v_1.σ_{change}=0$ and $v_2$ satisfies $v_2.σ_{change}=0$, then the composed effect defined by $σ_{change}=v_1.σ_{change}+v_2.σ_{change}$, $j_{bar}$ multiplier equal to the product of the two multipliers, and gap multiplier likewise equal to the product, also satisfies $σ_{change}=0$.
background
VirtueEffect is a structure carrying three real numbers: the change in σ (skew or imbalance), a positive multiplier for jbar, and a positive multiplier for gap. The predicate preservesSigma holds precisely when the sigma_change field is zero. The operation compose adds the two sigma_change values and multiplies the two pairs of multipliers while preserving positivity. The module states that this algebraic rule supplies the foundation for the DREAM ethical framework when virtues are applied in sequence.
proof idea
The proof unfolds preservesSigma and compose at the goal and hypotheses, then applies simp using the two equalities h₁ and h₂. The resulting goal reduces to showing that the sum of two zeros is zero, which simplification discharges immediately.
why it matters
The result is used by L3_scope in Papers.ClaimBoundaries to support the E-3 claim that DREAM virtues function as ethical generators. It closes the basic invariance step in the virtue-composition chain inside the Recognition Science ethics layer, ensuring that balanced effects remain balanced under sequential application.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.