pith. sign in
module module high

IndisputableMonolith.Relativity.Cosmology.OpticalExtension

show as:
view Lean formalization →

This module defines the optical rescaling factor Upsilon(a) that incorporates an ILG enhancement at late times to modify Ricci focusing in FRW cosmologies. Researchers modeling modified gravity effects on light propagation and distance measures would cite it when extending standard optical equations. The module structures a set of definitions and lemmas around this rescaling, directly importing the ILG kernel and FRW metric without internal proofs.

claimThe optical rescaling factor $Upsilon(a)$ incorporates the ILG kernel enhancement $w(k,a)=1+C(a/(k tau_0))^alpha$ at late times, modifying the Ricci focusing term in the Sachs optical equation for FRW backgrounds.

background

The module sits inside the Recognition Science cosmology extension and imports the ILG kernel together with the FRW metric. The ILG kernel supplies the wave-number-dependent weight $w(k,a)=1+C(a/(k tau_0))^alpha$ that becomes active at late times. The FRWMetric supplies the standard expanding background against which optical quantities are computed. The module then introduces the rescaling factor Upsilon(a) that multiplies the usual Ricci focusing term, together with the extended Sachs equation and the rescaled angular-diameter and luminosity distances.

proof idea

This is a definition module, no proofs. It declares the central object Upsilon, the extended Sachs equation, the rescaled distances DA_rescaled and DL_rescaled, and the two lemmas etherington_duality_preserved and optical_reduces_to_gr that close the optical extension.

why it matters in Recognition Science

The module supplies the optical layer required for late-time ILG modifications inside the broader cosmology chain. It feeds the rescaled distance measures and duality preservation statements that appear as sibling declarations, allowing downstream calculations of observable cosmology to incorporate the ILG kernel without changing the early-universe FRW evolution. The construction directly supports the Recognition Science program of deriving modified gravity effects from the single functional equation while preserving Etherington duality.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)