NarrativeBeat
plain-language theorem explainer
NarrativeBeat supplies the natural-number carrier for beat counts in narrative realizations of logic. Constructions of narrative cost and interpretation functions cite it to equip LogicRealization with a Peano object. The declaration is a direct abbreviation of Nat that supplies the required carrier type.
Claim. Let NarrativeBeat denote the set of natural numbers $N$, serving as the carrier type whose elements count beats generated by an inciting event.
background
The module NarrativeRealization supplies a lightweight carrier for narrative order. Its doc states that the carrier is the beat count generated by an inciting event and that narrative order carries the same forced Peano object. NarrativeBeat is the type used for this carrier. Downstream definitions equip it with a cost function that returns 0 on equality and 1 otherwise, together with an interpretation map from LogicNat.
proof idea
Direct abbreviation of Nat; supplies the Peano naturals as the beat carrier with no further construction.
why it matters
NarrativeBeat is the carrier in narrativeRealization, which instantiates LogicRealization with Carrier := NarrativeBeat, Cost := Nat, compare := narrativeCost and zero := 0. This supplies the structural claim that narrative order carries the forced Peano object, feeding the universal forcing setup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.