structure
definition
ThreeActNarrative
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Aesthetics.NarrativeGeodesic on GitHub at line 305.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
302
303/-- Three-act narrative state. Act 1 has J-cost `s`, Act 2 (climax)
304 has J-cost `c > s`, Act 3 (resolution) has J-cost `0`. -/
305structure ThreeActNarrative where
306 setup_cost : ℝ
307 climax_cost : ℝ
308 resolution_cost : ℝ
309 setup_pos : 0 < setup_cost
310 climax_higher : setup_cost < climax_cost
311 resolution_zero : resolution_cost = 0
312
313/-- Resolution strictly below climax. -/
314theorem three_act_resolution_below_climax (n : ThreeActNarrative) :
315 n.resolution_cost < n.climax_cost := by
316 rw [n.resolution_zero]
317 linarith [n.setup_pos, n.climax_higher]
318
319/-! ## §8. Master certificate -/
320
321/-- **NARRATIVE GEODESIC MASTER CERTIFICATE (deepened).**
322
323 The seven Booker plot families are in explicit bijection with the
324 seven non-zero vectors of `F2Power 3`. The count `7` is
325 `2 ^ 3 - 1`, derived from the dimension `D = 3` of the narrative
326 state space. Every non-zero state-change vector is encoded by
327 some plot (no eighth plot). Composition is XOR-additive. The
328 weight decomposition `1 + 3 + 3 + 1` of `F2Power 3` matches
329 Booker's primary/compound/transcendent grouping. Narrative
330 tension is the J-cost of the deviation between actual and target
331 intensity, vanishing at resolution. -/
332structure NarrativeGeodesicCert where
333 seven_plot_families :
334 Fintype.card BookerPlotFamily = 7
335 plot_count_is_2_pow_3_minus_1 :