IndisputableMonolith.Ethics.VirtueComposition

   1import Mathlib
   2
   3/-!
   4# Virtue Composition — Composed Virtues Produce Compound Effects
   5
   6When virtues are applied in sequence, their effects compose.
   7If both virtues preserve σ (skew/imbalance), their composition
   8preserves σ as well. This provides the algebraic foundation
   9for the DREAM ethical framework.
  10-/
  11
  12namespace IndisputableMonolith.Ethics.VirtueComposition
  13
  14noncomputable section
  15
  16structure VirtueEffect where
  17  sigma_change : ℝ
  18  jbar_multiplier : ℝ
  19  gap_multiplier : ℝ
  20  jbar_mult_pos : jbar_multiplier > 0
  21  gap_mult_pos : gap_multiplier > 0
  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
  56  ext <;> simp [add_assoc, mul_assoc]
  57
  58end
  59
  60end IndisputableMonolith.Ethics.VirtueComposition
  61