Upsilon
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not alter the Einstein field equations or the spacetime metric.
- Does not apply any enhancement when the scale factor a is non-positive.
- Does not change the algebraic form of Etherington duality.
- Does not introduce new dynamical degrees of freedom beyond the two kernel parameters C and alpha.
formal statement (Lean)
26noncomputable def Upsilon (P : ILG.KernelParams) (a : ℝ) : ℝ :=
proof body
Definition body.
27 if a ≤ 0 then 1 else 1 + P.C * a ^ P.alpha
28
29/-- The modified Sachs focusing equation (Target G).
30 For angular diameter distance D_A along an affine parameter λ:
31 d²D_A/dλ² + (1/2) * Upsilon(a) * R_μν k^μ k^ν * D_A = 0
32 where Ricci focusing is rescaled by Upsilon. -/