ph004_objective_morality_certificate
plain-language theorem explainer
Recognition Science derives objective morality by identifying moral goodness with zero J-cost defect at the fixed point x=1. The certificate asserts existence and uniqueness of the moral ideal, equivalence of morally good actions with those reaching x=1, totality of the moral ordering, and improvability of any non-ideal state. Ethicists and philosophers of physics working on naturalized ethics would cite this result. The proof proceeds by term construction, directly exhibiting the ideal action at x=1 and discharging the remaining conjuncts via
Claim. There exists an ethical action whose resulting configuration equals 1; this ideal is unique; an action is morally good if and only if its resulting configuration equals 1; the relation of being morally better is total on ethical actions; and every ethical action whose resulting configuration differs from 1 admits a strictly better successor.
background
In Recognition Science the J-cost function J(x) = ½(x + x⁻¹) − 1 is the unique cost forced by the Recognition Composition Law. An EthicalAction consists of a before-configuration and an after-configuration, both positive reals, whose moral cost is the defect of the after-state. MorallyIdeal means the after-state equals 1, the unique zero-defect point. MorallyGood means moral cost equals zero. MorallyBetter means lower or equal moral cost. The module resolves Hume's is-ought problem by showing that the normative 'ought' is identified with the descriptive 'is' of lower defect. Upstream, defect_at_one establishes defect(1)=0 and defect_zero_iff_one gives the characterization defect(x)=0 iff x=1 for x>0.
proof idea
The proof is a term-mode construction. It exhibits the ideal action as the transition to after=1, applies moral_ideal_is_unique to obtain uniqueness, invokes ethics_is_objective for the total ordering, and for the is-ought bridge uses defect_zero_iff_one together with defect_at_one to equate MorallyGood with after=1. The final conjunct follows by applying better_action_exists to any non-ideal action.
why it matters
This declaration is the central certificate (PH-004) of the ObjectiveMoralityStructure module, establishing that objective ethics is forced by the J-cost structure of Recognition Science. It dissolves Hume's guillotine by equating goodness with stability at x=1 and feeds the DREAM theorem that generates the 14 virtues as cost-minimizing transformations. The result sits downstream of the Law of Existence and the defect lemmas, closing the philosophy track by proving that moral progress is always possible from any non-ideal state.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.