PreferLex
plain-language theorem explainer
PreferLex encodes lexicographic ethical preference by placing admissibility checks ahead of cost comparison for actions under a fixed period and CQ alignment. Decision theorists formalizing ethics within Recognition Science cite it when ordering actions that must respect experience thresholds before minimizing cost. The definition is a direct disjunctive construction that first tests strict admissibility advantage then falls back to the underlying Prefer relation.
Claim. Let $M$ be a cost model over actions of type $A$, $p$ a natural-number period, $c$ a CQ alignment, $e_A$ and $e_B$ experience propositions, and $a,b$ actions. The relation PreferLex$(M,p,c,e_A,e_B,a,b)$ holds precisely when $(Admissible(p,c,e_A) ∧ ¬Admissible(p,c,e_B)) ∨ (Admissible(p,c,e_A) ∧ Admissible(p,c,e_B) ∧ Prefer(M,a,b))$, where Admissible$(p,c,e)$ is true if no experience is required for $c$ at period $p$ or $e$ holds, and Prefer$(M,a,b)$ means the cost of $a$ is at most the cost of $b$.
background
CostModel is the structure that equips any carrier type $A$ with a cost function to nonnegative reals together with the nonnegativity axiom. CQ is the alignment predicate imported from Measurement that asserts a score meets a fixed threshold. Admissible$(p,c,e)$ is the predicate that returns true unless experience is required for the given CQ at period $p$ and the experience proposition $e$ is false; Prefer$(M,a,b)$ is simply the cost comparison $M.cost a ≤ M.cost b$ lifted from the same module.
proof idea
This is a definition that directly assembles the lexicographic order as a disjunction of two clauses. The first clause captures the case where $a$ is admissible and $b$ is not; the second clause handles the joint-admissible case by invoking the cost-based Prefer relation. No lemmas are applied; the body is the explicit propositional combination of the referenced Admissible and Prefer predicates.
why it matters
PreferLex supplies the primary ordering primitive inside the Ethics.CostModel module and therefore sits at the base of any downstream ethical decision procedure that must respect physical periods and CQ thresholds. It directly implements the lexicographic priority of admissibility over cost that the module doc-comment describes, linking the phi-derived period function from Astrophysics to ethical preference. No parent theorems are yet recorded as users, leaving its integration into larger ethics lattices open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.