dftMode_count
plain-language theorem explainer
The theorem establishes that the DFT mode type has exactly eight elements. Researchers working on the Recognition Science frequency comb cite it to anchor the eight-mode structure to the Q₃ lattice and the eight-tick octave. The proof is a one-line decision procedure that evaluates the cardinality of Fin 8 directly.
Claim. $|DFTMode| = 8$, where $DFTMode$ is the finite type with eight elements indexed by $k = 0, 1, ..., 7$ corresponding to the DFT modes of the RS frequency comb.
background
In the CrossDomain.DFTHarmonicSpectrum module the DFT modes supply the basis for the RS frequency comb with frequencies ν_k = (k · 5φ / 8) Hz. DFTMode is defined as the finite type Fin 8. This supplies the eight-tick structure required by the Recognition Science framework (T7 eight-tick octave) and matches the Q₃ vertex count from SpectralEmergence, where the structure forces 24 chiral fermion flavors and |Aut(Q₃)| = 48.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card (Fin 8) and confirms equality to 8.
why it matters
This theorem supplies the modes_eight field in the downstream dftHarmonicSpectrumCert definition that certifies the full harmonic spectrum. It fills the structural claim of the C24 DFT-8 Harmonic Spectrum section, linking the eight modes to the eight-tick octave (T7) and the 2³ universality from TwoCubeUniversality. It touches the embedding of these modes into physical theta-band applications via the phi-ladder frequencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.