etherington_duality_preserved
plain-language theorem explainer
The theorem establishes that Etherington duality holds after optical rescaling of luminosity and angular diameter distances via the Upsilon factor. Cosmologists studying ILG modifications to Ricci focusing for late-time demagnification would cite this to confirm consistency with distance relations. The proof is a direct algebraic reduction that unfolds the rescaled luminosity definition, substitutes the background duality hypothesis, and normalizes via field and ring simplification.
Claim. Let $z, D_A^{bg}, D_L^{bg} ∈ ℝ$ and let $P$ be ILG kernel parameters. If the background distances satisfy $D_L^{bg} = (1 + z)^2 D_A^{bg}$, then the rescaled luminosity distance equals $(1 + z)^2$ times the rescaled angular diameter distance, where the rescaling multiplies the background angular diameter distance by $1/√Υ(P, 1/(1+z))$ and constructs the luminosity distance to enforce the same scaling.
background
The optical rescaling route keeps the Einstein equations fixed while multiplying the Ricci focusing term in the Sachs equation by Υ(a) = 1 + C a^α (a > 0). The angular diameter distance is modeled as the background value multiplied by the inverse square root of this factor evaluated at scale factor 1/(1+z). The luminosity distance is defined to enforce duality by applying the same rescaled angular diameter construction to the adjusted background luminosity value and then multiplying back by (1+z)^2. KernelParams supplies the explicit RS-derived constants α and C for this construction.
proof idea
The proof unfolds the definition of the rescaled luminosity distance, which rewrites it as the rescaled angular diameter distance applied to the background luminosity divided by (1+z)^2, then multiplied by (1+z)^2. It substitutes the given background duality hypothesis directly into this expression. Field simplification clears the resulting denominators and ring normalizes the identity to equality.
why it matters
This is the main theorem (Target G) for the optical rescaling route, confirming that Etherington duality survives the Υ modification to Ricci focusing. The result supports the module claim that the route preserves metricity and duality while allowing mild late-time demagnification, as stated in the Dark-Energy.tex reference. It provides the algebraic consistency check needed before comparing the model to GR limits when the coupling vanishes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.