all_length
plain-language theorem explainer
The theorem establishes that the explicit list of seven Booker plot families has cardinality exactly seven. Researchers mapping narrative archetypes to the nonzero vectors of F_2^3 would cite this cardinality result when closing structural counts. The proof is a one-line wrapper that unfolds the list definition and decides the equality by direct computation.
Claim. Let $L$ be the list of Booker plot families $[M, R, Q, V, C, T, B]$ corresponding to the seven nonzero elements of the vector space $F_2^3$. Then the length of $L$ equals 7.
background
The Narrative Geodesic module places Booker's seven plot families in explicit bijection with the seven nonzero vectors of $F_2^3 = (Z/2Z)^3$, as described in the module documentation and the referenced paper Theorem 9. The definition all constructs the concrete list [overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn, comedy, tragedy, rebirth]. Parallel length theorems appear in sibling modules: KinshipSystem.all has length 8 and OreClass.all has length 7, establishing a uniform counting pattern over discrete structures on the cube.
proof idea
The proof is a one-line wrapper that unfolds the definition of all and applies the decide tactic to verify the length by direct computation.
why it matters
This cardinality supplies the count used by downstream certificates including kinshipGraphCohomologyCert, asteroidOreSpectroscopyCert, and modalPreferenceCert. It closes the seven-plot count in the aesthetics section, confirming the match to $2^3 - 1$ and aligning with the T7 eight-tick octave landmark of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.