eventCost_self
plain-language theorem explainer
eventCost_self shows that the narrative cost between any event state and itself is zero. Researchers building strict logic realizations cite it to satisfy the zero element axiom for the cost structure. The proof is a one-line simp reduction on the piecewise definition of eventCost.
Claim. For every event state $a$, the cost function returns zero on identical arguments: eventCost$(a,a)=0$.
background
The module develops strict narrative realizations over event states carrying natural-number coordinates for act and beat, with the inciting beat-step as generator. EventState is the structure whose fields are two natural numbers act and beat, equipped with decidable equality and Repr. The upstream definition eventCost returns 0 precisely when its two arguments coincide and 1 otherwise.
proof idea
One-line wrapper that applies simp to unfold the definition of eventCost.
why it matters
It supplies the zero-cost instance required by strictNarrativeRealization, which instantiates StrictLogicRealization with EventState as carrier, Nat as cost type, and eventCost as the compare operation. This anchors the narrative model inside the Recognition Science forcing chain by guaranteeing the identity element for cost composition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.