all_nodup
The theorem establishes that the explicit enumeration of Booker's seven plot families contains no repeated elements. Researchers mapping narrative archetypes onto the vector space F_2^3 cite it to justify the Fintype instance for BookerPlotFamily and the subsequent cardinality result. The proof is a one-line tactic that unfolds the list definition and lets the decision procedure confirm pairwise distinctness.
claimLet $all$ be the list of the seven Booker plot families. Then $all$ is duplicate-free.
background
BookerPlotFamily is the inductive type whose seven constructors are the plot families (Overcoming the Monster, Rags to Riches, The Quest, Voyage and Return, Comedy, Tragedy, Rebirth). The definition all enumerates them in that order. The module NarrativeGeodesic realises the bijection, stated in the paper Theorem 9, between these families and the seven nonzero vectors of F2Power 3 = (Z/2)^3. The same pattern of all-plus-all_nodup appears in the sibling modules AsteroidOreSpectroscopy and ModalPreferenceFromPhi.
proof idea
The proof is a one-line wrapper: it unfolds the definition of all and invokes the decide tactic, which reduces the finite distinctness check to a decidable proposition that Lean discharges automatically.
why it matters in Recognition Science
all_nodup supplies the nodup field required by the Fintype instance for BookerPlotFamily, which in turn feeds the downstream theorems booker_count_eq_F2Power3_nonzero and plotEncoding_image_eq_nonzero. These close the structural identification of the seven plots with the nonzero elements of Q_3, realising the 2^3-1 count that aligns with the eight-tick octave (T7) in the Recognition Science forcing chain.
scope and limits
- Does not construct or verify the plotEncoding function.
- Does not prove the bijection with nonzero vectors of F2Power 3.
- Does not address any metric or geodesic structure on the narrative cube.
- Does not extend to lists of other cardinalities or other inductive families.
Lean usage
instance : Fintype BookerPlotFamily where elems := { val := ⟦all⟧, nodup := all_nodup } complete := by intro x; cases x <;> decideformal statement (Lean)
122theorem all_nodup : all.Nodup := by
proof body
Tactic-mode proof.
123 unfold all; decide
124
125instance : Fintype BookerPlotFamily where
126 elems := { val := ⟦all⟧, nodup := all_nodup }
127 complete := by
128 intro x; cases x <;> decide
129
130/-- `BookerPlotFamily` has exactly seven elements. -/