Upsilon
plain-language theorem explainer
Upsilon defines the optical rescaling factor applied to the Ricci focusing term in the Sachs equation under the ILG optical extension route. It remains unity for non-positive scale factors and introduces a power-law enhancement 1 + C a^alpha for positive a using kernel parameters. Cosmologists extending distance measures in modified gravity would cite this when deriving rescaled DA and DL while preserving Etherington duality. The definition is a direct conditional expression with no auxiliary lemmas.
Claim. The optical rescaling factor is given by the piecewise function $1$ if $a ≤ 0$ and $1 + C_P a^{α_P}$ otherwise, where $P$ collects the ILG kernel parameters with coupling $C_P$ and exponent $α_P$, and $a$ is the cosmological scale factor.
background
In the optical rescaling route the Einstein equations stay unchanged while the Ricci term in the Sachs focusing equation is multiplied by Υ(a). The kernel parameters P encode the global constraint inherited from the recognition functional equation and supply the constants C and alpha that control the late-time correction. Upstream constants include the RS-native gravitational constant G = λ_rec² c³ / (π ℏ) and the fine-structure constant α, which set the scale for admissible kernel values.
proof idea
The definition is a direct conditional: return 1 when a ≤ 0, otherwise return 1 + P.C * a ^ P.alpha. No lemmas or tactics are required beyond ordinary real arithmetic.
why it matters
Upsilon supplies the factor appearing in SachsEquation_Extended, DA_rescaled and DL_rescaled, enabling the mild late-time demagnification described in the referenced dark-energy paper section while keeping Etherington duality intact. It feeds the bounds theorem upsilon_star_bounds that guarantees positive stellar mass-to-light ratios and appears in the SPARC falsifier comparison. The construction sits inside the broader ILG framework that derives G and α from the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.