eventCompose_assoc
plain-language theorem explainer
Event composition on narrative event states is associative under componentwise addition of act and beat values. Admissible realization proofs cite this result to confirm the composition law holds for the narrative domain. The proof reduces both sides via unfolding to two independent applications of natural number addition associativity.
Claim. Let $a, b, c$ be event states, each a pair of natural numbers $(act, beat)$. Let composition be defined by adding the act components and the beat components separately. Then $(a + b) + c = a + (b + c)$, where $+$ denotes event composition.
background
The Rich Domain Costs module supplies concrete theorems for the five domains (Music, Biology, Narrative, Ethics, Metaphysical) that realize the StrictLogicRealization with actual laws instead of placeholders. For the narrative domain, EventState is the carrier structure consisting of two natural-number fields act and beat. The operation eventCompose adds these fields pairwise. The upstream theorem add_assoc from ArithmeticFromLogic proves that addition on the underlying numbers is associative, which is invoked here.
proof idea
Unfold the definition of eventCompose on both sides of the target equality. Apply the congr tactic with argument 1 to split the resulting pair equality into separate equations for the act and beat components. Discharge each equation by direct appeal to the associativity of natural-number addition.
why it matters
This supplies the associativity axiom for narrative composition in the definition of narrative_admissible, which constructs an AdmissibleRealization. It is also packaged into richDomainCostsCert_holds, the top-level certificate for all domain costs. In the Recognition framework it closes the composition law for the narrative strict realization, allowing narrative structures to participate in the forcing chain without reducing to trivial placeholders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.