MorallyIdeal
plain-language theorem explainer
MorallyIdeal defines an ethical action as reaching the configuration x=1, the unique J-minimum with zero defect. Researchers deriving objective ethics from the Recognition Science cost structure cite this as the base predicate for the is-ought resolution. It is a direct abbreviation that equates moral ideality with the after-state being exactly unity.
Claim. An ethical action is morally ideal precisely when its final configuration equals 1.
background
EthicalAction is a structure with an initial positive real configuration before and a final positive real configuration after, representing a transition evaluated by its effect on ledger defect. The defect functional equals J(x) = (x + x^{-1})/2 - 1, which is zero only at x=1 by the uniqueness forced in the T5 step of the unified forcing chain. This module derives objective morality from physics by identifying moral preference with defect reduction under the Recognition Composition Law.
proof idea
This is a one-line definition that directly equates the predicate to equality of the after field with 1, using the structure fields of EthicalAction.
why it matters
This definition anchors the objective morality theorems, including hume_guillotine_dissolved and the PH-004 certificate that resolves the is-ought problem. It connects to the J-minimum at x=1 from the forcing chain T5-T8 and feeds moral_ideal_is_unique together with ideal_iff_good, establishing that ethics has a single objective answer derived from stability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.