Physlib

PhyslibAlpha.ClassicalMechanics.NortonDome.NewtonianSystem

Conservative Newtonian systems and determinism

i. Overview

A conservative Newtonian system is a point mass `m` in a configuration space `X` under a potential `V`, with equation of motion `m r̈ = -∇V(r)`. Physics takes for granted that position and velocity at one instant fix the motion at all instants. This file makes that a theorem and states what it costs.

The main result is `NewtonianSystem.isDeterministic_of_hasLocallyLipschitzForce`: if the force is locally Lipschitz, two solutions with the same position and velocity at one instant coincide at every instant; in the form usually quoted, `NewtonianSystem.isDeterministic_of_hasC2Potential`, a `C²` potential suffices. Continuity of the force is not enough: the Norton dome has a continuous force and a `C¹` potential, and a particle at rest on its apex may stay or leave at any time (see `NortonDome.Determinism`).

The `NewtonianSystem` defined here asks only for a differentiable potential, the least under which the equation of motion makes sense. Newton's laws, as stated, are silent on how regular the force must be, and the dome shows that without some regularity the equation does not determine the motion. A definition that is to be deterministic must add something the laws do not state, a regularity condition on the force or a restriction on the admissible motions; whether that is part of the theory or a choice about it is debated. Each candidate condition is a separate predicate, so that what it buys is a theorem, and the file takes no side. The predicates are:

- `IsDeterministic`: position and velocity at one instant fix the solution. - `SatisfiesFirstLaw`: a body at rest where the force vanishes stays at rest. It follows from determinism and is the form of the first law the dome violates. The interval reading follows from the second law for every system (`IsSolution.deriv_eq_of_force_eq_zero_on`, section B.3). - `HasLocallyLipschitzForce`: the hypothesis of the ODE uniqueness theorem. `HasLipschitzForce` and `HasC2Potential` are the stronger conditions usually assumed; each implies it and neither implies the other. - `HasLocalSolutions`: existence, kept separate. For a continuous force on a finite-dimensional configuration space it follows from Peano's theorem, whose proof is pending in Mathlib; section E derives it from the statement in `NortonDome.PeanoExistence`, marked `@[sorryful]`.

The proof of determinism turns the equation of motion into the first-order system `(r, v)' = (v, F(r)/m)` on `X × X`, applies Mathlib's local uniqueness theorem for integral curves, and extends to all time by connectedness of the real line. So continuity buys existence and local Lipschitz continuity buys uniqueness; the file records what each condition does, not which one is right.

ii. Key results

- `NewtonianSystem.isDeterministic_of_hasLocallyLipschitzForce`: a locally Lipschitz force gives determinism, hence `NewtonianSystem.satisfiesFirstLaw_of_hasLocallyLipschitzForce` the first law. `NewtonianSystem.isDeterministic_of_hasC2Potential` and `NewtonianSystem.isDeterministic_of_hasLipschitzForce` are the forms usually quoted; the chain of implications is drawn in section D.3. - `NewtonianSystem.ODE_solution_unique_of_locallyLipschitz`: integral curves of a locally Lipschitz vector field through a common point coincide for all time. - `NewtonianSystem`, `NewtonianSystem.force`, `NewtonianSystem.EquationOfMotion` and `NewtonianSystem.IsSolution`: the system, the force `-∇V`, Newton's second law, and its twice differentiable solutions; `NewtonianSystem.isSolution_const` is rest at an equilibrium. - `NewtonianSystem.IsSolution.deriv_eq_of_force_eq_zero_on`: the first law read on an interval, a consequence of the second law for every system. - `NewtonianSystem.IsDeterministic`, `NewtonianSystem.SatisfiesFirstLaw`, `NewtonianSystem.HasLocallyLipschitzForce`, `NewtonianSystem.HasLipschitzForce` and `NewtonianSystem.HasC2Potential`: the predicates, with `NewtonianSystem.HasLipschitzForce.hasLocallyLipschitzForce` and `NewtonianSystem.HasC2Potential.hasLocallyLipschitzForce`. - `NewtonianSystem.HasLocalSolutions` and `NewtonianSystem.hasLocalSolutions_of_continuous_force`: Peano's theorem for Newtonian systems, a continuous force on a finite-dimensional configuration space gives local solutions (pending the upstream proof).

iii. Table of contents

- A. Conservative Newtonian systems - A.1. The structure - A.2. The force and the equation of motion - A.3. Solutions - B. Determinism and the first law - B.1. The properties - B.2. Determinism implies the first law - B.3. The interval reading of the first law - C. Regularity conditions - D. A locally Lipschitz force gives determinism - D.1. The phase-space vector field - D.2. The phase curve of a solution - D.3. The uniqueness theorem - E. A continuous force gives local solutions - E.1. Local existence - E.2. The hypotheses of Peano's theorem - E.3. The existence theorem

iv. References

- Earman, J., *A Primer on Determinism*, Reidel (1986). - Laplace, P.-S., *Essai philosophique sur les probabilités* (1814). - Montague, R., *Deterministic theories*, in *Formal Philosophy*, Yale University Press (1974). - Norton, J. D., *The dome: an unexpectedly simple failure of determinism*, Philosophy of Science 75 (2008), 786–798. - `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Solution` (the same uniqueness argument for the pendulum).

A. Conservative Newtonian systems

A.1. The structure

The potential is asked to be differentiable and no more, so that the force `-∇V` exists and the equation of motion can be written pointwise; further regularity is added in section C. Physlib's general notion is `ClassicalMechanics.PointParticle.NewtonianSystem`, finitely many particles with explicit forces in a reference frame. The structure here is a single mass in a potential, which is all the dome needs; the two live in different namespaces and no file opens both.

A.2. The force and the equation of motion

A.3. Solutions

A solution is a twice differentiable curve, position and velocity both differentiable, satisfying the equation of motion: the regularity of `ClassicalMechanics.ReferenceFrame.Particle` and the least under which the acceleration exists. It is demanded because the pointwise equation, whose derivatives are zero wherever they do not exist, admits rough accidental solutions. Continuity of the acceleration is not demanded; for a continuous force it is automatic.

B. Determinism and the first law

B.1. The properties

Determinism is the statement that position and velocity at one instant fix the motion at all instants. The first law, in the reading that says more than the second law, is the statement that a body at rest where no force acts stays at rest; section B.3 compares the readings. Both are properties of the system, not of a motion.

The definition of determinism is the naive one. Laplace's formulation is about knowledge; the notion used since Montague and Earman is about models, a theory being deterministic if any two models agreeing at one instant agree at every instant. `IsDeterministic` is that notion, with the models taken to be the twice differentiable solutions of one system, defined for all time, and the state taken to be position and velocity. Four things follow.

- It is a property of one system. That Newtonian mechanics is deterministic is a claim about every system in some class, and which class is what this folder is about. - It is uniqueness only. A system with no solution from some initial datum, or with solutions not defined for all time, counts as deterministic here, whereas on Earman's account such failures of existence count against determinism. Existence is kept separate, as `HasLocalSolutions`. - It is relative to the class of solutions. Demanding smooth or analytic solutions would exclude the departing motions of the dome, which vanish on a half-line and are not `C⁴`, and so restore uniqueness by fiat. - It does not distinguish future from past. The time-reversed motions of the dome arrive at rest on the apex and stay, so the state there fixes neither past nor future; Earman's futuristic and historical determinism both fail.

B.2. Determinism implies the first law

The curve staying at the equilibrium is a solution with the same position and velocity as the given one at the given instant, so by determinism it is the given one.

B.3. The interval reading of the first law

The first law can be read instantaneously (no force at an instant, no acceleration then), with an interval in the hypothesis (no force on an interval, constant velocity on it), or with an interval in the conclusion (at rest at an instant where no force acts, at rest forever). The first two follow from the second law for every system, the second being the lemma below, and both hold for the dome. The third, `SatisfiesFirstLaw`, is determinism at an equilibrium; it is what the dome violates and what Norton's argument is about, so it is the reading taken here.

C. Regularity conditions

The hypothesis of the ODE uniqueness theorem is a locally Lipschitz force, `HasLocallyLipschitzForce`. The two stronger conditions usually stated are a globally Lipschitz force, `HasLipschitzForce`, and a `C²` potential, `HasC2Potential`, whose force is `C¹`. Neither implies the other: for example, `x ^ 4` has a `C¹` force of unbounded slope, and `x * |x| / 2` has the Lipschitz force `-|x|` but is not `C²`. The structure `NewtonianSystem` of section A assumes none of these conditions; they are separate predicates on it.

D. A locally Lipschitz force gives determinism

The equation of motion becomes the first-order system `(r, v)' = (v, F(r)/m)` on `X × X`. If the force is locally Lipschitz so is this vector field, and the local uniqueness theorem `ODE_solution_unique_of_eventually` of Mathlib, with the connectedness of the real line, gives determinism, as in `SimplePendulum.equationOfMotion_unique`.

D.1. The phase-space vector field

D.2. The phase curve of a solution

D.3. The uniqueness theorem

Local uniqueness makes the set of instants at which two integral curves through a common point agree open, continuity makes it closed, and the real line is connected. Applied to the phase-space vector field this gives the theorem of the file, and sections B, C and D form one chain, each arrow a theorem:

``` HasC2Potential ────┐ ├──▶ HasLocallyLipschitzForce ──▶ IsDeterministic ──▶ SatisfiesFirstLaw HasLipschitzForce ─┘ ```

Naming follows Mathlib: `isDeterministic_of_hasC2Potential` is the arrow from `HasC2Potential` to `IsDeterministic`.

E. A continuous force gives local solutions

Determinism is uniqueness; the complementary existence property is that every initial position and velocity is the initial datum of some solution for a short time. For a continuous force on a finite-dimensional configuration space this is Peano's theorem applied to the phase-space vector field, as Picard–Lindelöf gives it for the pendulum in `SimplePendulum.exists_local_solution`. The statement of Peano's theorem is that of `NortonDome.PeanoExistence`, pending in Mathlib, so the results here are marked `@[sorryful]`.

E.1. Local existence

E.2. The hypotheses of Peano's theorem

The phase-space vector field is continuous if the force is, and is bounded on the closed unit ball about the initial datum by compactness; a short enough time interval then gives the hypotheses of Peano's theorem.

E.3. The existence theorem

Peano's theorem gives an integral curve through the initial datum, differentiable in the sense of `HasDerivWithinAt` on the closed interval, hence with an honest derivative on the open one. Its first component, pulled back to `Time` through `Time.toRealCLE`, is the required curve; its derivatives are read off with `Time.deriv_comp_toRealCLE_of_hasDerivAt`.

30 declarations

theorem

Mass of a Newtonian System m≠0m \neq 0

For any conservative Newtonian system SS, the mass mm of the point mass is non-zero, i.e., m≠0m \neq 0.

definition

Force of a Newtonian system F=−∇VF = -\nabla V

For a conservative Newtonian system with potential function VV, the force FF at a position xx in the configuration space XX is defined as the negative gradient of the potential at that point, given by F(x)=−∇V(x)F(x) = -\nabla V(x).

definition

Newton's second law mr¨=F(r)m \ddot{r} = F(r)

For a conservative Newtonian system SS with mass mm and force function FF, a trajectory r:Time→Xr: \text{Time} \to X satisfies the equation of motion if at every instant t∈Timet \in \text{Time}, the product of the mass and the second time derivative of the position (acceleration) is equal to the force at that position. This is expressed by the formula: mr¨(t)=F(r(t))m \ddot{r}(t) = F(r(t)) where r¨\ddot{r} denotes the second derivative of rr with respect to time.

definition

Solution of a Newtonian system

A curve r:Time→Xr: \text{Time} \to X is a solution of a Newtonian system SS if it is twice differentiable—meaning both the position rr and the velocity r˙\dot{r} are differentiable—and it satisfies the equation of motion: mr¨(t)=F(r(t))m \ddot{r}(t) = F(r(t)) at every instant t∈Timet \in \text{Time}, where mm is the mass of the particle and FF is the force acting on it.

theorem

A Solution to a Newtonian System is Differentiable

Let SS be a Newtonian system and r:Time→Xr: \text{Time} \to X be a solution of the system SS. Then the position curve rr is differentiable with respect to time.

theorem

Velocity of a Newtonian Solution is Differentiable

Let SS be a Newtonian system on a configuration space XX. If a curve r:Time→Xr : \text{Time} \to X is a solution of the system SS, then its velocity r˙=drdt\dot{r} = \frac{dr}{dt} is differentiable with respect to time.

theorem

Solutions of a Newtonian system satisfy the equation of motion mr¨=F(r)m \ddot{r} = F(r)

For a conservative Newtonian system SS with mass mm and force FF, if a trajectory r:Time→Xr: \text{Time} \to X is a solution of the system, then it satisfies the equation of motion mr¨(t)=F(r(t))m \ddot{r}(t) = F(r(t)) at every instant t∈Timet \in \text{Time}, where r¨\ddot{r} is the second derivative of the position with respect to time.

theorem

A point with zero force defines a constant solution r(t)=xr(t) = x

Let SS be a conservative Newtonian system with configuration space XX. If the force F(x)F(x) vanishes at a point x∈Xx \in X (i.e., F(x)=0F(x) = 0), then the constant curve r:Time→Xr: \text{Time} \to X, defined by r(t)=xr(t) = x for all tt, is a solution to the system.

definition

Determinism of a Newtonian system

A Newtonian system SS is defined to be deterministic if any two solutions x,y:Time→Xx, y: \text{Time} \to X that share the same position and velocity at some instant t0∈Timet_0 \in \text{Time} are identical. Specifically, if xx and yy satisfy the equation of motion and there exists t0t_0 such that x(t0)=y(t0)x(t_0) = y(t_0) and x˙(t0)=y˙(t0)\dot{x}(t_0) = \dot{y}(t_0), then x(t)=y(t)x(t) = y(t) for all tt. Here, x˙\dot{x} (or ∂tx\partial_t x) denotes the time derivative of the position. This property represents the uniqueness of twice-differentiable solutions defined for all time, independent of whether such solutions exist for all initial conditions.

definition

Newtonian system SS satisfies the first law

A Newtonian system SS satisfies the first law if every solution r:Time→Xr : \text{Time} \to X that is at rest at an instant t0t_0 (i.e., ∂tr(t0)=0\partial_t r(t_0) = 0) where the force vanishes (i.e., F(r(t0))=0F(r(t_0)) = 0) remains at that position for all time, such that r(t)=r(t0)r(t) = r(t_0) for all tt.

theorem

Determinism Implies the First Law for Newtonian Systems

If a Newtonian system SS is deterministic, then it satisfies the first law. Specifically, a system is deterministic if any two solutions x,y:Time→Xx, y: \text{Time} \to X that share the same position x(t0)=y(t0)x(t_0) = y(t_0) and velocity x˙(t0)=y˙(t0)\dot{x}(t_0) = \dot{y}(t_0) at some instant t0t_0 are identical for all tt. The first law states that any solution r:Time→Xr: \text{Time} \to X that is at rest (r˙(t0)=0\dot{r}(t_0) = 0) at a point where the force vanishes (F(r(t0))=0F(r(t_0)) = 0) must remain at that position (r(t)=r(t0)r(t) = r(t_0)) for all time tt.

theorem

Vanishing Force on an Interval Implies Constant Velocity

Let SS be a Newtonian system and r:Time→Xr: \text{Time} \to X be a solution to its equation of motion. For any time interval [a,b][a, b], if the force F(r(t))F(r(t)) acting on the particle is zero for all t∈[a,b]t \in [a, b], then the velocity r˙(t)\dot{r}(t) of the particle is constant throughout that interval, satisfying r˙(t)=r˙(a)\dot{r}(t) = \dot{r}(a) for all t∈[a,b]t \in [a, b]. This result represents the "interval reading" of Newton's first law as a consequence of the second law.

definition

Newtonian system with a locally Lipschitz force FF

A Newtonian system SS is said to have a **locally Lipschitz force** if its force function F(x)=−∇V(x)F(x) = -\nabla V(x) is locally Lipschitz continuous on the configuration space XX. This means that for every point x∈Xx \in X, there exists a neighborhood of xx on which FF is Lipschitz continuous. This property is a standard hypothesis required for the uniqueness theorem of ordinary differential equations.

definition

Newtonian system with globally Lipschitz force FF

A Newtonian system SS has a globally Lipschitz force if there exists a constant K∈[0,∞)K \in [0, \infty) such that the force function F(x)=−∇V(x)F(x) = -\nabla V(x) is KK-Lipschitz continuous on the configuration space XX. That is, for all x1,x2∈Xx_1, x_2 \in X, the inequality ∥F(x1)−F(x2)∥≤K∥x1−x2∥\|F(x_1) - F(x_2)\| \le K \|x_1 - x_2\| holds.

definition

Newtonian system with V∈C2V \in C^2 potential

A Newtonian system SS is said to have a C2C^2 potential if its potential function VV is twice continuously differentiable (V∈C2V \in C^2). This degree of regularity is required for the uniqueness theory of ordinary differential equations to apply to the resulting equation of motion.

theorem

A globally Lipschitz force is locally Lipschitz

For a Newtonian system SS, if the force function F=−∇VF = -\nabla V is globally Lipschitz continuous on the configuration space XX, then it is also locally Lipschitz continuous on XX.

theorem

The gradient of a C2C^2 potential is C1C^1

If the potential function VV of a Newtonian system is twice continuously differentiable (C2C^2), then its gradient ∇V\nabla V is once continuously differentiable (C1C^1).

theorem

A C2C^2 Potential Implies a Locally Lipschitz Force

For a Newtonian system SS with potential function VV, if VV is twice continuously differentiable (V∈C2V \in C^2), then the resulting force function F=−∇VF = -\nabla V is locally Lipschitz continuous on the configuration space.

definition

Phase-space vector field (r,v)↦(v,F(r)/m)(r, v) \mapsto (v, F(r)/m)

The phase-space vector field of a Newtonian system with mass m m and force function F F is a map from the phase space X×X X \times X to itself. For a state p=(r,v)∈X×X p = (r, v) \in X \times X , where r r is the position and v v is the velocity, the vector field is defined as (v,1mF(r)) (v, \frac{1}{m} F(r)) .

theorem

Locally Lipschitz Force Implies Locally Lipschitz Phase-Space Vector Field

Consider a Newtonian system with mass mm and force function F:X→XF: X \to X on a configuration space XX. If the force FF is locally Lipschitz, then the associated phase-space vector field Φ:X×X→X×X\Phi: X \times X \to X \times X, defined by Φ(r,v)=(v,1mF(r))\Phi(r, v) = (v, \frac{1}{m} F(r)) for position rr and velocity vv, is also locally Lipschitz.

theorem

The Phase Curve of a Solution is an Integral Curve of the Phase-Space Vector Field

Consider a Newtonian system with mass mm and force function F:X→XF: X \to X on a configuration space XX. Let r:Time→Xr: \text{Time} \to X be a trajectory such that rr and its time derivative r˙\dot{r} (denoted ∂tr\partial_t r) are differentiable. If rr satisfies the equation of motion mr¨(t)=F(r(t))m \ddot{r}(t) = F(r(t)), then for any τ∈R\tau \in \mathbb{R}, the derivative of the phase curve τ↦(r(t),r˙(t))\tau \mapsto (r(t), \dot{r}(t)) (where tt is the time instance identified with τ\tau via the continuous linear equivalence between Time\text{Time} and R\mathbb{R}) is equal to the phase-space vector field Φ(r,v)=(v,1mF(r))\Phi(r, v) = (v, \frac{1}{m} F(r)) evaluated at the current state (r(t),r˙(t))(r(t), \dot{r}(t)).

theorem

Global Uniqueness of Integral Curves for Locally Lipschitz Vector Fields

Let EE be a real normed space and v:E→Ev: E \to E be a locally Lipschitz vector field. Let f,g:R→Ef, g: \mathbb{R} \to E be two curves such that for every t∈Rt \in \mathbb{R}, ff and gg are differentiable at tt with f′(t)=v(f(t))f'(t) = v(f(t)) and g′(t)=v(g(t))g'(t) = v(g(t)). If there exists some t0∈Rt_0 \in \mathbb{R} such that f(t0)=g(t0)f(t_0) = g(t_0), then f=gf = g.

theorem

A Locally Lipschitz Force Implies Determinism in Newtonian Systems

Consider a Newtonian system SS with a potential VV and configuration space XX. Suppose the force function F(x)=−∇V(x)F(x) = -\nabla V(x) is locally Lipschitz continuous on XX. Then the system is deterministic: for any two twice-differentiable solutions r1,r2:Time→Xr_1, r_2 : \text{Time} \to X of the equation of motion mr¨(t)=F(r(t))m \ddot{r}(t) = F(r(t)), if there exists an instant t0t_0 such that r1(t0)=r2(t0)r_1(t_0) = r_2(t_0) and r˙1(t0)=r˙2(t0)\dot{r}_1(t_0) = \dot{r}_2(t_0), then r1(t)=r2(t)r_1(t) = r_2(t) for all t∈Timet \in \text{Time}.

theorem

A Globally Lipschitz Force Implies Determinism in a Newtonian System

A Newtonian system with a globally Lipschitz force is deterministic. This result is a version of the Picard–Lindelöf theorem for Newtonian systems: if the force F(x)=−∇V(x)F(x) = -\nabla V(x) satisfies a global Lipschitz condition ∥F(x1)−F(x2)∥≤K∥x1−x2∥\|F(x_1) - F(x_2)\| \le K \|x_1 - x_2\| for some constant K≥0K \ge 0 and all x1,x2∈Xx_1, x_2 \in X, then any two twice-differentiable solutions x(t)x(t) and y(t)y(t) to the equation of motion mx¨=F(x)m \ddot{x} = F(x) that share the same position and velocity at some instant t0t_0 (i.e., x(t0)=y(t0)x(t_0) = y(t_0) and x˙(t0)=y˙(t0)\dot{x}(t_0) = \dot{y}(t_0)) must be identical for all tt.

theorem

A C2C^2 potential implies determinism in Newtonian systems

Let SS be a Newtonian system. If SS has a C2C^2 potential (meaning its potential function VV is twice continuously differentiable), then SS is deterministic. Specifically, for any two trajectories x,y:Time→Xx, y : \text{Time} \to X that satisfy the equation of motion, if there exists an instant t0∈Timet_0 \in \text{Time} such that x(t0)=y(t0)x(t_0) = y(t_0) and x˙(t0)=y˙(t0)\dot{x}(t_0) = \dot{y}(t_0), then x(t)=y(t)x(t) = y(t) for all tt.

theorem

Locally Lipschitz Force Implies Newton's First Law

A Newtonian system SS with a locally Lipschitz force FF satisfies the first law. That is, for any solution r:R→Xr: \mathbb{R} \to X to the equation of motion, if there exists an instant t0t_0 such that the particle is at rest (r˙(t0)=0\dot{r}(t_0) = 0) and the force at that position vanishes (F(r(t0))=0F(r(t_0)) = 0), then the particle remains at that position for all time: r(t)=r(t0)r(t) = r(t_0) for all t∈Rt \in \mathbb{R}.

definition

Existence of local solutions for a Newtonian system

A Newtonian system SS with mass mm and force function FF has local solutions if, for every initial position x0∈Xx_0 \in X and initial velocity v0∈Xv_0 \in X, there exists a duration ϵ>0\epsilon > 0 and a trajectory r:Time→Xr: \text{Time} \to X such that: 1. The initial conditions are satisfied: r(0)=x0r(0) = x_0 and r˙(0)=v0\dot{r}(0) = v_0, where r˙\dot{r} denotes the time derivative ddtr\frac{d}{dt}r. 2. For all t∈Timet \in \text{Time} within the interval ∣t∣≤ϵ|t| \leq \epsilon, the trajectory rr and its velocity r˙\dot{r} are differentiable at tt. 3. For all tt in that interval, the equation of motion mr¨(t)=F(r(t))m \ddot{r}(t) = F(r(t)) holds, where r¨\ddot{r} is the second time derivative of rr.

theorem

Continuous force implies continuous phase-space vector field

For a Newtonian system with mass mm and force F:X→XF: X \to X, if the force FF is continuous, then the associated phase-space vector field defined by (r,v)↦(v,1mF(r))(r, v) \mapsto (v, \frac{1}{m} F(r)) is also continuous on the phase space X×XX \times X.

theorem

A continuous force implies the phase-space vector field satisfies Peano's hypotheses

Let SS be a Newtonian system with a finite-dimensional configuration space XX. If the force F:X→XF: X \to X is continuous, then for any initial state p0=(r0,v0)p_0 = (r_0, v_0) in the phase space X×XX \times X, there exists a positive time interval [−δ,δ][-\delta, \delta] and a bound LL such that the time-independent phase-space vector field (r,v)↦(v,1mF(r))(r, v) \mapsto (v, \frac{1}{m} F(r)) satisfies the hypotheses of Peano's existence theorem (the `IsPeano` predicate) centered at the initial time t=0t=0 and state p0p_0, within a spatial ball of radius 11.

theorem

Continuous Force Implies Local Solutions for Newtonian Systems (Peano's Theorem)

Let SS be a Newtonian system with a finite-dimensional configuration space XX and force function F:X→XF: X \to X. If FF is continuous, then the system has local solutions. That is, for any initial position x0∈Xx_0 \in X and initial velocity v0∈Xv_0 \in X, there exists a duration ϵ>0\epsilon > 0 and a trajectory r:[−ϵ,ϵ]→Xr: [-\epsilon, \epsilon] \to X such that: 1. r(0)=x0r(0) = x_0 and r˙(0)=v0\dot{r}(0) = v_0. 2. rr and r˙\dot{r} are differentiable on [−ϵ,ϵ][-\epsilon, \epsilon]. 3. The equation of motion mr¨(t)=F(r(t))m \ddot{r}(t) = F(r(t)) holds for all t∈[−ϵ,ϵ]t \in [-\epsilon, \epsilon].