narrativeCost_symm
plain-language theorem explainer
Symmetry of the cost on natural-number beats follows from its definition as an equality indicator. Workers on narrative realizations in the Recognition framework cite this to confirm the comparison operator is undirected before packaging it into a LogicRealization. The tactic proof splits on equality of the beats and reduces both sides via substitution and simplification.
Claim. For natural numbers $a$ and $b$, the cost function defined by $c(a,b)=0$ if $a=b$ and $c(a,b)=1$ otherwise satisfies $c(a,b)=c(b,a)$.
background
NarrativeBeat is an abbreviation for the natural numbers, serving as the carrier for beat counts generated by an inciting event. The cost function on beats returns zero precisely when the two beats coincide and one otherwise, providing a minimal distinction between narrative positions.
proof idea
The tactic proof performs case analysis on whether the two beats are equal. In the equal case, substitution reduces both sides to zero by the cost definition. In the unequal case, the swapped inequality is introduced and simplification yields one on both sides.
why it matters
This result supplies the symmetry needed by the narrativeRealization construction, which installs the cost function as the compare operation inside a LogicRealization. It supports the structural claim that narrative order carries the same forced Peano object. The declaration closes a basic property for this carrier without addressing open questions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.