cost_ordering_gives_ethics
plain-language theorem explainer
Any real-valued cost function on a set of actions supplies an ethical ordering in which lower cost counts as morally preferable. Recognition Science researchers cite the result when identifying physical stability with objective goodness via J-cost. The proof is a one-line term that applies reflexivity of the biconditional.
Claim. For any set $A$ and cost function $c : A → ℝ$, and for any $a, b ∈ A$, the inequality $c(a) ≤ c(b)$ holds if and only if it holds, thereby equating ethical preference with cost minimization.
background
The module resolves the is-ought problem by treating J-cost as the normative structure forced by the Recognition Composition Law. J-cost is the function $J(x) = ½(x + x^{-1}) - 1$, whose zero-defect fixed point at $x = 1$ defines stable configurations. The local setting equates goodness with defect zero and derives moral ordering directly from any cost model that respects this structure.
proof idea
The proof is a one-line wrapper that applies Iff.rfl to the cost inequality, establishing the biconditional by reflexivity.
why it matters
The declaration anchors the PH-004 certificate by making moral ordering identical to cost ordering. It feeds the summary claim that ought follows from is via J-cost identification and defect minimization at $x = 1$. The result sits inside the forcing chain after T5 J-uniqueness and before the DREAM theorem that supplies the 14 virtues as cost-minimizing generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.