N_vertices
plain-language theorem explainer
Defines the spatial vertex count of a Q₃ cell as the cardinality of Fin 8, hence eight vertices. Anyone normalizing gap weights over the fundamental RS interface cell cites this constant. The body is a one-line Fintype cardinality abbreviation, marked simp for automatic unfolding.
Claim. The number of spatial vertices in a $Q_3$ cell is $N_{\mathrm{vertices}} := |\mathrm{Fin}\, 8| \in \mathbb{N}$, i.e. the cardinality of an eight-element finite type.
background
The GapWeight.Projection module makes two historically implicit choices explicit: the $\sin^2(\pi k/8)$ spectral weights from the discrete Laplacian on the 8-tick cyclic shift, and the normalization factor $64 = 8 \times 8$. That product is the size of the fundamental RS interface cell: eight ticks (the octave clock) times eight spatial vertices.
A $Q_3$ cell is the 3-cube graph; it has eight vertices. This definition records that count as Fintype.card (Fin 8), so downstream formulas can name the vertex factor without a magic numeral. Together with the companion tick count, it supplies the measure that turns a scale-invariant weight fraction into a per-cell integrated weight.
proof idea
Pure definition: set the natural number equal to the Fintype cardinality of Fin 8. No proof obligations. The @[simp] attribute lets the simplifier replace the name by its value in later goals; the sibling equality theorem then discharges the concrete numeral 8 by decide.
why it matters
Closes claim hygiene on the normalization side of gap weights. Downstream, N_vertices_eq proves the value is exactly 8, and the module doc ties $8 \times 8 = 64$ to the fundamental cell index set (ticks $\times$ vertices). That factor is what converts spectral fractions into per-cell integrated weights, removing a hidden degree of freedom in the weight formulas.
Framework-wise this sits on the eight-tick octave (T7) and the $Q_3$ spatial cell consistent with $D = 3$ (T8). Without an explicit vertex count, the 64-normalization would look arbitrary; naming it here pins the operator/measure choice to the RS interface geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.