Gravity Gravitational Lensing Solar Deflection Positive

The positive deflection

Gravitational lensing is the bending of light by mass. When a ray of light passes a massive body, its path curves toward the body, so a distant observer sees the source shifted from its true position. For the Sun, the standard prediction of general relativity is that light grazing the solar limb is deflected by about 1.75 arcseconds. Arthur Eddington's expedition of 1919 measured a value close to this, and the result became one of the first dramatic confirmations of Einstein's theory.

The deflection angle depends on the mass M of the lens and the impact parameter b, the closest distance between the light ray and the lens center. In natural units where G = c = 1, the general-relativistic deflection is θ = 2r_s/b, where r_s = 2M is the Schwarzschild radius, the radius of a black hole of that mass. This is exactly twice the Newtonian prediction that treats light as a fast particle. The factor of 2 arises because both the temporal and spatial parts of the metric contribute equally to the bending.

In the Recognition Science framework, a machine-checked library of formal theorems, the same physics is derived from the framework's action principle. The library defines the solar deflection as the general-relativistic formula applied to the Sun's mass and radius, and proves the theorem solar_deflection_positive: this quantity is strictly greater than zero. The proof is a direct application of a more general theorem, deflection_positive, which states that for any positive mass and positive impact parameter, the deflection angle is positive. The solar case follows because the Sun's mass and radius are both positive numbers.

The theorem is a structural fact, not a new measurement. It says that the framework's mathematical model of lensing produces a positive deflection, meaning light bends toward the Sun rather than away from it or not at all. The numerical value, about 1.75 arcseconds, comes from plugging the Sun's mass and radius into the formula, not from the theorem itself. The theorem also does not establish that the framework's model is correct; that would require comparing its predictions against observations, which is a separate empirical check.

What the theorem does is close a logical gap. A model of lensing could in principle predict negative deflection, light bending away from mass, which would contradict observation. The library proves that the framework's model cannot do that: the deflection is always positive for physical parameters. This is a consistency result, a guarantee that the framework's lensing model behaves sensibly in the simplest case, before any comparison with experiment is attempted.

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

/-- 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 structural fact: solar deflection is positive. -/
theorem solar_deflection_positive : 0 < solar_deflection := by
  unfold solar_deflection
  apply deflection_positive <;> norm_num

What this page does not claim

The theorem does not measure the solar deflection; it only proves positivity in the framework's model. The theorem does not establish that the framework's lensing model is physically correct. The theorem does not derive the numerical value 1.75 arcseconds; that value comes from the definition of solar_deflection using the Sun's mass and radius.

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: