moral_progress_is_defect_decrease
plain-language theorem explainer
moral_progress_is_defect_decrease shows that one ethical action is morally better than another exactly when the defect of its resulting configuration is smaller or equal. Researchers formalizing objective ethics from the J-cost structure would cite this as the direct link between moral ordering and defect reduction. The proof is a one-line reflexivity that follows from the definition of moral cost as the defect of the after state.
Claim. Let $a$ and $b$ be ethical actions. Then $a$ is morally better than $b$ if and only if the defect of the configuration reached by $a$ is at most the defect of the configuration reached by $b$.
background
The module derives objective morality from the J-cost function forced by the Recognition Composition Law. An EthicalAction is a structure with a positive real before state and a positive real after state; it maps one configuration to another. MorallyBetter is defined by comparing the moral costs of two actions, where moral cost equals the defect of the resulting state.
proof idea
This is a term-mode proof consisting of the single line Iff.rfl. It holds by reflexivity because MorallyBetter is defined directly in terms of the defect comparison on the after states, using the defect functional from LawOfExistence.
why it matters
The declaration fills the central step in PH-004 by equating moral ordering with defect decrease, dissolving Hume's is-ought gap via the identification of goodness with stability under J-cost. It supports downstream results such as moral_ideal_is_unique and the DREAM theorem on virtues as defect-reducing transformations. In the framework it realizes good(x) ≡ defect(x) = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.