actionCost_self
plain-language theorem explainer
The theorem establishes zero self-cost for any action state under the ethical cost function. Researchers verifying minimal-improvement generators in strict ethical realizations would cite it to confirm the identity case. The proof is a one-line simp wrapper that unfolds the actionCost definition.
Claim. For any action state $a$, the cost of $a$ to itself satisfies $actionCost(a,a)=0$.
background
ActionState is a structure with fields agent and improvementRank, both natural numbers, equipped with decidable equality. The actionCost function is defined to return 0 precisely when its two arguments are identical and 1 otherwise. The module develops domain-rich ethical realizations over these states, taking the smallest recognized improvement step as generator.
proof idea
The proof is a one-line simp wrapper that applies the definition of actionCost and reduces the equality case directly to zero.
why it matters
The result is invoked inside the definition of strictEthicsRealization, which assembles a StrictLogicRealization whose compare operation is actionCost. It supplies the required zero-cost identity for self-transitions, ensuring the ethical model is consistent with the minimal-improvement generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.