mode_zero
The theorem establishes that the zero DFT mode carries frequency zero, serving as the DC component in the RS frequency comb defined by ν_k = k · 5φ / 8 Hz. Researchers certifying brain-rhythm or sound-therapy spectra in Recognition Science would cite this when confirming the full eight-mode set. The proof is a short tactic sequence that unfolds the harmonicFrequency definition and simplifies the resulting arithmetic expression to zero.
claimThe zero mode frequency satisfies $ν_0 = 0$, where $ν_k = k · 5φ / 8$ Hz for DFT modes $k = 0, …, 7$.
background
The module defines the DFT-8 harmonic spectrum with frequencies ν_k = (k · 5φ / 8) Hz for k = 0 to 7, where the carrier 5φ lies in the theta band. The upstream definition harmonicFrequency (k : DFTMode) : ℝ := (k.val : ℝ) * 5 * phi / 8 computes each term directly from this formula. This theorem verifies the k = 0 case as the direct-current component, consistent with the module claim that all frequencies are non-negative.
proof idea
The proof unfolds harmonicFrequency and applies simp, which reduces the expression (0 : ℝ) * 5 * phi / 8 directly to zero.
why it matters in Recognition Science
This supplies the mode_zero_dc field inside dftHarmonicSpectrumCert, which certifies the complete DFT-8 spectrum including eight modes, theta-band carrier, non-negativity, and the highest mode below 9 Hz. It fills the k = 0 slot in the C24 RS frequency comb and supports the eight-tick octave structure. No open scaffolding questions are addressed.
scope and limits
- Does not establish frequencies for modes 1 through 7.
- Does not derive the numerical carrier value 5φ.
- Does not map modes to Q₃ vertices or physical units.
- Does not address experimental validation or sound-therapy applications.
Lean usage
dftHarmonicSpectrumCert where mode_zero_dc := mode_zeroformal statement (Lean)
74theorem mode_zero : harmonicFrequency ⟨0, by decide⟩ = 0 := by
proof body
Term-mode proof.
75 unfold harmonicFrequency
76 simp
77
78/-- Mode 7 = highest harmonic: 35φ/8. -/