quadratic1D_equilibrium
plain-language theorem explainer
In the quadratic RRF model with cost functional equal to the squared Euclidean norm, the zero state satisfies the ledger balance condition that total cost vanishes. Researchers modeling continuous optimization or testing RRF equilibrium properties would cite this base case. The proof is a one-line term simplification that unfolds the balance predicate and the quadratic strain definition.
Claim. In the quadratic model on state space $ℝ$ with cost $J(x) = ‖x‖²$, the state $0$ satisfies the balance condition that total cost equals zero.
background
The module presents the quadratic model as a testbed for RRF structures on continuous state spaces, taking $J(x) = ‖x‖²$ to illustrate optimization and minimizer theorems. The isBalanced predicate, drawn from the RRF core and cosmology modules, requires that total cost on the ledger equals zero. This result instantiates the general equilibrium statement from NonlinearDynamicsFromRS that J-cost vanishes at equilibrium.
proof idea
The proof is a term-mode one-liner that applies simp to the definitions of StrainFunctional.isBalanced and quadratic1DStrain, reducing the claim directly to the evaluation of the cost at zero.
why it matters
This theorem supplies the equilibrium fact used by quadratic1D_hasUniqueMin to prove uniqueness of the minimum and by quadratic1DOctave_wellPosed to establish well-posedness of the octave model. It confirms that the RRF balance condition holds inside the quadratic setting, aligning with the equilibrium step in the forcing chain and the J-cost vanishing property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.