`plotEncoding`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Aesthetics.NarrativeGeodesic on GitHub at line 142.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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.