147theorem is_implies_ought : 148 -- IS (structural facts) 149 (∀ x : ℝ, 0 < x → 0 ≤ defect x) ∧ 150 (∀ x : ℝ, 0 < x → (defect x = 0 ↔ x = 1)) ∧ 151 -- OUGHT (derived from IS via cost identification) 152 -- Good = zero defect = x = 1 153 (∀ a : EthicalAction, MorallyGood a ↔ a.after = 1) ∧ 154 -- Better = lower defect 155 (∀ a b : EthicalAction, MorallyBetter a b ↔ moral_cost a ≤ moral_cost b) := by
proof body
Term-mode proof.
156 refine ⟨fun x hx => defect_nonneg hx, fun x hx => defect_zero_iff_one hx, ?_, fun _ _ => Iff.rfl⟩ 157 intro a 158 constructor 159 · intro h 160 unfold MorallyGood moral_cost at h 161 exact (defect_zero_iff_one a.after_pos).mp h 162 · intro h 163 unfold MorallyGood moral_cost 164 rw [h] 165 exact defect_at_one 166 167/-- **Theorem (Hume's Guillotine Dissolved)**: 168 Hume's claim "no 'ought' from 'is'" is dissolved. 169 In RS, the IS-OUGHT gap is bridged by identifying: 170 171 good(x) = (defect(x) = 0) 172 173 This identification is not arbitrary — it is forced by the RS framework: 174 stable configurations (RSExists) are exactly those with zero defect. 175 And "stable" in RS is the meaning of "real" and "good." -/
depends on (28)
Lean names referenced from this declaration's body.