narrativeZero
plain-language theorem explainer
narrativeZero supplies the zero element of the EventState structure as the pair with both act and beat coordinates equal to zero. Researchers formalizing strict narrative realizations within the universal forcing chain cite it as the neutral element for event composition. The definition is a direct one-line structure constructor with no additional obligations.
Claim. The zero element of the event-state structure is the pair $0_E := (0,0)$ where the first coordinate is the act index and the second is the beat index, both drawn from the natural numbers.
background
EventState is the structure whose fields are two natural-number coordinates, act and beat, serving as the carrier type for strict narrative realizations. The Narrative module constructs domain-rich realizations in which beat succession acts as the generator. The upstream EventState definition supplies the concrete type on which composition and cost are later defined.
proof idea
One-line definition that applies the EventState constructor directly to the pair of literals 0 and 0.
why it matters
narrativeZero supplies the neutral element required by the left-identity theorem eventCompose_left_id and is instantiated inside the admissible-realization construction narrative_admissible. It completes the strictNarrativeRealization by providing the zero element of the carrier, anchoring the narrative layer of the universal forcing framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.