ExampleConstruction: AI-adaptedVerification: 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.

The harmonic oscillator on a long interval: the stationary curve is neither a local minimum nor a local maximum

Physical scope

A worked check that stationarity is not minimisation, on a harmonic oscillator embedded in three-dimensional configuration space and moving along one fixed unit vector, with positive stiffness: on intervals longer than pi divided by the angular frequency, arbitrarily small fixed-endpoint variations in the declared dimensionless C^2 metric around the zero stationary curve produce both strictly larger and strictly smaller actions, so the stationary curve is neither a local minimiser nor a local maximiser; on shorter intervals every sine-mode variation in the checked family increases the action. The computation uses exact model actions and exact trigonometric integrals; no experimental values are reported.

Example

Fix a duration $T > 0$ and declare a one-label model of the force branch of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance with $N = 1$ , mass $m > 0$ , time window $I_{0} = R$ , configuration domain $Q = R^{3}$ , a fixed unit vector $e \in R^{3}$ with dimensionless components, and force map $F (t, x, v) = - k (e \cdot x) e$ with constant $k > 0$ . This is the global potential model with $U (x) = \frac{1}{2} k (e \cdot x)^{2}$ and no residual forces (Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets), with mechanical Lagrangian $L (t, x, v) = \frac{1}{2} m ∣ v ∣_{2}^{2} - \frac{1}{2} k (e \cdot x)^{2}$ (The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions). Under Dimensions and SI unit conventions of the non-relativistic classical mechanics framework, $[m] = μ$ , $[e] = 1$ , $[x] = ℓ$ , $[t] = [T] = τ$ , $[k] = μ τ^{- 2}$ , $[ω] = τ^{- 1}$ and $[ℓ_{0}] = ℓ$ , where $ω : = \sqrt{k / m} > 0$ . Fix a length scale $ℓ_{0} > 0$ and let $η_{n} (t) : = ℓ_{0} \sin (n π t / T) e$ ; the scalar $ε$ below is dimensionless. Consider curves on $[0, T]$ .

Then:

the zero curve $x_{*} \equiv 0$ is stationary for the action $S$ ;
for every integer $n \geq 1$ the map $η_{n}$ is a variation of $x_{*}$ , and for every dimensionless real $ε$ one has the exact identity $S (ε η_{n}) = \frac{m T ℓ_{0}^{2}}{4} ε^{2} ((\frac{n π}{T})^{2} - ω^{2});$
if $T > π / ω$ , then $S (ε η_{1}) < 0$ and $S (ε η_{n}) > 0$ for every integer $n > ω T / π$ and every $ε \neq 0$ ; since $ε η_{n} \to 0$ in the dimensionless $C^{2}$ metric defined below as $ε \to 0$ , the stationary curve $x_{*}$ is neither a local minimiser nor a local maximiser in that topology;
if $0 < T < π / ω$ , then $S (ε η_{n}) > 0$ for every $n \geq 1$ and every $ε \neq 0$ : every variation in this family increases the action, and no claim of global minimality is made.

Facts & Assumptions

Given: The model data of the Example, $T > 0$ , the zero curve $x_{*}$ , the maps $η_{n} (t) = ℓ_{0} \sin (n π t / T) e$ , and a dimensionless real $ε$ .

[F1]

The model and its stationarity criterion (The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions, The stationary-action criterion and the potential-part Euler-Lagrange equation): $x_{*}$ is stationary if and only if $m x^{''} (t) = - k (e \cdot x (t)) e$ for all $t \in [0, T]$ ; the zero curve satisfies this.

[F2]

Trigonometric facts (Sine and cosine defined by their real power series, The derivatives of sine and cosine are cosine and minus sine, A function differentiable at $c$ is continuous at $c$ , The addition formulas for sine and cosine, The zero sets of sine and cosine and the least positive common period 2 pi, Parity and the Pythagorean identity for sine and cosine): $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , the product-to-sum identity $2 \sin^{2} u = 1 - \cos (2 u)$ (the addition formula for the cosine with $u = u$ ), the basic values $\sin 0 = 0$ , $\cos 0 = 1$ and $\sin (m π) = 0$ for every integer $m$ , and $\sin^{2} + \cos^{2} = 1$ ; iterating the derivative identities twice gives $η_{n} \in C^{2}$ , since the derivatives through order two are scalar multiples of $\sin$ or $\cos$ , which are continuous by differentiability and A function differentiable at $c$ is continuous at $c$ . Consequently $e \cdot η_{n} (t) = ℓ_{0} \sin (n π t / T)$ and $η_{n}^{'} (t) = ℓ_{0} (n π / T) \cos (n π t / T) e$ , while $η_{n}$ vanishes at $t = 0$ and $t = T$ for every integer $n \geq 1$ .

[F3]

Integral and order calculus (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Absolute value in an ordered field): the integral is linear, continuous integrands are integrable, and for $α \neq 0$ the function $t \mapsto \sin (α t) / α$ is a primitive of $t \mapsto \cos (α t)$ on $[0, T]$ by the chain rule and the fundamental theorem; hence $\int_{0}^{T} \cos (α t) d t = (\sin (α T) - \sin 0) / α$ . The Archimedean property gives, for $T > π / ω$ , an integer $n > ω T / π$ (Every complete ordered field is Archimedean); and $ω = \sqrt{k / m}$ exists uniquely by Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ .

[F4]

The topology used for local extrema: on $C^{2}$ curves $h : [0, T] \to R^{3}$ define $d_{T, ℓ_{0}} (f, g) : = \sup_{t \in [0, T]} (\frac{∣ f (t) - g (t) ∣_{2}}{ℓ_{0}} + \frac{T ∣ f^{'} (t) - g^{'} (t) ∣_{2}}{ℓ_{0}} + \frac{T^{2} ∣ f^{''} (t) - g^{''} (t) ∣_{2}}{ℓ_{0}}) .$ This is a dimensionless metric: finiteness follows from continuity on the compact interval $[0, T]$ (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value), and the metric axioms follow componentwise from the Euclidean norm and its triangle inequality (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation). A local minimiser or maximiser means one relative to the fixed-endpoint $C^{2}$ curve class with this metric. For fixed $n$ , $d_{T, ℓ_{0}} (ε η_{n}, 0) \leq ∣ ε ∣ (1 + n π + n^{2} π^{2})$ by the trigonometric bounds, so it tends to zero as $ε \to 0$ .

Verification

technique · direct; evaluate the action of the scaled sine variations in closed form and read off the two signs

1.1F1F2given

Stationarity of the zero curve: $M x^{''} = m \cdot 0 = - k (e \cdot 0) e$ on $[0, T]$ , so by [F1] $x_{*}$ is stationary; and each $η_{n}$ is a variation because it is $C^{\infty}$ on $[0, T]$ with $η_{n} (0) = η_{n} (T) = 0$ by [F2].

1.2F2F3algebra

The two integrals: with $α : = 2 n π / T \neq 0$ and the product-to-sum identity $2 \sin^{2} u = 1 - \cos (2 u)$ of [F2] applied to $u = n π t / T$ , the linearity of the integral and the primitive of [F3] give $\int_{0}^{T} (e \cdot η_{n} (t))^{2} d t = \frac{ℓ_{0}^{2}}{2} \int_{0}^{T} (1 - \cos (α t)) d t = ℓ_{0}^{2} T / 2,$ because $α T = 2 n π$ is an integer multiple of $2 π$ and $\sin (2 n π) = 0 = \sin 0$ by [F2]; and $\int_{0}^{T} ∣ η_{n}^{'} (t) ∣_{2}^{2} d t = ℓ_{0}^{2} (n π / T)^{2} \int_{0}^{T} \cos (n π t / T)^{2} d t = ℓ_{0}^{2} (n π / T)^{2} T / 2,$ using $\cos^{2} = 1 - \sin^{2}$ of [F2] and the value just computed.

2.1F3step 1.2algebra

Exact action of the scaled variation: since $x_{*} = 0$ and the integrand is quadratic, for every dimensionless real $ε$ one has $S (ε η_{n}) = \frac{ε^{2}}{2} \int_{0}^{T} (m ∣ η_{n}^{'} (t) ∣_{2}^{2} - k (e \cdot η_{n} (t))^{2}) d t = \frac{ε^{2}}{2} (m \int_{0}^{T} ∣ η_{n}^{'} ∣_{2}^{2} d t - k \int_{0}^{T} (e \cdot η_{n})^{2} d t) .$ Inserting the two integrals of step 1.2 gives $S (ε η_{n}) = \frac{ε^{2}}{2} \cdot \frac{ℓ_{0}^{2} T}{2} (m (\frac{n π}{T})^{2} - k) = \frac{m T ℓ_{0}^{2}}{4} ε^{2} ((\frac{n π}{T})^{2} - ω^{2}),$ using $k = m ω^{2}$ with $ω = \sqrt{k / m}$ of [F3]. This proves clause 2.

3.1F3step 2.1algebra

Signs for $T > π / ω$ : the coefficient $((n π / T)^{2} - ω^{2})$ is negative for $n = 1$ because $π / T < ω$ ; it is positive for every integer $n > ω T / π$ because then $n π / T > ω$ ; both statements are read off the identity of step 2.1, and [F3] provides such an integer. Hence for $ε \neq 0$ the actions $S (ε η_{1})$ and $S (ε η_{n})$ differ in sign from $S (x_{*}) = 0$ .

3.2F3step 2.1algebra

Signs for $0 < T < π / ω$ : then $π / T > ω$ , hence $(n π / T)^{2} \geq (π / T)^{2} > ω^{2}$ for every $n \geq 1$ , and step 2.1 gives $S (ε η_{n}) > 0$ for $ε \neq 0$ . This is a statement about this family of variations only; no global minimality is asserted.

4.1F4step 3.1

Smallness: by [F4] the curves $ε η_{n}$ converge to $x_{*}$ in the declared dimensionless $C^{2}$ metric as $ε \to 0$ , so every neighbourhood of $x_{*}$ in the fixed-endpoint curve class contains curves of strictly smaller and of strictly larger action by step 3.1; the zero curve is neither a local minimiser nor a local maximiser.

5.1step 1.1step 2.1step 3.1step 4.1step 3.2∎

Clauses 1-4 are proved; all quantities are exact model values under the declared oscillator idealization.

Remarks

The computation shows the explicit threshold: for $T < π / ω$ the oscillator's zero curve increases the action along every sine-mode variation, while for $T > π / ω$ both signs occur. The mathematical analogue with the dimensionless Lagrangian $\frac{1}{2} (v^{2} - ω^{2} q^{2})$ and its second variation is recorded in the verification page of the mathematics track.

The harmonic oscillator on a long interval: the stationary curve is neither a local minimum nor a local maximum

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources