narrativeGeodesicCert

formal source

 347    ∀ (n : ThreeActNarrative), n.resolution_cost < n.climax_cost
 348
 349/-- The master certificate is inhabited. -/
 350def narrativeGeodesicCert : NarrativeGeodesicCert where
 351  seven_plot_families := BookerPlotFamily.card_eq_seven
 352  plot_count_is_2_pow_3_minus_1 := booker_seven_eq_2_pow_3_minus_1
 353  Q3_subgroup_count := Q3_nontrivial_subgroup_count
 354  encoding_injective := plotEncoding_injective
 355  encoding_image_nonzero := plotEncoding_image_nonzero
 356  no_eighth_plot_holds := no_eighth_plot
 357  resolution_zero := narrativeTension_resolution
 358  three_act_below_climax := three_act_resolution_below_climax
 359
 360/-! ## §9. Single-statement summary -/
 361
 362/-- **NARRATIVE GEODESIC: ONE-STATEMENT THEOREM (deepened).**
 363
 364    (1) `Fintype.card BookerPlotFamily = 2 ^ 3 - 1 = 7`, with the
 365        count derived from the cube `F2Power 3`, not asserted.
 366    (2) Explicit injective encoding `plotEncoding : BookerPlotFamily
 367        → F2Power 3` whose image is exactly the non-zero vectors.
 368    (3) No eighth plot: every non-zero `δ : F2Power 3` is encoded by
 369        some plot.
 370    (4) Tension `T(a, t) = J(a/t)` vanishes at resolution `a = t`.
 371    (5) Three-act narrative has resolution strictly below climax. -/
 372theorem narrative_geodesic_one_statement :
 373    Fintype.card BookerPlotFamily = 2 ^ 3 - 1 ∧
 374    Function.Injective plotEncoding ∧
 375    (∀ δ : F2Power 3, δ ≠ 0 → ∃ p : BookerPlotFamily, plotEncoding p = δ) ∧
 376    (∀ (target : ℝ) (h : target ≠ 0),
 377      narrativeTension target target h = 0) ∧
 378    (∀ (n : ThreeActNarrative), n.resolution_cost < n.climax_cost) := by
 379  refine ⟨booker_seven_eq_2_pow_3_minus_1,
 380          plotEncoding_injective,