hume_guillotine_dissolved
plain-language theorem explainer
The theorem shows that a unique morally ideal action exists in the Recognition Science model, where ideality means reaching the zero-defect state x=1, and every non-ideal action admits a successor that lowers defect. Philosophers and physicists examining objective ethics cite it as the explicit dissolution of Hume's is-ought gap via the forced identification of stability with zero J-cost. The proof is a term construction that supplies the constant action at x=1 for existence, invokes the sibling uniqueness lemma, and applies the better-action-1
Claim. There exists an ethical action reaching the configuration $x=1$ of zero J-cost. Any two ethical actions that both reach $x=1$ have identical final states. For every ethical action whose final state differs from $1$, there exists a morally better successor action that reduces ledger defect.
background
An EthicalAction is a structure carrying a before-configuration and an after-configuration, both positive reals; its moral cost is the defect of the after-state. MorallyIdeal holds precisely when the after-state equals 1, the unique fixed point of the J-function. MorallyBetter holds when the moral cost of the first action is at most that of the second. The module derives objective morality from J-cost minimization: J(x) = ½(x + x⁻¹) − 1 is the unique cost forced by the Recognition Composition Law, and stable configurations (RSExists) are exactly those with defect zero. Upstream results supply the defect functional from LawOfExistence and the ledger factorization that calibrates J.
proof idea
The term proof constructs the three conjuncts directly. Existence is witnessed by the constant action whose before and after are both 1. Uniqueness is obtained by direct appeal to the sibling lemma moral_ideal_is_unique. The improvement clause is obtained by applying better_action_exists to any non-ideal action and projecting out the witness and the MorallyBetter proof.
why it matters
This result closes the is-ought derivation in the Philosophy.ObjectiveMoralityStructure module by exhibiting the concrete bridge from defect structure to moral ordering. It rests on the J-uniqueness and phi-fixed-point steps of the T0-T8 forcing chain and on the identification good(x) ≡ defect(x) = 0. The theorem supplies the terminal claim that objective ethics is forced by the same cost function that governs physical stability, completing the moral-ordering block that begins with moral_cost and MorallyGood.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.