plotEncoding_image_eq_nonzero
The declaration shows that the plot encoding map from Booker's seven narrative archetypes lands exactly on the seven nonzero vectors in the three-dimensional vector space over the field with two elements. Narrative theorists and algebraists studying finite geometries would reference this to ground the claimed bijection in a formal count. The argument combines an inclusion check with a cardinality comparison that invokes the known count of nonzero elements and the injectivity of the encoding.
claimLet $P$ be the set of Booker plot families and let $e: P → ℱ₂³ be the axis encoding map. Then the image $e(P)$ equals the set of all nonzero vectors in ℱ₂³.
background
The module develops a structural correspondence between Booker's seven plot families and the nonzero elements of the elementary abelian 2-group of rank 3. BookerPlotFamily is the inductive type with seven constructors corresponding to the archetypes Overcoming the Monster, Rags to Riches, The Quest, Voyage and Return, Comedy, Tragedy, and Rebirth. The function plotEncoding assigns each family to a distinct nonzero vector in F2Power 3, which is defined as Fin 3 → Bool with pointwise XOR. Upstream results establish that this encoding is injective and that every image vector is nonzero, while F2Power.nonzero_card_three supplies the cardinality 7 for the nonzero vectors.
proof idea
The proof applies the lemma Finset.eq_of_subset_of_card_le. It first verifies the subset relation by showing that every element in the image satisfies the nonzero predicate, using plotEncoding_image_nonzero. For the cardinality bound it rewrites the image cardinality via Finset.card_image_of_injective applied to plotEncoding_injective, equates it to the cardinality of BookerPlotFamily via card_eq_seven, and matches this against the nonzero cardinality from F2Power.nonzero_card_three.
why it matters in Recognition Science
This result supplies the surjectivity half of the bijection between BookerPlotFamily and the nonzero elements of F2Power 3, which is invoked directly by the downstream theorem no_eighth_plot. That theorem serves as Falsifier 1 of the paper, establishing that no eighth plot family exists on three axes. The construction ties into the Recognition Science framework through the forcing of D = 3 spatial dimensions and the eight-tick octave structure, here manifested as the 2³ - 1 count of nontrivial elements.
scope and limits
- Does not specify the explicit vector assignments for each plot family.
- Does not extend the correspondence to dimensions other than three.
- Does not address continuous or infinite narrative structures.
- Does not prove uniqueness of the encoding up to automorphism of F2Power 3.
Lean usage
rw [← plotEncoding_image_eq_nonzero]formal statement (Lean)
163theorem plotEncoding_image_eq_nonzero :
164 Finset.univ.image plotEncoding =
165 Finset.univ.filter (fun v : F2Power 3 => v ≠ 0) := by
proof body
Tactic-mode proof.
166 apply Finset.eq_of_subset_of_card_le
167 · intro v hv
168 rcases Finset.mem_image.mp hv with ⟨p, _, hp⟩
169 rw [Finset.mem_filter, ← hp]
170 exact ⟨Finset.mem_univ _, plotEncoding_image_nonzero p⟩
171 · rw [F2Power.nonzero_card_three]
172 have : (Finset.univ.image plotEncoding).card =
173 Fintype.card BookerPlotFamily := by
174 rw [Finset.card_image_of_injective _ plotEncoding_injective]
175 rfl
176 rw [this, BookerPlotFamily.card_eq_seven]
177
178/-! ## §3. The count theorem (replaces the asserted `:= 7`) -/
179
180/-- The number of non-trivial 1-dimensional subgroups of
181 `Q₃ = F2Power 3` is `2 ^ 3 - 1 = 7`. This is the actual count
182 theorem, chained off `F2Power.nonzero_card_three`. -/