eventCost_symm
plain-language theorem explainer
Event cost between pairs of event states is symmetric. Researchers formalizing strict narrative realizations cite this to confirm the compare operation is undirected. The proof splits on whether the states coincide, substitutes in the equal case, and simplifies using the definition in both branches.
Claim. Let $C(a,b)$ be the event cost on states $a,b$, equal to zero when $a=b$ and one otherwise. Then $C(a,b)=C(b,a)$ for all event states $a,b$.
background
In the Strict/Narrative module, EventState is the structure pairing two natural numbers (act, beat) with decidable equality. The function eventCost returns zero on identical states and one otherwise, serving as the compare operation in narrative realizations generated by inciting beat-steps. This local setting supplies the cost measure for StrictLogicRealization. The theorem depends only on the definition of eventCost and the equality structure of EventState.
proof idea
The tactic proof opens with case analysis on a = b. The equal branch substitutes and simplifies directly from the eventCost definition. The unequal branch constructs the symmetric inequality b ≠ a and simplifies again, yielding the desired equality in both cases.
why it matters
The result feeds strictNarrativeRealization, which installs eventCost as the compare field of StrictLogicRealization. It supplies the symmetry property required for the cost to serve as a well-behaved measure in domain-rich narrative realizations. Within the Recognition framework this is a basic consistency check on the generator before composition and realization steps are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.