hasUniqueMin
plain-language theorem explainer
The definition states that a strain functional S has a unique minimum precisely when exactly one state satisfies the isBalanced predicate. RRF model builders cite it to guarantee a single equilibrium in concrete strain functionals such as the quadratic case. The definition is a direct abbreviation of the unique-existence quantifier applied to the balance condition.
Claim. A strain functional $S$ on states has a unique minimum when there exists a unique state $x$ such that $S$ is balanced at $x$, written $∃! x, S.isBalanced x$.
background
The RRF.Core.Strain module treats strain as the fundamental deviation from equilibrium, with the law that strain tends to zero. A StrainFunctional is a structure assigning a non-negative real-valued cost $J$ to each state, where $J(x)=0$ if and only if the state is balanced. The module supplies the abstract interface for such functionals on an arbitrary State type.
proof idea
One-line definition that directly encodes the unique-existence quantifier $∃! x, S.isBalanced x$ as the named property hasUniqueMin.
why it matters
This definition is invoked by the downstream theorem quadratic1D_hasUniqueMin to establish uniqueness for the quadratic strain model. It supplies the uniqueness half of equilibrium statements inside the RRF framework and aligns with the J-uniqueness step (T5) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.