booker_count_eq_F2Power3_nonzero
plain-language theorem explainer
The theorem equates the cardinality of the inductive type BookerPlotFamily to the number of nonzero vectors in the 3-dimensional F2-vector space. Researchers mapping narrative archetypes to finite geometry in the Recognition Science aesthetics module would cite this equality. The proof is a one-line rewrite that substitutes the explicit count of seven families on the left and the nonzero cardinality theorem on the right.
Claim. Let $B$ be the set of Booker plot families. Then $|B| = |{v ∈ (ℤ/2ℤ)^3 | v ≠ 0}|$.
background
BookerPlotFamily is the inductive type whose seven constructors are the classic plot families (overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, rebirth). Each constructor is placed in explicit bijection with a nonzero vector of F2Power 3 via the encoding map defined in the same module. F2Power D is the elementary abelian 2-group of rank D, realized as Fin D → Bool with pointwise XOR; for D = 3 this is the cube Q₃ = (ℤ/2ℤ)^3. The upstream theorem card_eq_seven states that Fintype.card BookerPlotFamily = 7. The companion result Q3_nontrivial_subgroup_count states that the filtered cardinality of nonzero vectors in F2Power 3 equals 7, obtained directly from F2Power.nonzero_card_three.
proof idea
The proof is a one-line wrapper that applies the rewrite tactic to the two upstream theorems: BookerPlotFamily.card_eq_seven on the left-hand side and Q3_nontrivial_subgroup_count on the right-hand side.
why it matters
This equality is the immediate parent of the downstream theorem booker_seven_eq_2_pow_3_minus_1, which rewrites the same cardinality as 2^3 - 1 and thereby shows that the count is forced by the dimension D = 3 rather than by a hardcoded numeral. The result closes the structural identification of the seven plot families with the nonzero elements of Q₃, consistent with the T8 forcing of three spatial dimensions and the eight-tick octave in the Recognition Science chain. It replaces an earlier hardcoded count with a derivation that depends on the F2Power construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.