threeAxis_plots
plain-language theorem explainer
The theorem states that the Rebirth plot family carries narrative weight 3 under the axis encoding into the three-dimensional binary cube. Researchers examining structural narratology or the aesthetics component of Recognition Science would cite this when verifying the assignment of the all-ones vector. The proof reduces directly by unfolding the weight and encoding definitions then applying decidable evaluation.
Claim. Let $w$ denote Hamming weight on vectors in $F_2^3$. Then $w$ of the encoding of the Rebirth Booker plot family equals 3.
background
The module constructs a narrative geodesic by placing Booker's seven plot families in explicit bijection with the seven nonzero vectors of $F_2^3 = (Z/2Z)^3$. The plotEncoding definition supplies the axis assignment: protagonist status, world status, and value alignment. plotWeight is defined as the Hamming weight of the resulting vector, which counts the number of narrative axes transformed by the plot. F2Power models the space as Fin D → Bool and hammingWeight counts the true coordinates.
proof idea
The term proof unfolds plotWeight, plotEncoding, and F2Power.hammingWeight, then invokes the decide tactic to evaluate the concrete vector for Rebirth.
why it matters
This result verifies the three-axis assignment for Rebirth, completing the weight enumeration inside the narrative geodesic on Q3. It supports the structural closure of the aesthetics section by confirming the bijection with nonzero elements of F2Power 3, consistent with the three-dimensional setting of the Recognition framework. The declaration relies on the upstream count of exactly seven nonzero vectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.