carrier_lt_8point1
plain-language theorem explainer
The theorem establishes that the carrier frequency 5φ is strictly less than 8.1, anchoring the DFT-8 spectrum inside the theta band. Researchers modeling Recognition Science frequency combs cite it to confirm that all eight modes remain below the upper theta threshold. The proof is a term-mode reduction that unfolds the carrier definition and applies the known phi bound via linear arithmetic.
Claim. The carrier frequency of the DFT-8 harmonic spectrum satisfies $5phi < 8.1$.
background
In the CrossDomain.DFTHarmonicSpectrum module the DFT-8 spectrum consists of eight modes with frequencies given by ν_k = (k · 5φ / 8) Hz for k = 0 to 7. The carrier frequency is defined as 5 * phi, yielding the approximate value 8.09 Hz that lies in the theta band. This construction is part of the RS frequency comb for sound-therapy and brain-rhythm applications.
proof idea
The term proof unfolds the definition of carrierFreq to 5 * phi, invokes the upstream lemma phi_lt_onePointSixTwo that supplies phi < 1.62, and closes the inequality with linarith.
why it matters
The result supplies the upper half of the carrier_in_theta_band pair inside dftHarmonicSpectrumCert, which certifies the full set of DFT-8 properties including eight modes and non-negative harmonics. It directly supports the module claim that the spectrum resides in the theta band and aligns with the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.