Gravity Gravitational Lensing Deflection Positive

The positive deflection theorem

Gravitational lensing is the bending of light by mass, a prediction of general relativity confirmed by Arthur Eddington's 1919 solar eclipse expedition. When a photon passes a mass M at a closest approach distance b, its path curves by an angle θ = 4GM/(c²b), where G is the gravitational constant and c is the speed of light. The formula, derived from the null geodesic equation in the Schwarzschild metric, gives about 1.75 arcseconds for light grazing the Sun's limb. A key structural fact follows immediately: for any positive mass and any positive impact parameter, the deflection angle is strictly greater than zero.

The deflection angle being positive means light always bends toward the mass, never away from it, and never passes through undeflected. This is not a numerical estimate but a theorem in the framework's machine-checked library of formal theorems. The declaration deflection_positive states that if the mass M is positive and the impact parameter b is positive, then the general-relativistic deflection angle is positive. The proof unfolds the definition of the deflection angle and applies a positivity tactic; it is a direct algebraic consequence of the formula, not an empirical claim.

In Recognition Science, the same result appears as part of a broader derivation of gravitational lensing from the framework's action principle. The framework models the deflection angle using the Schwarzschild metric, the same spacetime geometry general relativity uses for a spherical non-rotating mass. The theorem gr_is_twice_newton in the same library shows the general-relativistic deflection is exactly twice the Newtonian value, because both temporal and spatial metric components contribute equally. The positive-deflection result is the simplest of these: it guarantees the sign of the effect under the stated conditions.

The theorem also supports a monotonicity statement: a photon passing closer to the mass (smaller b) bends more than one passing farther away, since the deflection scales as 1/b. The positivity result is the foundation for that comparison. It confirms the direction of the effect for all positive masses and distances, which is what makes gravitational lensing a usable tool for mapping dark matter and measuring galaxy masses.

/-- 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

/-- **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

/-- 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 prove that light bends in any theory other than general relativity. The theorem does not establish the numerical value of the deflection for any specific astrophysical object. The theorem does not address the ILG weak lensing correction, which is a separate definition in the library.

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: