Upsilon
plain-language theorem explainer
The optical rescaling factor equals 1 for non-positive scale factor a and otherwise equals 1 plus the product of coupling strength C and a raised to exponent alpha. Cosmologists modeling modified Ricci focusing in the Sachs equation cite this definition when extending distance measures under ILG while keeping the metric fixed. The definition is a direct piecewise function that activates the enhancement only after a exceeds zero.
Claim. The optical rescaling factor satisfies $a=0$ implies $1$, and otherwise $1 + C a^alpha$, where $C$ and $alpha$ are the coupling strength and exponent carried by the kernel parameters.
background
This definition sits in the Optical Rescaling Extension module. The module formalizes an ILG route in which the Einstein equations stay fixed but the Ricci focusing term of the Sachs equation is multiplied by the factor. The module documentation quotes the relevant paper passage on an optical rescaling of the Ricci focusing that preserves metricity and Etherington duality while producing mild late-time demagnification.
proof idea
This is a direct definition expressed as a conditional. It returns 1 whenever a is at most zero and returns the enhanced expression 1 plus C times a to the power alpha otherwise. No lemmas or tactics are required.
why it matters
The definition provides the rescaling factor applied in the angular-diameter and luminosity distance definitions as well as the extended Sachs equation. It is used to establish bounds on the stellar mass-to-light ratio and to compare ILG performance against MOND on SPARC data. It fills the optical rescaling proposal from the dark-energy paper and connects to the Recognition Science forcing chain that fixes the spatial dimension and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.