module module high

`IndisputableMonolith.Gravity.GravitationalLensing`

This module supplies definitions and basic theorems for gravitational lensing observables inside the Recognition Science framework. Researchers comparing light deflection and Shapiro delay predictions to general relativity or to RS-derived constants would cite these results. The module is a collection of direct definitions and short positivity proofs built on the imported time quantum and J-cost core.

claimThe Schwarzschild radius is $r_s = 2GM/c^2$. The Newtonian deflection angle is $2GM/(c^2 b)$, the GR deflection is twice that value, the squared Einstein angle satisfies $4GM D_{LS}/(c^2 D_L D_S)$, and the Shapiro delay is $(2GM/c^3) ln(4 D_L D_S / b^2)$.

background

Recognition Science obtains gravitational effects from the J-cost functional obeying the Recognition Composition Law, with the fundamental time quantum fixed at one tick. The module imports the RS-native constants and the J-cost core to introduce the characteristic length scale for a central mass. It then defines the impact parameter, lensing geometry distances, and the two deflection regimes together with the associated time delay.

proof idea

This is a definition module, no proofs. It introduces the listed quantities by direct transcription from the imported constants and establishes the listed positivity and doubling statements by elementary algebraic comparison.

why it matters in Recognition Science

The module supplies the explicit lensing formulas that translate the abstract J-cost and phi-ladder structure into measurable deflection and delay observables. It anchors the gravitational sector of the framework and prepares the ground for quantitative comparison with astronomical data.

scope and limits

Does not derive the deflection formulas from a full spacetime metric.
Does not treat strong lensing or multiple-image configurations.
Does not incorporate quantum or higher-order post-Newtonian corrections.
Does not evaluate numerical predictions for specific astrophysical lenses.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (16)

def schwarzschild_radius L29
def lensing_param L32
def deflection_newtonian L38
def deflection_GR L42
theorem gr_is_twice_newton L47
theorem deflection_angle_formula L59
theorem deflection_positive L65
theorem deflection_inverse_b L71
def einstein_angle_sq L87
theorem einstein_radius_positive L91
def shapiro_delay L102
theorem shapiro_delay_positive L106
def solar_deflection L122
theorem solar_deflection_positive L126
def ilg_convergence_correction L139
theorem ilg_correction_enhances L143