Gravity Backreaction Audit E G Pos

The positivity of E_G

The E_G statistic is a standard tool in observational cosmology. It compares the strength of gravitational lensing to the velocity dispersion of galaxies, and it is used to test whether the laws of gravity are the same on cosmic scales as they are in the solar system. In the Recognition Science framework, the statistic is modeled as E_G = (Ω_s0 / f) × w, where Ω_s0 is a matter density parameter, f is the growth rate of cosmic structure, and w is a weighting function.

What the declaration E_G_pos proves is a simple algebraic fact: if all three inputs are positive, then the product is positive. The theorem is checked by the framework's machine-checked library of formal theorems, and it is a direct consequence of the positivity of division and multiplication. This is not a claim about the physical values of the inputs, nor about the size of the statistic. It is a guarantee that the model does not produce a negative or zero E_G when its ingredients are positive.

The declaration is part of a larger audit of the framework's gravitational model. The same file proves that the model leaves the background cosmic expansion unchanged, that its scale and time derivatives mirror each other, and that it reduces to general relativity in the strong-field limit. The positivity result is the least ambitious of these, but it is the one that makes the others usable: a statistic that could flip sign would be useless for comparing theory to observation.

In plain terms, the theorem says the model is internally consistent at the level of signs. It does not say that the model matches any measured value of E_G, and it does not say that the inputs are positive in the real universe. Those are empirical questions, and they are not settled by this declaration.

/-- E_G is positive when all inputs are positive. -/
theorem E_G_pos (omega f w : ℝ) (ho : 0 < omega) (hf : 0 < f) (hw : 0 < w) :
    0 < E_G_ilg omega f w := by
  unfold E_G_ilg
  exact mul_pos (div_pos ho hf) hw

What this page does not claim

The theorem does not claim that E_G matches any measured cosmological value. The theorem does not claim that the inputs omega, f, and w are positive in the real universe. The theorem does not claim that the ILG model itself is correct, only that this algebraic consequence follows from its definitions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/BackreactionAudit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: