eventCost_decidable
plain-language theorem explainer
EventState equality is made decidable by this definition in the Narrative domain. Researchers formalizing strict logic realizations cite it to confirm excluded-middle content for domain costs. The implementation is a one-line wrapper that retrieves the automatically derived DecidableEq instance on the structure.
Claim. For all Narrative event states $a, b$, the equality predicate $a = b$ is decidable.
background
EventState is a structure with fields act : Nat and beat : Nat, carrying an automatically derived DecidableEq instance. The Rich Domain Cost Theorems module supplies the concrete decidability, zero-cost, and composition statements that replace placeholder instances in the five domain modules (Music, Biology, Narrative, Ethics, Metaphysical). Each domain thereby obtains a first-class StrictLogicRealization with excluded_middle_law realized by decidability of its cost predicate.
proof idea
One-line wrapper that applies inferInstance to the DecidableEq instance derived from the EventState structure definition.
why it matters
This supplies the excluded-middle law for the Narrative domain cost, one of the six required properties listed in the module documentation for non-trivial strict realizations. It supports the overall claim that each domain satisfies composition, invariance, and decidability without axioms. In the Recognition framework it anchors the decidability step needed before invoking the composition law and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.