mode_seven_lt_9
mode_seven_lt_9 establishes that the seventh mode frequency in the RS DFT comb satisfies 35 phi /8 <9. Brain-rhythm and sound-therapy models cite the bound to keep the entire eight-mode spectrum inside the theta band. The proof rewrites the explicit expression for mode seven then applies the numerical upper bound on phi together with linear arithmetic.
claimThe frequency of the seventh DFT mode satisfies $35 phi / 8 < 9$, where $phi$ denotes the golden ratio and the frequency is given by $nu_k = k cdot 5 phi / 8$ Hz.
background
The module states that the eight DFT modes carry physical content via the fundamental frequency 5 phi Hz (theta band). The full RS frequency comb is defined by $nu_k = (k cdot 5 phi / 8)$ Hz for k = 0 to 7. The definition harmonicFrequency computes this value for a DFTMode k, and the theorem mode_seven supplies the explicit case 35 phi /8 for k=7. Upstream, phi_lt_onePointSixTwo supplies the concrete bound phi < 1.62.
proof idea
The term proof first rewrites via mode_seven to obtain the explicit expression 35 phi /8. It then brings in the lemma phi_lt_onePointSixTwo and finishes with linarith on the resulting numerical comparison.
why it matters in Recognition Science
The result is referenced inside dftHarmonicSpectrumCert as the field mode_seven_under_9. It completes the C24 structural claim that the highest mode remains below 9 Hz while the carrier sits near 8.09 Hz. In the Recognition framework this supports the eight-tick octave by keeping all frequencies inside the theta band.
scope and limits
- Does not derive the frequency formula from the J-cost or forcing chain.
- Does not bound any mode other than k=7.
- Does not convert the bound into SI units or experimental frequencies.
- Does not address stability of the comb under small changes in phi.
formal statement (Lean)
95theorem mode_seven_lt_9 : harmonicFrequency ⟨7, by decide⟩ < 9 := by
proof body
Term-mode proof.
96 rw [mode_seven]
97 have := phi_lt_onePointSixTwo
98 -- 35φ/8 < 35 · 1.62 / 8 = 56.7/8 = 7.0875 < 9
99 linarith
100
101/-- Strict monotonicity of the comb. -/