module module high

`IndisputableMonolith.Aesthetics.NarrativeGeodesic`

Booker's seven plot families are placed in explicit bijection with the seven non-zero vectors of F_2^3 via plotEncoding. Pattern classification and Recognition Science workers cite the module when enumerating discrete aesthetic structures or extending the count to gauge families. The module defines the families as an inductive type, supplies the encoding map, and verifies the bijection by direct cardinality and injectivity checks against the F2Power algebra.

claimThe seven Booker plot families stand in bijection with the non-zero elements of the vector space $F_2^3$ under the map plotEncoding.

background

F2Power D supplies the elementary abelian 2-group of rank D, so that F2Power 3 consists of exactly seven non-zero vectors. Constants fixes the RS time quantum τ₀ = 1 tick. Cost supplies the J-cost and defectDist primitives that underlie recognition. The companion paper Seven_Plots_Three_Dimensions.tex asserts that the count 7 arises from (Z/2Z)^3 minus the origin; the present module converts that assertion into a proved bijection.

proof idea

This is a definition module. BookerPlotFamily is introduced as an inductive enumeration of seven cases. plotEncoding is defined by case analysis onto F2Power 3. Injectivity, non-zero image, and cardinality seven are established by exhaustive checking against the F2Power structure and the lemmas all_nodup and card_eq_seven.

why it matters in Recognition Science

The module supplies the explicit combinatorial count of seven that is reused in Patterns.TwoToTheDMinusOne to obtain the 2^D - 1 Count Law. That law applies the same fact to seven gauge-boson families at D = 3 and three opponent-color channels at D = 2. It thereby discharges the combinatorial claim left open in the Seven_Plots_Three_Dimensions paper.

scope and limits

Does not derive the plot families from the J-cost or Recognition Composition Law.
Does not address continuous deformations or narrative geodesics beyond the discrete encoding.
Does not extend the bijection to dimensions D other than 3.
Does not compute explicit J-cost values for any encoded plot.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Patterns.TwoToTheDMinusOne module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Algebra.F2Power module_import
IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (29)

inductive BookerPlotFamily L90
def name L103
def all L113
theorem all_length L118
theorem all_nodup L122
theorem card_eq_seven L131
def plotEncoding L142
theorem plotEncoding_injective L152
theorem plotEncoding_image_nonzero L157
theorem plotEncoding_image_eq_nonzero L163
theorem Q3_nontrivial_subgroup_count L183
theorem booker_count_eq_F2Power3_nonzero L189
theorem booker_seven_eq_2_pow_3_minus_1 L197
theorem no_eighth_plot L206
theorem plot_composition_xor_additive L217
theorem plot_composition_cancels_iff L227
theorem plot_count_scaling L245
def plotWeight L253
theorem singleAxis_plots L258
theorem twoAxis_plots L267
theorem threeAxis_plots L275
def narrativeTension L284
theorem narrativeTension_resolution L288
theorem narrativeTension_nonneg L295
structure ThreeActNarrative L305
theorem three_act_resolution_below_climax L314
structure NarrativeGeodesicCert L332
def narrativeGeodesicCert L350
theorem narrative_geodesic_one_statement L372