justiceEffect
plain-language theorem explainer
The justice effect definition supplies a concrete instance of the virtue effect structure with zero sigma change, unit jbar multiplier, and gap multiplier of 1.1. Researchers modeling ethical compositions in the DREAM framework cite it when verifying sigma preservation under virtue composition. The definition is a direct record construction that uses norm_num to establish the required positivity conditions.
Claim. The justice effect is the VirtueEffect record whose sigma-change component is 0, whose jbar-multiplier is 1, whose gap-multiplier is 1.1, and whose positivity proofs for the two multipliers hold.
background
VirtueEffect is the structure that records the change in the imbalance parameter sigma, the scaling factor for the average jbar, and the scaling factor for the gap, together with proofs that the scaling factors are positive. The module shows that when virtues are applied in sequence their effects compose, and that if both preserve sigma then the composition does as well. This supplies the algebraic foundation for the DREAM ethical framework. The upstream result is the definition of the VirtueEffect carrier itself.
proof idea
The definition constructs the VirtueEffect record by setting the three numeric fields explicitly and applying norm_num to the two positivity hypotheses.
why it matters
This definition is invoked by the theorem that the composition of the love effect and the justice effect preserves sigma. It fills the role of a concrete virtue instance in the algebraic foundation for ethical compositions within Recognition Science. No open question is directly touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.