exp_preserves_argmin
plain-language theorem explainer
The theorem shows that if a real number x minimizes the quadratic strain J(x) = x squared, then x also minimizes the composition of the exponential with J. Researchers modeling continuous optimization inside the RRF interface would cite this when verifying that strictly increasing maps leave argmin sets unchanged. The proof is a one-line wrapper that invokes the monotonicity of the real exponential on the given minimizer hypothesis.
Claim. Let $J(x) = x^2$. If $x$ satisfies $J(x) = J(y)$ for no $y$ with $J(y) < J(x)$, then $e^{J(x)} = e^{J(y)}$ for no $y$ with $e^{J(y)} < e^{J(x)}$.
background
The quadratic model supplies a concrete StrainFunctional on the real line whose J-cost is the square function. The isMinimizer predicate, imported from the Strain module, declares that a state x is minimal precisely when it is weakly better than every alternative under this cost. The module itself is presented as a testing ground for continuous optimization inside the RRF interface, an abbrev that maps finite-dimensional states to real values.
proof idea
The proof is a one-line wrapper that applies Real.exp_le_exp.mpr directly to the hypothesis that x is a minimizer of quadratic1DStrain.
why it matters
The result confirms that the exponential transform preserves argmin sets inside the quadratic RRF model, reinforcing the claim that strain minimization remains the fundamental drive after monotonic reparameterization. It sits among sibling lemmas that establish uniqueness and ledger closure for the same one-dimensional quadratic. No downstream theorems are recorded, so the declaration functions as an auxiliary fact supporting further model extensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.