optical_reduces_to_gr
plain-language theorem explainer
When the ILG coupling constant C vanishes, the optical rescaling factor Upsilon reduces to unity so the angular diameter distance DA_rescaled equals the supplied background value bg_DA at every redshift. Cosmologists examining modified Sachs focusing or late-time demagnification routes would cite this reduction to recover the GR limit. The proof is a direct term-mode reduction that unfolds the two definitions and simplifies under the hypothesis C=0.
Claim. When the coupling constant satisfies $C=0$, the angular diameter distance under optical rescaling equals the background value: $D_A(z, D_A^{bg}, P) = D_A^{bg}$.
background
The OpticalExtension module implements the Upsilon route in which the Einstein equations stay unchanged while the Ricci term in the Sachs equation is multiplied by the rescaling factor Upsilon(a). This factor is defined piecewise as 1 + C a^alpha for a>0 (and 1 otherwise), with C and alpha taken from the KernelParams structure that bundles the RS-derived constants. The rescaled angular diameter distance is then constructed as bg_DA multiplied by the reciprocal square root of Upsilon evaluated at the scale factor a=1/(1+z).
proof idea
The proof is a one-line wrapper that unfolds the definitions of DA_rescaled and Upsilon, then applies simp with the hypothesis hC that C equals zero. The substitution forces Upsilon to 1 everywhere, the square-root factor collapses to 1, and the equality follows immediately.
why it matters
This result supplies the GR-recovery case for the optical rescaling route whose module documentation quotes the paper proposition on Upsilon(a) preserving metricity and Etherington duality while producing mild late-time demagnification. It anchors the vanishing-coupling limit inside the Relativity.Cosmology.OpticalExtension module and confirms consistency with standard FRW distances when the ILG amplitude C is absent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.