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

plotEncoding

show as:
view Lean formalization →

The plotEncoding definition supplies the explicit assignment of each of Booker's seven plot families to a distinct nonzero vector in the three-dimensional vector space over F2. Researchers formalizing narrative structure within the Recognition Science cube model would reference this mapping when verifying the bijection between plots and state changes. The definition is realized by direct case analysis on the inductive constructors of BookerPlotFamily, routing each to the appropriate axis vector.

claimLet $B$ be the inductive type whose constructors are the seven Booker plot families. The function $plotEncoding : B → (ℤ/2ℤ)^3$ sends ragsToRiches to $(1,0,0)$, voyageAndReturn to $(0,1,0)$, comedy to $(0,0,1)$, theQuest to $(1,1,0)$, tragedy to $(1,0,1)$, overcomingTheMonster to $(0,1,1)$, and rebirth to $(1,1,1)$.

background

The module treats the cube $Q_3 = (ℤ/2ℤ)^3$ as the state space for narrative transitions, with nonzero vectors representing distinct plot-driven changes. BookerPlotFamily is the inductive type with exactly seven constructors, one for each classic plot family. The F2Power 3 algebra supplies the vector space operations together with the concrete axis vectors: axis1 for protagonist status, axis2 for world status, and axis3 for value alignment, plus their sums axis12, axis13, axis23, and axis123.

proof idea

The definition is given by exhaustive pattern matching on the seven constructors of BookerPlotFamily. Each case returns the corresponding axis vector supplied by the F2Power module: ragsToRiches maps to axis1, voyageAndReturn to axis2, comedy to axis3, theQuest to axis12, tragedy to axis13, overcomingTheMonster to axis23, and rebirth to axis123. No lemmas or tactics are invoked.

why it matters in Recognition Science

This definition supplies the concrete bijection required by the NarrativeGeodesicCert structure and the one-statement theorem narrative_geodesic_one_statement. It realizes the explicit encoding of Theorem 9 in the paper Seven_Plots_Three_Dimensions.tex and confirms that the seven plots arise precisely as the nonzero elements of F2Power 3 when the narrative state space has dimension D = 3. The mapping is the foundation for the subsequent results on injectivity, image coverage, and XOR-additive composition.

scope and limits

Lean usage

example : plotEncoding .ragsToRiches = axis1 := rfl

formal statement (Lean)

 142def plotEncoding : BookerPlotFamily → F2Power 3
 143  | .ragsToRiches         => axis1     -- (true, false, false)
 144  | .voyageAndReturn      => axis2     -- (false, true, false)
 145  | .comedy               => axis3     -- (false, false, true)
 146  | .theQuest             => axis12    -- (true, true, false)
 147  | .tragedy              => axis13    -- (true, false, true)
 148  | .overcomingTheMonster => axis23    -- (false, true, true)
 149  | .rebirth              => axis123   -- (true, true, true)
 150
 151/-- The encoding is injective: distinct plots map to distinct vectors. -/

used by (16)

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

depends on (14)

Lean names referenced from this declaration's body.