Physlib

PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism

The Norton dome and the determinism of Newtonian mechanics

i. Overview

A particle at rest on the apex of the Norton dome may stay there forever or slide off at any instant, in obedience to Newton's second law with a continuous force. This file states what that does and does not show, in the terms of `NortonDome.NewtonianSystem`.

The dome is such a system (`toNewtonianSystem`). It is not deterministic (`not_isDeterministic`) and it violates the first law (`not_satisfiesFirstLaw`). Since a locally Lipschitz force gives determinism, the dome must fail that hypothesis and everything implying it, and it does (`not_hasLocallyLipschitzForce`, `not_hasLipschitzForce`, `not_hasC2Potential`). Its force `m √r` is continuous but has infinite slope at the apex, and its potential is `C¹` but not `C²`.

Put together, this is `exists_continuous_force_not_isDeterministic`: a continuous force does not make a Newtonian system deterministic, while a locally Lipschitz force, or a `C²` potential, does. Newton's laws do not say which requirement, if any, belongs in the definition of a Newtonian system. The theorems say what each requirement buys and that the dome is what each excludes, and leave the choice open. Malament's proposal, a regularity condition on the constraint surface in physical space rather than on the potential, is not formulated here. With Peano's theorem, whose proof is pending in Mathlib, the dome has solutions from every initial datum (`hasLocalSolutions`), so its failure is one of uniqueness alone.

ii. Key results

- `NortonDome.not_isDeterministic`: the dome is not deterministic. - `NortonDome.not_satisfiesFirstLaw`: the dome violates the first law. - `NortonDome.exists_continuous_force_not_isDeterministic`: Norton's claim, a Newtonian system with a continuous force that is not deterministic. - `NortonDome.not_hasLocallyLipschitzForce`, `NortonDome.not_hasLipschitzForce` and `NortonDome.not_hasC2Potential`: the dome satisfies none of the regularity conditions. - `NortonDome.toNewtonianSystem` is the dome as a Newtonian system, with `toNewtonianSystem_force`, `toNewtonianSystem_equationOfMotion_iff` and `toNewtonianSystem_isSolution_iff` identifying its force, equation of motion and solutions with those of `NortonDome.Basic`. - `NortonDome.hasLocalSolutions` and `NortonDome.exists_hasLocalSolutions_not_isDeterministic`: the dome has local solutions from every initial datum, by Peano's theorem, so its failure of determinism is a failure of uniqueness alone (pending the upstream proof).

iii. Table of contents

- A. The dome as a Newtonian system - B. The properties the dome fails - B.1. Determinism and the first law - B.2. The regularity conditions - C. Norton's claim - D. Existence without uniqueness

iv. References

- Norton, J. D., *The dome: an unexpectedly simple failure of determinism*, Philosophy of Science 75 (2008), 786–798. - Malament, D. B., *Norton's slippery slope*, Philosophy of Science 75 (2008), 799–816.

A. The dome as a Newtonian system

The dome has a differentiable potential, so it is a Newtonian system whose force, equation of motion and solutions are by definition those of `NortonDome.Basic`.

B. The properties the dome fails

B.1. Determinism and the first law

Determinism fails by the non-uniqueness proved in `NortonDome.Solution`. The first law fails along the motion leaving the apex at the instant `1`: at the instant `0` it is at rest at the apex, where the force vanishes, and at the instant `2` it is off the apex.

B.2. The regularity conditions

The force is not Lipschitz on any closed ball about the apex, `not_lipschitzOnWith_force`, hence not locally Lipschitz; the two stronger conditions imply a locally Lipschitz force, so they fail too.

C. Norton's claim

D. Existence without uniqueness

The force is continuous and the configuration space is finite-dimensional, so by Peano's theorem, `NewtonianSystem.hasLocalSolutions_of_continuous_force`, every initial datum has a local solution: the failure of determinism is purely one of uniqueness. Pending the proof of Peano's theorem in Mathlib, these results are marked `@[sorryful]`.

12 declarations

definition

The Norton dome as a Newtonian system

The Norton dome is modeled as a conservative Newtonian system in a one-dimensional Euclidean space R\mathbb{R} (representing the arc length along the dome's surface). The system is defined by a mass mm and a potential energy function V(r)V(r), both provided by the underlying parameters of the dome SS. This definition ensures that the mass is positive (m>0m > 0) and that the potential energy function is differentiable.

theorem

The Force of the Norton Dome as a Newtonian System Equals its Basic Force

For a Norton dome SS, the force function derived from its representation as a Newtonian system (defined as the negative gradient of its potential energy −∇V-\nabla V) is equal to the specific force function FF defined in the dome's basic model.

theorem

The Equation of Motion of the Norton Dome as a Newtonian System is Equivalent to its Basic Equation of Motion

For a Norton dome SS, a trajectory r:Time→Rr: \text{Time} \to \mathbb{R} (where the position is represented as a point in a one-dimensional Euclidean space) satisfies the equation of motion derived from the dome's formulation as a general Newtonian system if and only if it satisfies the equation of motion defined in the dome's basic model.

theorem

The Solutions of the Norton Dome as a Newtonian System are Equivalent to its Basic Solutions

For a Norton dome SS, a trajectory r:Time→Rr: \text{Time} \to \mathbb{R} (where the position is represented as a point in a one-dimensional Euclidean space) is a solution of the dome viewed as a Newtonian system if and only if it is a solution of the dome as defined in its basic model.

theorem

The Norton dome is not deterministic

The Newtonian system associated with the Norton dome SS is not deterministic. That is, it is not the case that any two solutions to the equations of motion which share the same position and velocity at some initial time t0t_0 must be identical for all time tt.

theorem

The Norton dome violates Newton's first law

For a Norton dome SS modeled as a Newtonian system, Newton's first law is not satisfied. Specifically, a particle at rest at the apex of the dome, where the net force vanishes, does not necessarily remain at rest for all time.

theorem

The force of the Norton dome is not locally Lipschitz

For a Norton dome SS, the force function of its associated Newtonian system is not locally Lipschitz continuous. Specifically, the force is not Lipschitz on any neighborhood of the apex of the dome.

theorem

The force of the Norton dome is not globally Lipschitz

For a Norton dome SS, the force function FF of its associated Newtonian system is not globally Lipschitz continuous.

theorem

The potential of the Norton dome is not C2C^2

For a Norton dome SS, the potential energy function VV of its associated Newtonian system is not twice continuously differentiable (i.e., V∉C2V \notin C^2).

theorem

Existence of a non-deterministic Newtonian system with a continuous force

There exists a Newtonian system in one-dimensional Euclidean space R1\mathbb{R}^1 such that its associated force function FF is continuous, but the system is not deterministic. In this context, a system is non-deterministic if there exist at least two distinct trajectories x(t)x(t) and y(t)y(t) that satisfy the equations of motion and share the same position and velocity at some initial time t0t_0, yet diverge at other times.

theorem

Existence of Local Solutions for the Norton Dome

For a Norton dome SS, modeled as a Newtonian system in a one-dimensional Euclidean space R\mathbb{R}, there exist local solutions for every initial position and velocity. Specifically, for any initial position x0∈Rx_0 \in \mathbb{R} and initial velocity v0∈Rv_0 \in \mathbb{R}, there exists a duration ϵ>0\epsilon > 0 and a trajectory r:[−ϵ,ϵ]→Rr: [-\epsilon, \epsilon] \to \mathbb{R} such that: 1. The initial conditions are satisfied: r(0)=x0r(0) = x_0 and r˙(0)=v0\dot{r}(0) = v_0. 2. The trajectory rr and its velocity r˙\dot{r} are differentiable on the interval. 3. The Newtonian equation of motion mr¨(t)=F(r(t))m \ddot{r}(t) = F(r(t)) is satisfied for all t∈[−ϵ,ϵ]t \in [-\epsilon, \epsilon], where mm is the mass and FF is the force function associated with the dome.

theorem

Existence of a Non-Deterministic Newtonian System with Continuous Force and Local Solutions

There exists a Newtonian system NN with a one-dimensional configuration space R\mathbb{R} such that the force function FF is continuous and the system admits local solutions for every initial position x0x_0 and initial velocity v0v_0, yet the system is not deterministic (i.e., the solutions to the equation of motion mr¨(t)=F(r(t))m \ddot{r}(t) = F(r(t)) are not unique for all initial conditions).