IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# C24: DFT-8 Harmonic Spectrum — Wave 64 Cross-Domain
   6
   7Structural claim: the eight DFT modes carry physical content via the
   8fundamental frequency 5φ Hz (theta band). The full RS frequency comb is
   9
  10  ν_k = (k · 5φ / 8) Hz   for k = 0, 1, ..., 7
  11
  12This is the canonical RS sound-therapy and brain-rhythm frequency comb
  13(RS_PAT_026, RS_PAT_025).
  14
  15Key properties:
  16  • 8 modes (k = 0..7), one per Q₃ vertex
  17  • Carrier frequency 5φ ≈ 8.09 Hz (theta band)
  18  • All ν_k are non-negative
  19  • Highest mode ν_7 = 35φ/8 ≈ 7.08 Hz (still theta band)
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum
  25
  26open Constants
  27
  28/-- The DFT mode index. -/
  29abbrev DFTMode : Type := Fin 8
  30
  31theorem dftMode_count : Fintype.card DFTMode = 8 := by decide
  32
  33/-- The k-th harmonic frequency of the RS comb: ν_k = k · 5φ / 8 Hz. -/
  34noncomputable def harmonicFrequency (k : DFTMode) : ℝ :=
  35  (k.val : ℝ) * 5 * phi / 8
  36
  37/-- Carrier frequency: 5φ ≈ 8.09 Hz (theta band). -/
  38noncomputable def carrierFreq : ℝ := 5 * phi
  39
  40theorem carrierFreq_pos : 0 < carrierFreq := by
  41  unfold carrierFreq
  42  exact mul_pos (by norm_num) phi_pos
  43
  44/-- Theta-band lower bound: 5φ > 5 · 1.6 = 8. -/
  45theorem carrier_gt_8 : carrierFreq > 8 := by
  46  unfold carrierFreq
  47  have := phi_gt_onePointSixOne
  48  linarith
  49
  50/-- Theta-band upper bound: 5φ < 5 · 1.62 = 8.1. -/
  51theorem carrier_lt_8point1 : carrierFreq < 8.1 := by
  52  unfold carrierFreq
  53  have := phi_lt_onePointSixTwo
  54  linarith
  55
  56/-- All harmonics are non-negative. -/
  57theorem harmonics_nonneg (k : DFTMode) : 0 ≤ harmonicFrequency k := by
  58  unfold harmonicFrequency
  59  apply div_nonneg
  60  · apply mul_nonneg
  61    apply mul_nonneg
  62    · exact Nat.cast_nonneg _
  63    · norm_num
  64    · exact le_of_lt phi_pos
  65  · norm_num
  66
  67/-- The k-th harmonic is k · (carrier / 8). -/
  68theorem harmonics_factored (k : DFTMode) :
  69    harmonicFrequency k = (k.val : ℝ) * (carrierFreq / 8) := by
  70  unfold harmonicFrequency carrierFreq
  71  ring
  72
  73/-- Mode 0 has frequency 0 (DC). -/
  74theorem mode_zero : harmonicFrequency ⟨0, by decide⟩ = 0 := by
  75  unfold harmonicFrequency
  76  simp
  77
  78/-- Mode 7 = highest harmonic: 35φ/8. -/
  79theorem mode_seven : harmonicFrequency ⟨7, by decide⟩ = 35 * phi / 8 := by
  80  unfold harmonicFrequency
  81  push_cast; ring
  82
  83/-- Mode 7 < carrier (since 7/8 < 1). -/
  84theorem mode_seven_lt_carrier :
  85    harmonicFrequency ⟨7, by decide⟩ < carrierFreq := by
  86  rw [mode_seven]
  87  unfold carrierFreq
  88  -- 35φ/8 < 5φ iff 35/8 < 5, which is 4.375 < 5
  89  have hpos := phi_pos
  90  rw [div_lt_iff₀ (by norm_num : (8 : ℝ) > 0)]
  91  -- Goal: 35*phi < 5*phi*8 = 40*phi
  92  linarith [phi_pos]
  93
  94/-- The highest harmonic is bounded above by 9 Hz (still theta band). -/
  95theorem mode_seven_lt_9 : harmonicFrequency ⟨7, by decide⟩ < 9 := by
  96  rw [mode_seven]
  97  have := phi_lt_onePointSixTwo
  98  -- 35φ/8 < 35 · 1.62 / 8 = 56.7/8 = 7.0875 < 9
  99  linarith
 100
 101/-- Strict monotonicity of the comb. -/
 102theorem harmonic_strict_mono (j k : DFTMode) (hjk : j.val < k.val) :
 103    harmonicFrequency j < harmonicFrequency k := by
 104  unfold harmonicFrequency
 105  apply div_lt_div_of_pos_right _ (by norm_num : (8 : ℝ) > 0)
 106  apply mul_lt_mul_of_pos_right _ phi_pos
 107  · exact mul_lt_mul_of_pos_right (Nat.cast_lt.mpr hjk) (by norm_num)
 108
 109structure DFTHarmonicSpectrumCert where
 110  modes_eight : Fintype.card DFTMode = 8
 111  carrier_in_theta_band : 8 < carrierFreq ∧ carrierFreq < 8.1
 112  all_modes_nonneg : ∀ k : DFTMode, 0 ≤ harmonicFrequency k
 113  mode_zero_dc : harmonicFrequency ⟨0, by decide⟩ = 0
 114  mode_seven_under_9 : harmonicFrequency ⟨7, by decide⟩ < 9
 115  comb_monotone : ∀ j k : DFTMode, j.val < k.val →
 116    harmonicFrequency j < harmonicFrequency k
 117
 118noncomputable def dftHarmonicSpectrumCert : DFTHarmonicSpectrumCert where
 119  modes_eight := dftMode_count
 120  carrier_in_theta_band := ⟨carrier_gt_8, carrier_lt_8point1⟩
 121  all_modes_nonneg := harmonics_nonneg
 122  mode_zero_dc := mode_zero
 123  mode_seven_under_9 := mode_seven_lt_9
 124  comb_monotone := harmonic_strict_mono
 125
 126end IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum
 127