Gravity Gravitational Lensing

Gravitational lensing

Gravitational lensing is the bending of light paths by mass, a consequence of gravity acting on the geometry of spacetime. In Recognition Science (RS), this effect is not an independent phenomenon but a derived consequence of the framework's action principle applied to the Schwarzschild metric. The module establishes the core formulas that describe how light is deflected, how a ring image forms under perfect alignment, and how light is delayed in time near a massive body.

The central result is the deflection angle formula, which states that for a photon passing a mass M at impact parameter b, the deflection angle is θ = 4GM/(c²b), or equivalently 2r_s/b in natural units where G = c = 1. This is derived from the null geodesic equation in the Schwarzschild metric. A key theorem proves that this general relativistic deflection is exactly twice the Newtonian value, a factor of 2 that arises because both temporal and spatial metric components contribute equally to photon deflection. The deflection angle is positive for positive mass and impact parameter, and it scales inversely with the impact parameter, meaning stronger lensing occurs at smaller distances.

The module also derives the Einstein radius, the angular radius of the ring image formed when source, lens, and observer are perfectly aligned. Its square is given by θ_E² = (2 r_s) × D_LS / (D_L × D_S), and this quantity is positive for positive distances. In addition, the Shapiro time delay is derived: a photon passing near a massive body is delayed by Δt = r_s × ln(4 r₁ r₂ / b²), which is positive when the photon passes close enough to the mass. For the solar limb, the module computes a deflection of approximately 1.75 arcseconds, a positive value.

Finally, the module introduces a scale-dependent correction to the standard gravitational lensing convergence, predicted by the Information Ledger Gravity (ILG) extension of RS. The convergence κ_RS(ℓ) equals κ_GR(ℓ) × (1 + α_t × (ℓ/ℓ₀)^(−β)), where α_t = (1 − φ⁻¹)/2 and β ≈ 0.0557. A theorem proves that this correction enhances the convergence, making it strictly larger than the standard GR value when α_t is positive.

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

/-- The Einstein radius is real and positive for positive distances. -/
theorem einstein_radius_positive (M DL DS DLS : ℝ)
    (hM : 0 < M) (hDL : 0 < DL) (hDS : 0 < DS) (hDLS : 0 < DLS) :
    0 < einstein_angle_sq M DL DS DLS := by
  unfold einstein_angle_sq schwarzschild_radius
  positivity

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

/-- The ILG correction is positive for α_t > 0. -/
theorem ilg_correction_enhances (κ_GR α_t ℓ ℓ₀ β : ℝ)
    (hκ : 0 < κ_GR) (hα : 0 < α_t) (hℓ : 0 < ℓ) (hℓ₀ : 0 < ℓ₀) :
    κ_GR < ilg_convergence_correction κ_GR α_t ℓ ℓ₀ β := by
  unfold ilg_convergence_correction
  have hterm : 0 < α_t * (ℓ / ℓ₀) ^ (-β) := by
    apply mul_pos hα
    apply rpow_pos_of_pos
    positivity
  nlinarith

What this page does not claim

The module does not derive the Schwarzschild metric itself from RS principles. The ILG correction is a definitional model, not a established consequence of the core forcing chain. The numerical value of the solar deflection is not a measured quantity in this module.

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: