Pith. sign in
module module low

IndisputableMonolith.Relativity.ILG.LensingDerived

show as:
view Lean formalization →

Module for gravitational lensing quantities derived inside the ILG sector of Recognition Science relativity. Relativists comparing RS lensing predictions to GR or to survey data would land here. The file is organizational: it gathers derived lensing maps and identities rather than proving a single end theorem.

claimDerived gravitational lensing observables (deflection, convergence, shear) obtained from the ILG effective metric and potential in the Recognition Science relativity stack.

background

ILG is the Recognition Science gravity sector used in place of, or as a controlled deformation of, standard GR for galactic and cosmological scales. Lensing is read off the null geodesics and the projected potential of that effective geometry.

In the broader RS stack, constants and the cost functional $J$ are already fixed upstream (T5 J-uniqueness, $\phi$ as self-similar fixed point). This module sits downstream of those forcings and of the ILG field equations; it does not re-derive $c$, $\hbar$, or $G$.

Notation follows the Relativity.ILG hierarchy: effective potential, deflection angle, convergence $\kappa$, and shear $\gamma$ expressed in RS-native units where applicable.

proof idea

This is a module page, not a single theorem. Content is a mix of definitions of lensing maps from the ILG potential and short derived identities. Expect thin wrappers around upstream ILG metric lemmas plus algebraic projections to the lens plane; no monolithic tactic proof spans the file.

why it matters in Recognition Science

Places RS gravity in contact with observational lensing (weak shear, strong arcs, time delays). Parent consumers are higher-level Relativity.ILG phenomenology and any comparison theorems against GR lensing or survey constraints. Ties to the RS forcing chain only indirectly: once $J$, $\phi$, and $D=3$ are fixed, the ILG effective description and its lensing readout become the bridge to data. Does not itself close T0--T8.

scope and limits