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

neutralNarrative

show as:
view Lean formalization →

neutralNarrative supplies the zero element of the three-axis boolean space that classifies narratives. Researchers formalizing Booker's seven universal plots in Recognition Science cite it as the excluded trivial case when counting the seven non-zero vectors of F₂³. The definition is a direct one-line structure constructor on the false triple.

claimThe neutral narrative assignment is the triple $(false, false, false)$ with components protagonist agency, conflict origin, and resolution type.

background

The module links Booker's seven story patterns to the seven non-zero elements of the vector space F₂³ in three dimensions. NarrativeAssignment is the structure carrying three boolean fields that encode the binary choices on the protagonist agency axis, the conflict origin axis, and the resolution type axis. This definition supplies the origin element used to isolate the seven non-trivial assignments.

proof idea

The definition is a one-line wrapper that applies the structure constructor of NarrativeAssignment to the all-false triple.

why it matters in Recognition Science

It is referenced by IsBookerStory to define the seven Booker stories as those assignments unequal to neutralNarrative, thereby realizing the count |F₂³ ∖ {0}|. The construction anchors the aesthetic application of the D=3 lattice within Recognition Science. It closes the base case for the correspondence between recognition sequences and the seven universal plots.

scope and limits

formal statement (Lean)

  36def neutralNarrative : NarrativeAssignment := ⟨false, false, false⟩

proof body

Definition body.

  37

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.