bookerStoryCount
plain-language theorem explainer
The theorem asserts that the inductive type BookerStory enumerating seven universal story patterns has cardinality exactly 7, matching the count of non-zero vectors in F₂³. Workers in Recognition Science aesthetics would cite it to anchor narrative structures to the D=3 lattice. The proof is a direct decision procedure on the Fintype instance derived from the inductive definition.
Claim. Let BookerStory be the inductive type with constructors overcomingMonster, ragsToRiches, theQuest, voyageAndReturn, comedy, tragedy, rebirth. Then its cardinality satisfies $|BookerStory| = 7$.
background
The module NarrativeStructureFromF2Cube interprets Booker's seven story patterns as the non-trivial elements of F₂³, the three-dimensional vector space over the field with two elements, consistent with the Recognition Science derivation of D=3. BookerStory is defined as an inductive type with seven constructors and derives DecidableEq, Repr, BEq, Fintype for direct cardinality computation. The upstream result is precisely this inductive definition of BookerStory.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance of BookerStory, which enumerates the seven constructors and computes the cardinality as 7.
why it matters
This theorem supplies the seven_booker_stories field in the NarrativeStructureCert definition, which certifies the full correspondence between narrative axes and the F₂³ lattice. It instantiates the framework landmark T8 that D=3 yields 2³-1=7 non-trivial elements, closing the enumeration step in the aesthetics module. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.