externalization

formal source

  28  target_delta_j : ℝ
  29
  30/-- Sigma externalization: J-cost increase imposed on target. -/
  31noncomputable def externalization (a : MoralAction) : ℝ :=
  32  max a.target_delta_j 0
  33
  34/-- An action externalizes sigma iff the target's J-cost increases. -/
  35def externalizesSigma (a : MoralAction) : Prop :=
  36  a.target_delta_j > 0
  37
  38/-- Externalization creates measurable debt on the receiving agent. -/
  39theorem externalization_creates_debt (a : MoralAction)
  40    (h : externalizesSigma a) :
  41    0 < externalization a := by
  42  simp only [externalization, externalizesSigma] at *
  43  exact lt_max_of_lt_left h
  44
  45/-- A just action has zero sigma externalization. -/
  46def isJust (a : MoralAction) : Prop :=
  47  a.target_delta_j ≤ 0
  48
  49/-- Just actions don't create debt on others. -/
  50theorem just_no_debt (a : MoralAction) (h : isJust a) :
  51    externalization a = 0 := by
  52  simp only [externalization, isJust] at *; exact max_eq_right h
  53
  54/-- Injustice cost: the J-cost imposed minus the source's own reduction.
  55    If injustice > 0, the action was net harmful. -/
  56noncomputable def injusticeCost (a : MoralAction) : ℝ :=
  57  a.target_delta_j + a.source_delta_j
  58
  59/-- Mutual benefit: both sides reduce J-cost. -/
  60def isMutuallyBeneficial (a : MoralAction) : Prop :=
  61  a.source_delta_j ≤ 0 ∧ a.target_delta_j ≤ 0