actionCost_symm
plain-language theorem explainer
Symmetry of the transition cost holds for every pair of states each specified by an agent identifier and improvement rank. Researchers constructing strict ethical realizations cite it to confirm the cost measure is undirected. The proof splits on whether the states coincide and reduces each case by simplification against the zero-one definition.
Claim. For all states $a$ and $b$, each consisting of a natural-number agent identifier and improvement rank, the transition cost from $a$ to $b$ equals the transition cost from $b$ to $a$.
background
ActionState pairs a natural-number agent identifier with a natural-number improvement rank and supplies decidable equality. The transition cost between two such states is defined to be zero when the states coincide and one otherwise. The module develops a domain-rich ethical realization over these states, with the generator given by the smallest recognized improvement step.
proof idea
The proof performs case analysis on whether the states are equal. When equal, substitution reduces the goal to reflexivity after simplification with the cost definition. When distinct, the symmetric inequality is derived and both inequalities are supplied to the simplifier, yielding equality of the unit costs.
why it matters
The result is invoked by the strict ethical realization, which instantiates the carrier with these states and the compare operation with the cost function. It supplies the required symmetry for the minimal improvement generator inside the universal forcing framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.