booker_seven_eq_2_pow_3_minus_1
plain-language theorem explainer
The theorem states that the cardinality of BookerPlotFamily equals 2^3 minus 1. Researchers tracing narrative structure to the cube geometry in Recognition Science cite it to derive the seven plots from dimension D=3 rather than enumeration. The proof is a two-step rewrite that first equates the family count to the non-zero vectors in F2Power 3 and then invokes the general nonzero_card formula.
Claim. The cardinality of the set of Booker plot families equals $2^3 - 1$.
background
In the NarrativeGeodesic module the inductive type BookerPlotFamily carries seven constructors (overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn, comedy, tragedy, rebirth) placed in explicit bijection with the non-zero vectors of F2Power 3 via the encoding map plotEncoding. F2Power D is defined as the type Fin D → Bool equipped with pointwise XOR, so that F2Power 3 models the elementary abelian 2-group (Z/2Z)^3 whose non-zero elements number exactly 2^D - 1. The module document records that this count replaces an earlier hardcoded 7 and is the Lean counterpart of the structural claim in the paper Seven_Plots_Three_Dimensions.tex.
proof idea
The term proof rewrites the left-hand side by the sibling theorem booker_count_eq_F2Power3_nonzero, which replaces Fintype.card BookerPlotFamily by the cardinality of the non-zero subset of F2Power 3; it then applies the upstream lemma F2Power.nonzero_card at D=3 to obtain the closed expression 2^3 - 1.
why it matters
The result supplies the plot_count_is_2_pow_3_minus_1 field of the master certificate narrativeGeodesicCert and appears directly in the one-statement theorem narrative_geodesic_one_statement. It realizes the paper's claim that the seven plots arise from the cube geometry of Q3 rather than from an arbitrary list, thereby linking the aesthetics module to the forcing-chain step T8 that fixes D=3 and to the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.