quadratic1D_minimizer
plain-language theorem explainer
The quadratic strain functional on the real line attains its global minimum at the origin. Researchers modeling continuous optimization within the Recognition framework cite this when confirming that the quadratic model satisfies the core minimizer predicate from RRF Core. The proof reduces the claim directly to the non-negativity of squares after unfolding the strain definitions.
Claim. Let $J : ℝ → ℝ$ be the quadratic strain functional given by $J(x) = x^2$. Then $0$ is a minimizer, meaning $J(0) ≤ J(y)$ for every real number $y$.
background
The module introduces a quadratic model for RRF where the state space is $ℝ^n$ and the strain functional is $J(x) = ‖x‖². This serves as a testing ground for theorems about minimizers in continuous settings, as stated in the module documentation.
proof idea
The proof is a direct term-mode argument. It introduces an arbitrary real number y, simplifies the weaklyBetter relation using the definitions of StrainFunctional and quadratic1DStrain, and applies the fact that squares are non-negative.
why it matters
This theorem verifies that the quadratic model satisfies the fundamental minimizer property required by the RRF framework, supporting the use of continuous optimization examples. It contributes to the demonstration that RRF structures can handle continuous cases. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.