mode_seven_lt_carrier
plain-language theorem explainer
The theorem shows that the seventh harmonic frequency in the RS DFT-8 comb lies strictly below the carrier frequency 5φ Hz. Researchers modeling Recognition Science brain-rhythm combs or sound-therapy spectra cite this bound to confirm all modes stay inside the theta band. The short proof substitutes the explicit seventh-mode expression, normalizes by the positive factor φ, and finishes with linear arithmetic.
Claim. Let the harmonic frequencies be given by $ν_k = k · 5φ / 8$ for $k = 0,…,7$ and let the carrier frequency be $5φ$. Then $ν_7 < 5φ$.
background
The module defines the DFT-8 frequency comb of Recognition Science as $ν_k = (k · 5φ / 8)$ Hz for the eight modes $k=0$ to $7$, with carrier frequency $5φ ≈ 8.09$ Hz placed in the theta band. The upstream definition carrierFreq sets this carrier to $5 · φ$, while harmonicFrequency computes the scaled term $(k.val : ℝ) · 5 · φ / 8$. The sibling theorem mode_seven supplies the explicit value $35φ/8$ for the highest mode. This construction follows the eight-tick octave structure, ensuring all frequencies remain non-negative and the highest mode stays below the carrier.
proof idea
The term-mode proof begins by rewriting with the mode_seven equality, replacing the left-hand side by $35φ/8$. It unfolds the carrier definition, invokes div_lt_iff₀ after confirming positivity of the denominator, and reduces the goal to the comparison $35φ < 40φ$. The final step applies linarith using the positivity of φ.
why it matters
The result verifies the module statement that the highest harmonic remains inside the theta band, completing the structural claim for the C24 DFT-8 spectrum. It directly supports the assertion that all eight modes satisfy $ν_k < 5φ$, consistent with the Q₃ vertex assignment and the eight-tick octave of the framework. No downstream theorems are listed, so the bound functions as a local closure for the frequency-comb properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.