Zulip Chat Archive

Stream: maths

Topic: Proving physical laws


view this post on Zulip Xu Miao (Dec 08 2019 at 08:37):

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

view this post on Zulip Kevin Buzzard (Dec 08 2019 at 10:16):

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

view this post on Zulip Xu Miao (Dec 08 2019 at 21:38):

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.

view this post on Zulip Simon Hudon (Dec 08 2019 at 21:45):

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

view this post on Zulip Xu Miao (Dec 09 2019 at 01:31):

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?

Ek=m0c2(11v2c21)Ek=mc2m0c2E=Ek+m0c2=mc2E_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

view this post on Zulip Simon Hudon (Dec 09 2019 at 01:47):

Sorry, my physics is a bit rusty. I assume EkE_k is kinetic energy and m0m_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.

view this post on Zulip Simon Hudon (Dec 09 2019 at 02:13):

[...] 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.

view this post on Zulip Xu Miao (Dec 09 2019 at 05:08):

@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.

view this post on Zulip Simon Hudon (Dec 09 2019 at 05:15):

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

view this post on Zulip David Michael Roberts (Dec 09 2019 at 05:21):

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.

view this post on Zulip Simon Hudon (Dec 09 2019 at 05:23):

Is there a Lean package that does that?

view this post on Zulip David Michael Roberts (Dec 09 2019 at 06:21):

Graded algebras? I don't know.

view this post on Zulip Mario Carneiro (Dec 09 2019 at 07:57):

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.

view this post on Zulip Xu Miao (Dec 09 2019 at 10:23):

@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?

view this post on Zulip Xu Miao (Dec 09 2019 at 10:25):

@Mario Carneiro that is interesting. any detail?

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:28):

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.

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:29):

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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:34):

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

view this post on Zulip Xu Miao (Dec 09 2019 at 20:44):

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

view this post on Zulip David Michael Roberts (Dec 09 2019 at 23:34):

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

view this post on Zulip Xu Miao (Dec 10 2019 at 03:20):

@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.

view this post on Zulip David Michael Roberts (Dec 12 2019 at 09:38):

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.


Last updated: May 11 2021 at 15:12 UTC