mode_zero
plain-language theorem explainer
Mode zero of the DFT-8 frequency comb equals the DC term at frequency zero. Models of RS brain rhythms and sound-therapy combs cite this to fix the origin of the eight-mode ladder. The proof unfolds the linear definition of harmonicFrequency and reduces the k=0 case by simplification.
Claim. $ν_0 = 0$, where $ν_k = k · 5φ / 8$ Hz is the frequency assigned to the k-th DFT mode.
background
The module defines an eight-mode frequency comb on the DFT-8 structure, with each mode indexed by DFTMode (values 0 through 7) and frequency given by the linear map harmonicFrequency(k) = (k.val : ℝ) * 5 * phi / 8. This implements the structural claim that the comb runs from DC through the theta band with carrier 5φ ≈ 8.09 Hz. The upstream definition harmonicFrequency supplies the explicit scaling used by every mode property in the module.
proof idea
One-line wrapper that unfolds harmonicFrequency and applies simp to obtain the arithmetic identity 0 * 5 * phi / 8 = 0.
why it matters
Supplies the mode_zero_dc field required by dftHarmonicSpectrumCert, which assembles the full spectrum certificate (eight modes, carrier bounds, non-negativity, and mode-seven bound). The result anchors the k=0 case of the RS frequency comb that realizes the eight-tick octave (T7) with fundamental 5φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.