Cosmology Gravitational Lensing From Rs Deflection Angle

The deflection ladder

Gravitational lensing is the bending of light from a distant source by the gravity of an intervening mass, the effect that lets astronomers see distorted arcs, multiple images, and magnified galaxies. In the Recognition Science framework, the declaration deflectionAngle defines a ladder of such bending angles. It assigns to each whole number k a deflection angle equal to phi raised to the k-th power, where phi is the golden ratio, about 1.618. The framework proves that each step up the ladder multiplies the previous angle by phi exactly, and that every angle on the ladder is positive. The declaration also names five canonical lensing regimes, weak lensing, strong lensing, microlensing, cluster lensing, and time-delay, and proves that there are exactly five of them.

The golden ratio is the number that solves r squared equals r plus 1, the proportion that appears in pentagons, Fibonacci numbers, and spiral growth. The framework's library, a machine-checked collection of formal theorems, proves that the ratio of consecutive deflection angles is phi and that all deflection angles are positive. These proofs are checked by the library's kernel, so the claims hold within the framework's formal system. The framework models the five lensing regimes as a finite set with exactly five members, and the deflection ladder as a sequence indexed by natural numbers.

What the declaration does not claim is equally important. It does not assert that any measured deflection angle in the sky equals phi to some power. The measured bending of light by a galaxy cluster or a black hole is an empirical fact, and the framework's ladder is a mathematical structure, not a measurement. The declaration also does not claim that the five named regimes are the only possible kinds of lensing, or that real lenses divide cleanly into these five categories. It defines a formal classification and a formal ladder, and proves the internal relationships among them.

The consequence of the declaration is a clear, checkable picture: within the framework, gravitational lensing deflection angles form a discrete ladder with a fixed ratio, and the five regimes sit as a finite set beside it. That is what the formal declaration establishes, nothing more and nothing less.

noncomputable def deflectionAngle (k : ℕ) : ℝ := phi ^ k

theorem deflection_ratio (k : ℕ) :
    deflectionAngle (k + 1) / deflectionAngle k = phi := by
  unfold deflectionAngle
  have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  rw [div_eq_iff hpos.ne', pow_succ]
  ring

theorem deflection_pos (k : ℕ) : 0 < deflectionAngle k := pow_pos phi_pos k

theorem lensingRegime_count : Fintype.card LensingRegime = 5 := by decide

What this page does not claim

No measured deflection angle is asserted to equal phi to some power. The five regimes are not claimed to be the only possible kinds of lensing. The framework does not claim that real lenses divide cleanly into these five categories.

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/Cosmology/GravitationalLensingFromRS.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: