card_eq_seven
plain-language theorem explainer
The inductive type BookerPlotFamily enumerating the seven classic plot families has finite cardinality exactly seven. Researchers mapping narrative archetypes to the vector space over GF(2) of dimension three cite this result to fix the exact count matching the nonzero elements of F2Power 3. The proof is a one-line reflexivity check that follows directly from the seven-constructor inductive definition.
Claim. Let $B$ be the inductive type whose constructors are the seven Booker plot families. Then the Fintype cardinality satisfies $|B| = 7$.
background
The module Narrative Geodesic on the Cube $Q_3 = (Z/2Z)^3$ realizes the bijection from Booker's plot families to the nonzero vectors of $F2Power 3$, where $F2Power D$ is the type $Fin D → Bool$ with pointwise XOR. BookerPlotFamily is the inductive type with exactly the seven constructors overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn, comedy, tragedy, rebirth. The module replaces an earlier hardcoded count with theorems that depend on the algebra of $F2Power$. Upstream, the nonzero cardinality of $F2Power 3$ is supplied by the algebra library as $2^3 - 1 = 7$.
proof idea
The proof is a one-line reflexivity tactic. It evaluates the Fintype.card computation directly from the seven-constructor inductive definition of BookerPlotFamily, which derives DecidableEq.
why it matters
This theorem supplies the cardinality anchor for the master certificate narrativeGeodesicCert and is invoked by booker_count_eq_F2Power3_nonzero to equate the plot-family count with the nonzero cardinality of $F2Power 3$. It realizes the $D = 3$ spatial dimensions from the forcing chain T8 and the eight-tick octave structure $2^3 - 1$, closing the earlier scaffolding around Q3_nontrivial_subgroup_count in the aesthetics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.