N_cell_eq

The GapWeight.Projection module makes two historically implicit choices explicit: the spectral $\sin^2(\pi k/8)$ factor from the discrete Laplacian on the 8-tick cycle, and the normalization denominator $64$. That denominator is the size of the fundamental RS interface cell.

The cell index set is the product of the octave clock (8 ticks, forced by the T7 eight-tick period $2^3$) with the eight vertices of the $Q_3$ spatial cell. The definition N_cell is exactly Fintype.card (Fin 8 × Fin 8). The companion equalities for tick count and vertex count sit beside it; together they pin the measure that converts a scale-invariant fraction into a per-cell integrated weight.

One-line decision proof. After unfolding the definition to Fintype.card (Fin 8 × Fin 8), decide evaluates the finite product cardinality $8 \cdot 8 = 64$ by computation. No intermediate lemmas are required beyond the standard Mathlib finite-type card instance for products of Fin n.

This equality discharges the numeric content of the cell-size definition so that projectionScale_eq can conclude the projection scaling is exactly $64$ by a single simp. That scaling is the claim-hygiene step that removes a hidden degree of freedom in gap-weight normalization: fractions become per-cell weights with an operator/measure choice written in the open.

Framework-wise it sits on the T7 eight-tick octave and the eight-vertex $Q_3$ cell geometry. Downstream weight constructions that integrate over the RS interface cell inherit a fixed, non-negotiable denominator rather than an adjustable constant.