mode_seven
The theorem proves that the seventh DFT mode in the RS harmonic spectrum equals 35φ/8 Hz. Engineers modeling theta-band neuromodulation or sound-therapy combs would cite this exact value for the highest mode. The proof is a one-line term wrapper that unfolds the harmonicFrequency definition and reduces via push_cast and ring.
claimThe frequency of the seventh mode satisfies $ν_7 = 35φ/8$, where the DFT-8 spectrum is given by $ν_k = k · 5φ/8$ Hz for $k = 0,…,7$ and $φ$ denotes the golden ratio.
background
The module defines the DFT-8 spectrum with eight modes, one per Q₃ vertex, using the fundamental frequency 5φ Hz (theta band). The definition harmonicFrequency computes ν_k explicitly as (k.val : ℝ) * 5 * phi / 8. Upstream carrier definitions from cortical neuromodulation and phantom GW antenna modules both set the carrier to 5 * phi, confirming the same base frequency.
proof idea
The term proof unfolds harmonicFrequency on the mode with value 7, producing the expression 7 * 5 * phi / 8. It then applies push_cast to normalize the natural-number cast and ring to algebraically simplify the product to 35 * phi / 8.
why it matters in Recognition Science
This supplies the explicit highest-mode value required by the C24 claim that the eight DFT modes carry physical content. It is invoked directly by mode_seven_lt_9 (to bound the mode below 9 Hz) and mode_seven_lt_carrier (to show it lies below the carrier). In the Recognition Science framework it instantiates the eight-tick octave (T7) with the frequency comb tied to the phi-ladder and theta-band applications.
scope and limits
- Does not prove any physical interaction mechanism between these frequencies and cortical columns.
- Does not extend the spectrum to modes outside k=0..7.
- Does not supply numerical approximations or error estimates for the frequencies.
- Does not address non-harmonic or transient components in the underlying signal.
Lean usage
rw [mode_seven]formal statement (Lean)
79theorem mode_seven : harmonicFrequency ⟨7, by decide⟩ = 35 * phi / 8 := by
proof body
Term-mode proof.
80 unfold harmonicFrequency
81 push_cast; ring
82
83/-- Mode 7 < carrier (since 7/8 < 1). -/