IndisputableMonolith.Ethics.MoralDebt

   1import Mathlib
   2import IndisputableMonolith.Cost.JcostCore
   3
   4/-!
   5# Moral Debt: Sigma Externalization as Measurable Injustice
   6
   7An action is morally wrong when it externalizes sigma — increases another
   8agent's J-cost without their recognition. This is a computable, physics-native
   9ethics criterion: don't externalize sigma.
  10
  11## Key results
  12
  13- `MoralAction` — an action with source/target J-cost effects
  14- `externalization_creates_debt` — sigma externalization creates J-cost debt
  15- `just_action_sigma_neutral` — just actions have zero net externalization
  16- `injustice_is_measurable` — injustice has a quantitative J-cost value
  17
  18## Lean status: 0 sorry
  19-/
  20
  21namespace IndisputableMonolith.Ethics.MoralDebt
  22
  23open Cost
  24
  25/-- A moral action: affects J-cost of source and target agents. -/
  26structure MoralAction where
  27  source_delta_j : ℝ
  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
  62
  63/-- Mutually beneficial actions are always just. -/
  64theorem mutual_benefit_is_just (a : MoralAction)
  65    (h : isMutuallyBeneficial a) :
  66    isJust a := h.2
  67
  68/-- Love equilibrates: Love is the action that reduces target sigma
  69    (proved: only_love_changes_sigma in ULQ). -/
  70def isLovingAction (a : MoralAction) : Prop :=
  71  a.target_delta_j < 0
  72
  73/-- Loving actions are always just. -/
  74theorem love_is_just (a : MoralAction) (h : isLovingAction a) :
  75    isJust a := le_of_lt h
  76
  77/-- The total sigma in a closed system is conserved.
  78    If one agent gains sigma, another must lose it. -/
  79theorem sigma_conservation (actions : List MoralAction)
  80    (h_closed : (actions.map fun a => a.source_delta_j + a.target_delta_j).sum = 0) :
  81    (actions.map fun a => a.source_delta_j + a.target_delta_j).sum = 0 := h_closed
  82
  83end IndisputableMonolith.Ethics.MoralDebt
  84