phi_lt_1619

formal source

  76    exact Real.sqrt_lt_sqrt (by norm_num) h
  77  linarith
  78
  79private lemma phi_lt_1619 : phi < (1.619 : ℝ) := by
  80  simp only [phi]
  81  have h5 : Real.sqrt 5 < (2.238 : ℝ) := by
  82    have h : (5 : ℝ) < (2.238 : ℝ) ^ 2 := by norm_num
  83    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.238)]
  84    exact Real.sqrt_lt_sqrt (by norm_num) h
  85  linarith
  86
  87/-! ## Part II: The Schumann Formula
  88
  89**Definition**: f(n) = (4n − 1)·φ + 3
  90
  91This is the RS prediction for the n-th Schumann harmonic (n ≥ 1).
  92Uses only D = 3 (T8) and φ (T6). Zero free parameters. -/
  93
  94/-- RS-predicted n-th Schumann harmonic frequency.
  95    f(n) = (4n − 1)·φ + 3, valid for n ≥ 1. -/
  96def schumannRS (n : ℕ) : ℝ := (4 * (n : ℝ) - 1) * phi + 3
  97
  98/-- Measured Schumann resonance harmonics (Hz). -/
  99def schumannMeasured : Fin 5 → ℝ
 100  | ⟨0, _⟩ => 7.83
 101  | ⟨1, _⟩ => 14.3
 102  | ⟨2, _⟩ => 20.8
 103  | ⟨3, _⟩ => 27.3
 104  | ⟨4, _⟩ => 33.8
 105
 106/-! ## Part III: Coefficient Reduction
 107
 108Reduce schumannRS at each harmonic number to a clean φ-expression. -/
 109