dftHarmonicSpectrumCert
plain-language theorem explainer
The declaration supplies a certified eight-mode DFT harmonic spectrum whose carrier lies in the theta band at 5φ Hz. Cross-domain modelers working on RS brain-rhythm or sound-therapy combs would invoke this certificate to guarantee the full set of frequency properties. The definition is assembled by direct field assignment from eight sibling theorems that separately establish mode cardinality, carrier bounds, non-negativity, zero mode, upper bound on mode seven, and strict monotonicity.
Claim. Let DFTMode be the finite type with eight elements and let the harmonic frequencies be given by ν_k = k · 5φ / 8 for k = 0,…,7. Then the spectrum satisfies |DFTMode| = 8, 8 < 5φ < 8.1, ν_k ≥ 0 for every k, ν_0 = 0, ν_7 < 9, and ν_j < ν_k whenever j.val < k.val.
background
Module CrossDomain.DFTHarmonicSpectrum defines the DFT-8 spectrum for the Recognition Science frequency comb ν_k = (k · 5φ / 8) Hz with carrier 5φ ≈ 8.09 Hz inside the theta band. The structure DFTHarmonicSpectrumCert packages six properties: exact cardinality eight, carrier bounds, non-negativity of all modes, zero at DC, mode seven below 9 Hz, and strict increase with index.
proof idea
One-line wrapper that constructs the structure by field assignment: modes_eight receives dftMode_count, carrier_in_theta_band receives the pair of theorems carrier_gt_8 and carrier_lt_8point1, all_modes_nonneg receives harmonics_nonneg, mode_zero_dc receives mode_zero, mode_seven_under_9 receives mode_seven_lt_9, and comb_monotone receives harmonic_strict_mono.
why it matters
The definition realizes the eight-tick octave (T7) as the canonical RS frequency comb cited in C24 for sound-therapy and brain-rhythm applications. It supplies the single certificate that downstream cross-domain statements can cite without re-proving the individual bounds or monotonicity. No used_by edges are recorded yet, leaving open the question of which larger theorems will consume the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.