plotEncoding_injective
The assignment of Booker's seven plot families to vectors in the three-dimensional space over GF(2) is one-to-one. Researchers formalizing narrative structures within Recognition Science cite this to secure the bijection with the non-zero elements of the cube Q3. The proof is a compact term-mode case analysis that exhausts all constructor pairs and resolves equalities or contradictions by reflexivity and the decide tactic.
claimThe map sending each Booker plot family to its assigned non-zero vector in $F_2^3$ is injective: distinct plots receive distinct vectors.
background
The module sets up the structural correspondence between Booker's seven plot families and the geometry of the cube $Q_3 = F_2^3$. BookerPlotFamily is the inductive type whose seven constructors are ragsToRiches, voyageAndReturn, comedy, theQuest, tragedy, overcomingTheMonster and rebirth. The function plotEncoding supplies the explicit axis assignment (protagonist status, world status, value alignment) that realizes the table in Theorem 9 of Seven_Plots_Three_Dimensions.tex, sending each constructor to a unique non-zero vector such as axis1 for ragsToRiches. Upstream the definition plotEncoding provides the case-by-case mapping; the module imports F2Power and Cost to ground the vectors in the Recognition algebra.
proof idea
The proof introduces plots p and q together with the hypothesis that their encodings coincide. It applies cases on both p and q, then uses a first tactic that either returns reflexivity when the constructors match or derives a contradiction by reverting the equality and invoking decide on the mismatched encodings.
why it matters in Recognition Science
Injectivity is required to inhabit the master certificate narrativeGeodesicCert and to prove the one-statement theorem narrative_geodesic_one_statement that asserts exactly seven plots with no eighth. It also supplies the injective field of the CountLaw instance bookerCountLaw in Patterns.TwoToTheDMinusOne. Within the framework the result closes the aesthetics module by confirming the bijection between narrative families and the seven non-zero elements of F2Power 3, thereby linking story structure to the D=3 cube and the eight-tick octave.
scope and limits
- Does not prove that the image covers all non-zero vectors of F2Power 3.
- Does not compute the cardinality of BookerPlotFamily.
- Does not treat narrative tension or geodesic cancellation properties.
- Does not invoke physical constants, forcing chain steps or mass formulas.
- Does not extend to plot classifications outside Booker's seven families.
Lean usage
def cert : NarrativeGeodesicCert := { seven_plot_families := BookerPlotFamily.card_eq_seven, plot_count_is_2_pow_3_minus_1 := booker_seven_eq_2_pow_3_minus_1, Q3_subgroup_count := Q3_nontrivial_subgroup_count, encoding_injective := plotEncoding_injective, encoding_image_nonzero := plotEncoding_image_nonzero }formal statement (Lean)
152theorem plotEncoding_injective : Function.Injective plotEncoding := by
proof body
Term-mode proof.
153 intro p q hpq
154 cases p <;> cases q <;> first | rfl | (exfalso; revert hpq; decide)
155
156/-- Every encoded vector is non-zero. -/