mode_seven_lt_9
plain-language theorem explainer
mode_seven_lt_9 establishes that the seventh mode frequency in the RS DFT comb satisfies 35 phi /8 <9. Brain-rhythm and sound-therapy models cite the bound to keep the entire eight-mode spectrum inside the theta band. The proof rewrites the explicit expression for mode seven then applies the numerical upper bound on phi together with linear arithmetic.
Claim. The frequency of the seventh DFT mode satisfies $35 phi / 8 < 9$, where $phi$ denotes the golden ratio and the frequency is given by $nu_k = k cdot 5 phi / 8$ Hz.
background
The module states that the eight DFT modes carry physical content via the fundamental frequency 5 phi Hz (theta band). The full RS frequency comb is defined by $nu_k = (k cdot 5 phi / 8)$ Hz for k = 0 to 7. The definition harmonicFrequency computes this value for a DFTMode k, and the theorem mode_seven supplies the explicit case 35 phi /8 for k=7. Upstream, phi_lt_onePointSixTwo supplies the concrete bound phi < 1.62.
proof idea
The term proof first rewrites via mode_seven to obtain the explicit expression 35 phi /8. It then brings in the lemma phi_lt_onePointSixTwo and finishes with linarith on the resulting numerical comparison.
why it matters
The result is referenced inside dftHarmonicSpectrumCert as the field mode_seven_under_9. It completes the C24 structural claim that the highest mode remains below 9 Hz while the carrier sits near 8.09 Hz. In the Recognition framework this supports the eight-tick octave by keeping all frequencies inside the theta band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.