spacing_pos

formal source

 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]⟩
 177
 178/-- f(2) = 7φ + 3 ∈ (14.326, 14.333): matches measured 14.3 Hz within 0.04 Hz. -/
 179theorem harmonic2_bounds : 14.326 < schumannRS 2 ∧ schumannRS 2 < 14.333 := by
 180  rw [harmonic2_eq]
 181  exact ⟨by nlinarith [phi_gt_1618], by nlinarith [phi_lt_1619]⟩