module module high

`IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum`

The module defines the DFT mode index and associated harmonic spectrum objects for cross-domain use in Recognition Science. Researchers modeling discrete spectra on the eight-tick structure would reference these definitions to index modes and bound carrier frequencies. The module consists of type definitions, count lemmas, and elementary inequalities with no complex proofs.

claimThe DFT mode index $k$ ranges over a finite set of size $dftMode_count$, with harmonic frequency function $f(k)$ built from base carrier frequency $f_c$ satisfying $8 < f_c < 8.1$.

background

The module sits in the cross-domain section and imports the RS time quantum from Constants, where the fundamental tick satisfies τ₀ = 1. It introduces the DFT mode index as the discrete label for harmonic components, together with the count of modes, the explicit harmonic frequency map, and the carrier frequency with its positivity and bounding lemmas. These objects align with the eight-tick octave period in the forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the spectral index and frequency definitions that enable cross-domain harmonic analysis, feeding the eight-tick octave structure from the forcing chain T7. It prepares tools for later application of the Recognition Composition Law to discrete spectra, though no downstream theorems are recorded yet.

scope and limits

Does not derive DFT modes from the J-cost or phi-ladder.
Does not prove orthogonality or completeness of the harmonic basis.
Does not relate carrier frequency to physical constants such as alpha.
Does not compute explicit numerical values for individual harmonics.

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