eventCost_symm
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute numerical costs for concrete act or beat values.
- Does not address event composition or beat succession.
- Does not extend the cost beyond the binary equality indicator.
formal statement (Lean)
27theorem eventCost_symm (a b : EventState) : eventCost a b = eventCost b a := by
proof body
Tactic-mode proof.
28 by_cases h : a = b
29 · subst h
30 simp [eventCost]
31 · have h' : b ≠ a := by intro hb; exact h hb.symm
32 simp [eventCost, h, h']
33