shiftedQuadraticStrain
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not extend the construction to vector states in R^n for n > 1.
- Does not prove uniqueness of the minimizer.
- Does not link to the phi-ladder or discrete Recognition Science structures.
- Does not address time evolution or dynamics.
formal statement (Lean)
94def shiftedQuadraticStrain (a : ℝ) : StrainFunctional ℝ where
95 J := fun x => (x - a) ^ 2
proof body
Definition body.
96
97instance (a : ℝ) : StrainFunctional.NonNeg (shiftedQuadraticStrain a) where
98 nonneg := fun x => sq_nonneg (x - a)
99