def definition def or abbrev

`harmonicFrequency`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  34noncomputable def harmonicFrequency (k : DFTMode) : ℝ :=

Definition body.

  35  (k.val : ℝ) * 5 * phi / 8
  36
  37/-- Carrier frequency: 5φ ≈ 8.09 Hz (theta band). -/

From the project-wide theorem graph. These declarations reference this one in their body.

DFTHarmonicSpectrumCert in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
harmonics_factored in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
harmonics_nonneg in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
harmonic_strict_mono in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
mode_seven in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
mode_seven_lt_9 in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
mode_seven_lt_carrier in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
mode_zero in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use

Lean names referenced from this declaration's body.

DFTMode in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
DFTMode in IndisputableMonolith.CrossDomain.TwoCubeUniversality decl_use
band in IndisputableMonolith.Foundation.PreLogicalCost decl_use
theta in IndisputableMonolith.NumberTheory.RiemannHypothesis.BRFPlumbing decl_use