module module moderate

`IndisputableMonolith.Gravity.GravitationalLensing`

This module assembles definitions and basic properties for gravitational lensing in Recognition Science, centered on the Schwarzschild radius and deflection formulas. Gravity modelers working in RS-native units would cite it when adapting standard lensing observables to the phi-ladder and J-cost framework. Content is organized as a flat collection of definitions and elementary lemmas with no deep proof structure.

claimDefines the Schwarzschild radius $r_s = 2GM/c^2$ together with lensing parameter, Newtonian and GR deflection angles, Einstein angle and radius, and Shapiro delay, all expressed in RS units with $c=1$.

background

The module sits in the Gravity domain and imports the RS time quantum $ au_0 = 1$ tick from Constants plus the J-cost core machinery. It adapts classical gravitational lensing quantities to the Recognition Science setting where constants are fixed by the forcing chain (T5 J-uniqueness, T8 D=3). The supplied doc-comment identifies the central object as the Schwarzschild radius $r_s = 2GM/c^2$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the lensing toolkit required by any downstream Recognition Science treatment of light deflection or time delay. It directly implements the Schwarzschild radius landmark and prepares the ground for observational tests that would use the alpha band and phi-ladder mass formula.

scope and limits

Does not derive deflection from the Recognition Composition Law.
Does not compute numerical predictions for specific lens masses.
Does not address strong-field or multi-image lensing regimes.
Does not incorporate Berry creation threshold or dream fraction.

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