Alphabeta Math
Physics theoremStatement: AI-adaptedProof: AI-adaptedprecheck pass
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A strict local minimum of the potential is a Lyapunov stable equilibrium of the conservative one-dimensional model, and its linearisation is an oscillator-type model

Physical scope

The equilibrium theory of a conservative one-dimensional model near a strict local minimum of its potential: the rest point is Lyapunov stable, with the Euclidean phase-plane norm, and its linearisation is the oscillator-type model with data (m,0,U''(x_),0), which is the harmonic model with spring constant U''(x_) when that number is positive. The statement is conditional on the declared potential and its strict local minimum; it asserts no asymptotic stability, no attraction and no instability in any case, and no measured value.

Statement

Adopt a conservative one-dimensional model as in Existence, uniqueness and conservation of energy for a one-dimensional conservative model: phase curves lie in energy level sets and the velocity is determined by the position and energy up to sign: the class of The one-dimensional force models: data, motions, phase system, potential presentation, energy and equilibria with force law F(x)=−U′(x) for a potential U:Q→R of class C2, phase system GF(x,v)=(v,−U′(x)/m) on Q×R, and energy E=12mv2+U. Let x∗∈Q be a strict local minimum of U: there is r0>0 with B‾(x∗,r0)⊆Q and U(x)>U(x∗) for 0<∣x−x∗∣<r0. Then:

  1. Lyapunov stability. (x∗,0) is a Lyapunov stable rest point of the phase system in the sense of Equilibria, Lyapunov stability and asymptotic stability of an autonomous first-order system: for every ε>0 with B‾((x∗,0),ε)⊆Q×R there is δ>0 such that the unique maximal solution of the autonomous phase equation through the datum of every motion x of the model with ∥(x(t0),x′(t0))−(x∗,0)∥2<δ for some t0∈I0 is defined for all t≥t0 and satisfies ∥(x(t)−x∗, x′(t))∥2<ε(t≥t0). Here x in the displayed all-time bound denotes that maximal extension; on the original motion interval it agrees with the given motion. The autonomous equation is read on R×Q×R, even when the declared time window I0 is smaller; no enlargement of that declared window is asserted. The norm is the Euclidean norm on R2 of The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn; the balls are those of Open ball, closed ball and sphere in a metric space. No asymptotic stability and no attraction are asserted.

  2. Linearisation. U′′(x∗) exists (Ck Euclidean maps and diffeomorphisms), the phase field GF is totally differentiable at (x∗,0) with DGF(x∗,0)(δx,δv)=(δv, −U′′(x∗)m δx), and the linearised equation is m ξ′′+U′′(x∗) ξ=0, which is the equation of the oscillator-type model of clause (f) of The one-dimensional force models: data, motions, phase system, potential presentation, energy and equilibria with data (m,0,U′′(x∗),0) (The damped driven oscillator model: second-order equation, phase-plane system and characteristic data). If in addition U′′(x∗)>0, then that linearised model is the harmonic model of The harmonic (linear restoring) model: a declared linear force law with parameter k>0 with spring constant U′′(x∗), and its undamped frequency in the sense of The damped driven oscillator model: second-order equation, phase-plane system and characteristic data is U′′(x∗)/m.

The statement is conditional on the potential U and on the strict local minimum; no conclusion is drawn for a critical point that is only a weak minimum, a maximum, or a point where U′′ vanishes identically on one side.

Facts & Assumptions

Given: The conservative one-dimensional model with potential U, the strict local minimum x∗, and the quantity D2U:=U′′(x∗).

[L1]

The phase field GF(x,v)=(v,−U′(x)/m) is exactly the mechanical vector field of The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart with n=1, Ω:=Q, the constant kinetic metric field M(x)≡m (symmetric positive definite, of class C2 because it is constant), and the potential U: for a constant field M, DqM=0 and ∇q(12vTMv)=0, so the second component of G is M(x)−1(0−0−U′(x))=−U′(x)/m. Its energy E(x,v)=12vTMv+U(x) is the energy of The phase plane of a one-dimensional model: phase curves, the energy function and its level sets, and turning points clause (b). [given, The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart]

[L2]

A strict local minimum of the potential gives a Lyapunov stable equilibrium of the mechanical system, by energy conservation: for n≥1, an open Ω⊆Rn, a C2 field M of symmetric positive definite matrices, a C2 potential U and a strict local minimum q0 of U, the point (q0,0) is a Lyapunov stable equilibrium of the mechanical system of [L1]'s definition: for every ε>0 with B‾((q0,0),ε)⊆Ω×Rn there is δ>0 such that every maximal solution (q,v) with ∥(q(0),v(0))−(q0,0)∥2<δ is defined for all t≥0 and satisfies ∥(q(t),v(t))−(q0,0)∥2<ε for every t≥0. The statement uses no asymptotic stability.

[L3]

Linearisation of the mechanical system at an equilibrium: M(q_0) xi'' + D²U(q_0) xi = 0, and the small-oscillation quadratic model: at a mechanical equilibrium q0 of the data of [L1]'s definition, the mechanical vector field is totally differentiable at (q0,0) with DG(q0,0)(δq,δv)=(δv,−M(q0)−1D2U(q0)δq); the linearised equation is M(q0)ξ′′+D2U(q0)ξ=0.

[L4]

Model definitions (The one-dimensional force models: data, motions, phase system, potential presentation, energy and equilibria clauses (b), (e), (f), The damped driven oscillator model: second-order equation, phase-plane system and characteristic data, The harmonic (linear restoring) model: a declared linear force law with parameter k>0): motions of the model are exactly the curves whose phase curves solve z′=GF(z) on intervals J⊆I0; x∗ is an equilibrium exactly when U′(x∗)=0, which holds at a strict local minimum; the oscillator-type data (m,0,k,0) with k=U′′(x∗) have equation mξ′′+kξ=0; and the harmonic model of the postulate has force law −kx and potential 12kx2.

[L5]

Since U is C2, the unrestricted autonomous phase field (t,x,v)↦(v,−U′(x)/m) is C1 on R×Q×R. It is continuous and locally Lipschitz in the state, locally uniformly in time, by A C1 map is locally Lipschitz on compact coordinate subsets. Thus Every Picard–Lindelöf initial value problem has one maximal solution on an open interval gives a unique maximal solution through each datum; every solution through that datum is its restriction.

Proof

Proof technique: direct; identify the scalar phase system with the one-dimensional instance of the mathematical mechanical system, apply the energy-stability theorem to it, and read the linearisation from the linearisation proposition.

1.1givenL1L4

By [L1] the phase field GF of the model is the mechanical vector field of the mathematical data (n,Ω,M,U)=(1,Q,m,U) with the constant positive definite metric field M≡m. On intervals J⊆I0, the phase curves of model motions are exactly the solutions (q,v) of that mechanical system; unrestricted solutions are model motions only on their restrictions to the declared time window. Its energy is E. At the strict minimum, the difference quotient (U(x∗+h)−U(x∗))/h is nonnegative for small h>0 and nonpositive for small h<0. Its common two-sided limit U′(x∗) is therefore zero, as required by [L2] and [L3].

2.1givenstep 1.1L2L4L5

Clause 1. Let ε>0 with B‾((x∗,0),ε)⊆Q×R. Apply [L2] with Ω=Q, M≡m, the potential U and q0=x∗: it produces δ>0 such that every maximal solution (q,v) of the mechanical system with ∥(q(0),v(0))−(x∗,0)∥2<δ is defined for all t≥0 and satisfies ∥(q(t),v(t))−(x∗,0)∥2<ε for all t≥0. Now let x:J→Q be a motion of the model and t0∈J with ∥(x(t0),x′(t0))−(x∗,0)∥2<δ. The phase system is autonomous, so the translate s↦(x(t0+s),x′(t0+s)), defined for s with t0+s∈J, is a solution of the same system with initial value (x(t0),x′(t0)) at s=0; it has a unique maximal extension for this unrestricted autonomous equation by [L5], and by step 1.1 and the defining property of δ that extension is defined for all s≥0 and stays at distance <ε from (x∗,0). Translating the maximal extension back yields a maximal curve whose domain contains [t0,∞) and which agrees with x on J, and ∥(x(t)−x∗,x′(t))∥2<ε for all t≥t0. Since ε was arbitrary, (x∗,0) is Lyapunov stable in the sense of Equilibria, Lyapunov stability and asymptotic stability of an autonomous first-order system.

3.1givenstep 1.1L3L4∎

Clause 2, differentiability and linearised equation. U is C2, so D2U(x∗)=U′′(x∗) exists and x∗ is a mechanical equilibrium because U′(x∗)=0 at a strict local minimum. Applying [L3] with q0=x∗, M(q0)=m and D2U(q0)=U′′(x∗) gives the displayed total derivative and the linearised equation mξ′′+U′′(x∗)ξ=0. By [L4] this is exactly the oscillator-type model with data (m,0,U′′(x∗),0). If U′′(x∗)>0, then k:=U′′(x∗)>0 and [L4] identifies the equation with that of the harmonic model with spring constant k; the frequency k/m is the undamped frequency ω0 attached to the data (m,0,k,0) by The damped driven oscillator model: second-order equation, phase-plane system and characteristic data, and it is quoted here only as the linearised frequency, not as a property of the nonlinear motion.

Remarks

  • Stability is not attraction. Clause 1 asserts only Lyapunov stability: nearby motions stay nearby, with no claim that they approach the rest point. For the conservative model the energy is conserved, and the companion results do not make the rest point attracting; the dissipative model is where attraction is proved.

  • The weak-minimum and saddle cases are not decided here. If a critical point with vanishing U′′ is still a strict minimum, clause 1 applies; at other degenerate critical points or a strict local maximum this item says nothing about stability or instability of the rest point; the linearised model with U′′(x∗)<0 is the repulsive oscillator, whose explicit growing solution is recorded in the companion pages of the mathematics track, but transferring that growth to the nonlinear model requires a separate nonlinear argument that this page does not supply.

  • Why the identification is legitimate. The mechanical system of The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart is a mathematical chart model with an arbitrary positive definite C2 metric field; the model of this page is its one-dimensional constant-metric instance, and the identification in step 1.1 is a computation, not a modelling assumption.

Depends on

Dependency tree · 2 levels

Sources