structure
definition
NarrativeStructureCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Aesthetics.NarrativeStructureFromF2Cube on GitHub at line 56.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
53theorem bookerCount_eq_F2cube_minus_one :
54 Fintype.card BookerStory = 2^3 - 1 := by decide
55
56structure NarrativeStructureCert where
57 three_axes : Fintype.card NarrativeAxis = 3
58 seven_stories_via_decide : (Finset.univ.filter IsBookerStory).card = 7
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