no_eighth_plot
plain-language theorem explainer
Every nonzero vector in the three-dimensional vector space over F_2 is the image of some Booker plot family under the explicit encoding map. Narrative theorists formalizing structural models of story would cite this when confirming that the seven classic plots exhaust the possibilities on three axes. The proof is a short tactic sequence that first places the vector in the filtered nonzero set, rewrites via the pre-established image equality, then extracts the witness from image membership.
Claim. For every nonzero vector $δ ∈ ℝ_2^3$, there exists a Booker plot family $p$ such that the encoding of $p$ equals $δ$.
background
The module develops the narrative geodesic on the cube $Q_3 = (ℤ/2ℤ)^3$. BookerPlotFamily is the inductive type whose seven constructors are the classic plot families (overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, rebirth). The map plotEncoding sends each family to one of the seven nonzero vectors in F2Power 3, with the three axes interpreted as protagonist status, world status, and value alignment. The upstream theorem plotEncoding_image_eq_nonzero states that the image of plotEncoding equals exactly the set of all nonzero vectors in F2Power 3.
proof idea
The tactic first builds membership of δ in the filtered Finset of nonzero vectors by simplification. It rewrites that membership using the equality plotEncoding_image_eq_nonzero. It then applies Finset.mem_image.mp to obtain a pair (p, hp) witnessing that plotEncoding p = δ and returns the existential.
why it matters
This supplies the surjectivity half of the bijection, completing the one-statement theorem narrative_geodesic_one_statement. It is invoked directly as the surjective_on_nonzero field in bookerCountLaw (which instantiates CountLaw 3) and as the witness in plot_composition_xor_additive. Within the Recognition framework it furnishes the structural closure for the aesthetics module, confirming that the seven plots fill the nonzero elements of the three-dimensional cube without remainder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.