PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck 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 pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound

Statement

Let $g > 0$ and $l > 0$ , put $ω : = (g / l)^{1 / 2} > 0$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ), and define the field

$F : R^{2} \to R^{2}, F (θ, v) : = (v, - ω^{2} \sin θ),$

so that $z^{'} = F (z)$ for $z = (θ, v)$ is the first-order form of the pendulum equation $θ^{''} = - ω^{2} \sin θ$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral for the componentwise first-order reduction). Put

$A : = (\begin{array}{cc} 0 & 1 \\ - ω^{2} & 0 \end{array}), L : = \max {1, ω^{2}} .$

Then:

$F$ is of class $C^{\infty}$ (in particular continuous and locally Lipschitz in the state variable), $F (0) = 0$ , $A = D F (0)$ is the total derivative of $F$ at the origin, and for every $r > 0$ and every $z = (θ, v)$ with $∥ z ∥_{2} \leq r$ (Open ball, closed ball and sphere in a metric space for the ball, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ for the norm)

$∥ F (z) - A z ∥_{2} = ω^{2} ∣ \sin θ - θ ∣ \leq \frac{ω^{2}}{6} ∣ θ ∣^{3} \leq \frac{ω^{2} r}{6} ∥ z ∥_{2}^{2}, ∥ F (z) ∥_{2} \leq L ∥ z ∥_{2};$

moreover $F$ is globally Lipschitz in the state variable with constant $L$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction), and the operator norm of $A$ for the Euclidean norm is $∥ A ∥ = L$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum); 2. let $z_{0} \in R^{2}$ with $δ : = ∥ z_{0} ∥_{2} > 0$ , let $T > 0$ and $r > 0$ satisfy $δ e^{L T} < r$ , and let $y : R \to R^{2}$ be the solution of the linear initial value problem $y^{'} = A y$ , $y (0) = z_{0}$ (Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential). Then the maximal solution $z$ of $z^{'} = F (z)$ , $z (0) = z_{0}$ , is defined on $[0, T]$ with $∥ z (t) ∥_{2} \leq δ e^{L t}$ for $t \in [0, T]$ , and for every $t \in [0, T]$

$∥ z (t) - y (t) ∥_{2} \leq \frac{ω^{2} r}{6} δ^{2} \int_{0}^{t} e^{∥ A ∥ (t - s)} e^{2 L s} d s \leq \frac{ω^{2} r}{6} δ^{2} t e^{(∥ A ∥ + 2 L) t}$

(Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate); 3. the linear system $y^{'} = A y$ is the linearised pendulum: writing $y = (y_{1}, y_{2})$ one has $y_{1}^{''} = - ω^{2} y_{1}$ and $y_{2} = y_{1}^{'}$ , and the first components satisfy $∣ z_{1} (t) - y_{1} (t) ∣ \leq ∥ z (t) - y (t) ∥_{2}$ with the bounds of clause 2. The estimate is a finite-time statement of order $δ^{2}$ : it neither states nor implies that the nonlinear pendulum is exactly harmonic, and it makes no claim beyond $[0, T]$ .

Facts & Assumptions

Given: The parameters $g > 0$ , $l > 0$ , the number $ω = (g / l)^{1 / 2}$ , the field $F (θ, v) = (v, - ω^{2} \sin θ)$ , the matrix $A$ and the constant $L = \max {1, ω^{2}}$ .

[F1]

The linearisation theorem (Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate): if $F : U \to R^{n}$ is continuous and locally Lipschitz in the state variable on an open $U ∋ 0$ , and $r > 0$ , $C \geq 0$ , $L \geq 0$ , $A \in M_{n} (R)$ satisfy $\overline{B} (0, r) \subseteq U$ , $∥ F (z) - A z ∥_{2} \leq C ∥ z ∥_{2}^{2}$ , $∥ F (z) ∥_{2} \leq L ∥ z ∥_{2}$ for $∥ z ∥_{2} \leq r$ , then for every datum with $δ : = ∥ z_{0} ∥_{2} > 0$ and every $T > 0$ with $δ e^{L T} < r$ the maximal solution $z$ of $z^{'} = F (z)$ , $z (0) = z_{0}$ is defined on $[0, T]$ , satisfies $∥ z (t) ∥_{2} \leq δ e^{L t}$ , and with the solution $y$ of $y^{'} = A y$ , $y (0) = z_{0}$ obeys the two displayed bounds with $∥ A ∥$ the operator norm.

[F2]

Trigonometric calculus (The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series, Signs, monotonicity intervals, and ranges of sine and cosine, The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ , A uniform derivative bound gives a uniform Taylor remainder bound, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ): $\sin$ and $\cos$ are differentiable with $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , $\sin 0 = 0$ ; both have range $[- 1, 1]$ ; for all reals $θ, θ^{'}$ the mean value theorem gives $∣ \sin θ - \sin θ^{'} ∣ \leq ∣ θ - θ^{'} ∣$ and $∣ \sin θ ∣ \leq ∣ θ ∣$ ; and the Taylor remainder bound with $n = 2$ and $M = 1$ gives $∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6$ for every real $θ$ .

[F3]

Total derivative (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, $C^{k}$ Euclidean maps and diffeomorphisms): the partial derivatives of $F$ are $\partial F_{1} / \partial θ = 0$ , $\partial F_{1} / \partial v = 1$ , $\partial F_{2} / \partial θ = - ω^{2} \cos θ$ , $\partial F_{2} / \partial v = 0$ , all continuous, so $F$ is $C^{1}$ with $D F (θ, v) = (\begin{array}{cc} 0 & 1 \\ - ω^{2} \cos θ & 0 \end{array})$ ; a $C^{1}$ map is continuous and locally Lipschitz in the state variable (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F4]

Norms (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Real and complex inner product spaces, with the inner product linear in the first argument, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Open ball, closed ball and sphere in a metric space): for $z = (θ, v)$ , $∥ z ∥_{2}^{2} = θ^{2} + v^{2}$ , $∥ A z ∥_{2}^{2} = ω^{4} θ^{2} + v^{2}$ , $∥ F (z) ∥_{2}^{2} = v^{2} + ω^{4} \sin^{2} θ$ and $∥ F (z) - A z ∥_{2}^{2} = ω^{4} (\sin θ - θ)^{2}$ ; the operator norm of $A$ is the supremum of $∥ A z ∥_{2}$ over $∥ z ∥_{2} \leq 1$ .

[F5]

Linear systems (Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes): for every datum there is exactly one solution of $y^{'} = A y$ on $R$ ; the equation $y^{'} = A y$ is the pair $y_{1}^{'} = y_{2}$ , $y_{2}^{'} = - ω^{2} y_{1}$ .

Proof

Proof technique: direct; compute the derivative of the pendulum field, bound the quadratic remainder by the cubic sine estimate, identify the Lipschitz and operator norms, and instantiate the linearisation theorem.

1.1givenF2F3algebra

Derivative and regularity: by [F3], $F$ is $C^{1}$ with $D F (θ, v) = (\begin{array}{cc} 0 & 1 \\ - ω^{2} \cos θ & 0 \end{array})$ ; since $\sin$ and $\cos$ are $C^{\infty}$ the field is in fact $C^{\infty}$ . Also $F (0, 0) = (0, - ω^{2} \sin 0) = (0, 0)$ and $A = D F (0, 0) = (\begin{array}{cc} 0 & 1 \\ - ω^{2} & 0 \end{array})$ .

1.2givenF2F4algebra

Remainder and growth bounds: for $∥ z ∥_{2} \leq r$ , [F2] gives $∥ F (z) - A z ∥_{2} = ω^{2} ∣ \sin θ - θ ∣ \leq \frac{ω^{2}}{6} ∣ θ ∣^{3}$ , and $∣ θ ∣^{3} \leq r θ^{2} \leq r (θ^{2} + v^{2}) = r ∥ z ∥_{2}^{2}$ ; moreover $∥ F (z) ∥_{2}^{2} = v^{2} + ω^{4} \sin^{2} θ \leq v^{2} + ω^{4} θ^{2} \leq L^{2} (θ^{2} + v^{2})$ because $L = \max {1, ω^{2}}$ , so $∥ F (z) ∥_{2} \leq L ∥ z ∥_{2}$ .

2.1step 1.2F2F4algebra

Lipschitz constant and operator norm: for $z = (θ, v)$ and $z^{'} = (θ^{'}, v^{'})$ , $∥ F (z) - F (z^{'}) ∥_{2}^{2} = (v - v^{'})^{2} + ω^{4} (\sin θ - \sin θ^{'})^{2} \leq (v - v^{'})^{2} + ω^{4} (θ - θ^{'})^{2} \leq L^{2} ∥ z - z^{'} ∥_{2}^{2}$ by [F2] and $L = \max {1, ω^{2}}$ , so $L$ is a global Lipschitz constant for $F$ ; and $∥ A z ∥_{2}^{2} = ω^{4} θ^{2} + v^{2} \leq L^{2} ∥ z ∥_{2}^{2}$ with equality at $e_{1}$ if $ω^{2} \geq 1$ and at $e_{2}$ if $1 \geq ω^{2}$ , so the operator norm is $∥ A ∥ = L$ .

3.1step 1.1step 1.2step 2.1F1given

Instantiation of the linearisation theorem: take $n = 2$ , $U = R^{2}$ , the field $F$ of clause 1, the matrix $A$ , the constants $L$ and $C : = ω^{2} r / 6$ , and the datum $z_{0}$ with $δ = ∥ z_{0} ∥_{2} > 0$ and $δ e^{L T} < r$ . Steps 1.1, 1.2 and 2.1 verify every hypothesis of [F1], so the maximal solution $z$ of $z^{'} = F (z)$ , $z (0) = z_{0}$ is defined on $[0, T]$ , $∥ z (t) ∥_{2} \leq δ e^{L t}$ there, and the two integral bounds of [F1] hold with the displayed $C$ and $∥ A ∥ = L$ ; this is clause 2.

4.1step 3.1F4F5algebra∎

Linearised equation and scope: by [F5] the system $y^{'} = A y$ reads $y_{1}^{'} = y_{2}$ , $y_{2}^{'} = - ω^{2} y_{1}$ , hence $y_{1}^{''} = - ω^{2} y_{1}$ , the exactly harmonic linearised pendulum; and $∣ z_{1} (t) - y_{1} (t) ∣ \leq ∥ z (t) - y (t) ∥_{2}$ because $∥ (w_{1}, w_{2}) ∥_{2}^{2} = w_{1}^{2} + w_{2}^{2}$ . The bounds of clause 2 are finite-time and of order $δ^{2}$ ; no identification of the nonlinear solution with the harmonic one beyond this estimate is claimed.

Remarks

The constant $ω^{2} r / 6$ is exactly the quadratic-remainder constant obtained from the cubic bound $∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6$ on the ball of radius $r$ : the remainder is cubic in the angle and quadratic in the state norm, which is what the linearisation theorem of Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate requires.
The scope sentence of clause 3 is part of the claim: the estimate is a conditional consequence of the explicit model $θ^{''} = - ω^{2} \sin θ$ and its stated smallness hypotheses, and it is not a statement about any measured pendulum.

The pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources