eventCost_zero_iff
plain-language theorem explainer
eventCost_zero_iff establishes that the narrative event cost vanishes exactly when the two states coincide. Researchers verifying strict realizations of domain costs cite it to confirm the zero-cost equivalence property. The proof reduces directly from the piecewise definition via case analysis on equality followed by simplification.
Claim. Let $E$ be the set of narrative event states, each a pair of natural numbers (act, beat). Let $c: E times E to mathbb{N}$ be defined by $c(a,b)=0$ if $a=b$ and $c(a,b)=1$ otherwise. Then $c(a,b)=0 iff a=b$ for all $a,b in E$.
background
The Rich Domain Costs module supplies the concrete theorems for the five domains (Music, Biology, Narrative, Ethics, Metaphysical) after placeholders in the source modules. For Narrative, EventState is the structure carrying natural numbers act and beat that derives DecidableEq. The eventCost function is the indicator returning 0 on the diagonal and 1 elsewhere, as defined in the Narrative module.
proof idea
The proof unfolds the definition of eventCost, applies by_cases on equality of the two states, and simplifies each branch to obtain the biconditional.
why it matters
This result is collected inside richDomainCostsCert_holds, which bundles the zero-cost, associativity, and identity properties across all five domains. It supplies the first-class statement for the narrative domain that the module documentation requires when claiming the strict realization is non-trivially law-bearing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.