actionCost
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.