spacing_eq

formal source

 143  rw [harmonic1_eq, ← three_phi_sq_eq_phi4_plus_1, phi_sq_eq]; ring
 144
 145/-- Consecutive Schumann harmonics are spaced by exactly 4φ = (D+1)·φ. -/
 146theorem spacing_eq (n : ℕ) :
 147    schumannRS (n + 1) - schumannRS n = 4 * phi := by
 148  simp only [schumannRS, Nat.cast_add, Nat.cast_one]; ring
 149
 150/-- The spacing 4φ is positive. -/
 151theorem spacing_pos : 0 < 4 * phi :=
 152  mul_pos (by norm_num : (0 : ℝ) < 4) phi_pos
 153
 154/-- The Schumann harmonics increase strictly. -/
 155theorem schumannRS_strictMono : ∀ m n : ℕ, m < n → schumannRS m < schumannRS n := by
 156  intro m n hmn
 157  have h : schumannRS n - schumannRS m = 4 * phi * (n - m : ℝ) := by
 158    simp only [schumannRS]; ring
 159  have hpos : 0 < 4 * phi * (n - m : ℝ) := by
 160    apply mul_pos spacing_pos
 161    exact sub_pos.mpr (Nat.cast_lt.mpr hmn)
 162  linarith
 163
 164/-! ## Part V: Bounds Matching Measured Values
 165
 166Each RS-predicted harmonic is proved to match its measured Schumann
 167resonance within a tight tolerance. -/
 168
 169/-- f(1) = 3φ + 3 ∈ (7.854, 7.857): matches measured 7.83 Hz within 0.03 Hz. -/
 170theorem harmonic1_bounds : 7.854 < schumannRS 1 ∧ schumannRS 1 < 7.857 := by
 171  rw [harmonic1_eq]
 172  exact ⟨by nlinarith [phi_gt_1618], by nlinarith [phi_lt_1619]⟩
 173
 174theorem harmonic1_matches : |schumannRS 1 - 7.83| < 0.03 := by
 175  rw [harmonic1_eq, abs_lt]
 176  exact ⟨by nlinarith [phi_gt_1618], by nlinarith [phi_lt_1619]⟩