prefer_refl
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove transitivity or totality of the preference relation.
- Does not invoke Recognition constants such as phi or the eight-tick octave.
- Applies only to cost-based preference and does not extend to modal actualization or mass formulas.
formal statement (Lean)
29lemma prefer_refl (M : CostModel A) (a : A) : Prefer M a a := by
proof body
Term-mode proof.
30 dsimp [Prefer]
31 exact le_rfl
32
33/-- Transitivity: if `a ≼ b` and `b ≼ c`, then `a ≼ c`. -/