Gravity Coercive Projection Operator Positivity Pointwise

The positivity lemma

The declaration operator_positivity_pointwise proves a small algebraic fact: if a real number w is at least 1, then for any real number f, the square f² is no larger than w times f². In symbols, w ≥ 1 implies f² ≤ w·f². The proof is a direct application of the fact that a square is never negative. This is a theorem in the machine-checked library of formal theorems, meaning the reasoning has been verified step by step.

This lemma matters because it is one piece of a larger framework called Recognition Science, which models gravity as a consequence of information limits. In that framework, a weight operator w multiplies a density field f, and the energy of a configuration is built from terms like w·f². The positivity lemma guarantees that when the weight is at least 1 everywhere, the energy is bounded below by the plain square of the field. That lower bound is the first step toward showing the energy has a unique minimum, a property called coercivity. The framework's library proves the coercivity constant is 49/162, which lies between 0.30 and 0.31.

The lemma itself is deliberately narrow. It says nothing about physics, about gravity, or about why w should be at least 1. It is a statement about real numbers and squares, and its proof uses only the nonnegativity of squares. The framework's larger claims, such as the equivalence between a modified Poisson equation and standard Poisson with an effective pressure, rest on additional definitions and theorems, not on this lemma alone. The positivity lemma is a load-bearing but small brick in that wall.

What the declaration does not claim is equally important. It does not assert that the weight operator is positive in any functional-analytic sense beyond the pointwise inequality. It does not claim that the energy minimizer exists, only that the energy is bounded below. It does not claim that the framework's model of gravity is correct or that its constants match observation. Those are separate questions, addressed by other theorems and by empirical checks. The lemma is a piece of mathematics, and it is honest about being only that.

/-- The ILG weight operator is positive: if w(x) >= 1 for all x,
    then <f, w*f> >= ||f||^2 (in L^2 inner product sense).

    We formalize this pointwise: w(x) * f(x)^2 >= f(x)^2. -/
theorem operator_positivity_pointwise (w_val f_val : ℝ) (hw : 1 ≤ w_val) :
    f_val ^ 2 ≤ w_val * f_val ^ 2 := by
  nlinarith [sq_nonneg f_val]

theorem c_coercive_value : c_coercive = 49 / 162 := rfl

theorem c_coercive_approx : (0.30 : ℚ) < c_coercive ∧ c_coercive < (0.31 : ℚ) := by
  unfold c_coercive; constructor <;> norm_num

What this page does not claim

The lemma does not assert that the energy minimizer exists, only that the energy is bounded below. The lemma does not claim that the weight operator is positive in any functional-analytic sense beyond the pointwise inequality. The lemma does not claim that the framework's model of gravity is correct or that its constants match observation.

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/CoerciveProjection.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: