MorallyIdeal

formal source

  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
  98/-- **Theorem (Morally Ideal = Morally Good)**:
  99    An action is morally ideal iff it is morally good (zero cost). -/
 100theorem ideal_iff_good (a : EthicalAction) : MorallyIdeal a ↔ MorallyGood a := by
 101  unfold MorallyIdeal MorallyGood moral_cost
 102  constructor
 103  · intro h; rw [h]; exact defect_at_one
 104  · intro h; exact (defect_zero_iff_one a.after_pos).mp h
 105
 106/-- **Theorem (Moral Ordering)**:
 107    The ethical ordering (MorallyBetter) is a preorder on actions.
 108    This gives an objective moral preference structure. -/
 109theorem moral_ordering_refl (a : EthicalAction) : MorallyBetter a a :=
 110  le_refl _
 111
 112theorem moral_ordering_trans (a b c : EthicalAction)
 113    (hab : MorallyBetter a b) (hbc : MorallyBetter b c) :
 114    MorallyBetter a c :=
 115  le_trans hab hbc
 116