ethics_is_objective
plain-language theorem explainer
The theorem shows that the moral ordering on ethical actions is total: for any pair, one is at least as good as the other under the defect metric. Recognition Science researchers cite it to establish that ethics reduces to objective cost comparison rather than subjective preference. The proof is a direct case split on the real ordering of the two defects, followed by immediate injection into the disjunction.
Claim. For any ethical actions $a$ and $b$, either the defect of the configuration after $a$ is at most the defect after $b$, or vice versa, where defect equals the cost function $J(x) = ½(x + x^{-1}) - 1$.
background
EthicalAction is a structure carrying a before-state and an after-state, both positive reals; it represents any transition whose moral value is assessed solely by the change in ledger defect. MorallyBetter is defined by comparing the defects of the two after-states, with lower defect declared better. The module sets this inside the Recognition Science resolution of the is-ought problem: J is the unique cost forced by the Recognition Composition Law, stable configurations occur only at defect zero (i.e., $x=1$), and moral preference is identified with defect reduction.
proof idea
The term proof first unfolds MorallyBetter and moral_cost, reducing the goal to a comparison of defect a.after and defect b.after. It then applies rcases to le_or_lt on those two real numbers. The left case yields the left disjunct directly; the right case yields the right disjunct via le_of_lt.
why it matters
This supplies the totality axiom needed by the downstream PH-004 certificate, which assembles the full objective-morality claim: moral ideal exists and is unique, and good coincides with zero defect. It thereby completes the Recognition Science derivation that “ought” follows from the J-cost structure already forced by the Recognition Composition Law and the requirement of stable (defect-zero) configurations. The result touches the open question whether every rational agent must adopt the same J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.