  22
  23def preservesSigma (v : VirtueEffect) : Prop := v.sigma_change = 0
  24
  25def compose (v₁ v₂ : VirtueEffect) : VirtueEffect :=
  26  { sigma_change := v₁.sigma_change + v₂.sigma_change
  27    jbar_multiplier := v₁.jbar_multiplier * v₂.jbar_multiplier
  28    gap_multiplier := v₁.gap_multiplier * v₂.gap_multiplier
  29    jbar_mult_pos := mul_pos v₁.jbar_mult_pos v₂.jbar_mult_pos
  30    gap_mult_pos := mul_pos v₁.gap_mult_pos v₂.gap_mult_pos }
  31
  32def loveEffect : VirtueEffect :=
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.