plot_composition_cancels_iff
plain-language theorem explainer
The theorem states that for any two of Booker's seven plot families, their vector encodings in the three-dimensional space over the field with two elements sum to zero precisely when the families coincide. Narrative theorists and Recognition Science researchers mapping story archetypes to the Q3 cube would invoke this result to confirm that plot cancellations correspond exactly to identical inputs. The proof is a direct algebraic reduction that invokes the characteristic-two cancellation law and the injectivity of the encoding function.
Claim. Let $p, q$ be elements of the set of Booker's seven plot families. Then the sum of their encodings in the vector space over the field with two elements equals zero if and only if $p = q$.
background
The module formalizes the bijection between Booker's seven plot families and the seven nonzero vectors of the elementary abelian 2-group F2Power 3, which models the cube Q3. BookerPlotFamily is the inductive type whose constructors are overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn, comedy, tragedy, and rebirth. The function plotEncoding maps each family to a distinct nonzero vector in F2Power 3 by the axis assignment of the paper's Theorem 9. The upstream result plotEncoding_injective establishes that this assignment is one-to-one, while F2Power.add_self states that every vector satisfies v + v = 0.
proof idea
The proof uses the constructor tactic to split the biconditional. In the forward direction, it assumes the sum is zero, applies congrArg to add the second encoding to both sides, then simplifies using add_assoc, F2Power.add_self, and the zero laws to obtain equality of the encodings; injectivity then yields p = q. In the reverse direction, it substitutes the equality and applies F2Power.add_self.
why it matters
This equivalence serves as the companion to Falsifier 3 in cardinality form, confirming that plot cancellation in the composite corresponds to the trivial transition only when the inputs match. It anchors the aesthetics module's mapping of narrative structures to the cube Q3 in the Recognition Science framework. The result closes a key algebraic property needed for verifying the seven-plot count against 2^3 - 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.