compose
plain-language theorem explainer
Virtue effects combine by summing their sigma changes and multiplying their jbar and gap multipliers. Workers on the DREAM ethical framework cite this construction when forming sequences of virtues. The definition builds the output record directly from the input fields and reuses the positivity proofs via the multiplication lemma.
Claim. For virtue effects $v_1$ and $v_2$, their composition is the effect with sigma-change equal to the sum of the two sigma-changes, jbar multiplier equal to the product of the two jbar multipliers, and gap multiplier equal to the product of the two gap multipliers, where positivity of the products follows from the positivity of the factors.
background
A VirtueEffect records a real-valued change in the imbalance measure sigma together with positive real multipliers for the jbar and gap quantities. The module states that sequential application of virtues produces compound effects and that preservation of sigma is closed under this operation. This algebraic setup supplies the composition law required by the DREAM framework inside Recognition Science.
proof idea
The definition constructs the result by adding the sigma_change components and multiplying the multiplier components, then applies the mul_pos lemma to the positivity hypotheses to obtain the required positivity proofs for the products.
why it matters
This supplies the binary operation used by the theorems on preservation of sigma under composition, the specific love-justice example, and the associativity result. It is referenced by the CostMorphism structure in the algebra layer and by locality and canonicality results in the foundation. The construction realizes the composition law needed to embed ethical structure into the same multiplicative framework that governs the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.