better_action_exists
plain-language theorem explainer
Any non-ideal ethical action admits a strictly better successor under the moral ordering induced by defect cost. Researchers deriving objective ethics from physical cost minimization cite this result to establish that improvement is always possible short of the ideal state. The term proof directly exhibits the successor by mapping the current outcome to unity and invokes non-negativity plus strict positivity of the defect functional.
Claim. For any ethical action $a$ with resulting configuration $a_ {after} ≠ 1$, there exists an ethical action $b$ such that the defect of $b$'s resulting state is at most that of $a$'s and strictly smaller.
background
The module PH-004 derives objective morality from the Recognition Science cost structure. An ethical action is a mapping between positive real configurations whose moral cost equals the defect of the final configuration, where defect coincides with the J-functional $J(x) = ½(x + x^{-1}) - 1$. MorallyBetter holds precisely when one action yields a result of lower or equal defect than another.
proof idea
The term proof refines the existential witness to the concrete action that takes the current after-state of the input action to the ideal value 1. Unfolding MorallyBetter and moral_cost reduces the inequalities to defect(1) = 0 together with defect nonnegativity and the strict inequality defect(x) > 0 for x ≠ 1, which are supplied by the upstream lemmas defect_at_one, defect_nonneg, and defect_pos_of_ne_one.
why it matters
The result is invoked by hume_guillotine_dissolved to establish that the is-ought gap is bridged via cost identification and by ph004_objective_morality_certificate to certify that objective morality follows from physics. It realizes the Recognition Science claim that moral progress equals defect reduction on the J-cost ladder, with the unique ideal at zero defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.