plot_composition_xor_additive
plain-language theorem explainer
Plot composition under vector addition in the three-dimensional cube over GF(2) closes within the seven-plot set whenever the result is nonzero. Structural narratologists modeling story archetypes as elements of (Z/2Z)^3 would invoke this when checking algebraic closure of the plot families. The argument reduces immediately to the lemma that every nonzero vector in the cube encodes some plot.
Claim. Let $P$ denote the set of seven plot families. Let $ε : P → (ℤ/2ℤ)^3$ be the bijection mapping each family to a unique nonzero vector. For any $p, q ∈ P$ such that $ε(p) + ε(q) ≠ 0$, there exists $r ∈ P$ with $ε(r) = ε(p) + ε(q)$.
background
The module realizes Booker's seven narrative archetypes as the nonzero vectors of the vector space (Z/2Z)^3, with the explicit axis assignment (protagonist status, world status, value alignment) given by the encoding map. This bijection is proved via the cardinality result that exactly seven nonzero vectors exist in F2Power 3, replacing any prior hardcoded count. The local setting is the structural closure of narrative geodesics on the cube Q3, as the Lean counterpart to the paper Seven Plots Three Dimensions.
proof idea
The proof is a one-line wrapper that applies the no_eighth_plot lemma directly to the nonzero sum hypothesis, yielding the required plot family whose encoding matches the composite vector.
why it matters
This supplies Falsifier 3 of the paper, confirming that plot composition remains inside the seven families under the induced XOR operation on the cube. It closes the algebraic structure on the narrative side, consistent with the derivation of three spatial dimensions from the self-similar fixed point in the forcing chain. No downstream uses appear, but the statement supports further development of narrative geodesics as paths on Q3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.