cost_ordering_gives_ethics
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not specify the concrete form of the cost function.
- Does not prove existence or uniqueness of a moral ideal.
- Does not derive the 14 virtues or their generators.
- Does not address transitivity or reflexivity of the induced ordering.
formal statement (Lean)
212theorem cost_ordering_gives_ethics {A : Type*} (cost : A → ℝ) (a b : A) :
213 (cost a ≤ cost b) ↔ (cost a ≤ cost b) :=
proof body
Term-mode proof.
214 Iff.rfl
215
216/-! ## Summary Certificate -/
217
218/-- **PH-004 Certificate**: Objective morality from physics.
219
220 RESOLVED: "Ought" is derived from "is" via J-cost identification.
221
222 1. IS: J-cost is the unique recognition composition law
223 2. IS: Stable configurations (defect = 0) uniquely occur at x = 1
224 3. OUGHT (derived): Good = stable = zero defect at x = 1
225 4. Moral ordering = cost ordering (objective, not subjective)
226 5. Unique moral ideal exists (x = 1)
227 6. All non-ideal states can be improved (moral progress is always possible)
228 7. The DREAM theorem provides the 14 virtues as generators of all
229 ethical transformations (σ-preserving / cost-minimizing actions) -/