actionCost_decidable
plain-language theorem explainer
The declaration supplies a Decidable instance for equality on ActionState records, which carry an agent identifier and improvement rank. Researchers establishing excluded-middle content for domain costs in strict forcing realizations would cite it when replacing placeholder laws. The proof is a one-line wrapper that invokes the DecidableEq instance derived on the structure.
Claim. Let $a$ and $b$ be states each consisting of an agent identifier and an improvement rank, both natural numbers. Then equality $a = b$ is decidable.
background
The Rich Domain Cost Theorems module supplies concrete decidability, zero-cost, and composition results for five domains (Music, Biology, Narrative, Ethics, Metaphysical) that realize StrictLogicRealization instances. For the Ethics domain the state type is ActionState, a record with fields agent : Nat and improvementRank : Nat. The upstream structure ActionState derives DecidableEq, which directly supplies the instance used here.
proof idea
One-line wrapper that applies the DecidableEq instance derived for the ActionState structure.
why it matters
This definition completes the excluded-middle law for the Ethics domain cost, one of the five required to replace the placeholder laws in the source modules. It supports the claim that the strict realization is non-trivially law-bearing, as described in the module documentation. It participates in the overall proof that each domain satisfies the composition, invariance, and decidability requirements of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.