The definition of a second.

Stream: PhysLean

[Joseph Tooby-Smith]

I had a stab at formalizing the definition of a second in this PR.
I'm not trying to formalize units here, just the concept of a second.

Copying the explanation from the relevant file here:

The type Time is defined as ℝ.

The type ℝ carries the instance of NormedField, giving us one way to define distances between times.

However, this norm (since it is defined through the field structure on ℝ)
gives special meaning to 1, which it does not have in the context of time.
After all, time does not form a field - the product of two times is not a time.
In fact we can rescale the norm on ℝ to give a different, but completely
valid definition of distance between two times.

This ambiguity is removed if we pick the time between two events p1 and p2
in SpaceTime and define distances in time relative to the difference in time between p1 and p2.

If we fix p1 and p2 to correspond to the start and end of 9 192 631 770
hyperfine transitions of the unperturbed ground-state of caesium-133 atom, this relative distance corresponds to a second.

So how do we tell Lean about p1 and p2? We do this by
introducing an axiom.

I don't have plans to do much with this yet, except maybe add something to

https://github.com/HEPLean/PhysLean_notes

about it. But would be keen to hear any feedback.

I'm hoping the definition I've given actually reflects the real-world use of seconds. That is it compares the time between two events relative to the time measured for some standard event.

[Joseph Tooby-Smith]

In this PR I have the following axiom:

axiom secondAxiom : {p : SpaceTime × SpaceTime |
  Lorentz.Vector.causallyFollows p.1 p.2}

But maybe it is worth attempting to define a more general axiom for experimental observations. I guess something similar to Classical.choice except with some mechanism that stops two items defined with it been equal i.e. preventing

noncomputable def p1 : Fin 4 := Classical.choice (instNonemptyOfInhabited)

noncomputable def p2 : Fin 4 := Classical.choice (instNonemptyOfInhabited)

example : p1 = p2 := by rfl

[Alex Meiburg]

When I saw the title of this thread, I thought you might be defining the fock space of a Caesium-133 atom, and its hyperfine splitting... :)

[Alex Meiburg]

(I don't endorse this as a useful definition of a second (at the moment!) but it would be a hilarious / cool project!)

[Joseph Tooby-Smith]

Haha, I did have a think about whether that would be possible - but I still think, in the end, you would need to include an axiom corresponding to measurement, although it would be a slightly more 'fundamental' axiom then what I have :).

[Joseph Tooby-Smith]

(I'm also not claiming that my definition is very good - it just shows one way of dealing with this I think).

[Alex Meiburg]

I think it's a (hyper)fine way to do it for reasonable purposes, yeah :)