eventCost
plain-language theorem explainer
eventCost defines a binary cost on EventState pairs that returns zero exactly when the states coincide and one otherwise. Researchers constructing admissible narrative realizations cite it to verify the zero-cost axiom in strict logic realizations. The definition is introduced by a direct case split on decidable equality of the two states.
Claim. Let $c$ be the function from pairs of event states to natural numbers given by $c(a,b) := 0$ if $a=b$ and $c(a,b):=1$ otherwise, where an event state is a pair of natural numbers (act, beat).
background
In the Strict Narrative module, event states are structures carrying two natural-number coordinates (act and beat) equipped with decidable equality. The module supplies a domain-rich realization of narrative structures whose generator is the inciting beat-step. The cost function supplies the compare operation inside the strict logic realization that packages carrier, cost, zero, compare, and compose.
proof idea
The definition is a direct conditional expression that branches on equality of the two EventState arguments, returning zero on the affirmative branch and one on the negative branch. No lemmas or tactics are applied.
why it matters
eventCost supplies the compare field of strictNarrativeRealization, which is the carrier for narrative_admissible. It thereby anchors the zero-cost condition required for admissible realizations in the universal forcing chain and feeds the symmetry and zero-self theorems that appear in RichDomainCosts. The definition closes the narrative-to-cost interface without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.