narrativeCost
plain-language theorem explainer
The narrativeCost function assigns a natural-number cost to pairs of narrative beats, returning zero precisely when the beats coincide. It supports the formalization of narrative realizations as discrete comparisons in the UniversalForcing module. The definition proceeds by a direct case distinction on equality.
Claim. For narrative beats $a, b$ in the natural numbers, the cost is $0$ if $a = b$ and $1$ otherwise.
background
NarrativeBeat is defined as the type of natural numbers, serving as beat counts generated by an inciting event. The module supplies a lightweight narrative realization in which the carrier is this beat count. This formalizes the structural claim that narrative order carries the same forced Peano object. The sole upstream item is the abbreviation that sets NarrativeBeat to the naturals.
proof idea
The definition is implemented directly as a conditional expression that checks equality of the two inputs and returns the corresponding natural number.
why it matters
This definition supplies the compare operation for narrativeRealization, which builds a LogicRealization whose carrier is NarrativeBeat and whose cost type is the naturals. It thereby anchors the claim that narrative order carries the forced Peano object inside the Recognition Science framework. Downstream results establish that the cost is zero on the diagonal and symmetric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.