ilg_correction_enhances
plain-language theorem explainer
The theorem establishes that the RS Information Ledger Gravity correction strictly increases the lensing convergence beyond its pure GR value when the tuning parameters are positive. Gravitational lensing analysts in the Recognition Science framework would cite it to confirm the enhancement direction of the scale-dependent term. The proof unfolds the multiplicative definition and applies nlinarith after verifying positivity of the added correction factor.
Claim. Assume $0 < κ_{GR}$, $0 < α_t$, $0 < ℓ$, $0 < ℓ_0$. Then $κ_{GR} < κ_{GR} (1 + α_t (ℓ/ℓ_0)^{-β})$.
background
The module derives gravitational lensing quantities from the RS action principle and Schwarzschild metric. The upstream definition gives the ILG convergence correction as κ_RS(ℓ) = κ_GR(ℓ) × (1 + α_t × (ℓ/ℓ₀)^{-β}), where α_t = (1 - φ^{-1})/2 and β ≈ 0.0557. The doc-comment states that the ILG correction is positive for α_t > 0.
proof idea
The proof unfolds the definition of the correction function. It establishes positivity of the term α_t * (ℓ/ℓ₀)^{-β} by mul_pos and rpow_pos_of_pos. nlinarith then yields the strict inequality directly from the positivity of the multiplier.
why it matters
This auxiliary result confirms the directional effect of the RS correction in lensing models and supports the derivations of deflection angle and Einstein radius in RS_Gravitational_Lensing.tex. It aligns with the framework's gravity section by ensuring the correction term enhances convergence under positive parameters. No downstream uses are recorded, leaving open how the specific β value fits observational data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.