actionCost
actionCost assigns a natural-number cost to pairs of action states, returning zero exactly when the states coincide. It is cited as the compare operation in constructions of strict ethical realizations and admissible classes. The definition is a direct conditional on equality of the states.
claimFor action states $a$ and $b$, each a pair of a natural-number agent identifier and improvement rank, the cost is defined by $actionCost(a,b) := 0$ if $a = b$, and $1$ otherwise.
background
ActionState is the structure pairing a natural-number agent identifier with an improvement rank, equipped with decidable equality. The Strict Ethics module develops domain-rich ethical realizations in which the generator is the smallest recognized improvement step. actionCost supplies the compare operation for these realizations, depending only on the ActionState definition.
proof idea
The definition is given directly by a conditional expression: return 0 if the two action states are equal and 1 otherwise. It relies on the decidable equality instance derived for ActionState.
why it matters in Recognition Science
This supplies the compare field for strictEthicsRealization, which is used to construct ethics_admissible in the AdmissibleClass module. It realizes the minimal improvement generator in ethical domains, supporting symmetry and zero-cost properties. It contributes to admissible realizations that interface with the forcing chain.
scope and limits
- Does not apply to structures other than ActionState.
- Does not satisfy the triangle inequality.
- Does not yield real-valued or continuous costs.
- Does not define preference composition or arithmetic operations.
Lean usage
theorem example (a : ActionState) : actionCost a a = 0 := by simp [actionCost]formal statement (Lean)
22def actionCost (a b : ActionState) : Nat :=
proof body
Definition body.
23 if a = b then 0 else 1
24