pith. machine review for the scientific record. sign in
theorem proved tactic proof

lambda_PBM_approx

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 165theorem lambda_PBM_approx : abs (lambda_PBM - 766e-9) < 5e-9 := by

proof body

Tactic-mode proof.

 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,
 196giving Σ s(k) = 0 — exact 8-window neutrality. -/
 197
 198/-- The RS-coherent 8-beat modulation pattern values.
 199    Derived from s(k) = cos(kπ/4) + (1/φ)·cos(kπ/2). -/

depends on (26)

Lean names referenced from this declaration's body.