Gravity Gravitational Lensing Deflection Inverse B

The inverse-b law

Gravitational lensing is the bending of light by mass, a prediction of general relativity confirmed by Arthur Eddington's 1919 solar eclipse expedition. The deflection angle θ for a photon passing a mass M at a closest approach distance, the impact parameter b, is θ = 4GM/(c²b), where G is Newton's constant and c is the speed of light. The formula has a simple consequence: halve the impact parameter and the deflection doubles. The theorem deflection_inverse_b in the framework's machine-checked library of formal theorems captures exactly this monotonic relationship, proving that for any two positive impact parameters b₁ < b₂, the deflection at b₂ is strictly less than the deflection at b₁.

The theorem is a formal statement about the framework's own definition of the general-relativistic deflection angle, deflection_GR, which the framework models as twice the Schwarzschild radius divided by the impact parameter. The proof is a direct algebraic manipulation: it unfolds the definition and applies a positivity argument. It does not derive the deflection formula from the null geodesic equation; that work lives in a separate theorem, deflection_angle_formula, which the pack lists without a machine-checked proof. The inverse-b theorem takes the formula as given and establishes the ordering property that follows from it.

In plain language, the theorem says that the closer a ray of light grazes a massive object, the more it bends. This is the qualitative content of the 1/b scaling that makes strong lensing visible only for nearly aligned sources and lenses. The theorem's hypotheses are explicit: the mass M and both impact parameters must be positive, and the comparison b₁ < b₂ is strict. Under those conditions, the inequality deflection_GR M b₂ < deflection_GR M b₁ holds as a proved statement.

What the theorem does not claim is just as precise. It does not assert that the deflection formula itself is correct physics; that is a separate claim about the framework's derivation from the Schwarzschild metric. It does not say anything about the Einstein radius, the Shapiro time delay, or the ILG weak-lensing correction, all of which appear elsewhere in the same source file. It does not compare the framework's deflection to any measured value, and it does not state that the inverse-b scaling holds for all possible impact parameters, only for the positive ones in its hypotheses. The theorem is a narrow, exact statement about a monotonic relationship, and its value lies in being one more link in a chain of formally verified results.

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

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

What this page does not claim

The inverse-b theorem does not prove the deflection formula itself. The theorem does not compare the deflection to any measured astronomical value. The theorem says nothing about the Einstein radius or the Shapiro time delay.

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: