virtue_composition_associative
plain-language theorem explainer
Composition of ethical effects, each defined by a sigma change together with positive jbar and gap multipliers, is associative. Workers on the DREAM ethical framework cite the result when constructing sequences of virtues in the LNAL semantic core. The proof reduces the equality to componentwise associativity of addition and multiplication after unfolding the composition definition.
Claim. For ethical effects $v_1, v_2, v_3$, each a triple of a real sigma change with positive real jbar and gap multipliers, the composition defined by adding sigma changes and multiplying the multipliers satisfies $(v_1 ∘ v_2) ∘ v_3 = v_1 ∘ (v_2 ∘ v_3)$.
background
The VirtueEffect structure models an ethical effect by a sigma change (skew or imbalance), a jbar multiplier, and a gap multiplier, each multiplier required to be positive. Composition of two effects adds their sigma changes and multiplies the jbar multipliers and the gap multipliers separately, preserving positivity by the multiplication-positivity lemma.
proof idea
The proof unfolds the compose definition to expose the field-wise operations. Structure extensionality then reduces the equality to three componentwise statements. Simplification applies associativity of real addition to the sigma field and associativity of multiplication to the two multiplier fields.
why it matters
This theorem supplies the associativity axiom needed for the algebraic structure of composed virtues in the DREAM framework. It is referenced inside the L3_scope definition of Papers.ClaimBoundaries, which outlines the LNAL 5-op semantic core and positions DREAM virtues as ethical generators. Within Recognition Science it mirrors the Recognition Composition Law by furnishing a consistent binary operation, though the present result remains inside the ethics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.