name
plain-language theorem explainer
Maps each of the seven Booker plot families to its display string. Workers on the narrative geodesic would reference it for rendering the families that correspond to the nonzero vectors in (Z/2)^3. The definition proceeds by exhaustive pattern matching on the constructors of BookerPlotFamily.
Claim. Let $B$ be the inductive type of Booker plot families. The function $name : B → String$ is defined by $name(overcomingTheMonster) = $ ``Overcoming the Monster'', $name(ragsToRiches) = $ ``Rags to Riches'', $name(theQuest) = $ ``The Quest'', $name(voyageAndReturn) = $ ``Voyage and Return'', $name(comedy) = $ ``Comedy'', $name(tragedy) = $ ``Tragedy'', and $name(rebirth) = $ ``Rebirth''.
background
The module NarrativeGeodesic realizes a bijection between Booker's seven plot families and the seven nonzero elements of $F_2^3 = (Z/2)^3$. BookerPlotFamily is the inductive type whose seven constructors are overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn, comedy, tragedy, and rebirth. The assignment follows the explicit table in the paper (Theorem 9) that pairs each family with a unique nonzero vector.
proof idea
The definition is a direct pattern match that returns the corresponding string literal for each of the seven constructors of BookerPlotFamily.
why it matters
This supplies the human-readable labels required to display the narrative structures that close the bijection with $Q_3$. It completes the mapping from abstract cube elements to the seven plot families listed in the Seven Plots Three Dimensions paper. The definition supports rendering and documentation layers without touching the cardinality proof or the encoding injectivity proved elsewhere in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.