EthicalAction

formal source

  64
  65/-- An ethical action: something that can be evaluated by its effect on ledger defect.
  66    An action maps from one configuration to another. -/
  67structure EthicalAction where
  68  /-- The initial configuration (current moral state) -/
  69  before : ℝ
  70  before_pos : 0 < before
  71  /-- The final configuration (resulting moral state) -/
  72  after : ℝ
  73  after_pos : 0 < after
  74
  75/-- The moral cost of an ethical action: the defect of the resulting state.
  76    Lower is better. -/
  77noncomputable def moral_cost (a : EthicalAction) : ℝ := defect a.after
  78
  79/-- An action is **morally better** than another if it results in lower defect. -/
  80def MorallyBetter (a b : EthicalAction) : Prop := moral_cost a ≤ moral_cost b
  81
  82/-- An action is **morally good** (optimal) if it achieves zero defect. -/
  83def MorallyGood (a : EthicalAction) : Prop := moral_cost a = 0
  84
  85/-- An action is **morally ideal** if it reaches x = 1 (the unique J-minimum). -/
  86def MorallyIdeal (a : EthicalAction) : Prop := a.after = 1
  87
  88/-! ## Fundamental Moral Theorems -/
  89
  90/-- **Theorem (Unique Moral Ideal)**: There is a unique morally ideal outcome.
  91    The J-minimum x = 1 is the sole configuration with zero defect.
  92    Objective ethics has ONE correct answer, not many. -/
  93theorem moral_ideal_is_unique :
  94    ∀ a b : EthicalAction, MorallyIdeal a → MorallyIdeal b → a.after = b.after := by
  95  intro a b ha hb
  96  rw [ha, hb]
  97