quadratic1D_hasUniqueMin
plain-language theorem explainer
The one-dimensional quadratic strain functional admits a unique equilibrium at the origin. Researchers embedding continuous optimization into the RRF framework cite this result to verify that the squared-norm cost satisfies the core unique-minimizer requirement. The term proof supplies zero as the balanced point via the equilibrium lemma and reduces every other candidate to it by the uniqueness companion.
Claim. Let $S$ be the quadratic strain functional on $ℝ$ with $J(x)=x^2$. Then there exists a unique $x∈ℝ$ such that $S$ is balanced at $x$.
background
The quadratic model sets State to $ℝ$ and defines the cost functional by the squared Euclidean norm, providing a concrete continuous-optimization instance inside the RRF setting. The predicate hasUniqueMin, imported from RRF.Core.Strain, asserts exactly one point where the strain functional is balanced. The module doc describes this construction as a testing ground for minimizer theorems.
proof idea
The term proof supplies the witness 0, applies quadratic1D_equilibrium to establish that the origin is balanced, then invokes quadratic1D_unique_equilibrium to convert any other balanced point into equality with zero.
why it matters
This theorem verifies that the quadratic model satisfies the unique-minimizer property required by RRF.Core.Strain. It supports the module's goal of demonstrating that RRF structures can host continuous optimization. No downstream theorems yet depend on it, leaving open its integration into larger ledger or octave constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.