E_G_pos
plain-language theorem explainer
The positivity of the E_G statistic under ILG factorization holds for any positive background density parameter, growth rate, and weight. Cosmologists auditing source-side observables in modified gravity would cite this to confirm the sign of the derived quantity. The proof is a one-line term-mode reduction that unfolds the product definition and applies the standard positivity rules for division and multiplication on the reals.
Claim. If $0 < Omega_{s0}$, $0 < f$, and $0 < w$, then $Omega_{s0}/f * w > 0$.
background
In the ILG setting the E_G statistic is introduced as the product of the background density parameter divided by the growth rate and the ILG weight function. This factorization is used to express the observable in terms of two separately computable ILG quantities. The surrounding module formalizes results from the ILG source-side kernel tests paper, including zero Buchert backreaction for potential-flow modifications and X-reciprocity between scale and time slopes.
proof idea
The proof is a direct term-mode reduction. It unfolds the definition of the E_G statistic to expose the product form, then applies the lemmas for positivity of division followed by positivity of multiplication on the positive reals.
why it matters
This theorem closes the basic positivity requirement for the E_G factorization inside the backreaction audit. It supports the module's core claims that ILG produces no Buchert backreaction and recovers GR in the large-X limit. The result sits at the level of elementary sign preservation and does not engage the eight-tick octave or phi-ladder structures directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.