Prefer
plain-language theorem explainer
Prefer defines the ethical preference relation on actions under a cost model by declaring a preferred to b precisely when the cost of a is at most the cost of b. Researchers extending Recognition Science into ethical decision theory cite it when establishing reflexivity, transitivity, or composition monotonicity. The definition is a direct one-line abbreviation of the cost inequality.
Claim. For a cost model $M$ over actions of type $A$, the preference relation satisfies $a ≼ b$ if and only if the cost of $a$ under $M$ is at most the cost of $b$.
background
CostModel is a structure pairing a cost function $A → ℝ$ with the axiom that all costs are nonnegative. This definition of Prefer appears in the Ethics.CostModel module and relies on cost functions imported from ObserverForcing (cost equals J-cost of a recognition event) and MultiplicativeRecognizerL4 (derived cost on positive ratios). The active edge parameter A is imported as the constant 1 from IntegrationGap and Masses.Anchor, anchoring costs to the phi-power balance at D=3.
proof idea
The declaration is a one-line definition that sets Prefer M a b to the proposition M.cost a ≤ M.cost b.
why it matters
Prefer supplies the base ordering predicate for downstream results including prefer_refl, prefer_trans, Composable, prefer_comp_mono, PreferLex, and prefer_by_cq. It connects the ethical layer to Recognition Science cost functions, permitting extension of J-uniqueness (T5) and the eight-tick octave (T7) into action selection. It leaves open how experience requirements modify the ordering inside the Admissible predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.