eventCost
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assign any cost value other than zero or one.
- Does not incorporate the numerical values of act or beat beyond equality testing.
- Does not enforce the triangle inequality or any metric axioms.
- Does not depend on external parameters or additional structure.
formal statement (Lean)
21def eventCost (a b : EventState) : Nat :=
proof body
Definition body.
22 if a = b then 0 else 1
23