`plotWeight`

definition

show as: view math explainer →

module: IndisputableMonolith.Aesthetics.NarrativeGeodesic
domain: Aesthetics
line: 253 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Aesthetics.NarrativeGeodesic on GitHub at line 253.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 250
 251/-- The Hamming weight of a Booker plot's encoding equals the number
 252    of narrative axes the plot transforms. -/
 253def plotWeight (p : BookerPlotFamily) : ℕ :=
 254  F2Power.hammingWeight (plotEncoding p)
 255
 256/-- The three single-axis plots (primary): Rags to Riches, Voyage and
 257    Return, Comedy. -/
 258theorem singleAxis_plots :
 259    plotWeight .ragsToRiches = 1 ∧
 260    plotWeight .voyageAndReturn = 1 ∧
 261    plotWeight .comedy = 1 := by
 262  refine ⟨?_, ?_, ?_⟩ <;>
 263    (unfold plotWeight plotEncoding F2Power.hammingWeight; decide)
 264
 265/-- The three two-axis plots (compound): Quest, Tragedy, Overcoming
 266    the Monster. -/
 267theorem twoAxis_plots :
 268    plotWeight .theQuest = 2 ∧
 269    plotWeight .tragedy = 2 ∧
 270    plotWeight .overcomingTheMonster = 2 := by
 271  refine ⟨?_, ?_, ?_⟩ <;>
 272    (unfold plotWeight plotEncoding F2Power.hammingWeight; decide)
 273
 274/-- The unique three-axis plot (transcendent): Rebirth. -/
 275theorem threeAxis_plots :
 276    plotWeight .rebirth = 3 := by
 277  unfold plotWeight plotEncoding F2Power.hammingWeight
 278  decide
 279
 280/-! ## §6. Narrative tension as J-cost -/
 281
 282/-- Narrative tension between actual and target intensity. This is
 283    the recognition cost of the deviation. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.