harmonics_nonneg
The theorem proves every harmonic frequency in the eight-mode RS DFT comb is non-negative. Researchers modeling theta-band brain rhythms or sound-therapy combs cite it to confirm the spectrum lies in the non-negative reals. The proof is a direct term-mode reduction that unfolds the explicit formula and applies real-number non-negativity lemmas for multiplication and division.
claimFor every mode index $k$ in the finite set of eight DFT modes, the harmonic frequency satisfies $0 ≤ ν_k$ where $ν_k = (k · 5φ)/8$ and $φ$ denotes the golden ratio.
background
The module treats the DFT-8 Harmonic Spectrum as a frequency comb with eight modes indexed by DFTMode, defined as the type Fin 8. The harmonic frequency is introduced by the sibling definition harmonicFrequency k := (k.val : ℝ) * 5 * phi / 8, with carrier frequency 5 phi drawn from upstream engineering modules on cortical neuromodulation and phantom-coupled GW antennas. The local setting is the canonical RS comb ν_k = k · 5φ / 8 Hz for k = 0 to 7, one mode per vertex of the 2³ cube, lying inside the theta band.
proof idea
The term proof unfolds harmonicFrequency to expose the quotient expression. It applies div_nonneg, reducing the goal to non-negativity of the numerator. Two successive mul_nonneg steps are discharged by Nat.cast_nonneg on the integer mode index, norm_num on the numeric constants, and le_of_lt phi_pos for the positivity of phi.
why it matters in Recognition Science
The result supplies the all_modes_nonneg field inside dftHarmonicSpectrumCert, which certifies the complete set of spectrum properties required by the CrossDomain module. It closes the basic positivity check for the eight-tick octave frequency comb (T7) and supports downstream claims that all modes remain non-negative while the carrier stays inside the theta band. No open scaffolding remains on this specific positivity statement.
scope and limits
- Does not bound the frequencies above zero or prove strict positivity for nonzero modes.
- Does not extend the non-negativity claim to continuous or non-integer indices.
- Does not address physical units, scaling, or conversion outside RS-native normalization.
- Does not prove the frequencies are distinct or span a closed interval.
Lean usage
example (k : DFTMode) : 0 ≤ harmonicFrequency k := harmonics_nonneg kformal statement (Lean)
57theorem harmonics_nonneg (k : DFTMode) : 0 ≤ harmonicFrequency k := by
proof body
Term-mode proof.
58 unfold harmonicFrequency
59 apply div_nonneg
60 · apply mul_nonneg
61 apply mul_nonneg
62 · exact Nat.cast_nonneg _
63 · norm_num
64 · exact le_of_lt phi_pos
65 · norm_num
66
67/-- The k-th harmonic is k · (carrier / 8). -/