projectionScale

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 that turns a scale-invariant energy fraction into a per-cell integrated weight.

The cell index set is the product of the octave clock with the spatial vertices of the $Q_3$ cell. Its cardinality is defined as $N_{\mathrm{cell}} := |\mathrm{Fin},8 \times \mathrm{Fin},8|$, documented as ticks × vertices = $8\times 8 = 64$. The projection scale is simply that natural number viewed as a real.

This sits in the constants layer that feeds gap-weight formulas; the eight-tick factor is the T7 octave of the forcing chain.

One-line definition: coerce the natural number $N_{\mathrm{cell}}$ to $\mathbb{R}$. No lemmas are applied; the @[simp] attribute exposes the coercion for downstream simplification (notably via the sibling equality that evaluates the cardinality to 64).

This constant is the explicit measure factor that closes the “weights + normalization” ambiguity flagged in the module doc. Downstream, w8_projected multiplies the raw DFT energy ratio by the projection scale, converting a dimensionless fraction into a per-cell weight; nonnegativity lemmas for that weight and for total DFT energy depend on the scale being nonnegative. The sibling equality theorem pins the numeric value at 64. Framework-wise it records the $8\times 8$ interface cell (T7 eight-tick octave times eight $Q_3$ vertices), so the normalization is forced rather than free.