narrativeStructureCert
plain-language theorem explainer
A definition assembles the certificate confirming that three narrative axes generate exactly seven universal story patterns matching the non-zero elements of the three-dimensional binary cube. Formal aestheticians working within Recognition Science would cite it to anchor Booker's catalog in the lattice structure. The construction is a direct record instantiation that inserts four pre-decided cardinality theorems into the structure fields.
Claim. The certificate structure asserts that the number of narrative axes is three, that the number of stories satisfying the Booker condition is seven, that the number of Booker stories is seven, and that this number equals two to the third power minus one. The provided definition populates this structure with the established cardinalities for each assertion.
background
The module treats Booker's seven universal story patterns as the non-trivial elements of the F₂³ lattice in three dimensions. Each pattern is a sequence of recognition events generated by three binary axes: protagonist agency (reactive versus proactive), conflict origin (internal versus external), and resolution type (restoration versus transformation). These axes produce the seven weight-1, 2, and 3 combinations that match the listed archetypes: Overcoming the Monster, Rags to Riches, The Quest, Voyage and Return, Comedy, Tragedy, and Rebirth.
proof idea
The definition is a record constructor that supplies the value from the theorem on axis cardinality to the three-axes field, the value from the filtered story count theorem to the seven-stories-via-decide field, the value from the Booker story cardinality theorem to the seven-Booker-stories field, and the value from the equality-to-seven theorem to the count-equals-flip field. Each source theorem is established by the decide tactic.
why it matters
This definition supplies the concrete witness for the correspondence between the seven Booker stories and the seven non-zero elements of the F₂³ cube, as stated in the module documentation. It completes the certification step that embeds narrative archetypes into the Recognition Science aesthetics layer, relying on the D=3 result from the forcing chain. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.