EthicalAction
plain-language theorem explainer
EthicalAction packages a pair of positive real numbers as the initial and final ledger configurations whose moral value is judged by the defect of the final state. Researchers deriving objective ethics from the Recognition Composition Law cite it as the basic object type for the is-ought identification. The declaration is a direct structure with two fields and their positivity proofs; no lemmas are invoked.
Claim. An ethical action is a pair of positive real numbers $(b, a)$ with $b > 0$ and $a > 0$, representing an initial configuration and a resulting configuration; its moral cost is the defect $J(a)$ of the final state.
background
In Recognition Science the defect functional is defined by defect(x) := J(x) where J(x) = ½(x + x⁻¹) − 1. The module PH-004 treats this cost as the sole criterion for moral evaluation, identifying lower defect with ethical improvement and zero defect with the unique stable configuration x = 1. Upstream structures supply the supporting cost definitions: LedgerFactorization calibrates J on the positive reals, ObserverForcing and MultiplicativeRecognizerL4 both reduce recognition cost to J-cost, and LawOfExistence records defect(x) = 0 precisely when x = 1.
proof idea
The declaration is a plain structure definition that introduces the type EthicalAction together with the two positivity hypotheses. No tactics or lemmas are applied; the fields are simply declared and the positivity constraints attached directly.
why it matters
EthicalAction supplies the carrier type for the entire PH-004 development. It is instantiated in better_action_exists to exhibit strictly improving sequences, in ethics_is_objective to obtain deterministic moral comparisons, and in hume_guillotine_dissolved to equate the moral ideal with zero defect. The structure thereby closes the is-ought gap by making the J-cost ordering the sole source of ethical preference, consistent with the Recognition Composition Law and the uniqueness of the phi-fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.