ilg_convergence_correction
plain-language theorem explainer
The ILG convergence correction supplies an explicit multiplicative factor modifying the GR lensing convergence to include RS scale dependence, yielding κ_RS(ℓ) = κ_GR(ℓ) × (1 + α_t × (ℓ/ℓ₀)^{-β}) with α_t = (1 - φ^{-1})/2. Researchers modeling deviations from standard GR lensing at varying angular scales would cite this expression when fitting observations. The definition is implemented as a direct algebraic formula without lemmas or tactics.
Claim. $κ_{RS}(ℓ) = κ_{GR} ⋅ (1 + α_t ⋅ (ℓ/ℓ₀)^{-β})$, where α_t = (1 - φ^{-1})/2 and β ≈ 0.0557.
background
The Gravitational Lensing module derives deflection angles, Einstein radii, and Shapiro delays from the RS action principle applied to the Schwarzschild metric. Prior results in the module establish that the GR deflection angle is twice the Newtonian value and that time delays remain positive. This definition encodes the Information Ledger Gravity correction, which multiplies the standard GR convergence by a term that depends on the ratio of angular scale ℓ to a reference scale ℓ₀. The parameter α_t is fixed by the golden ratio φ, consistent with the self-similar fixed point in the forcing chain.
proof idea
The definition is a one-line algebraic expression that multiplies the input GR convergence by the enhancement factor (1 + α_t ⋅ (ℓ / ℓ₀)^{-β}). No lemmas are applied and no tactics are required beyond the explicit formula.
why it matters
This definition supplies the concrete expression invoked by the theorem proving that the corrected convergence exceeds the GR value for positive α_t. It completes the RS gravitational lensing derivation by embedding the scale-dependent prediction from Information Ledger Gravity, linking to the phi fixed point and eight-tick octave in the unified forcing chain. The module references the paper RS_Gravitational_Lensing.tex for the broader context.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.