DFTHarmonicSpectrumCert
plain-language theorem explainer
The DFTHarmonicSpectrumCert structure records that the eight DFT modes carry frequencies forming a monotone comb with carrier 5φ in the open interval (8, 8.1) and all values nonnegative and below 9. Cross-domain modelers cite it when embedding the RS theta-band comb into larger simulations. The definition simply packages six independently verified properties of the frequency map.
Claim. Let DFTMode be the finite set of cardinality 8. The structure asserts that the carrier frequency satisfies $8 < 5φ < 8.1$, the harmonic frequencies $ν_k = k · 5φ / 8$ for $k = 0,…,7$ satisfy $ν_k ≥ 0$, $ν_0 = 0$, $ν_7 < 9$, and $j < k$ implies $ν_j < ν_k$.
background
The module establishes the DFT-8 harmonic spectrum as the canonical RS frequency comb with fundamental 5φ Hz. DFTMode is the type Fin 8 indexing the modes. The function harmonicFrequency maps each mode k to (k.val : ℝ) * 5 * phi / 8, while carrierFreq is defined as 5 * phi. This construction sits inside the cross-domain layer that links the eight-tick octave to physical frequency assignments. Upstream results supply the explicit formulas for carrierFreq and harmonicFrequency together with the cardinality fact that |DFTMode| = 8.
proof idea
The declaration is a structure definition that collects six field propositions. Each field is discharged by a sibling lemma: dftMode_count for the cardinality, carrier_gt_8 and carrier_lt_8point1 for the band condition, harmonics_nonneg for nonnegativity, mode_zero for the DC term, and mode_seven_lt_9 together with the monotonicity lemma for the ordering.
why it matters
This certificate closes the structural claim C24 for the DFT-8 spectrum inside the Recognition framework. It supplies the concrete frequency assignments that downstream constructions such as dftHarmonicSpectrumCert invoke when building cross-domain models. The eight modes align with the T7 eight-tick octave and the theta-band placement connects to the phi-ladder constants used throughout the mass and frequency formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.