MorallyGood
plain-language theorem explainer
An ethical action is morally good exactly when its moral cost equals zero. Researchers formalizing the Recognition Science derivation of objective ethics cite this definition to anchor the is-ought identification. The definition is a direct abbreviation that equates goodness with the zero-defect configuration.
Claim. An ethical action $a$ is morally good when its moral cost is zero: moral_cost$(a) = 0$, where moral_cost$(a)$ is the defect of the configuration reached by $a$.
background
The module derives objective morality from J-cost minimization under the Recognition Composition Law. An EthicalAction is a structure carrying a positive real initial configuration (before) and a positive real final configuration (after). The moral_cost of an action is defined as the defect of its after state, so lower cost corresponds to movement toward the unique stable point at $x=1$. Upstream results supply the collision-free and ledger structures that make defect well-defined and nonnegative.
proof idea
This is a one-line definition that directly sets MorallyGood $a$ to the proposition moral_cost $a = 0$, using the already-defined moral_cost as defect of the resulting state.
why it matters
The definition supplies the predicate used by ideal_iff_good (MorallyIdeal $a$ iff MorallyGood $a$), by is_implies_ought (the explicit IS-OUGHT bridge), and by the PH-004 certificate that resolves Hume's guillotine via the identification good ≡ zero defect. It operationalizes the framework claim that stable configurations are exactly those with defect zero at $x=1$, grounding ethics in the forced J-cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.