no_retuning
plain-language theorem explainer
no_retuning encodes the uniqueness property for a global weight function w_global in the ILG energy functional: any distinct w' must violate the quadratic inequality w_global(x) x^2 <= w'(x) x^2 at some x. Galaxy-dynamics modelers working under coercive projection would cite it to rule out per-object retuning of kernels. The property is delivered by direct encoding of the strict-minimizer condition in the definition body.
Claim. A function $w : {R} {to} {R}$ satisfies the no-retuning property when, for every $w' {neq} w$, the inequality $w(x) x^2 {leq} w'(x) x^2$ forces $w'(x) = w(x)$ at every $x$. Equivalently, no other kernel can produce a lower or equal energy contribution under the quadratic form.
background
The Coercive Projection Law module formalizes the ILG energy functional as possessing a unique minimizer when a single global kernel w is used for all galaxies. Core supporting facts are the coercivity constant c = 49/162, the net constant K_net = (9/7)^2 derived from eight-tick epsilon = 1/8, and the positivity statement that w >= 1 implies <f, w f> >= ||f||^2. The module also records equivalence of the ILG modified Poisson equation to the standard Poisson equation with effective pressure source p = w rho_b.
proof idea
Direct definition. The body states the uniqueness condition for the quadratic form w x^2 by requiring that any candidate w' differing from w_global must fail the inequality at least at one point, thereby preventing a lower-energy alternative.
why it matters
The definition closes the per-galaxy retuning loophole inside the Coercive Projection Law, confirming that the global kernel is the sole energy minimizer. It aligns with the ILG positivity of the weight operator and the eight-tick structure underlying K_net. No downstream theorems are recorded; the result supports the broader claim that uniform kernels are required by energy minimization in the Recognition Science gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.