Proving physical laws

Stream: maths

[Xu Miao]

Has anyone tried to prove Einstein's energy-mass equivalence theorem? Thanks!

[Kevin Buzzard]

What would be the axioms you'd use to prove that theorem?

[Xu Miao]

Something like special relativity? I am not sure how to represent the equation as a type : energy(o) = mass(o) * C^2 and how to generate a proof derived from the special relativity.

[Simon Hudon]

You could declare a structure like:

structure physical_object :=
(energy : real)

def physical_object.mass (o : physical_object) : real := o.energy / C^2

or

structure physical_object :=
(energy mass : real)
(special_relativity : energy = mass * C^2)

Because the equation is functional, the second approach is heavier than necessary but if you want it to satisfy more equations by construction and that they're not all functional, this might be necessary

[Xu Miao]

Thanks @Simon Hudon . The second one makes more sense to me but it seems missing the concept that both energy and mass are attributes of the same physical object. If a type defines the equivalence theorem, how can I proceed to define a proof?

$E_k = m_0 c^2 \left(\frac{1}{\sqrt{1- \frac{v^2}{c^2}}}-1\right)\\ E_k=mc^2 -m_0c^2\\ E=E_k+m_0c^2=mc^2$

[Simon Hudon]

Sorry, my physics is a bit rusty. I assume $E_k$ is kinetic energy and $m_0$ is mass at rest. You can encode those as:

structure physical_object :=
(energy mass kinetic_energy mass_at_rest velocity : real)
(special_relativity : energy = mass * C^2)
(eqn_1 : /- first equation -/)
(eqn_2 : /- second equation -/)

then your third equation seems to be derivable from the first two:

lemma eqn_3 (o : physical_object) : o.energy = o.kinetic_energy + o.mass_at_rest * C^2 := ...

You can also choose different equations to be axioms vs derived laws. You can also choose different variables to be fundamental quantities vs derived quantities. The fields of the structure are the fundamental quantities and the derived ones would be definitions.

[Simon Hudon]

[...] but it seems missing the concept that both energy and mass are attributes of the same physical object.

If you have two objects, o o' : physical_object, each has their energy and mass and they each satisfy the physical laws that you encode in the structure physical_object.

[Xu Miao]

@Simon Hudon , thanks a lot for the explanation. I think I start to understand the approach. I will need some time to digest these a little bit.

[Simon Hudon]

If you decide to model gravity and attraction also it will get a bit more complicated / interesting

[David Michael Roberts]

One thing that is worthwhile is thinking of numerical physical quantities as living in a _graded_ algebra, with the gradings given by units of dimension. So if you multiply a length by linear density, you get a mass. This also means that equations have to 'typecheck' (in the sense of dimensional analysis) in order to work. Thus if one is missing a conversion factor that happens to be set to 1 in the current system of units, Lean would complain.

[Simon Hudon]

Is there a Lean package that does that?

[David Michael Roberts]

Graded algebras? I don't know.

[Mario Carneiro]

One possibility might be to try to derive the laws of special relativity from the principle of equivalence, as in https://en.wikipedia.org/wiki/Derivations_of_the_Lorentz_transformations . I can see this being turned into a completely mathematical statement of the form "the only transformations that preserve an appropriately defined metric are Lorentz transformations", and most of the math regarding inertial mass vs rest mass can derive from there.

[Xu Miao]

@David Michael Roberts, I think that was my motivation for proving equality instead of quantitively calculating equality because the physical law should be scale-invariant. Any way to avoid that?

[Xu Miao]

@Mario Carneiro that is interesting. any detail?

[Mario Carneiro]

I think the primary problem is that your question is not a formal one. There is a huge hurdle to even phrasing physics questions in a way such that it is clear what is to be proven, rather than just writing a bunch of equations and calling it a day.

[Mario Carneiro]

Even looking at the wikipedia page, equations are interspersed with physical intuitions such that it's not clear what the axioms or the setting are

[Mario Carneiro]

For example, the Invariance of interval section talks about a "system $K$" and later quantifies over other systems $K'$. I challenge you to determine the type of $K$, i.e. a definition of what constitutes a "system"

[Xu Miao]

Yeah, it is not formal enough. I guess physical systems refer to 4-dimensional Hilbert spaces. $K$ vs $K'$ are affine projections to each other?

[David Michael Roberts]

I'm sorry, what have 4d Hilbert spaces got to do with it? Do you mean Minkowski spaces?

[Xu Miao]

@David Michael Roberts I was answering @Mario Carneiro 's question about "what constitutes a system" for the wiki page invariance of interval. You are right, Minkowski spacetime fits special relativity better. I thought Hilbert space is more general and with the principle of equivalence, we could derive the special relativity.

[David Michael Roberts]

Hilbert spaces are 'more general', they are a completely different type of thing. Minkowski space is a geometric object, and a Hilbert space is an algebraic object, both with more structure (different in each case) than the bare underlying 4-dimensional Euclidean space.