harmonics_nonneg
plain-language theorem explainer
The theorem shows that every frequency in the RS DFT-8 comb is non-negative. Workers on theta-band frequency combs or neuromodulation protocols cite it to anchor the spectrum in the non-negative reals. The proof is a direct term-mode reduction that unfolds the frequency definition and chains non-negativity lemmas for multiplication and division.
Claim. For each index $k$ in the finite set of eight DFT modes, the frequency defined by $k.val$ times $5$ times $phi$ divided by $8$ satisfies $0$ less than or equal to that value.
background
DFTMode is the type Fin 8, indexing the eight modes of the DFT-8 structure. The function harmonicFrequency maps each such index to the real number (k.val : ℝ) * 5 * phi / 8, which is the k-th term in the comb ν_k = (k · 5φ / 8) Hz. The carrier frequency 5φ appears in sibling modules as the theta-band reference, and the module states that all eight modes lie in the non-negative reals with the highest mode still inside the theta band.
proof idea
The term proof first unfolds the definition of harmonicFrequency. It then applies div_nonneg, whose two arguments are supplied by mul_nonneg (itself built from mul_nonneg, Nat.cast_nonneg, norm_num, and le_of_lt phi_pos) and a final norm_num.
why it matters
The result supplies the all_modes_nonneg field inside dftHarmonicSpectrumCert, which certifies the full RS frequency comb. It directly supports the C24 structural claim that the eight-tick octave produces a non-negative spectrum, consistent with the T7 eight-tick octave and the requirement that all harmonics remain non-negative before further physical interpretation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.