narrativeGeodesicCert
plain-language theorem explainer
The master certificate for the narrative geodesic on the three-dimensional cube over F2 is defined by direct construction from the supporting lemmas. A researcher working on the Recognition Science extension to narrative structure or the structural closure of Booker's seven plots would cite this as the inhabited master certificate. The definition is a record literal that supplies each field of NarrativeGeodesicCert from its dedicated lemma.
Claim. The structure NarrativeGeodesicCert is inhabited, requiring that the set of Booker plot families has cardinality 7 which equals $2^3-1$, that the encoding map to the nonzero vectors of $(Z/2Z)^3$ is injective with image exactly those vectors, that narrative tension vanishes at perfect resolution, and that every nonzero vector in the cube is realized by some plot.
background
This module develops the narrative geodesic on the cube $Q_3 = (Z/2)^3$ as the Lean counterpart to the paper Seven Plots Three Dimensions. Booker's seven plot families stand in explicit bijection with the seven nonzero elements of F2Power 3 via the assignment table given in the module documentation. The count 7 is derived from the dimension D=3 rather than asserted directly.
proof idea
The definition constructs an instance of NarrativeGeodesicCert by supplying each field from its supporting result: seven_plot_families from card_eq_seven, plot_count_is_2_pow_3_minus_1 from booker_seven_eq_2_pow_3_minus_1, Q3_subgroup_count from Q3_nontrivial_subgroup_count, encoding_injective from plotEncoding_injective, encoding_image_nonzero from plotEncoding_image_nonzero, no_eighth_plot_holds from no_eighth_plot, and resolution_zero from narrativeTension_resolution.
why it matters
This definition inhabits the master certificate that closes the aesthetics module, assembling the bijection between the seven Booker plots and the nonzero vectors of F2Power 3. It realizes the structural claim that the count 7 equals 2^3-1 derived from D=3 in the Recognition Science forcing chain and that every nonzero state-change vector receives a plot encoding. The certificate supplies the single-statement summary quoted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.