`narrativeStructureCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Aesthetics.NarrativeStructureFromF2Cube
domain: Aesthetics
line: 62 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Aesthetics.NarrativeStructureFromF2Cube on GitHub at line 62.

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

  59  seven_booker_stories : Fintype.card BookerStory = 7
  60  count_eq_flip : Fintype.card BookerStory = 2^3 - 1
  61
  62def narrativeStructureCert : NarrativeStructureCert where
  63  three_axes := narrativeAxisCount
  64  seven_stories_via_decide := booker_count
  65  seven_booker_stories := bookerStoryCount
  66  count_eq_flip := bookerCount_eq_F2cube_minus_one
  67
  68end IndisputableMonolith.Aesthetics.NarrativeStructureFromF2Cube

papers checked against this theorem

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