NarrativeAxis
plain-language theorem explainer
The three narrative axes generate Booker's seven universal story structures from the nonzero vectors in the F₂³ lattice within Recognition Science. Narrative theorists or RS aesthetics researchers would cite this to anchor the correspondence between story patterns and the D=3 binary space. The definition consists of an inductive type with three constructors that derives the necessary decidability and finiteness instances.
Claim. The set of narrative axes comprises three binary distinctions: protagonist agency (reactive versus proactive), conflict origin (internal versus external), and resolution type (restoration versus transformation).
background
Recognition Science derives narrative structures from recognition events on the three-dimensional F₂³ lattice. The module introduces three binary axes that label the coordinates of this space: protagonist agency (reactive versus proactive), conflict origin (internal versus external), and resolution type (restoration versus transformation). These generate the seven nontrivial combinations that correspond to Booker's universal story patterns: Overcoming the Monster, Rags to Riches, The Quest, Voyage and Return, Comedy, Tragedy, and Rebirth.
proof idea
The declaration is an inductive definition that introduces exactly three constructors and derives DecidableEq, Repr, BEq, and Fintype instances via the deriving clause.
why it matters
This supplies the axis set used in narrativeAxisCount to establish that there are exactly three axes and in NarrativeStructureCert to certify the seven stories via the equality Fintype.card BookerStory = 2^3 - 1. It realizes the module's claim that the seven structures correspond to the seven nonzero elements of F₂³. The construction connects aesthetics to the framework's result that spatial dimension D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.