module module moderate

`IndisputableMonolith.Gravity.GravitationalLensing`

The GravitationalLensing module supplies definitions for Schwarzschild radius, lensing parameters, deflection angles, and Shapiro delay in the Recognition Science gravity domain. Researchers modeling RS gravitational effects would cite these for lensing and time-delay predictions. The module consists of a sequence of definitions that import Constants and JcostCore without internal proofs.

claim$r_s = 2GM/c^2$ (Schwarzschild radius); related quantities include lensing parameter, Newtonian and GR deflection angles, Einstein angle, and Shapiro delay.

background

The module operates in the Gravity domain of Recognition Science and imports the fundamental RS time quantum τ₀ = 1 tick from Constants together with J-cost machinery from JcostCore. It introduces definitions that express gravitational lensing quantities using these primitives and the phi-ladder conventions already present in the imported modules.

The local theoretical setting treats gravitational parameters as extensions of the J-cost framework, with the supplied module documentation stating the Schwarzschild radius explicitly as r_s = 2GM/c².

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module establishes the core definitions for gravitational lensing calculations inside the RS framework. It supplies the base objects that later gravity results would apply, connecting to the forcing chain landmarks (T0-T8) and the expression of G in RS-native units. No direct used_by theorems are recorded.

scope and limits

Does not derive deflection formulas from the Recognition Composition Law.
Does not incorporate the mass formula or phi-ladder rung assignments.
Does not treat strong-field or multi-lens configurations.
Does not compare predictions against observational data.

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