narrativeCost_self
plain-language theorem explainer
The theorem confirms that the narrative cost of any beat with itself is zero. Researchers building narrative realizations in the Recognition Science framework cite it to establish the zero element for beat-count comparisons. The proof is a one-line simp wrapper that unfolds the definition of narrativeCost.
Claim. For any natural number $a$, the narrative cost satisfies $narrativeCost(a,a)=0$.
background
NarrativeBeat is an abbreviation for the natural numbers and serves as the carrier for beat counts generated by an inciting event. The function narrativeCost returns 0 when its two arguments are equal and 1 otherwise. The module supplies a lightweight narrative realization that formalizes the structural claim that narrative order carries the same forced Peano object.
proof idea
The proof is a one-line wrapper that applies simp to the definition of narrativeCost, reducing the self-equality case directly to zero via the if-then-else clause.
why it matters
This result supplies the zero-cost instance required by the downstream definition of narrativeRealization, which constructs a LogicRealization with Carrier equal to NarrativeBeat and Cost equal to Nat. It closes the zero element for the narrative interpretation inside the UniversalForcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.