Improves
Defines the strict improvement predicate on actions under a cost model, where a improves on b precisely when its assigned cost is strictly smaller. Decision theorists and mechanism designers extending Recognition Science to ethical preferences would cite it to establish monotonicity under composition. The definition is a direct abbreviation of the strict inequality on the model's cost function.
claimLet $M$ be a cost model over a set of actions $A$. Action $a$ strictly improves on $b$ if and only if the cost of $a$ is strictly less than the cost of $b$.
background
CostModel is a structure that equips any type $A$ of actions with a function cost : $A$ → ℝ together with the axiom that all costs are nonnegative. The module Ethics.CostModel builds an ethical preference layer on top of Recognition Science primitives, importing cost notions from observer forcing (where cost equals J-cost of the state) and from multiplicative recognizers. Upstream results include the definition of A as the active edge count per fundamental tick and the identification of recognition-event costs with J-cost.
proof idea
This is a direct definition that unfolds immediately to the strict inequality M.cost a < M.cost b.
why it matters in Recognition Science
It supplies the strict preference relation required by the Composable structure and by the theorem improves_comp_left that shows composition preserves improvements. The predicate therefore closes the link between Recognition Science cost functions and ethical mechanism design, feeding directly into subadditive and monotonic composition axioms.
scope and limits
- Does not specify any concrete form for the cost function beyond nonnegativity.
- Does not assert that the induced relation is a total order or transitive.
- Does not apply to cost models that violate the nonnegativity axiom.
- Does not encode any particular ethical theory beyond the lower-cost-is-better convention.
formal statement (Lean)
26def Improves (M : CostModel A) (a b : A) : Prop := M.cost a < M.cost b
proof body
Definition body.
27
28/-- Reflexivity: every action is at least as good as itself. -/