lambda_PBM_approx

formal source

 162      _ < (780e-9 : ℝ) := by norm_num [planck_h, speed_of_light, eV_to_J]
 163
 164/-- Tighter approximation: λ_PBM ≈ 766 nm (within ±5 nm). -/
 165theorem lambda_PBM_approx : abs (lambda_PBM - 766e-9) < 5e-9 := by
 166  unfold lambda_PBM
 167  have h_hc_pos : 0 < planck_h * speed_of_light :=
 168    mul_pos planck_h_pos speed_of_light_pos
 169  have ⟨h_lower, h_upper⟩ := div_bounds_of_E_PBM h_hc_pos
 170  have h_lo_ref :
 171      (761e-9 : ℝ) < planck_h * speed_of_light / (1.62 * eV_to_J) := by
 172    norm_num [planck_h, speed_of_light, eV_to_J]
 173  have h_hi_ref :
 174      planck_h * speed_of_light / (1.61 * eV_to_J) < (771e-9 : ℝ) := by
 175    norm_num [planck_h, speed_of_light, eV_to_J]
 176  have h_gt := lt_trans h_lo_ref h_lower
 177  have h_lt := lt_trans h_upper h_hi_ref
 178  exact abs_lt.mpr ⟨by linarith, by linarith⟩
 179
 180/-! ## Section 3: 8-Beat Modulation Pattern
 181
 182The RS-coherent modulation pattern is derived from a superposition of
 183DFT modes: s(k) = cos(kπ/4) + (1/φ)·cos(kπ/2).
 184
 185Using the identities 1/φ = φ - 1 and standard cosine values:
 186- s(0) = 1 + 1/φ = φ
 187- s(1) = √2/2
 188- s(2) = 0 - 1/φ = 1 - φ
 189- s(3) = -√2/2
 190- s(4) = -1 + 1/φ = φ - 2
 191- s(5) = -√2/2
 192- s(6) = 0 - 1/φ = 1 - φ
 193- s(7) = √2/2
 194
 195The φ terms and √2/2 terms each cancel pairwise,