name
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish or prove the bijection with nonzero vectors in $F_2^3$.
- Does not reference J-cost, phi-ladder, or forcing-chain steps.
- Does not compute cardinalities or injectivity properties.
- Does not depend on upstream structures from NucleosynthesisTiers or SpectralEmergence.
formal statement (Lean)
103def name : BookerPlotFamily → String
104 | overcomingTheMonster => "Overcoming the Monster"
105 | ragsToRiches => "Rags to Riches"
106 | theQuest => "The Quest"
107 | voyageAndReturn => "Voyage and Return"
108 | comedy => "Comedy"
109 | tragedy => "Tragedy"
110 | rebirth => "Rebirth"
111
112/-- The seven-element list of plot families. -/