Elastic collisions in 1d

Stream: PhysLean

[Joseph Tooby-Smith]

I was thinking about 1d elastic collisions and how one would formalize them into Lean.

Consider you have $n$-particles, $p_1, \ldots, p_n$, living in 1-dimensions, having masses $m_1, \ldots, m_n$, and at $t=0$ positions $x_1 \le \ldots \leq x_n$, velocities $v_1, \ldots, v_n$. Suppose these undergo elastic collisions. So far this is easy to formalize into Lean, one could define a structure e.g. OneDimensionCollisions which would contain all of this data.

Now let $\vec x(t)$ be the $n$-vector of the particles positions at time $t$. My question is, what is the correct definition of $\vec x(t)$ in Lean?

I'm thinking something along the lines of, the unique vector such that

1. Overall energy is conserved
2. Overall momentum is conserved
3. The order of the particles remains the same.
4. For a given $x_i(t)$ if the interval $[t_1, t_2]$ does not contain a collision involving $p_i$ then $x_i(t)$ within $[t_1, t_2]$ is smooth and satisfies Newton's second law.

But I'm not entirely sure that this uniquely defines $\vec x(t)$, and given (3) it does not generalize to higher dimensions (which may be tricky for now anyway).

[Joseph Tooby-Smith]

But I'm not entirely sure that this uniquely defines $\vec x(t)$,

Actually I think uniqueness is not guaranteed here, but I also think there is nothing one can do about it. The reason being, that if you have 3 or more particles colliding simultaneously, this model breaks down, see this physics stack exchange answer.

What should be true is that if in the time interval $[0, \tau)$ there are at most $2$-body collisions and $\vec x$ and $\vec y$ both satisfy the conditions above then $\vec x(t) = \vec y(t)$ for $t \in [0, \tau)$.