`alpha_value`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.LambShift
domain: QFT
line: 51 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.LambShift on GitHub at line 51.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  48def alpha_approx : ℚ := 1/137
  49
  50/-- **THEOREM**: α ≈ 1/137 (the famous value). -/
  51theorem alpha_value : alpha_approx = 1/137 := rfl
  52
  53/-- The Lamb shift as a fraction of the 2S binding energy.
  54    E_2S ≈ -3.4 eV, Lamb shift ≈ 4.4 μeV. -/
  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

papers checked against this theorem

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