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.

THEOREM deflection_angle_formula · IndisputableMonolith/Gravity/GravitationalLensing.lean

THEOREM gr_is_twice_newton · IndisputableMonolith/Gravity/GravitationalLensing.lean

THEOREM deflection_positive · IndisputableMonolith/Gravity/GravitationalLensing.lean

THEOREM einstein_radius_positive · IndisputableMonolith/Gravity/GravitationalLensing.lean

THEOREM shapiro_delay_positive · IndisputableMonolith/Gravity/GravitationalLensing.lean

THEOREM ilg_correction_enhances · IndisputableMonolith/Gravity/GravitationalLensing.lean

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: