EventState
plain-language theorem explainer
EventState introduces the carrier type for strict narrative events as a pair of natural numbers tracking action and beat counts. Researchers on universal forcing and narrative realization cite it as the domain for event composition and cost functions. The declaration is a direct structure with no proof obligations, deriving decidable equality automatically.
Claim. An event state is a pair of natural numbers $(a, b)$ where $a$ denotes the action coordinate and $b$ the beat coordinate, equipped with decidable equality.
background
The Narrative module supplies domain-rich narrative realization over event states whose coordinates are natural numbers for action and beat. The inciting beat-step serves as the generator for successive states. Downstream definitions build directly on this carrier: eventCompose adds the two coordinates componentwise while eventCost returns zero exactly when the states coincide.
proof idea
This is a direct structure definition with an empty proof body. It declares the two Nat fields and derives DecidableEq and Repr; no lemmas or tactics are applied.
why it matters
EventState supplies the state space for eventCompose, eventCost, narrativeZero, incitingBeat, and strictNarrativeRealization. It anchors the narrative layer of the strict forcing construction, where beat succession generates the sequence of states. The definition thereby closes the basic carrier needed before the arithmetic and symmetry properties of event costs are established.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.