E_G_ilg
plain-language theorem explainer
E_G_ilg encodes the factorization of the E_G statistic under the ILG model as the product of the initial matter density parameter divided by the growth factor and the ILG weight. Researchers auditing backreaction effects in gravity models cite this factorization when deriving monotonicity or positivity for comparisons to growth and lensing observations. The definition reduces to a direct algebraic product of the scaled density ratio and the weight term.
Claim. $E_G = (Omega_{s0} / f) * w$, where $f$ denotes the growth rate and $w$ the ILG weight at the relevant scale factor.
background
This module formalizes results from the dark-energy paper on ILG source-side kernel tests against distances, growth, and lensing. It establishes that ILG yields zero Buchert backreaction because it acts as a potential-flow source modification rather than a metric change, alongside X-reciprocity of scale slopes at fixed redshift and PPN safety with the weight approaching 1 in the large-X limit. The E_G factorization is introduced explicitly as a product of two ILG-computable functions.
proof idea
The declaration is a one-line definition that multiplies the ratio of the initial density parameter to the growth factor by the weight using ordinary real arithmetic.
why it matters
This definition supplies the base expression for the E_G_pos theorem and the E_G_monotone_prediction property within the same module. It directly implements the E_G factorization for ILG observables stated in the module documentation. In the Recognition Science setting it contributes to gravity backreaction audits without invoking the core forcing chain or recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.