moral_ordering_trans

formal source

 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
 117/-- **Theorem (Better Actions Exist)**: For any non-ideal action, a better one exists.
 118    This is the formal statement that moral improvement is always possible
 119    until the ideal is reached. -/
 120theorem better_action_exists (a : EthicalAction) (h_nonideal : a.after ≠ 1) :
 121    ∃ b : EthicalAction, MorallyBetter b a ∧ moral_cost b < moral_cost a := by
 122  refine ⟨⟨a.after, a.after_pos, 1, by norm_num⟩, ?_, ?_⟩
 123  · unfold MorallyBetter moral_cost
 124    simp [defect_at_one]
 125    exact defect_nonneg a.after_pos
 126  · unfold moral_cost
 127    simp [defect_at_one]
 128    exact defect_pos_of_ne_one a.after_pos h_nonideal
 129
 130/-! ## Hume's Guillotine Dissolved -/
 131
 132/-- **Theorem (IS-OUGHT Bridge)**:
 133    In RS, "is" (the cost structure) directly implies "ought" (the ethical ordering)
 134    via the identification: good ≡ low defect.
 135
 136    The key propositions:
 137    - IS: defect(x) ≥ 0 for all positive x
 138    - IS: defect(x) = 0 iff x = 1
 139    - IS: The ledger minimizes defect toward 1
 140
 141    OUGHT (derived, not assumed):
 142    - Actions that reduce defect are better