harmonics_factored
plain-language theorem explainer
The declaration shows that each harmonic frequency in the DFT-8 spectrum equals the mode index times the carrier frequency divided by eight. Workers on RS brain-rhythm combs or theta-band therapies cite this identity to confirm the comb structure. The proof is a direct algebraic reduction obtained by unfolding the two definitions and normalizing with ring.
Claim. Let $k$ be an element of the finite set of eight DFT modes. Let $ν_k$ denote the frequency of the $k$-th harmonic and let $ω_c = 5φ$ be the carrier frequency. Then $ν_k = k · (ω_c / 8)$.
background
The module establishes the DFT-8 harmonic spectrum for cross-domain applications in Recognition Science. DFTMode is the type Fin 8 indexing the eight modes. The carrier frequency is defined as 5 times phi, approximately 8.09 Hz in the theta band. The harmonic frequency for mode k is defined as k.val times 5 times phi divided by 8. This factorization theorem confirms that the spectrum takes the form ν_k = k · 5φ / 8 Hz, matching the canonical RS sound-therapy frequency comb described in the module documentation.
proof idea
The proof unfolds the definitions of harmonicFrequency and carrierFreq, then applies the ring tactic to verify the algebraic identity.
why it matters
This result anchors the C24 structural claim that the eight DFT modes carry physical content through the fundamental frequency 5φ Hz. It directly supports the RS frequency comb ν_k = (k · 5φ / 8) Hz for k = 0 to 7, which is central to the eight-tick octave structure in the framework. No downstream uses are recorded yet, but it closes the algebraic part of the spectrum definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.