module module moderate

`IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum`

The CrossDomain.DFTHarmonicSpectrum module defines the DFT mode index together with harmonic frequencies, carrier frequency bounds near 8, and mode-specific facts. Researchers extending Recognition Science into spectral or frequency-domain applications would cite these definitions when building discrete harmonic models. The module consists of definitions and elementary properties with no complex proofs.

claimDFT mode index $m$ with harmonic frequency $f_m$, carrier frequency $f_c$ satisfying $f_c > 8$ and $f_c < 8.1$, and derived facts on non-negative harmonics and boundary modes.

background

The module imports Constants, whose doc-comment states the fundamental RS time quantum (RS-native) $ au_0 = 1$ tick. It introduces DFTMode as the DFT mode index and supplies supporting objects including harmonicFrequency, carrierFreq, and mode predicates at zero and seven. The local setting is the cross-domain section, where discrete frequency structures are developed from the imported time quantum.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies DFT harmonic spectrum definitions that support cross-domain extensions of Recognition Science. It aligns with framework landmarks such as the eight-tick octave by providing discrete mode indices and carrier constraints near the integer 8. No immediate parent theorems are listed in the used-by edges.

scope and limits

Does not define the full DFT summation operator.
Does not prove convergence or completeness of the harmonic basis.
Does not connect modes to physical constants beyond the imported time quantum.
Does not treat continuous Fourier transforms.

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