bookerCount_eq_F2cube_minus_one
plain-language theorem explainer
The equality establishes that the set of Booker story types has cardinality exactly 7, matching the count of nonzero vectors in the three-dimensional vector space over F₂. Researchers linking narrative theory to Recognition Science would cite this to embed the seven universal patterns inside the D=3 lattice geometry. The proof is a direct decision procedure that evaluates the finite-type cardinality from the inductive enumeration of the seven constructors.
Claim. Let $B$ be the inductive type whose constructors are the seven universal story patterns (overcoming the monster, rags to riches, the quest, voyage and return, comedy, tragedy, rebirth). Then $|B| = 2^3 - 1$.
background
The module extracts narrative structure from the F₂³ cube in the aesthetics sector of Recognition Science. BookerStory is the inductive type with exactly those seven constructors, equipped with DecidableEq, Repr, BEq and Fintype instances. The module documentation states that these seven patterns correspond to the seven nonzero elements of the three-dimensional binary vector space, realizing the D=3 lattice inside story sequences.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic computes Fintype.card directly from the inductive definition of BookerStory, confirming that the seven listed constructors yield cardinality 7, which equals 2^3 - 1.
why it matters
This theorem supplies the count_eq_flip field of the downstream narrativeStructureCert definition, which certifies the three narrative axes and seven stories. It realizes the T8 forcing-chain step that fixes D = 3 spatial dimensions via the eight-tick octave and the F₂³ geometry, thereby placing aesthetics on the same lattice foundation as the core Recognition Science derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.