pith. machine review for the scientific record. sign in
def definition def or abbrev high

all

show as:
view Lean formalization →

The definition supplies the ordered enumeration of Booker's seven plot families as a concrete list. Researchers establishing the bijection between narrative structures and the nonzero vectors of (Z/2)^3 cite this list when building the Fintype instance or proving exact cardinality seven. It is realized as a direct list literal of the seven inductive constructors.

claimLet $B$ be the inductive type whose constructors are the seven Booker plot families (overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, rebirth). Then the list $L$ is defined by $L = [B_1, B_2, B_3, B_4, B_5, B_6, B_7]$ where the ordering matches the explicit assignment table to the nonzero elements of $(Z/2)^3$.

background

The module develops the narrative geodesic on the cube $Q_3 = (Z/2)^3$, placing Booker's seven plot families in explicit bijection with the seven nonzero vectors of $F_2^3$. BookerPlotFamily is the inductive type with exactly those seven constructors; each constructor is assigned a unique nonzero vector via the map plotEncoding. The list all enumerates the constructors in the order required for the Fintype instance and the cardinality proofs that follow. Upstream results supply analogous exhaustive lists (kinship systems, ore classes, Greek modes) that likewise realize seven- or eight-element structures matching the geometry of $F_2^3$.

proof idea

The definition is a direct list literal containing the seven constructors of BookerPlotFamily. No tactics or lemmas are applied; the body simply writes the seven names in the order fixed by the assignment table.

why it matters in Recognition Science

This list realizes the concrete domain for the bijection between narrative families and the nonzero elements of $F_2^3$, as stated in the module documentation referencing Theorem 9 of the paper. It is the input to the downstream theorems all_length and all_nodup that establish cardinality exactly seven and the Fintype instance. Those results in turn support the convexity arguments for the J-action in FunctionalConvexity. The construction embodies the eight-tick octave in three spatial dimensions by excluding the zero vector of $Q_3$.

scope and limits

Lean usage

theorem all_length : all.length = 7 := by unfold all; decide

formal statement (Lean)

 113def all : List BookerPlotFamily :=

proof body

Definition body.

 114  [overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn,
 115   comedy, tragedy, rebirth]
 116
 117/-- The list has length 7. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.