Gravity Gravitational Lensing Gr Is Twice Newton

The factor of two

When light passes a massive body, its path bends. In 1919 Arthur Eddington's eclipse expedition measured the bending of starlight around the Sun, confirming that the deflection angle is about 1.75 arcseconds, roughly twice the value a Newtonian calculation would give if light were treated as a stream of particles. This factor of two became a hallmark of general relativity, the theory Albert Einstein published in 1915. The standard result, for a photon passing a mass M with closest approach distance b, is θ = 4GM/(c²b) in SI units, where G is the gravitational constant and c is the speed of light.

The factor of two arises because in the Schwarzschild metric, the geometry of spacetime around a spherical mass, both the temporal and the spatial parts of the metric contribute equally to the bending of light. A Newtonian treatment only accounts for the temporal part, missing half the effect. The deflection is also inversely proportional to b, so light passing closer to the mass bends more sharply. For the Sun, with mass M_sun and radius R_sun, the formula gives the measured 1.75 arcseconds at the solar limb.

In Recognition Science, a framework that derives physical laws from a discrete record of events called a ledger, the same result is encoded in a machine-checked theorem. The declaration gr_is_twice_newton proves, from the definitions of the Newtonian and general-relativistic deflection angles, that the general-relativistic deflection is exactly twice the Newtonian value for any positive mass and nonzero impact parameter. The proof is a direct algebraic consequence of the two definitions, which differ only by a factor of two in the numerator. This is a theorem about the definitions, not a new physical measurement; it restates, in the framework's formal language, the classical general-relativistic result.

The framework's library also proves related properties: the deflection angle is positive for a positive mass, it decreases as the impact parameter increases, and the Shapiro time delay, the extra travel time for light passing near a mass, is positive when the photon passes close enough. These are all consistent with standard general relativity. The framework does not claim to have measured the deflection itself, nor does it derive the factor of two from its own axioms; it takes the Schwarzschild metric and the null geodesic equation as given inputs and proves the arithmetic that follows.

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

/-- Shapiro delay is positive when 4r₁r₂ > b² (photon close to mass). -/
theorem shapiro_delay_positive (M r₁ r₂ b : ℝ)
    (hM : 0 < M) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (hb : 0 < b)
    (h : b ^ 2 < 4 * r₁ * r₂) :
    0 < shapiro_delay M r₁ r₂ b := by
  unfold shapiro_delay schwarzschild_radius
  apply mul_pos
  · linarith
  · apply Real.log_pos
    rw [one_lt_div (by positivity)]
    linarith

What this page does not claim

The framework does not measure the solar deflection; the 1.75 arcsecond value is a classical measurement, not a framework result. The factor of two is not derived from the ledger axioms; the framework takes the Schwarzschild metric as a given input. The theorem applies only to the weak-field, small-angle deflection of light, not to strong lensing or other relativistic effects.

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: