narrativeInterpret
plain-language theorem explainer
narrativeInterpret converts an element of the forced natural numbers into a beat count. It supplies the carrier type for the narrativeRealization instance of LogicRealization. The definition is a one-line wrapper around the iteration-count map from ArithmeticFromLogic.
Claim. The map sending a forced natural number (inductive type generated by the zero-cost identity and the step constructor) to its iteration count in $mathbb{N}$.
background
The module formalizes lightweight narrative realization: the carrier is the beat count generated by an inciting event. This encodes the claim that narrative order reuses the same forced Peano object as the arithmetic layer. NarrativeBeat is the abbreviation for the type of natural numbers. LogicNat is the inductive type whose constructors identity and step mirror the orbit closed under multiplication by the generator and containing the multiplicative identity. The upstream toNat function reads off the iteration count: identity to 0 and step n to the successor of toNat n.
proof idea
One-line wrapper that applies the toNat map from LogicNat to Nat.
why it matters
The definition supplies the Carrier field inside narrativeRealization, which builds the LogicRealization record with compare set to narrativeCost. It directly implements the module-level claim that narrative order carries the same forced Peano object. The construction reuses the arithmetic structure already forced in ArithmeticFromLogic and sits inside the UniversalForcing layer that prepares discrete beat counts for later cost comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.