N_ticks
plain-language theorem explainer
The fundamental octave is counted as eight discrete ticks, via the cardinality of the standard 8-element finite type. Gap-weight and spectral-projection normalizations cite this constant when building the RS interface cell measure. The definition is a one-line finite-type cardinality.
Claim. The number of ticks in the fundamental octave is the cardinality of an eight-element finite set: $N_{\mathrm{ticks}} := |\{0,\ldots,7\}|$.
background
Recognition Science forces an eight-tick octave (forcing-chain T7): the fundamental clock has period $2^3=8$. This module closes a historical ambiguity in gap-weight projections by naming the two factors in the cell measure explicitly.
The module doc states that normalization uses $64=8\times 8$, the product of octave ticks and the eight vertices of a $Q_3$ cell. The tick factor is this constant. DFT8 diagonalizes the cyclic shift on the same eight-point set, so spectral weights such as $\sin^2(\pi k/8)$ live on it.
proof idea
One-line definition: the natural number equal to the finite-type cardinality of Fin 8. The @[simp] attribute exposes the value to the simplifier. No lemmas or tactics are required.
why it matters
Downstream, the simp theorem equating this constant to 8 discharges every occurrence in projection-scale and weight formulas. Together with the matching eight-vertex count it justifies the factor 64 that converts a scale-invariant fraction into a per-cell integrated weight. That is the claim-hygiene goal of GapWeight.Projection: no hidden operator or measure choice. The definition is the tick half of the T7 eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.