BookerPlotFamily
plain-language theorem explainer
BookerPlotFamily defines the inductive type with seven constructors for Christopher Booker's plot families. Recognition Science researchers cite it when deriving the exact count of narrative structures as 2^3 - 1 from the nonzero vectors in F_2^3. The declaration is a direct inductive definition that automatically derives DecidableEq and Inhabited.
Claim. Let $B$ be the inductive type whose seven constructors are the plot families overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, and rebirth. Each element of $B$ stands in explicit bijection with one nonzero vector of the three-dimensional vector space over $F_2$ via the encoding map.
background
The module develops the narrative geodesic on the cube $Q_3 = (Z/2Z)^3$, placing aesthetics in the Recognition Science framework beyond music. Booker's seven plot families receive an explicit bijection with the seven nonzero elements of $F2Power 3$, with the assignment table taken from the paper's Theorem 9. The count itself is not asserted but follows from the dimension $D=3$ in the unified forcing chain.
proof idea
The declaration is a direct inductive definition that lists the seven constructors explicitly and derives DecidableEq and Inhabited. No lemmas or tactics are invoked; the structure is introduced as a primitive type in the module.
why it matters
This supplies the base type for all downstream results in the module, including the list all, the nodup theorem, card_eq_seven, booker_seven_eq_2_pow_3_minus_1, and the bijection theorems. It realizes the structural closure for the sevenfold symmetry required by $D=3$ in the forcing chain (T8) and the eight-tick octave (T7). The definition replaces an earlier hardcoded count with one that depends on $F2Power 3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.