N_ticks_eq
plain-language theorem explainer
The fundamental octave has exactly eight ticks: the named tick-count constant equals 8. Anyone normalizing gap weights or projection scales on the RS interface cell cites this. The proof is a one-line decidability check that the cardinality of Fin 8 is 8.
Claim. The number of ticks in the fundamental octave equals $8$.
background
In Recognition Science the fundamental clock is the eight-tick octave (forcing chain T7: period $2^3$). This module makes the gap-weight normalization explicit: the interface cell is counted as 8 ticks times 8 spatial vertices of a $Q_3$ cell, so the factor 64 is cardinality, not a free parameter.
The tick-count constant is defined as the fintype cardinality of Fin 8. The companion vertex count is modeled the same way. Together they fix the per-cell integrated weight that converts a scale-invariant spectral fraction into a dimensionful projection scale.
Upstream, the continuum bridge identifies discrete Laplacian action on the ledger with a weighted edge sum; the present constant only supplies the discrete tick measure that enters that normalization.
proof idea
One-line wrapper: decide discharges $N_{\mathrm{ticks}} = 8$ because the definition is Fintype.card (Fin 8) and Mathlib decides that cardinality equals 8. No lemmas beyond decidable equality on $\mathbb{N}$ are required.
why it matters
Claim hygiene for GapWeight.Projection: the module's stated goal is to remove the historical ambiguity in why normalization uses 64. Pinning the tick count at 8 (with the sibling vertex count also 8) makes $64 = 8 \times 8$ an explicit cardinality of the RS interface cell rather than a hidden choice.
This sits on the T7 eight-tick octave landmark and feeds the spectral story that geometric weights carry a $\sin^2(\pi k/8)$ factor from the discrete derivative on the cyclic shift. No downstream theorems are wired yet in the graph; the declaration is infrastructure for projectionScale and the projected $w_8$ weights in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.