moral_ideal_is_unique
plain-language theorem explainer
The theorem establishes uniqueness of the morally ideal outcome: any two ethical actions reaching the J-minimum share the same final configuration. Researchers deriving objective ethics from recognition science would cite it to show that the ethical optimum is single-valued rather than plural. The proof is a direct one-line rewriting that substitutes the definition of MorallyIdeal into the after-states.
Claim. For all ethical actions $a$ and $b$, if $a$ reaches the configuration with zero defect and $b$ reaches the configuration with zero defect, then the resulting state of $a$ equals the resulting state of $b$.
background
An EthicalAction is a structure with positive-real fields before and after that records the change in configuration under evaluation by ledger defect. MorallyIdeal is the predicate that the after-field equals 1, the unique point where the J-cost function $J(x) = (x + x^{-1})/2 - 1$ attains its global minimum of zero. The module PH-004 derives objective morality by identifying stable configurations (RSExists) with zero-defect states under the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that applies rewriting. After introducing the two actions and the two hypotheses that each is morally ideal, it rewrites the after-fields using those hypotheses to obtain equality.
why it matters
The result supplies the uniqueness conjunct required by hume_guillotine_dissolved and ph004_objective_morality_certificate. Those theorems certify that the is-ought gap is bridged by the forced identification good(x) ≡ defect(x) = 0 at the J-minimum x = 1. It directly instantiates the framework claim that the J-minimum is the sole stable configuration, confirming that objective ethics admits only one correct answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.