module module moderate

`IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum`

The CrossDomain.DFTHarmonicSpectrum module defines the DFT mode index together with harmonic and carrier frequencies. Researchers extending the eight-tick octave to spectral models would cite these objects. The module supplies only definitions and elementary bounds with no proof tactics required.

claimThe DFT mode index $m$ satisfies $0leq m<8$, with carrier frequency $c$ obeying $8<c<8.1$ and harmonic frequencies nonnegative and factored.

background

The module sits in the cross-domain layer and imports Constants, whose sole content is the RS time quantum τ₀ = 1 tick. It introduces the DFT mode index along with carrier frequency, harmonic frequency, and the eight-mode structure implied by the siblings mode_zero and mode_seven. The local setting therefore links the discrete Fourier transform to the period-2³ octave already fixed by the forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the DFT mode index required for any cross-domain spectral extension of the Recognition Science framework. It directly supports the eight-tick octave (T7) by furnishing the mode set {0,…,7} and the carrier bounds around 8. No downstream theorems are recorded, yet the definitions close the interface between harmonic analysis and the phi-ladder.

scope and limits

Does not prove any theorem about spectra.
Does not connect to the mass formula or phi-ladder rungs.
Does not reference the recognition composition law.
Does not address the alpha band or Berry threshold.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (16)

abbrev DFTMode L29
theorem dftMode_count L31
def harmonicFrequency L34
def carrierFreq L38
theorem carrierFreq_pos L40
theorem carrier_gt_8 L45
theorem carrier_lt_8point1 L51
theorem harmonics_nonneg L57
theorem harmonics_factored L68
theorem mode_zero L74
theorem mode_seven L79
theorem mode_seven_lt_carrier L84
theorem mode_seven_lt_9 L95
theorem harmonic_strict_mono L102
structure DFTHarmonicSpectrumCert L109
def dftHarmonicSpectrumCert L118