quadratic1D_unique_equilibrium
plain-language theorem explainer
In the quadratic one-dimensional RRF model with cost functional equal to the squared state variable, the zero-strain balance condition holds precisely when the state variable is at the origin. Researchers studying continuous optimization and minimizer theorems in Recognition Science frameworks would cite this uniqueness result. The proof is a direct term-mode simplification that unfolds the strain functional and model definitions.
Claim. Let $J(x) = x^2$ be the quadratic cost functional on the real line. The zero-strain balance condition holds if and only if $x = 0$.
background
The module presents the quadratic model as a concrete case with state space the real numbers and cost functional the squared Euclidean norm. This serves as a testing ground for optimization results inside Recognition Science structures. The isBalanced predicate is the zero-strain condition requiring total cost to vanish, specialized from the general strain functional definition.
proof idea
This is a one-line term proof that applies simplification to the definitions of the strain functional isBalanced and the quadratic model, reducing the biconditional directly to the algebraic fact that a real square vanishes only at zero.
why it matters
The result supplies the uniqueness step required to conclude that the quadratic model has a unique global minimum at the origin. It supports the framework's examination of equilibria and minimizers in simple models that test J-cost balance properties. It aligns with the emphasis on fixed-point behavior without invoking the full forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.