eventCost_zero_iff
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove decidability of the cost predicate.
- Does not establish associativity of event composition.
- Does not cover costs in the music or biology domains.
- Does not derive any triangle inequality.
- Does not address invariance under relabeling.
formal statement (Lean)
107theorem eventCost_zero_iff (a b : EventState) :
108 eventCost a b = 0 ↔ a = b := by
proof body
Term-mode proof.
109 unfold eventCost
110 by_cases h : a = b
111 · simp [h]
112 · simp [h]
113