DFTMode
plain-language theorem explainer
DFTMode is the finite index set of cardinality 8 that labels the modes of the discrete Fourier transform comb in Recognition Science. Workers on the theta-band frequency comb cite the type when proving the eight harmonics and their carrier bounds. The declaration is a direct abbreviation to the standard Fin 8 type that satisfies the 2^3 count condition.
Claim. Let $DFTMode$ denote the finite set of integers from 0 to 7.
background
The module C24 defines the DFT-8 harmonic spectrum whose frequencies are given by $ν_k = k · 5φ / 8$ Hz for $k = 0,…,7$. This realizes the eight-tick octave with carrier $5φ ≈ 8.09$ Hz inside the theta band. Upstream, HasTwoCubeCount requires that a type $T$ satisfy Fintype.card $T = 2^3 = 8$, and the inductive DFTMode in TwoCubeUniversality enumerates exactly eight constructors.
proof idea
One-line abbreviation that identifies DFTMode with the standard finite type Fin 8.
why it matters
The type supplies the domain for harmonicFrequency, dftMode_count, harmonics_nonneg and the spectrum certificate DFTHarmonicSpectrumCert. It closes the eight-tick octave (T7) step of the forcing chain and supplies the eight modes required by the RS frequency comb. The construction is used in the cross-domain universality results that link the DFT comb to the 2-cube structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.