pith. machine review for the scientific record. sign in
def definition def or abbrev

narrativeStructureCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  62def narrativeStructureCert : NarrativeStructureCert where
  63  three_axes := narrativeAxisCount

proof body

Definition body.

  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

depends on (5)

Lean names referenced from this declaration's body.