SachsEquation_Extended
plain-language theorem explainer
SachsEquation_Extended encodes the modified Sachs focusing equation in which the Ricci term is multiplied by the optical rescaling factor Upsilon(a). Cosmologists working on late-time demagnification in ILG models cite this definition when constructing angular-diameter distances under rescaled focusing. The body directly substitutes a = 1/(1+z) and states the second-order ODE with the Upsilon multiplier.
Claim. The extended Sachs equation states that for angular-diameter distance function $DA(z')$ the relation $D_A''(z') + Upsilon(P,a) · ricci_focusing · DA(z') = 0$ holds for all $z'$, where $a = 1/(1+z)$ and $Upsilon(P,a) = 1 + P.C · a^{P.alpha}$ when $a > 0$.
background
The optical rescaling route keeps the Einstein equations unchanged while multiplying the Ricci focusing term in the Sachs equation by Upsilon(a). Upsilon is defined to equal 1 for $a ≤ 0$ and to equal $1 + P.C · a^{P.alpha}$ otherwise, supplying a late-time enhancement controlled by the ILG kernel parameters P. The module documentation identifies this construction as Target G, the route that produces mild late-time demagnification while preserving metricity and Etherington duality.
proof idea
The declaration is a direct definition. It first binds the scale factor a = 1/(1+z), then asserts the universal quantification over z' of the second-derivative ODE with the Upsilon(P,a) factor applied to the supplied ricci_focusing coefficient.
why it matters
The definition supplies the precise statement of the optical-rescaling Sachs equation referenced in the module's Dark-Energy.tex citation. It forms the starting point for the sibling results on duality preservation and reduction to general relativity. The construction sits inside the Recognition Science optical route that leaves the metric intact while rescaling focusing, consistent with the eight-tick octave and phi-ladder calibration of the kernel constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.