dft8Fundamental_pos
plain-language theorem explainer
The positivity of the DFT-8 fundamental frequency 5φ/8 is established directly from its definition. Researchers constructing RS Fourier certificates would cite it to confirm the base frequency of the 8-tick harmonic comb lies in the positive reals. The proof is a term-mode reduction that unfolds the definition and applies standard positivity lemmas for multiplication and division.
Claim. $0 < 5φ/8$, where φ is the golden ratio.
background
The module Fourier Analysis from RS treats the DFT-8 mode structure as the 8-tick harmonic comb arising from the recognition period 2^D with D=3. The fundamental frequency is introduced by the sibling definition dft8Fundamental : ℝ := 5 * phi / 8, which supplies the explicit value 5φ/8 Hz. This local setting links five canonical Fourier operations to configDim D=5 and anchors the positivity result needed for downstream certificates.
proof idea
The term proof unfolds dft8Fundamental, then applies div_pos to reduce positivity of the quotient to positivity of the numerator. It invokes mul_pos on the constant factor 5 (via norm_num) and phi_pos, followed by norm_num on the denominator 8.
why it matters
The result supplies the fundamental_pos field required by the downstream fourierCert definition, which bundles five operations, the dft8_eq_8 mode count, and this positivity into a single certificate. It directly instantiates the eight-tick octave (T7) and D=3 from the forcing chain, ensuring the harmonic comb begins at a positive frequency inside the RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.