quadratic1D_hasUniqueMin
plain-language theorem explainer
The one-dimensional quadratic strain functional on the real line has a unique equilibrium at the origin. Modelers of continuous optimization within the Recognition framework cite this result to confirm that the quadratic case satisfies the core RRF balance condition. The proof supplies the candidate point zero and invokes the companion equilibrium and uniqueness lemmas to close the existence and uniqueness clauses.
Claim. Let $S$ be the strain functional on $ℝ$ with cost $J(x)=x^2$. Then there exists a unique $x∈ℝ$ such that $S$ is balanced at $x$.
background
The quadratic model takes State = $ℝ$ and cost functional $J(x)=‖x‖^2$, serving as a test case for RRF structures that perform continuous optimization. The predicate hasUniqueMin on a StrainFunctional asserts existence of exactly one balanced point, i.e., a unique equilibrium. The local module setting presents this model as non-trivial yet simple enough to verify minimizer theorems directly.
proof idea
The term proof supplies the candidate 0, applies the quadratic1D_equilibrium lemma to confirm it is balanced, and then uses quadratic1D_unique_equilibrium to establish that every other candidate fails the balance condition.
why it matters
This theorem verifies that the quadratic model meets the unique-minimum requirement built into the RRF core, completing a basic sanity check for the continuous case described in the module documentation. It supports downstream constructions such as the quadratic ledger and octave well-posedness statements within the same file. No open questions are flagged by the declaration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.