DL_rescaled
plain-language theorem explainer
DL_rescaled defines the luminosity distance in the optical rescaling route of ILG cosmology so that Etherington duality is preserved by construction. Cosmologists working on late-time demagnification models would cite it when extending the Sachs equation with a Upsilon factor while keeping the metric intact. The definition is a direct algebraic wrapper that feeds an adjusted background into the angular-diameter rescaling function and multiplies back by the redshift factor.
Claim. The rescaled luminosity distance is defined by $D_L(z, D_{L, bg}, P) := D_A(z, D_{L, bg}/(1+z)^2, P) · (1+z)^2$, where $D_A$ denotes the rescaled angular-diameter distance function and $P$ carries the ILG kernel parameters.
background
The Optical Rescaling Extension module keeps the Einstein equations unchanged while rescaling the Ricci focusing term in the Sachs equation by a factor Upsilon(a). This produces mild late-time demagnification while preserving metricity and Etherington duality, as stated in the module documentation referencing the Dark-Energy.tex paper. The definition relies on the sibling DA_rescaled function and on upstream constants such as G from the Constants and Cost.FunctionalEquation modules together with ledger structures from DAlembert.LedgerFactorization.
proof idea
This is a one-line definition that divides the supplied background luminosity distance by (1+z)^2, passes the result to DA_rescaled, and multiplies the output by (1+z)^2.
why it matters
The definition supplies the luminosity-distance side of the main theorem etherington_duality_preserved, which states that D_L = (1+z)^2 D_A continues to hold under arbitrary Upsilon rescaling. It thereby completes the Target G item in the optical-rescaling route for late-time cosmology. Within the Recognition Science framework the construction supports the Upsilon(a) modification of the Sachs equation without altering the underlying metric or the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.