N_vertices_eq
plain-language theorem explainer
The spatial vertex count of a Q₃ cell equals 8. Anyone normalizing gap weights by the fundamental RS interface cell (ticks × vertices) cites this equality. The proof is a one-shot decidable evaluation of the finite cardinality of Fin 8.
Claim. The number of spatial vertices in a $Q_3$ cell equals $8$: if $N_{\mathrm{vertices}}$ is defined as the cardinality of $\mathrm{Fin}\,8$, then $N_{\mathrm{vertices}}=8$.
background
The GapWeight.Projection module makes two historically implicit choices explicit: the $\sin^2(\pi k/8)$ spectral weight from the discrete Laplacian on the 8-tick cyclic shift, and the normalization factor $64=8\times 8$. That factor is the cardinality of the fundamental RS interface cell: 8 ticks (the octave clock) times 8 spatial vertices of a $Q_3$ cell.
Here $N_{\mathrm{vertices}}$ is defined as $\mathrm{Fintype.card}(\mathrm{Fin},8)$, i.e. the size of the standard 8-element finite type used to index those vertices. A sibling constant $N_{\mathrm{ticks}}$ plays the same role for the temporal side; their product is $N_{\mathrm{cell}}$.
This sits in the Constants domain and supports claim hygiene for gap-weight formulas: once the operator and measure are named, there is no free normalization parameter left in the projection.
proof idea
One-line decidable proof. Unfold $N_{\mathrm{vertices}}$ to $\mathrm{Fintype.card}(\mathrm{Fin},8)$ and run decide, which evaluates the finite cardinality to the numeral 8. No lemmas beyond the simp-tagged definition are required; the @[simp] attribute on both the def and the theorem makes downstream rewrites automatic.
why it matters
Closes the spatial half of the $64=8\times 8$ normalization story in GapWeight.Projection. Together with the tick count, it converts a scale-invariant spectral fraction into a per-cell integrated weight, removing a hidden degree of freedom in the geometric weights.
Framework landmark: T7 forces the eight-tick octave (period $2^3$); the dual spatial count of 8 is the vertex set of the $Q_3$ cell used as the RS interface. The module doc states the point directly: normalization uses 64 because the cell is ticks × vertices.
No downstream theorems currently list this declaration as a direct edge, but sibling equalities ($N_{\mathrm{ticks_eq}}$, $N_{\mathrm{cell_eq}}$, $\mathrm{projectionScale_eq}$) form the same hygiene layer for the projected weight $w_8$ and the DFT energy total.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.