shiftedQuadraticStrain
plain-language theorem explainer
The shifted quadratic strain functional on the reals sets J(x) = (x - a)^2 for fixed a in R, with its global minimum at a. Researchers testing continuous optimization models inside the RRF framework cite this construction when verifying equilibrium and minimizer properties. The definition is accompanied by a NonNeg instance that follows in one step from the non-negativity of squares.
Claim. The shifted quadratic strain functional on the state space R is the map J : R → R given by J(x) := (x - a)^2 for any fixed shift parameter a ∈ R.
background
A StrainFunctional on a state space assigns a cost J(x) ∈ R to each state x, with the structural requirement that J(x) = 0 precisely when x is at equilibrium. The NonNeg class constraint adds the axiom that J(x) ≥ 0 for every x. The module presents quadratic models as a non-trivial test case for RRF structures on continuous state spaces, here specialized to the one-dimensional real line with a simple shift.
proof idea
The definition directly installs the shifted-square expression as the J field. The accompanying NonNeg instance is a one-line wrapper that applies the sq_nonneg lemma to the term (x - a).
why it matters
This definition supplies the concrete strain functional required by the downstream theorems shifted_equilibrium and shifted_is_minimizer, which establish that a is both the equilibrium point and the global minimizer. It serves as the basic continuous test case inside the RRF quadratic model, confirming that the strain-based optimization framework handles real-valued states without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.