E_G_pos
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not claim positivity when any of the three inputs is non-positive.
- Does not address the explicit functional dependence of the growth rate or weight on wavenumber or scale factor.
- Does not derive or constrain the Buchert backreaction term itself.
- Does not connect to the full set of PPN safety bounds or X-reciprocity statements in the same module.
formal statement (Lean)
95theorem E_G_pos (omega f w : ℝ) (ho : 0 < omega) (hf : 0 < f) (hw : 0 < w) :
96 0 < E_G_ilg omega f w := by
proof body
Term-mode proof.
97 unfold E_G_ilg
98 exact mul_pos (div_pos ho hf) hw
99
100/-- E_G monotonicity: when both w and f increase (w1 ≤ w2, f1 ≤ f2),
101 the E_G statistic E_G = omega/f * w is non-decreasing.
102 (w increases with decreasing k at fixed a under ILG.) -/