harmonic2_eq

formal source

 110theorem harmonic1_eq : schumannRS 1 = 3 * phi + 3 := by
 111  unfold schumannRS; push_cast; ring
 112
 113theorem harmonic2_eq : schumannRS 2 = 7 * phi + 3 := by
 114  unfold schumannRS; push_cast; ring
 115
 116theorem harmonic3_eq : schumannRS 3 = 11 * phi + 3 := by
 117  unfold schumannRS; push_cast; ring
 118
 119theorem harmonic4_eq : schumannRS 4 = 15 * phi + 3 := by
 120  unfold schumannRS; push_cast; ring
 121
 122theorem harmonic5_eq : schumannRS 5 = 19 * phi + 3 := by
 123  unfold schumannRS; push_cast; ring
 124
 125/-! ## Part IV: Structural Identities
 126
 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