actionCost_zero_iff
plain-language theorem explainer
The equivalence establishes that action cost between two ActionStates is zero precisely when the states are identical. Researchers verifying strict realizations for the Ethics domain in the Recognition framework cite it to confirm the cost acts as a discrete metric. The argument unfolds the if-then-else definition of the cost and splits on decidable equality, simplifying in each branch to obtain both directions.
Claim. For action states $a$ and $b$, the cost function satisfies $C(a,b)=0$ if and only if $a=b$, where $C(a,b)$ equals $0$ when $a=b$ and $1$ otherwise.
background
ActionState is the structure whose fields are an agent identifier and an improvement rank, both natural numbers, with decidable equality derived. The action cost is the function returning the natural number $0$ on equal states and $1$ on unequal states. This theorem sits inside the Rich Domain Costs module, whose purpose is to replace placeholder StrictLogicRealization instances for the five domains (Music, Biology, Narrative, Ethics, Metaphysical) with concrete proofs of decidability, zero-cost equivalence, associativity, and left-identity laws.
proof idea
Unfold the definition of actionCost to expose the if-then-else on equality. Apply case analysis on whether the two states coincide. Simplification in the equal branch yields the forward direction; simplification in the unequal branch yields the converse.
why it matters
The result is assembled into richDomainCostsCert_holds, the top-level certificate that each domain cost satisfies the required laws. It supplies the concrete zero-cost content for the Ethics domain, replacing the earlier invariance-law placeholder. In the broader framework it supports the claim that the strict realizations are non-trivially law-bearing, consistent with the forcing-chain steps that derive composition and invariance from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.