HepLean

Stream: Natural sciences

[Joseph Tooby-Smith]

My paper on the use of Lean in High Energy Physics appeared on the arXiv today at:

https://arxiv.org/abs/2405.08863

In writing the paper I made some domain-specific choices. The most notably is the use of the word 'digitalisation', instead of `formalising'. This was done because the word "formal" means something else to the average high energy physicist.

[Eric Wieser]

A small comment: on page 8, the ![![x, y], ![z, 0]] notation shouldn't be used for matrices; you should use !![x, y; z, 0] instead.

[Joseph Tooby-Smith]

@Eric Wieser This probably explains why I've had trouble with matrices lately :). Thanks for pointing this out. Will update in V2.

[Eric Wieser]

One other: "MathLib" is not the preferred capitalization, I think "Mathlib" or "mathlib" is preferred.

[Eric Wieser]

A question for you: it looks likephaseShiftRelation is preserved by multiplication; if this is true, can you provide a stronger docs#Con structure that proves this on top of the Setoid one?

[Eric Wieser]

That will give you for free that Quotient CKMMatrixSetoid is a group.

[Joseph Tooby-Smith]

@Eric Wieser I don't believe it is preserved under multiplication. The equivalence relation is, $A\sim B$ iff
$A = \mathrm{diag}(e^{ia},e^{ib},e^{ic}) * B * \mathrm{diag}(e^{id},e^{ie},e^{if})$
Multiplying will give you two diagonal matrices 'in the middle' which do not cancel.