pith. machine review for the scientific record. sign in
def definition def or abbrev

narrativeGeodesicCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 350def narrativeGeodesicCert : NarrativeGeodesicCert where
 351  seven_plot_families := BookerPlotFamily.card_eq_seven

proof body

Definition body.

 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. -/

depends on (20)

Lean names referenced from this declaration's body.