carrier_gt_8
plain-language theorem explainer
The carrier frequency 5φ in the DFT-8 spectrum exceeds 8 Hz. Researchers modeling RS brain-rhythm combs cite this bound to confirm the theta-band placement of the fundamental mode. The proof unfolds the carrier definition and applies the golden-ratio lower bound via linear arithmetic.
Claim. The carrier frequency satisfies $5φ > 8$, where $φ$ is the golden ratio.
background
The CrossDomain.DFTHarmonicSpectrum module defines the DFT-8 spectrum with frequencies ν_k = (k · 5φ / 8) Hz for k = 0..7. The carrier frequency is introduced as carrierFreq = 5 * phi ≈ 8.09 Hz to anchor the comb in the theta band. This setting draws on the upstream lemma phi_gt_onePointSixOne, which states φ > 1.61.
proof idea
The proof unfolds carrierFreq to 5 * phi. It invokes the lemma phi_gt_onePointSixOne to obtain φ > 1.61. Linear arithmetic then yields the strict inequality 5 * phi > 8.
why it matters
This supplies the lower theta-band bound used inside dftHarmonicSpectrumCert to certify the full spectrum properties. It realizes the module claim that the eight DFT modes carry physical content via the 5φ Hz carrier, aligning with the eight-tick octave structure in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.