DA_rescaled
The angular diameter distance under optical rescaling equals the background value multiplied by the reciprocal square root of Upsilon evaluated at scale factor 1/(1+z). Cosmologists extending the Sachs equation for late-time demagnification in ILG models would cite this when comparing distance ladders. It is realized as a direct composition of the background distance with the rescaling factor from the modified focusing term.
claimThe rescaled angular diameter distance satisfies $D_A(z) = D_{A, bg} / sqrt(Upsilon(P, 1/(1+z)))$, where $Upsilon(P, a)$ is the optical rescaling factor that multiplies the Ricci term in the Sachs equation and $P$ denotes the ILG kernel parameters.
background
The module implements the optical rescaling route in which the Einstein equations stay unchanged while the Ricci focusing term in the Sachs equation is multiplied by Upsilon(a). Upsilon itself is defined to equal 1 plus C times a to the power alpha for positive scale factor a, with C and alpha drawn from the KernelParams structure that bundles the RS-derived constants. The upstream scale definition supplies the phi-powered ladder used to fix those constants, and the module documentation quotes the target of producing mild late-time demagnification while preserving metricity and Etherington duality.
proof idea
This is a one-line definition that multiplies the supplied background angular diameter distance by the inverse square root of Upsilon evaluated at the redshift-derived scale factor.
why it matters in Recognition Science
The definition supplies the rescaled D_A that DL_rescaled and the theorem etherington_duality_preserved both invoke to establish that duality D_L = (1+z)^2 D_A continues to hold after the Upsilon modification. It directly realizes the optical rescaling route described in the module documentation for Target G. In the Recognition framework it sits inside the ILG kernel extension that leaves the metric intact while altering only the focusing term.
scope and limits
- Does not derive the numerical values of C or alpha from the forcing chain.
- Does not include spatial curvature corrections to the distance formula.
- Does not integrate the modified Sachs equation along specific null geodesics.
- Does not address early-universe or high-redshift regimes where Upsilon equals 1.
Lean usage
DA_rescaled z bg_DA Pformal statement (Lean)
40noncomputable def DA_rescaled (z : ℝ) (bg_DA : ℝ) (P : ILG.KernelParams) : ℝ :=
proof body
Definition body.
41 -- Scale factor a = 1 / (1 + z)
42 bg_DA * (1 / sqrt (Upsilon P (1 / (1 + z))))
43
44/-- Luminosity distance D_L under optical rescaling.
45 To preserve Etherington duality, it must scale identically to D_A. -/