N_cell
plain-language theorem explainer
Defines the fundamental RS cell-index cardinality as the size of the product of two 8-element finite sets (ticks × vertices), equal to 64. Anyone normalizing gap weights or converting dimensionless spectral fractions into per-cell integrated weights cites this constant. The body is a one-line Fintype cardinality definition.
Claim. Let $N_{\mathrm{cell}}$ be the cardinality of the fundamental cell-index set $\{0,\ldots,7\}\times\{0,\ldots,7\}$ (eight ticks times eight spatial vertices). Then $N_{\mathrm{cell}}=|\mathrm{Fin}\,8\times\mathrm{Fin}\,8|\in\mathbb{N}$.
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 that turns a scale-invariant fraction into a per-cell integrated weight.
In Recognition Science the eight-tick octave (forcing chain T7) is the discrete time clock, and the spatial interface cell is the 3-cube $Q_3$ with eight vertices. The fundamental cell-index set is therefore the product of these two 8-element sets. Its cardinality is the natural measure factor for projecting dimensionless DFT energy fractions onto one RS interface cell.
Sibling constants in the same module name the separate factors ($N_{\mathrm{ticks}}=8$, $N_{\mathrm{vertices}}=8$) before combining them here.
proof idea
Pure definition: $N_{\mathrm{cell}}$ is declared equal to $\mathrm{Fintype.card}(\mathrm{Fin},8\times\mathrm{Fin},8)$. No proof obligations. The companion theorem $N_{\mathrm{cell}}=64$ is discharged separately by decide on the finite product cardinality.
why it matters
This constant is the explicit source of the factor 64 that closes the “weights + normalization” ambiguity for gap weights. Downstream, N_cell_eq records the numerical identity $N_{\mathrm{cell}}=64$, and projectionScale casts the same value to $\mathbb{R}$ as the scaling that converts a dimensionless fraction into a per-cell weight.
Framework landmarks: T7 forces the eight-tick octave; the eight vertices are those of the $Q_3$ cell consistent with $D=3$ (T8). By naming the product cardinality once, the module removes a hidden degree of freedom in how spectral weights are integrated over the RS interface cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.