Gravity Gravitational Lensing Einstein Radius Positive

The Einstein radius

When a massive object, like a galaxy or black hole, sits almost exactly between Earth and a more distant light source, the object's gravity bends the light around it. If the alignment is perfect, the bent light reaches us from all sides, and we see a ring of light instead of a point. This is the Einstein ring, named for the effect Albert Einstein predicted in 1936. The ring's angular radius, the Einstein radius, is the standard measure of how strong this gravitational lensing is.

The classical formula for the Einstein radius (in radians) is θ_E² = (4GM/c²) × D_LS / (D_L × D_S). Here G is the gravitational constant, M is the lens's mass, c is the speed of light, D_L is the distance from observer to lens, D_S is the distance from observer to source, and D_LS is the distance from lens to source. The formula shows two things at once: more mass makes a bigger ring, and the ring's size depends on the geometric arrangement of observer, lens, and source. The same formula appears in the framework's machine-checked library as the definition einstein_angle_sq, a discrete record of the squared angular radius.

The declaration einstein_radius_positive proves a simple but essential fact: for any positive lens mass and any positive distances, the squared Einstein radius is positive. This is the theorem einstein_radius_positive in the framework's library. It means the Einstein ring always has a real, nonzero angular size whenever the geometry is physically sensible. The proof is direct: it unfolds the definition and applies the positivity rule to each positive factor. This is not a physical measurement; it is a formal guarantee about the mathematical model.

In Recognition Science, this theorem is part of a larger derivation. The framework derives the deflection angle, Einstein radius, and Shapiro time delay from its action principle and the Schwarzschild metric. The key structural result is that general relativity's deflection is exactly twice the Newtonian value, because both temporal and spatial metric components contribute equally. The positive Einstein radius is a small but necessary piece of that chain: it confirms the model produces a ring, not a negative or imaginary radius, for any positive configuration.

What the theorem does not claim is just as important. It does not say that real Einstein rings exist, nor does it predict their observed sizes. It only guarantees positivity within the mathematical model, given the stated assumptions. The formula itself is classical general relativity, not a new Recognition Science prediction. The framework's contribution is the formal derivation and the machine-checked proof, not a new physical effect.

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

/-- **EINSTEIN RADIUS**: When source, lens, and observer are aligned,
    the image forms a ring of angular radius θ_E.

    θ_E² = (4GM/c²) × D_LS / (D_L × D_S)

    In natural units (with distances in units where G=c=1):
    θ_E² = (2 r_s) × D_LS / (D_L × D_S) -/
noncomputable def einstein_angle_sq (M DL DS DLS : ℝ) : ℝ :=
  schwarzschild_radius M * DLS / (DL * DS)

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

What this page does not claim

The theorem does not assert that any real Einstein ring has been observed. The theorem does not predict the numerical size of any specific Einstein ring. The theorem does not establish that the Einstein radius formula is new physics beyond general relativity.

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: