mode_seven
plain-language theorem explainer
Mode 7 of the DFT-8 harmonic spectrum equals 35 phi over 8 Hz. Cross-domain researchers modeling theta-band brain rhythms and neuromodulation devices cite this value to fix the upper end of the RS frequency comb. The result follows from direct substitution into the scaled frequency formula. Algebraic simplification via ring confirms the exact coefficient.
Claim. Let $k$ range over DFT modes with $k=7$. The frequency satisfies $k · 5φ / 8 = 35φ / 8$.
background
The module defines the DFT-8 spectrum with frequencies ν_k = k · 5φ / 8 Hz for k = 0 to 7, one per Q3 vertex. The carrier sits at 5φ ≈ 8.09 Hz inside the theta band. harmonicFrequency implements the scaling as (k.val : ℝ) * 5 * phi / 8. Upstream carrier definitions from CorticalNeuromodulationDevice and PhantomCoupledGWAntennaSensitivity both set the base to 5 * phi.
proof idea
Unfold harmonicFrequency to expose the product 7 * 5 * phi / 8. push_cast clears the natural-number cast. ring then reduces the arithmetic to 35 * phi / 8.
why it matters
The value feeds mode_seven_lt_9, which bounds the highest harmonic below 9 Hz, and mode_seven_lt_carrier, which places it below the carrier. It closes the explicit frequency assignment inside the C24 DFT-8 comb claim. The result keeps all eight modes inside the theta band while respecting the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.