harmonicFrequency
plain-language theorem explainer
The definition assigns to each DFT mode k the real value k * 5 * phi / 8, producing the eight frequencies of the RS harmonic comb with carrier at 5 phi Hz. Cross-domain and brain-rhythm modelers cite it as the canonical theta-band spectrum for the 2^3 structure. It is realized by a direct arithmetic expression on the mode index and the constant phi.
Claim. For each mode index $k$ in the finite type Fin 8, the frequency is given by $k = (k.val : ℝ) · 5 φ / 8$ Hz, where φ denotes the golden ratio.
background
The module CrossDomain.DFTHarmonicSpectrum defines the DFT-8 harmonic spectrum under claim C24. DFTMode is the type Fin 8, matching the 2³ count from HasTwoCubeCount in TwoCubeUniversality. The carrier frequency 5φ ≈ 8.09 Hz sits in the theta band, with all ν_k non-negative and the highest mode under 9 Hz. The constant phi is taken from the imported Constants module.
proof idea
This is a noncomputable definition whose body is the direct term (k.val : ℝ) * 5 * phi / 8. No lemmas or tactics are applied; it is a one-line wrapper that encodes the frequency formula from the module documentation.
why it matters
The definition supplies the frequency values used by DFTHarmonicSpectrumCert to certify eight modes, theta-band carrier, non-negativity, and mode bounds. It is unfolded in harmonics_factored, harmonics_nonneg, harmonic_strict_mono, mode_seven, and mode_seven_lt_9. In the Recognition framework it realizes the eight-tick octave (T7) with period 2³, placing the spectrum in the theta band consistent with the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.