booker_count
plain-language theorem explainer
The declaration asserts that exactly seven narrative assignments satisfy the non-neutral predicate, matching the count of nonzero vectors in the three-dimensional vector space over F₂. Researchers connecting Booker's seven universal story patterns to the Recognition Science D=3 lattice would cite this cardinality when verifying the geometric encoding of narrative axes. The proof is a direct decision procedure on the finite set of assignments.
Claim. The cardinality of the set of narrative assignments excluding the neutral element equals 7, which is the number of nonzero vectors in $F_2^3$.
background
The module encodes narrative structure via three binary axes (protagonist agency, conflict origin, resolution type) whose combinations form the type NarrativeAssignment. The neutral narrative is the zero vector, and IsBookerStory holds precisely when an assignment differs from neutral. This construction identifies Booker's seven patterns (Overcoming the Monster, Rags to Riches, The Quest, Voyage and Return, Comedy, Tragedy, Rebirth) with the seven weight-1, 2, and 3 elements of the F₂³ cube, consistent with the D=3 lattice derived from the forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the finite Finset.univ of NarrativeAssignment instances, filters by the decidable predicate IsBookerStory, and confirms the resulting cardinality equals 7.
why it matters
This supplies the seven_stories_via_decide component of NarrativeStructureCert, which bundles the axis count, story count, and equality to the F₂³ complement. It instantiates the framework result that D=3 yields precisely seven nontrivial elements, closing the link from the Recognition Composition Law through the eight-tick octave to aesthetic structures without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.