shifted_is_minimizer
plain-language theorem explainer
The quadratic model in RRF establishes that the strain functional shifted by a real parameter a remains minimized exactly at a. Researchers modeling continuous optimization in recognition frameworks cite this to confirm translation invariance of the argmin. The argument reduces the weaklyBetter inequality directly to non-negativity of squares after simplification.
Claim. For every real number $a$, the shifted quadratic strain function $f(y) = (y - a)^2$ satisfies $f(y) > f(a)$ for all $y$ with $y$ not equal to $a$, so that $a$ is its unique global minimizer.
background
The RRF quadratic model takes state space ℝ and cost functional J(x) = x². The shifted variant centered at parameter a is the function whose value at y equals (y - a)². The isMinimizer predicate, drawn from the RRF core glossary, asserts that a point realizes the global minimum via the weaklyBetter relation on strain values. Module documentation positions this construction as a test case for continuous optimization properties inside RRF structures.
proof idea
The term proof introduces an arbitrary y, simplifies the weaklyBetter condition using the definitions of shiftedQuadraticStrain and StrainFunctional, then applies the fact that the square of any real number is non-negative.
why it matters
This result verifies the minimizer property under shift for the quadratic strain, supporting the module's demonstration of monotone argmin invariance. It supplies a concrete instance for theorems about minimizers in continuous RRF models and aligns with the quadratic model's role as a testing ground for optimization statements. No downstream uses are recorded, but the surrounding comments link it to the exponential transform preserving the same argmin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.