prefer_by_cq
plain-language theorem explainer
In ethical cost models, equal costs between actions imply preference for the one with at least as high CQ alignment at threshold θ. Researchers modeling ethical ties in Recognition Science frameworks would cite this result when resolving costless choices via alignment scores. The proof reduces directly by unfolding the preference definition and simplifying with the cost equality hypothesis.
Claim. Let $M$ be a cost model over actions of type $A$. For actions $a,b$, CQ values $c_1,c_2$, and real number θ, if $0≤θ≤1$, if CQ alignment of $c_2$ at θ implies alignment of $c_1$ at θ, and if the cost of $a$ equals the cost of $b$ under $M$, then the cost of $a$ is at most the cost of $b$ under $M$.
background
CostModel is a structure supplying a function from actions to nonnegative reals together with a nonnegativity proof. Prefer is the relation on actions that holds precisely when the cost of the first is less than or equal to the cost of the second. CQAligned(θ,c) is the predicate asserting that θ lies in [0,1] and the score of c meets or exceeds θ; CQ itself is the alignment score type imported from Measurement.
proof idea
The proof is a one-line wrapper that applies dsimp to unfold Prefer into the cost inequality and then simp using the supplied cost equality hypothesis. No external lemmas beyond the local definitions are required.
why it matters
This result supplies the basic monotonicity rule for CQ alignment in cost ties inside the Ethics.CostModel module, supporting ethical preference construction. It parallels the aesthetic preference definition (negation of J-cost) from SymmetryGroupPreference and sits alongside the cost function from MultiplicativeRecognizerL4 and ObserverForcing. No downstream uses are recorded yet, leaving open how it composes into full ethical decision chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.