actionCost_self
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not specify the cost between distinct action states.
- Does not depend on concrete values of agent or improvementRank.
- Does not address composition of actions or preference relations.
formal statement (Lean)
25@[simp] theorem actionCost_self (a : ActionState) : actionCost a a = 0 := by
proof body
One-line wrapper that applies simp.
26 simp [actionCost]
27