NarrativeAssignment
plain-language theorem explainer
NarrativeAssignment encodes the three binary narrative axes as a triple of booleans. Researchers mapping literary structures to the F₂³ lattice in Recognition Science cite it to count the seven non-trivial story patterns. The declaration is a direct structure with derived decidable equality and finiteness instances.
Claim. A narrative assignment is a triple $(a, c, r) ∈ {0,1}^3$ where $a$ is protagonist agency (reactive or proactive), $c$ is conflict origin (internal or external), and $r$ is resolution type (restoration or transformation).
background
The module derives narrative structure from the F₂³ cube in D=3. Booker’s seven universal patterns are identified with the seven nonzero vectors in this vector space over GF(2). The three axes are protagonist agency, conflict origin, and resolution type; each combination of truth values labels one story pattern.
proof idea
Direct structure definition that introduces the three Bool fields and derives DecidableEq, BEq, Repr, and Fintype instances.
why it matters
This supplies the concrete type whose seven non-neutral elements realize the Booker stories. It is used by IsBookerStory (which excludes the zero vector) and neutralNarrative. The definition closes the link between the D=3 lattice and the seven weight-1/2/3 combinations, providing the data type needed for any further formalization of aesthetics inside Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.