moral_ordering_refl
plain-language theorem explainer
Reflexivity of the moral ordering on ethical actions follows directly from cost comparison. Researchers deriving objective ethics from Recognition Science J-cost minimization would cite this to anchor the preorder structure. The proof is a one-line wrapper applying the reflexivity of the underlying numerical ordering to moral costs.
Claim. For any ethical action $a$, the moral cost of $a$ satisfies moral cost of $a$ less than or equal to moral cost of $a$.
background
EthicalAction is a structure with an initial positive real configuration (before) and a resulting positive real configuration (after), representing a transition evaluated by its effect on ledger defect. MorallyBetter is the relation holding when the moral cost of one action is less than or equal to that of another, where moral cost measures the defect of the resulting state. Lower defect corresponds to greater stability under the J-cost function. The module derives objective morality from the Recognition Composition Law forcing J(x) as the unique cost, identifying goodness with zero defect. This theorem supplies the reflexive half of the preorder. It depends on the upstream le_refl establishing reflexivity of the ordering in the arithmetic foundation.
proof idea
One-line wrapper that applies le_refl from the arithmetic foundation directly to the moral cost of the input action.
why it matters
This establishes reflexivity of the moral ordering, the first step in showing MorallyBetter forms a preorder on actions. It supports the module's resolution of Hume's is-ought problem by grounding moral preference in J-cost minimization and defect reduction. The result precedes sibling theorems such as moral_ordering_trans and contributes to the claim that ought follows from is via stability at defect zero. It aligns with the framework's T5 J-uniqueness and the identification of good configurations with RSExists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.