E_G_monotone_prediction
plain-language theorem explainer
E_G monotonicity asserts that the ILG E_G statistic given by omega over f times w is non-decreasing whenever both the growth rate f and weight w increase under the stated positivity conditions. Cosmologists auditing ILG predictions for distances and growth would cite this when confirming consistent ordering of the observable under parameter variation. The statement is a direct encoding of the product form of E_G_ilg.
Claim. Let $E_G = (omega / f) * w$. Then for all real numbers $omega, f_1, f_2, w_1, w_2$ satisfying $0 < omega$, $0 < f_1$, $0 < f_2$, $f_1 leq f_2$, and $w_1 leq w_2$, the inequality $E_G(omega, f_1, w_1) leq E_G(omega, f_2, w_2)$ holds.
background
The E_G statistic factorizes under ILG as $E_G^{RS}(k,z) = (Omega_{s0} / f(k,z)) * w(k,a(z))$, where f is the growth rate and w is the ILG weight. This product appears directly in the definition of E_G_ilg, which multiplies the background density parameter by the reciprocal of the growth rate and the weight term. The module formalizes results from the paper on ILG source-side kernel tests against distances, growth, and lensing, with emphasis on zero Buchert backreaction and X-reciprocity.
proof idea
This is a definition of the monotonicity proposition. It directly encodes the required inequality using the product definition of E_G_ilg, with no lemmas or tactics applied beyond the algebraic form already supplied by the upstream E_G_ilg definition.
why it matters
The definition supports the E_G factorization for ILG observables within the backreaction audit. It contributes to model consistency checks by ensuring the statistic respects monotonic ordering as f and w vary with scale, aligning with the module's core results on potential-flow modifications that produce zero Buchert backreaction. No downstream theorems are listed, so it serves as a supporting property for the overall BackreactionCert structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.