`plot_count_scaling`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Aesthetics.NarrativeGeodesic on GitHub at line 245.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 242
 243/-- **Falsifier 2 of the paper, in cardinality form.** The plot count
 244    at general dimension `D` is `2 ^ D - 1`. -/
 245theorem plot_count_scaling (D : ℕ) :
 246    (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card = 2 ^ D - 1 :=
 247  F2Power.nonzero_card
 248
 249/-! ## §5. Weight decomposition matches Booker's primary/compound/transcendent -/
 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 :

papers checked against this theorem

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