harmonicFrequency
The definition assigns to each DFT mode k the real value k * 5 * phi / 8, producing the eight frequencies of the RS harmonic comb with carrier at 5 phi Hz. Cross-domain and brain-rhythm modelers cite it as the canonical theta-band spectrum for the 2^3 structure. It is realized by a direct arithmetic expression on the mode index and the constant phi.
claimFor each mode index $k$ in the finite type Fin 8, the frequency is given by $k = (k.val : ℝ) · 5 φ / 8$ Hz, where φ denotes the golden ratio.
background
The module CrossDomain.DFTHarmonicSpectrum defines the DFT-8 harmonic spectrum under claim C24. DFTMode is the type Fin 8, matching the 2³ count from HasTwoCubeCount in TwoCubeUniversality. The carrier frequency 5φ ≈ 8.09 Hz sits in the theta band, with all ν_k non-negative and the highest mode under 9 Hz. The constant phi is taken from the imported Constants module.
proof idea
This is a noncomputable definition whose body is the direct term (k.val : ℝ) * 5 * phi / 8. No lemmas or tactics are applied; it is a one-line wrapper that encodes the frequency formula from the module documentation.
why it matters in Recognition Science
The definition supplies the frequency values used by DFTHarmonicSpectrumCert to certify eight modes, theta-band carrier, non-negativity, and mode bounds. It is unfolded in harmonics_factored, harmonics_nonneg, harmonic_strict_mono, mode_seven, and mode_seven_lt_9. In the Recognition framework it realizes the eight-tick octave (T7) with period 2³, placing the spectrum in the theta band consistent with the phi-ladder.
scope and limits
- Does not derive the carrier value 5φ from the forcing chain T0-T8.
- Does not interpret the frequencies as physical waves or brain rhythms.
- Does not prove non-negativity or monotonicity (handled in separate theorems).
- Does not extend the spectrum beyond the eight DFT modes.
- Does not claim numerical agreement with experimental measurements.
formal statement (Lean)
34noncomputable def harmonicFrequency (k : DFTMode) : ℝ :=
proof body
Definition body.
35 (k.val : ℝ) * 5 * phi / 8
36
37/-- Carrier frequency: 5φ ≈ 8.09 Hz (theta band). -/