dftHarmonicSpectrumCert
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not derive the carrier value 5φ from the T0–T8 forcing chain.
- Does not establish numerical equivalence to measured brain-wave frequencies.
- Does not incorporate measurement uncertainty or quantization effects.
- Does not prove uniqueness of the comb among possible RS spectra.
formal statement (Lean)
118noncomputable def dftHarmonicSpectrumCert : DFTHarmonicSpectrumCert where
119 modes_eight := dftMode_count
proof body
Definition body.
120 carrier_in_theta_band := ⟨carrier_gt_8, carrier_lt_8point1⟩
121 all_modes_nonneg := harmonics_nonneg
122 mode_zero_dc := mode_zero
123 mode_seven_under_9 := mode_seven_lt_9
124 comb_monotone := harmonic_strict_mono
125
126end IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum