harmonic_strict_mono
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.