all
plain-language theorem explainer
Booker's seven plot families are enumerated explicitly as the list overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, rebirth. Researchers working on narrative bijections to F2Power 3 or structural counts in the Recognition framework cite this enumeration to fix the cardinality at 2^3 - 1. The definition is a direct list literal of the seven constructors from the inductive type.
Claim. The complete list of the seven plot families is [overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, rebirth].
background
The module develops the narrative geodesic on the cube Q_3 = (Z/2Z)^3. BookerPlotFamily is the inductive type whose seven constructors stand in explicit bijection with the nonzero vectors of F2Power 3 via the axis assignment table. Parallel enumerations of seven elements appear in the kinship systems module and the Greek modes module, each matching the dimension-three structure from the forcing chain.
proof idea
The definition is a direct list literal containing the seven constructors of BookerPlotFamily in the order given by the paper assignment table. No lemmas or tactics are invoked inside the body; downstream length and nodup properties are obtained by unfolding the literal and applying decide.
why it matters
This enumeration anchors the bijection between plot families and the seven nonzero vectors of F2Power 3, as described in the module documentation referencing Theorem 9 of the paper. It is used by all_length and all_nodup to establish cardinality and distinctness, which support the Fintype instance. Downstream it feeds convexity statements for the J-action and local quasi-triangle bounds on defect distance, closing the structural loop from T7 eight-tick octave and T8 D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.