pith. machine review for the scientific record. sign in
inductive definition def or abbrev high

NarrativeAxis

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  24inductive NarrativeAxis where
  25  | protagonistAgency | conflictOrigin | resolutionType
  26  deriving DecidableEq, Repr, BEq, Fintype
  27

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.