IsBookerStory
plain-language theorem explainer
IsBookerStory marks a narrative assignment as non-neutral by excluding the all-false triple of axes. Researchers in narrative theory or Recognition Science aesthetics would cite it when counting the seven universal story patterns from Booker. The definition reduces directly to inequality against neutralNarrative, with an accompanying decidability instance via instDecidableNot.
Claim. Let $n$ be a narrative assignment with boolean fields for protagonist agency, conflict origin, and resolution type. Then $n$ satisfies the predicate if and only if $n$ differs from the neutral assignment $(false, false, false)$.
background
NarrativeAssignment is the structure whose fields are three independent Bool values (protagonistAgency, conflictOrigin, resolutionType) equipped with DecidableEq, BEq, Repr, and Fintype. neutralNarrative is the constant triple of all false values, serving as the zero element of the F₂³ vector space spanned by the three axes. The module sets the local theoretical setting by identifying the seven non-zero elements of this lattice with Booker’s seven universal story patterns, each corresponding to a distinct combination of the binary narrative axes.
proof idea
The declaration is a one-line definition that applies the inequality n ≠ neutralNarrative. The accompanying instance supplies Decidable (IsBookerStory n) by reducing to instDecidableNot on the equality test.
why it matters
This predicate is the filter condition in booker_count, which proves that exactly seven assignments remain after exclusion and thereby certifies |F₂³ ∖ {0}| = 7. It is also referenced inside NarrativeStructureCert to close the three-axes and seven-stories clauses. The construction realizes the D = 3 spatial dimensions of the Recognition Science chain by mapping the three binary axes onto the weight-1, 2, and 3 vectors of the F₂³ lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.