harmonic_strict_mono
The theorem proves strict monotonicity for the harmonic frequencies in the eight-mode DFT comb of Recognition Science. A researcher verifying the ordering of theta-band modes in the RS frequency spectrum would cite this result. The proof unfolds the frequency definition and chains three real-number inequalities on the scaled mode indices.
claimLet $j, k$ be integers in $0..7$ with $j < k$. Then $ν_j < ν_k$ where $ν_m = m · 5φ / 8$ for the RS harmonic comb.
background
DFTMode is the type Fin 8 indexing the eight modes of the discrete Fourier transform on the 2³ cube. The harmonicFrequency definition assigns to mode k the real value (k.val) · 5 · phi / 8, producing the RS frequency comb ν_k = k · 5φ / 8 Hz whose carrier 5φ lies near 8.09 Hz in the theta band. The module C24 records the structural properties of this comb for RS sound-therapy and brain-rhythm models.
proof idea
Term-mode proof. Unfold harmonicFrequency, apply div_lt_div_of_pos_right on the positive denominator 8, then mul_lt_mul_of_pos_right using phi_pos, and finally mul_lt_mul_of_pos_right on the cast indices via Nat.cast_lt.
why it matters in Recognition Science
The result feeds dftHarmonicSpectrumCert by guaranteeing ordered frequencies across the eight modes. It supplies the monotonicity step inside the C24 DFT-8 spectrum claim ν_k = (k · 5φ / 8) Hz. In the framework it confirms the discrete ordering required by the eight-tick octave and the 2³ structure.
scope and limits
- Does not establish numerical theta-band bounds.
- Does not derive the carrier value 5φ.
- Does not map modes to physical brain rhythms.
- Does not extend to continuous spectra.
formal statement (Lean)
102theorem harmonic_strict_mono (j k : DFTMode) (hjk : j.val < k.val) :
103 harmonicFrequency j < harmonicFrequency k := by
proof body
Term-mode proof.
104 unfold harmonicFrequency
105 apply div_lt_div_of_pos_right _ (by norm_num : (8 : ℝ) > 0)
106 apply mul_lt_mul_of_pos_right _ phi_pos
107 · exact mul_lt_mul_of_pos_right (Nat.cast_lt.mpr hjk) (by norm_num)
108