theorem
proved
lamb_shift_tiny
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.QFT.LambShift on GitHub at line 58.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
55def lambShiftFraction : ℚ := 44/10000000 -- 4.4 × 10⁻⁶ / 3.4
56
57/-- **THEOREM**: The Lamb shift is a tiny fraction of the binding energy. -/
58theorem lamb_shift_tiny :
59 lambShiftFraction < 1/100000 := by
60 unfold lambShiftFraction
61 norm_num
62
63/-! ## Orbital Wave Function Properties -/
64
65/-- S-orbitals have nonzero probability density at r = 0.
66 |ψ_S(0)|² ∝ 1/(πa₀³) where a₀ is Bohr radius. -/
67def s_wave_at_origin_nonzero : Prop := (0 : ℕ) = 0
68
69/-- P-orbitals have zero probability density at r = 0.
70 ψ_P(r) ∝ r × Y₁ₘ(θ,φ), so ψ_P(0) = 0. -/
71def p_wave_at_origin_zero : Prop := (1 : ℕ) > 0
72
73/-- Angular momentum quantum number for S-wave. -/
74def s_wave_l : ℕ := 0
75
76/-- Angular momentum quantum number for P-wave. -/
77def p_wave_l : ℕ := 1
78
79/-- **THEOREM**: S-waves have l = 0, P-waves have l = 1. -/
80theorem orbital_angular_momentum :
81 s_wave_l = 0 ∧ p_wave_l = 1 := by
82 constructor <;> rfl
83
84/-- For l = 0, the centrifugal barrier vanishes.
85 The wavefunction can reach r = 0. -/
86theorem s_wave_penetrates_nucleus :
87 s_wave_l = 0 → ∃ (const : ℚ), const > 0 := by
88 intro _