all_nodup
plain-language theorem explainer
The explicit list of seven Booker plot families contains no duplicate entries. Researchers formalizing the bijection between narrative structures and the nonzero vectors of F₂³ cite this to ground the Fintype instance for BookerPlotFamily. The proof is a one-line decision after unfolding the list definition.
Claim. Let $L$ be the list of the seven plot families (overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, rebirth). Then $L$ is duplicate-free.
background
The module NarrativeGeodesic constructs the seven-element list all of BookerPlotFamily constructors and maps them bijectively to the nonzero elements of F₂³ via plotEncoding, as stated in the module doc and the paper Seven_Plots_Three_Dimensions. BookerPlotFamily is the inductive type whose seven cases correspond exactly to the seven nonzero vectors of F2Power 3. The upstream definition all enumerates the seven families in fixed order; Nodup is the standard predicate asserting pairwise distinctness. Parallel nodup theorems appear in KinshipGraphCohomology and AsteroidOreSpectroscopy for their respective seven-element lists.
proof idea
The tactic proof unfolds the definition of the list all and invokes the decide tactic, which reduces the finite distinctness check to a decidable equality computation on the seven constructors.
why it matters
This result supplies the nodup witness required by the Fintype instance for BookerPlotFamily immediately below it and is mirrored in the certification records asteroidOreSpectroscopyCert and modalPreferenceCert. It closes one step in the structural count that the module doc ties to Algebra.F2Power.nonzero_card_three, confirming that the seven plot families match the seven nonzero vectors without repetition. The declaration therefore supports the explicit bijection claimed in Theorem 9 of the referenced paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.