no_retuning_consistent
plain-language theorem explainer
The theorem shows that a weight function w bounded below by 1 everywhere keeps the quadratic form w(x) f² non-negative for every real f. Researchers modeling galactic dynamics in information-limited gravity cite it to confirm that a single global weight satisfies the positivity needed for energy minimization. The argument is a direct pointwise specialization of the energy-bounded-below lemma together with non-negativity of squares.
Claim. If a function $w : ℝ → ℝ$ satisfies $w(x) ≥ 1$ for every real $x$, then $w(x) f^2 ≥ 0$ for all real $x$ and $f$.
background
The Coercive Projection Law module encodes the unique-minimizer property of the ILG energy functional under a positive weight operator, together with the equivalence of the modified Poisson equation to standard gravity plus an effective pressure source. The upstream result energy_bounded_below states that operator positivity implies the energy functional is bounded below: if $w_val ≥ 1$ and $f_val^2 ≥ 0$ then $0 ≤ w_val · f_val^2$. The no-retuning hypothesis requires the same lower bound to hold uniformly rather than being adjusted per galaxy.
proof idea
The proof is a one-line term wrapper that applies energy_bounded_below pointwise. For arbitrary $x$ and $f$ it instantiates the lemma with the values $w x$, $f$, the hypothesis $hw x$, and the fact that $f^2$ is non-negative.
why it matters
This result closes the consistency check for the no-retuning assumption inside the Coercive Projection Law, confirming that a single global weight $w ≥ 1$ preserves the bounded-below property required for a unique energy minimizer. It directly supports the module statement that no per-galaxy retuning is consistent with the energy minimization principle and aligns with the eight-tick octave structure used to derive the ILG kernel prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.