NarrativeStructureCert
plain-language theorem explainer
NarrativeStructureCert packages four cardinality statements that equate three binary narrative axes with the seven non-zero elements of the F₂³ vector space and Booker's seven universal story patterns. Researchers in Recognition Science aesthetics cite it to formalize the D=3 lattice interpretation of narrative. The definition is a direct structure declaration that assembles the Fintype.card values from the inductive types for axes and stories together with the filter count on the non-neutral predicate.
Claim. Let $A$ be the set of narrative axes with $|A|=3$. Let $B$ be the set of Booker stories. Let $I$ be the predicate on narrative assignments that excludes the neutral case. Then $|B|=7$, the cardinality of the set of assignments satisfying $I$ equals 7, and $|B|=2^3-1$.
background
The module derives narrative structure from the F₂³ cube in the aesthetics domain. NarrativeAxis is the inductive type whose three constructors are protagonist agency, conflict origin, and resolution type; it derives Fintype so its cardinality is immediately 3. IsBookerStory is the decidable predicate that excludes the neutral narrative assignment. BookerStory is the inductive type enumerating the seven patterns: overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, rebirth.
proof idea
The structure is defined by directly stating the four cardinality equalities. No lemmas are applied; the values follow from the derived Fintype instances on the inductive types NarrativeAxis and BookerStory together with the decidable filter on IsBookerStory.
why it matters
This definition supplies the certification record instantiated by narrativeStructureCert, anchoring the aesthetics component of the Recognition Science framework. It equates Booker's seven stories with the seven non-zero vectors in F₂³, matching the module's description of weight-1, 2, and 3 combinations of the three binary axes. The construction touches the open question of how sequences of recognition events compose into universal story structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.