lensing_param

formal source

  29noncomputable def schwarzschild_radius (M : ℝ) : ℝ := 2 * M
  30
  31/-- Light deflection: small parameter ε = r_s / b ≪ 1 -/
  32noncomputable def lensing_param (M b : ℝ) : ℝ := schwarzschild_radius M / b
  33
  34/-! ## Newtonian vs. GR Deflection -/
  35
  36/-- **Newtonian deflection** (treating photon as particle):
  37    θ_Newton = 2GM/(c²b) = r_s / b -/
  38noncomputable def deflection_newtonian (M b : ℝ) : ℝ := schwarzschild_radius M / b
  39
  40/-- **GR deflection** (from null geodesic in Schwarzschild metric):
  41    θ_GR = 4GM/(c²b) = 2 × r_s / b = 2 × θ_Newton -/
  42noncomputable def deflection_GR (M b : ℝ) : ℝ := 2 * schwarzschild_radius M / b
  43
  44/-- **KEY THEOREM**: GR deflection is exactly twice the Newtonian value.
  45    The factor of 2 arises because both temporal AND spatial metric
  46    components contribute equally to photon deflection. -/
  47theorem gr_is_twice_newton (M b : ℝ) (hb : b ≠ 0) :
  48    deflection_GR M b = 2 * deflection_newtonian M b := by
  49  unfold deflection_GR deflection_newtonian
  50  ring
  51
  52/-- **DEFLECTION ANGLE THEOREM**:
  53    For a photon passing mass M at impact parameter b:
  54    θ = 4GM/(c²b) (in SI), or equivalently θ = 2r_s/b (natural units).
  55
  56    Derivation: null geodesic u'' + u = (3/2)r_s u² in Schwarzschild.
  57    Zeroth order: u₀ = sinφ/b.
  58    First order correction integrates to total bending 2r_s/b. -/
  59theorem deflection_angle_formula (M b : ℝ) (hM : 0 < M) (hb : 0 < b) :
  60    deflection_GR M b = 2 * schwarzschild_radius M / b := by
  61  unfold deflection_GR
  62  ring