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.

Local existence and uniqueness for the Newtonian initial-value problem, with the quantitative Picard-Lindelöf cylinder

Physical scope

The local existence, uniqueness and maximal-extension statement for the adopted Newtonian force model of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance on an open configuration domain: every initial datum with a configuration in the domain and an arbitrary coordinate velocity admits a unique motion through it, locally in time, and there is a unique maximal motion of which every motion with that datum is a restriction. The result is a conditional deduction from the adopted force postulate and the cited mathematical ODE theorems; it gives no global existence, no bound on the interval, no empirical statement and no claim that any physical system realizes the model.

Statement

Adopt the force model of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance: time window $I_{0}$ , open configuration domain $Q \subseteq R^{3 N}$ , masses $m_{1}, \dots, m_{N} > 0$ , and a force map $F$ continuous and locally Lipschitz in the state variable, locally uniformly in time, on $D = I_{0} \times Q \times (R^{3})^{N}$ . Let $F (t, x, v) = (v, M^{- 1} F (t, x, v))$ be the associated first-order field and let motions and maximal motions be as in The associated first-order system, motions, maximal motions and the Newtonian flow of a force model. Fix an initial datum $(t_{0}, x_{0}, v_{0}) \in I_{0} \times Q \times (R^{3})^{N}$ and write $z_{0} = (x_{0}, v_{0})$ .

Local existence. There is $h > 0$ and there is a motion $x$ of the model on $[t_{0} - h, t_{0} + h]$ with $x (t_{0}) = x_{0}$ and $\dot{x} (t_{0}) = v_{0}$ ; moreover such a motion is exactly one of class $C^{2}$ satisfying $m_{i} {\ddot{x}}_{i} (t) = F_{i} (t, x (t), \dot{x} (t))$ for all $i$ and all $t \in [t_{0} - h, t_{0} + h]$ .
Uniqueness. If $x : J \to Q$ and $\tilde{x} : \tilde{J} \to Q$ are motions of the model with the same initial datum, $x (t_{0}) = \tilde{x} (t_{0}) = x_{0}$ and $\dot{x} (t_{0}) = \dot{\tilde{x}} (t_{0}) = v_{0}$ , then $x = \tilde{x}$ on $J \cap \tilde{J}$ .
Quantitative cylinder. Let $h, r > 0$ satisfy $C : = [t_{0} - h, t_{0} + h] \times \overline{B} (z_{0}, r) \subseteq D$ , put $M : = \sup {∥ F (t, z) ∥_{2} : (t, z) \in C}$ and let $Λ$ be a state-Lipschitz constant of $F$ on $C$ . If $h M \leq r$ and $Λ h < 1$ , then there is exactly one motion on $[t_{0} - h, t_{0} + h]$ through the datum whose state graph $(t, (x (t), \dot{x} (t)))$ lies in $C$ , and every motion through the datum agrees with it on the intersection of its interval with $[t_{0} - h, t_{0} + h]$ .
Maximal motion. There is exactly one maximal motion with the datum: its maximal interval $J_{\max}$ is an open interval containing $t_{0}$ and contained in $I_{0}$ , and every motion with the datum is its restriction.

The statement is conditional on the adopted force model: clause 1 locates a solution only near $t_{0}$ and bounds no interval length in terms of the data, clause 4 asserts no completeness of $J_{\max}$ in $I_{0}$ , and no empirical content is claimed.

Facts & Assumptions

Given: The force model of the statement, its associated field $F$ on the open set $D$ , the initial datum $(t_{0}, x_{0}, v_{0})$ , and, for clause 3, the numbers $h, r, M, Λ$ of the statement.

[L1]

The associated first-order system, motions and their equivalence, initial data, maximal motions and maximal intervals, and the Newtonian flow are The associated first-order system, motions, maximal motions and the Newtonian flow of a force model; the state is $z = (x, v) \in Q \times R^{3 N}$ and its norm is the Euclidean norm of the concatenation $(R^{3 N} \times R^{3 N})$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ), so that $∥ z ∥_{2}^{2} = ∥ x ∥_{2}^{2} + ∥ v ∥_{2}^{2}$ .

[L2]

Force-model hypotheses (Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance, clauses (i), (iii)): $I_{0}$ is an open nondegenerate interval; $Q$ is open; $m_{i} > 0$ ; $F$ is continuous on $D$ and locally Lipschitz in the state variable $(x, v)$ , locally uniformly in time (Local Lipschitz continuity in the state variable, locally uniform in time and parameters): every compact cylinder $C \subseteq D$ carries a finite $L$ with $∥ F (t, z) - F (t, z^{'}) ∥_{2} \leq L ∥ z - z^{'} ∥_{2}$ whenever $(t, z), (t, z^{'}) \in C$ share a time coordinate.

[L3]

Picard–Lindelöf (Picard-Lindelöf local existence and uniqueness for first-order systems): if $[t_{0} - h, t_{0} + h] \times \overline{B} (z_{0}, r) \subseteq D$ for a continuous field $G$ that is locally Lipschitz in the state variable, if $∥ G ∥_{2} \leq M$ and $G$ has state-Lipschitz constant $L$ on that cylinder, and if $h M \leq r$ and $L h < 1$ , then exactly one solution of $z^{'} = G (t, z)$ , $z (t_{0}) = z_{0}$ exists on $[t_{0} - h, t_{0} + h]$ whose graph lies in the cylinder; any two solutions through the same initial data agree on every common subinterval containing $t_{0}$ .

[L4]

Maximal solutions (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval, Extensions, maximal solutions, maximal intervals, and global solutions): every initial value problem satisfying the Picard–Lindelöf hypotheses has a unique maximal solution, its domain is an open interval containing the initial time, and every other solution through the same data is its restriction.

[L5]

The Euclidean norm is a norm on $R^{m}$ , so it satisfies the triangle inequality and absolute homogeneity (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation); in particular $∥ v - v^{'} ∥_{2} \leq ∥ z - z^{'} ∥_{2}$ for states $z = (x, v)$ , $z^{'} = (x^{'}, v^{'})$ .

[L6]

A continuous real-valued function on a nonempty compact metric space attains its bounds (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value), so the supremum $M$ of clause 3 is finite and is attained.

Proof

technique · direct; verify the Picard–Lindelöf hypotheses for the associated first-order field, apply the theorem, and translate its solution back to the second-order motion

1.1L1L2L5algebra

$F$ is continuous on $D$ : its first component is the linear map $(x, v) \mapsto v$ , and its second is the composition of the continuous map $F$ with the linear map $M^{- 1}$ , so both components are continuous ([L1], [L2], algebra). $F$ is locally Lipschitz in the state variable, locally uniformly in time: let $C \subseteq D$ be a compact time-state cylinder and let $L$ be a state-Lipschitz constant of $F$ on $C$ ([L2]); then for $(t, z), (t, z^{'}) \in C$ with $z = (x, v)$ , $z^{'} = (x^{'}, v^{'})$ , the identity $F (t, z) - F (t, z^{'}) = (v - v^{'}, M^{- 1} (F (t, z) - F (t, z^{'})))$ gives, with $m_{\min} : = \min_{i} m_{i} > 0$ and $∥ M^{- 1} u ∥_{2} \leq m_{\min}^{} ∥ u ∥_{2}$ , $∥ F (t, z) - F (t, z^{'}) ∥_{2}^{2} = ∥ v - v^{'} ∥_{2}^{2} + ∥ M^{- 1} (F (t, z) - F (t, z^{'})) ∥_{2}^{2} \leq ∥ v - v^{'} ∥_{2}^{2} + \frac{L^{2}}{m_{\min}^{}} ∥ z - z^{'} ∥_{2}^{2} \leq (1 + \frac{L^{2}}{m_{\min}^{}}) ∥ z - z^{'} ∥_{2}^{2},$ so $F$ is state-Lipschitz on $C$ with constant $\sqrt{1 + L^{2} / m_{\min}^{}}$ , finite and depending on $C$ alone.

2.1step 1.1L2L3L6choosealgebra

Since $D$ is open and $(t_{0}, z_{0}) \in D$ , choose $H, r > 0$ with $C_{0} : = [t_{0} - H, t_{0} + H] \times \overline{B} (z_{0}, r) \subseteq D$ . On $C_{0}$ , step 1.1 supplies a finite state-Lipschitz constant $L$ , and [L6] gives a finite bound $M_{0} : = \sup_{C_{0}} ∥ F ∥_{2}$ . Choose $0 < h \leq \min {H, r / (M_{0} + 1), 1 / (2 (L + 1))}$ and let $C : = [t_{0} - h, t_{0} + h] \times \overline{B} (z_{0}, r)$ . Then $h M_{0} \leq r$ and $L h < 1$ , so [L3] gives exactly one solution $z$ on $[t_{0} - h, t_{0} + h]$ whose graph lies in $C$ ; its agreement clause applies to any two solutions through the datum.

2.2step 1.1L3given

For clause 3 with its own numbers $h, r, M, Λ$ : the same application of [L3] gives exactly one solution on $[t_{0} - h, t_{0} + h]$ with graph in $C$ , provided $h M \leq r$ and $Λ h < 1$ ; the agreement clause of [L3] then gives the stated uniqueness on intersections.

3.1step 2.1step 2.2L1algebra

Write the solution of step 2.1 as $z (t) = (x (t), v (t))$ . From $z^{'} = F (t, z)$ we get $x^{'} = v$ and $v^{'} = M^{- 1} F (t, x, v)$ ; hence $v$ is $C^{1}$ and $x$ is $C^{2}$ on $[t_{0} - h, t_{0} + h]$ , and multiplying $v^{'} = M^{- 1} F (t, x, v)$ by the masses returns $m_{i} {\ddot{x}}_{i} (t) = F_{i} (t, x (t), \dot{x} (t))$ for every $i$ ; moreover $x (t) \in Q$ and $t \in I_{0}$ because $(t, z (t)) \in C \subseteq D$ , and $x (t_{0}) = x_{0}$ , $\dot{x} (t_{0}) = v (t_{0}) = v_{0}$ . By the equivalence of clause (c) of [L1], $x$ is a motion of the model on $[t_{0} - h, t_{0} + h]$ ; this proves clause 1 and, with clause 3's cylinder hypotheses, the existence half of clause 3.

3.2step 2.1L1L3

Uniqueness: let $x : J \to Q$ and $\tilde{x} : \tilde{J} \to Q$ be motions with the same datum and let $z = (x, \dot{x})$ , $\tilde{z} = (\tilde{x}, \dot{\tilde{x}})$ be their state curves; by [L1] both solve $z^{'} = F (t, z)$ through $(t_{0}, z_{0})$ on their intervals, so the uniqueness clause of [L3] applied on a common cylinder gives $z = \tilde{z}$ on $J \cap \tilde{J}$ , hence $x = \tilde{x}$ there; this proves clause 2 and the uniqueness half of clause 3.

4.1step 3.2L1L4∎

Clause 4: by step 1.1 the field $F$ satisfies the Picard–Lindelöf hypotheses at every point of $D$ , so [L4] provides a unique maximal solution $z_{\max}$ of the associated first-order system through $(t_{0}, z_{0})$ whose domain is an open interval containing $t_{0}$ and contained in $I_{0}$ , every other solution through the datum being its restriction; writing $z_{\max} = (x_{\max}, {\dot{x}}_{\max})$ with $x_{\max}$ the corresponding motion by [L1], every motion with the datum is a restriction of $x_{\max}$ by step 3.2 and the equivalence of [L1]; this proves clause 4.

Remarks

What the theorem does not give. No growth bound, no lower bound on $h$ uniform over data, and no global existence in time; the interval length in clause 1 depends on the local Lipschitz data of $F$ near the datum through the cylinder construction of [L3]. Escape from the domain at a finite time is the subject of Maximal Newtonian motions and the compact-continuation criterion: finite-time breakdown requires escape from every compact subset of the time-state domain.
The regularity hypotheses are exactly used. Clause (iii) of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance supplies continuity and the state-local Lipschitz property, which are the two hypotheses of [L3]; neither is strengthened nor weakened here, and the companion counterexample on the examples page shows that continuity alone does not give clause 2.

Local existence and uniqueness for the Newtonian initial-value problem, with the quantitative Picard-Lindelöf cylinder

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources