justice
plain-language theorem explainer
The justice definition supplies the VirtueSignature record for the justice virtue, with name Justice, unit loading on the second family and zero elsewhere, plus sigma effect zero. Researchers modeling DREAM virtues as operators on global imbalance would cite this entry when proving redistribution properties. The definition is a direct structure instantiation requiring no lemmas or tactics.
Claim. The justice virtue signature is the structure with name ``Justice'', family loading $f : {0,1,2,3} → ℝ$ given by $f(1)=1$ and $f(i)=0$ otherwise, and sigma effect equal to zero.
background
The Ethics.VirtueSignatures module equips each DREAM virtue with a Born-profile signature. The referenced VirtueSignature structure is a record containing a name (String), a family loading function (Fin 4 → ℝ) that assigns real weights across four families, and a sigma effect (ℝ) that quantifies net change to global imbalance σ.
proof idea
Direct definition that populates the VirtueSignature record with the literal name, the piecewise family loading, and sigma effect zero. No upstream lemmas are invoked; the construction is purely by record literal.
why it matters
This supplies the concrete justice entry required by downstream results such as justice_preserves_sigma (which states justice.sigma_effect = 0) and each_virtue_distinct_signature (which separates the four base loadings). It realizes the module claim that justice redistributes without altering total imbalance, completing one slot in the 14-virtue basis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.