`plotEncoding`

definition

show as: view math explainer →

module: IndisputableMonolith.Aesthetics.NarrativeGeodesic
domain: Aesthetics
line: 142 · 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 142.

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

 139    Theorem 9 of `Seven_Plots_Three_Dimensions.tex`. The three
 140    axes are protagonist status (axis 1), world status (axis 2),
 141    and value alignment (axis 3). -/
 142def plotEncoding : BookerPlotFamily → F2Power 3
 143  | .ragsToRiches         => axis1     -- (true, false, false)
 144  | .voyageAndReturn      => axis2     -- (false, true, false)
 145  | .comedy               => axis3     -- (false, false, true)
 146  | .theQuest             => axis12    -- (true, true, false)
 147  | .tragedy              => axis13    -- (true, false, true)
 148  | .overcomingTheMonster => axis23    -- (false, true, true)
 149  | .rebirth              => axis123   -- (true, true, true)
 150
 151/-- The encoding is injective: distinct plots map to distinct vectors. -/
 152theorem plotEncoding_injective : Function.Injective plotEncoding := by
 153  intro p q hpq
 154  cases p <;> cases q <;> first | rfl | (exfalso; revert hpq; decide)
 155
 156/-- Every encoded vector is non-zero. -/
 157theorem plotEncoding_image_nonzero (p : BookerPlotFamily) :
 158    plotEncoding p ≠ 0 := by
 159  cases p <;> decide
 160
 161/-- The image of `plotEncoding` is exactly the seven non-zero
 162    vectors of `F2Power 3`. -/
 163theorem plotEncoding_image_eq_nonzero :
 164    Finset.univ.image plotEncoding =
 165      Finset.univ.filter (fun v : F2Power 3 => v ≠ 0) := by
 166  apply Finset.eq_of_subset_of_card_le
 167  · intro v hv
 168    rcases Finset.mem_image.mp hv with ⟨p, _, hp⟩
 169    rw [Finset.mem_filter, ← hp]
 170    exact ⟨Finset.mem_univ _, plotEncoding_image_nonzero p⟩
 171  · rw [F2Power.nonzero_card_three]
 172    have : (Finset.univ.image plotEncoding).card =

papers checked against this theorem

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