prefer_refl
plain-language theorem explainer
The lemma establishes reflexivity of the ethical preference relation induced by any cost model, showing that every action is preferred to itself under the cost ordering. Researchers modeling ethical decisions or preorder structures within Recognition Science would cite this as the foundational reflexivity axiom. The proof is a direct one-line reduction that unfolds the definition of Prefer and applies reflexivity of the real-number order.
Claim. For any cost model $M$ over actions of type $A$, and any action $a$, $a ≼ a$ holds, where $a ≼ b$ means the cost of $a$ is at most the cost of $b$.
background
A CostModel is a structure consisting of a function cost : A → ℝ together with the axiom that all costs are nonnegative. The preference relation Prefer M a b, written with infix ≼, is defined exactly by cost a ≤ cost b, so lower cost is strictly better. This module sits in the Ethics domain and imports from Gap45.Beat plus Mathlib to support the basic order properties on ℝ.
proof idea
The proof is a one-line wrapper. It applies dsimp to unfold the definition of Prefer, reducing the goal to cost a ≤ cost a, then invokes le_rfl for reflexivity of the real order.
why it matters
This lemma supplies the reflexivity base case for the preorder instance on actions under any cost model and directly supports the transitivity lemma prefer_trans in the same module. It completes the preorder construction for ethical preference within the Recognition cost framework. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.