Gravity Gravitational Lensing Rs3 From Jcost

The lensing coefficient

Gravitational lensing is the bending of light rays as they pass near a massive object. In Einstein's general relativity, the deflection angle for a ray grazing a mass M at a closest approach distance b is alpha = 4GM/(c^2 b), where G is the gravitational constant and c is the speed of light. The formula dates to 1916 and was first confirmed by Arthur Eddington's 1919 eclipse expedition.

The angle is tiny for ordinary distances: the Sun, with b set to its radius, deflects starlight by about 1.75 arcseconds. The effect becomes dramatic only near a black hole, where the denominator c^2 b shrinks toward the Schwarzschild radius r_Sch = 2GM/c^2. At that boundary, the deflection angle diverges, and light can orbit the hole.

In Recognition Science, the framework derives physical structure from a single forced cost function. The cost of recognition is J(x) = (x + 1/x)/2 - 1, a proved result in the machine-checked library of formal theorems. The framework models gravitational lensing by setting the cost argument x to m/e, a ratio of two masses, and calls the resulting expression domainCost. The module GravitationalLensingRS3FromJCost proves three general facts about this cost: it vanishes when m equals e, it is nonnegative for positive inputs, and the constant phi - 3/2 is positive, where phi is the golden ratio. These are facts about the cost function itself, not about lensing physics.

The research note attached to the module records a proposed connection: at a closest approach b = r_Sch * phi, the deflection angle becomes alpha = 4*J(phi), which evaluates to 0.472 radians. At b = r_Sch * phi^5, the angle is 4/phi^4, about 0.94 arcseconds. This is a structural guess linking the golden ratio to lensing geometry, not a proved theorem. The module itself contains no definition of m and e in physical terms, so it establishes only the cost function's general properties.

What the module does establish, in plain language, is a clean mathematical floor: the cost function that the framework uses everywhere has a sensible zero point, never goes negative on positive inputs, and has a positive threshold tied to the golden ratio. Those three facts hold for any ratio m/e, which is why they are reusable. The lensing interpretation remains a target, not a result.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The module does not prove that gravitational lensing follows the golden ratio. The module does not derive the Einstein deflection formula from the cost function. The 0.472 radian and 0.94 arcsecond values are research notes, not theorem outputs.

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/GravitationalLensingRS3FromJCost.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: