MorallyBetter
plain-language theorem explainer
Recognition Science defines moral betterness between ethical actions by comparing the defect costs of their resulting configurations. Researchers deriving objective ethics from J-cost minimization cite it when establishing preorder properties or bridging is-ought. The definition is introduced as a direct inequality on the defect functional applied to post-action states.
Claim. An ethical action $a$ is morally better than an ethical action $b$ when the defect of the resulting configuration of $a$ is at most the defect of the resulting configuration of $b$, i.e., $J(a_2) ≤ J(b_2)$ where $J$ is the cost function and $a_2, b_2$ are the after-states.
background
In the Recognition Science framework the J-cost is the unique function $J(x) = ½(x + x^{-1}) - 1$ forced by the Recognition Composition Law; defect is identified with this J-value for positive real configurations. The module ObjectiveMoralityStructure treats an EthicalAction as a transition from one positive real configuration (before) to another (after), so that moral evaluation reduces to the change in ledger defect. The moral cost of any such action is therefore the defect of its after-state, with zero defect occurring exactly at unity.
proof idea
The declaration is a direct definition that sets the predicate equal to the inequality of the two moral costs. No lemmas or tactics are invoked; the body simply unfolds the cost function and applies the standard ordering on reals.
why it matters
This definition supplies the comparison relation used by all downstream results in the module, including better_action_exists, ethics_is_objective, hume_guillotine_dissolved, and is_implies_ought. It realizes the module's central claim that the ethical ordering is forced by the same J-cost structure that governs physical stability, thereby dissolving Hume's guillotine by equating goodness with zero defect. The construction sits inside the T5–T8 forcing chain where J-uniqueness and the fixed point at unity determine both physical and moral preference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.