DFTHarmonicSpectrumCert
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not derive the value 5φ from the J-cost functional equation.
- Does not establish uniqueness of the comb among all possible 8-mode spectra.
- Does not address physical units or coupling to other RS quantities.
- Does not prove stability under perturbations of phi.
formal statement (Lean)
109structure DFTHarmonicSpectrumCert where
110 modes_eight : Fintype.card DFTMode = 8
111 carrier_in_theta_band : 8 < carrierFreq ∧ carrierFreq < 8.1
112 all_modes_nonneg : ∀ k : DFTMode, 0 ≤ harmonicFrequency k
113 mode_zero_dc : harmonicFrequency ⟨0, by decide⟩ = 0
114 mode_seven_under_9 : harmonicFrequency ⟨7, by decide⟩ < 9
115 comb_monotone : ∀ j k : DFTMode, j.val < k.val →
116 harmonicFrequency j < harmonicFrequency k
117