quadratic1DStrain
plain-language theorem explainer
The declaration defines the one-dimensional quadratic strain functional on the real line by assigning the cost map to the square function. Researchers modeling continuous optimization in the RRF component of Recognition Science cite it as the base case for equilibrium and minimizer theorems. The construction is a direct field assignment followed by an instance that invokes the standard square non-negativity lemma.
Claim. The one-dimensional quadratic strain functional is the map $J : ℝ → ℝ$ given by $J(x) = x^2$.
background
In the RRF quadratic model the state space is the real line and a strain functional supplies a cost map J. The NonNeg class requires J(x) ≥ 0 for every real x, while equilibrium states are those at which J vanishes. The module presents this construction as a concrete testing ground for theorems about minimizers in continuous settings. Upstream results include the statement that at equilibrium J equals zero and the definition of the NonNeg structure that encodes non-negativity.
proof idea
The definition directly populates the J field with the squaring map. Non-negativity is witnessed by applying the sq_nonneg lemma pointwise.
why it matters
This supplies the concrete strain functional for the quadratic model and is invoked by the proofs that zero is the unique equilibrium, the global minimizer, and the unique minimum. It supports the construction of the associated octave and strain ledger. The model illustrates how Recognition Science structures accommodate continuous optimization while remaining compatible with equilibrium conditions from the nonlinear dynamics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.