 122def first_acoustic_peak_ell : ℝ := 220
 123
 124/-- Peak positions scale as ℓ_n ≈ n × 220. -/
 125noncomputable def acoustic_peak (n : ℕ) : ℝ := n * first_acoustic_peak_ell
 126
 127theorem acoustic_peaks_positive (n : ℕ) (hn : 0 < n) :
 128    0 < acoustic_peak n := by
 129  unfold acoustic_peak first_acoustic_peak_ell
 130  positivity
 131
 132/-- Second peak at ℓ₂ ≈ 540, third at ℓ₃ ≈ 810. -/
 133theorem acoustic_peak_positions :
 134    acoustic_peak 1 = 220 ∧ acoustic_peak 2 = 440 ∧ acoustic_peak 3 = 660 := by
 135  simp [acoustic_peak, first_acoustic_peak_ell]
 136  norm_num
 137
 138/-! ## CMB Temperature Scaling -/
 139
 140/-- CMB temperature scales inversely with cosmic scale factor a = 1/(1+z). -/
 141theorem cmb_temperature_scales_with_redshift (T₀ z : ℝ)
 142    (hT₀ : 0 < T₀) (hz : -1 < z) :
 143    cmb_temperature (T₀ * (1 + z)) z = T₀ := by
 144  unfold cmb_temperature
 145  have hne : 1 + z ≠ 0 := by linarith
 146  field_simp [hne]
 147
 148/-- At z = 0 (now): T = T₀. -/
 149theorem cmb_temperature_now (T₀ : ℝ) (hT₀ : 0 < T₀) :
 150    cmb_temperature T₀ 0 = T₀ := by
 151  unfold cmb_temperature
 152  simp
 153
 154end CMB
 155end Physics

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.