Gravity Gravitational Lensing Deflection Angle Formula

The deflection formula

Gravitational lensing is the bending of light by mass, a consequence of general relativity where gravity curves spacetime and light follows that curvature. For a photon passing a mass M at a closest approach distance b, the total deflection angle is θ = 4GM/(c²b), where G is the gravitational constant and c is the speed of light. This is the standard result first computed by Einstein in 1915 and confirmed by Eddington's 1919 eclipse expedition, which measured the Sun's deflection at about 1.75 arcseconds. The formula is the foundation of modern lensing applications, from galaxy-scale arcs to exoplanet microlensing surveys.

The formula's most striking feature is the factor of 2. A simple Newtonian calculation, treating light as a particle moving at speed c, gives θ_Newton = 2GM/(c²b), exactly half the relativistic value. The extra factor arises because in general relativity both the temporal and spatial components of the metric contribute equally to the bending. This doubling was the first quantitative triumph of general relativity over Newtonian gravity, and it remains a standard test of the theory.

In Recognition Science, the framework's machine-checked library of formal theorems derives the same deflection formula. The library defines the Schwarzschild radius r_s = 2GM/c² and the deflection angle as θ = 2r_s/b in natural units, then proves a theorem named deflection_angle_formula that this equals the standard expression. The proof is a short algebraic identity: it unfolds the definition of deflection_GR and applies the ring tactic. The library also proves that the relativistic deflection is exactly twice the Newtonian value, that the angle is positive for positive mass and impact parameter, and that it decreases as the impact parameter increases, meaning stronger lensing occurs closer to the mass.

The framework's contribution here is not a new prediction but a formal verification. It takes the standard general relativity result, expresses it in the framework's own definitions, and confirms the algebraic relationships hold. The library also formalizes the Einstein radius for aligned source-lens-observer configurations and the Shapiro time delay, both positive under the stated conditions. These are structural facts about the standard theory, not empirical claims about the universe.

What the declaration does not claim is the physical derivation from first principles. The theorem assumes the Schwarzschild metric and the null geodesic equation as given; it does not derive general relativity from the framework's recognition cost function. The framework's information-ledger gravity model does propose a scale-dependent correction to lensing convergence, but that correction is a separate definition, not part of the deflection angle theorem. The deflection formula itself is a restatement of classical physics, verified for consistency, not a new physical law.

/-- **DEFLECTION ANGLE THEOREM**:
    For a photon passing mass M at impact parameter b:
    θ = 4GM/(c²b) (in SI), or equivalently θ = 2r_s/b (natural units).

    Derivation: null geodesic u'' + u = (3/2)r_s u² in Schwarzschild.
    Zeroth order: u₀ = sinφ/b.
    First order correction integrates to total bending 2r_s/b. -/
theorem deflection_angle_formula (M b : ℝ) (hM : 0 < M) (hb : 0 < b) :
    deflection_GR M b = 2 * schwarzschild_radius M / b := by
  unfold deflection_GR
  ring

/-- **KEY THEOREM**: GR deflection is exactly twice the Newtonian value.
    The factor of 2 arises because both temporal AND spatial metric
    components contribute equally to photon deflection. -/
theorem gr_is_twice_newton (M b : ℝ) (hb : b ≠ 0) :
    deflection_GR M b = 2 * deflection_newtonian M b := by
  unfold deflection_GR deflection_newtonian
  ring

/-- The deflection angle is positive for positive mass and impact parameter. -/
theorem deflection_positive (M b : ℝ) (hM : 0 < M) (hb : 0 < b) :
    0 < deflection_GR M b := by
  unfold deflection_GR schwarzschild_radius
  positivity

/-- Deflection angle scales as 1/b (stronger lensing at smaller impact). -/
theorem deflection_inverse_b (M b₁ b₂ : ℝ) (hM : 0 < M) (hb₁ : 0 < b₁) (hb₂ : 0 < b₂)
    (hb₁b₂ : b₁ < b₂) :
    deflection_GR M b₂ < deflection_GR M b₁ := by
  unfold deflection_GR schwarzschild_radius
  have hpos : (0 : ℝ) < 2 * (2 * M) := by linarith
  gcongr

What this page does not claim

The theorem does not derive general relativity from the framework's recognition cost function. The deflection formula is not a new prediction; it restates a standard general relativity result. The ILG convergence correction is a separate definition, not part of the deflection angle theorem.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/GravitationalLensing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: