energy_bounded_below
plain-language theorem explainer
For real w at least 1 and real f, the product w f squared is nonnegative. Researchers on information-limited gravity cite this to confirm the energy functional stays bounded below under the weight operator. The proof is a one-line wrapper applying nonnegativity of products after linear arithmetic confirms w is nonnegative.
Claim. Let $w,f$ be real numbers. If $w$ satisfies $w$ at least 1 and $f^2$ is nonnegative, then $w f^2$ is nonnegative.
background
The Coercive Projection module formalizes the ILG energy functional having a unique minimizer with coercivity constant 49/162. The weight operator is positive when w is at least 1, which forces the quadratic form to be bounded below. This sits inside the broader setting where the ILG modified Poisson equation equals standard Poisson with effective pressure source p equal to w times rho_b.
proof idea
The proof is a one-line wrapper that applies the nonnegativity of the product of two nonnegative reals, after linear arithmetic confirms that w at least 1 implies w itself is nonnegative.
why it matters
This feeds directly into the coercive projection certificate and the no-retuning consistency theorem. It supplies the operator positivity step required by the Coercive Projection Law of Gravity paper, confirming that the ILG weight operator aligns with the eight-tick octave and the net constant K_net equal to (9/7) squared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.