all_nodup
plain-language theorem explainer
The theorem proves that the explicit seven-element list of Booker plot families contains no duplicates. Researchers formalizing the bijection between narrative structures and nonzero vectors in F_2^3 cite this when building the Fintype instance for BookerPlotFamily. The proof is a one-line tactic that unfolds the list definition and invokes decide.
Claim. The list consisting of the seven plot families (overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, rebirth) contains no duplicate entries.
background
The module NarrativeGeodesic realizes Booker's seven plot families as an inductive type BookerPlotFamily whose constructors stand in explicit bijection with the seven nonzero elements of F_2^3 via plotEncoding. The definition all assembles these constructors into a concrete list of length 7. Nodup is the standard predicate asserting that a list has pairwise distinct elements. The local setting is the structural closure of the narrative geodesic on the cube Q_3, as described in the module documentation linking to the paper Seven_Plots_Three_Dimensions.
proof idea
The proof is a one-line tactic wrapper. It unfolds the definition of all to expose the concrete list and then applies the decide tactic, which discharges the nodup goal by exhaustive computation.
why it matters
This supplies the nodup witness required to equip BookerPlotFamily with a Fintype instance, which in turn feeds the cardinality equality booker_count_eq_F2Power3_nonzero. Parallel all_nodup theorems appear in AsteroidOreSpectroscopy and ModalPreferenceFromPhi, each enabling a corresponding certification object. The result closes one link in the explicit bijection between the seven plots and the nonzero vectors of F_2^3 stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.