justiceEffect

formal source

  33  { sigma_change := 0, jbar_multiplier := 0.8, gap_multiplier := 1.5,
  34    jbar_mult_pos := by norm_num, gap_mult_pos := by norm_num }
  35
  36def justiceEffect : VirtueEffect :=
  37  { sigma_change := 0, jbar_multiplier := 1.0, gap_multiplier := 1.1,
  38    jbar_mult_pos := by norm_num, gap_mult_pos := by norm_num }
  39
  40theorem composed_virtues_preserve_sigma
  41    (v₁ v₂ : VirtueEffect)
  42    (h₁ : preservesSigma v₁) (h₂ : preservesSigma v₂) :
  43    preservesSigma (compose v₁ v₂) := by
  44  unfold preservesSigma compose at *
  45  simp [h₁, h₂]
  46
  47theorem love_composed_with_justice :
  48    preservesSigma (compose loveEffect justiceEffect) := by
  49  unfold preservesSigma compose loveEffect justiceEffect
  50  norm_num
  51
  52theorem virtue_composition_associative
  53    (v₁ v₂ v₃ : VirtueEffect) :
  54    compose (compose v₁ v₂) v₃ = compose v₁ (compose v₂ v₃) := by
  55  unfold compose
  56  ext <;> simp [add_assoc, mul_assoc]
  57
  58end
  59
  60end IndisputableMonolith.Ethics.VirtueComposition