D

formal source

 127The formula's structure is forced by D = 3 and φ. -/
 128
 129/-- The RS-forced spatial dimension (from T8). -/
 130abbrev D : ℕ := 3
 131
 132/-- The Schumann fundamental equals D·φ² = 3(φ + 1). -/
 133theorem fundamental_eq_D_phi_sq : schumannRS 1 = D * phi ^ 2 := by
 134  rw [harmonic1_eq, phi_sq_eq]; push_cast; ring
 135
 136/-- Identity: 3φ² = φ⁴ + 1.
 137    The Schumann fundamental is one above the fourth power of phi. -/
 138theorem three_phi_sq_eq_phi4_plus_1 : 3 * phi ^ 2 = phi ^ 4 + 1 := by
 139  rw [phi_sq_eq, phi_fourth_eq]; ring
 140
 141/-- The Schumann fundamental equals φ⁴ + 1. -/
 142theorem fundamental_eq_phi4_plus_1 : schumannRS 1 = phi ^ 4 + 1 := by
 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