quadratic1DOctave_wellPosed
plain-language theorem explainer
The 1D quadratic octave possesses an equilibrium state. Researchers modeling continuous optimization in the Recognition framework cite this result to verify that the quadratic strain satisfies the minimal consistency condition for an octave. The proof is a direct term construction that supplies zero as the witness state.
Claim. Let $O$ be the octave with state space the real line and strain functional $J(x) = x^2$. Then there exists a state $x$ at which the strain is balanced.
background
The quadratic model supplies a concrete RRF instance whose state space is the real line and whose strain functional is the squared Euclidean norm. This construction tests whether RRF structures can represent continuous optimization problems. The well-posedness predicate on an octave is the existence statement that some state makes the strain balanced. The upstream quadratic1D_equilibrium theorem shows that the zero state satisfies the balance condition for this particular strain.
proof idea
The proof is a term-mode witness construction. It forms the pair consisting of the zero real number together with the quadratic1D_equilibrium theorem, thereby discharging the existential quantifier inside the wellPosed definition.
why it matters
The declaration closes the well-posedness check for the basic quadratic octave, confirming that the model meets the equilibrium-existence requirement before uniqueness or minimizer results are considered. It sits inside the RRF.Models.Quadratic module whose purpose is to demonstrate that RRF structures can encode continuous optimization. No downstream uses are recorded, so the result functions as a self-contained consistency lemma for the quadratic strain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.